1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Parallel.thy	Sun Jul 22 09:56:34 2012 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* Futures and parallel lists for code generated towards Isabelle/ML *}
     1.7 +
     1.8 +theory Parallel
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +subsection {* Futures *}
    1.13 +
    1.14 +datatype 'a future = fork "unit \<Rightarrow> 'a"
    1.15 +
    1.16 +primrec join :: "'a future \<Rightarrow> 'a" where
    1.17 +  "join (fork f) = f ()"
    1.18 +
    1.19 +lemma future_eqI [intro!]:
    1.20 +  assumes "join f = join g"
    1.21 +  shows "f = g"
    1.22 +  using assms by (cases f, cases g) (simp add: ext)
    1.23 +
    1.24 +code_type future
    1.25 +  (Eval "_ future")
    1.26 +
    1.27 +code_const fork
    1.28 +  (Eval "Future.fork")
    1.29 +
    1.30 +code_const join
    1.31 +  (Eval "Future.join")
    1.32 +
    1.33 +code_reserved Eval Future future
    1.34 +
    1.35 +
    1.36 +subsection {* Parallel lists *}
    1.37 +
    1.38 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.39 +  [simp]: "map = List.map"
    1.40 +
    1.41 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.42 +  "forall = list_all"
    1.43 +
    1.44 +lemma forall_all [simp]:
    1.45 +  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    1.46 +  by (simp add: forall_def list_all_iff)
    1.47 +
    1.48 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.49 +  "exists = list_ex"
    1.50 +
    1.51 +lemma exists_ex [simp]:
    1.52 +  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
    1.53 +  by (simp add: exists_def list_ex_iff)
    1.54 +
    1.55 +code_const map
    1.56 +  (Eval "Par'_List.map")
    1.57 +
    1.58 +code_const forall
    1.59 +  (Eval "Par'_List.forall")
    1.60 +
    1.61 +code_const exists
    1.62 +  (Eval "Par'_List.exists")
    1.63 +
    1.64 +code_reserved Eval Par_List
    1.65 +
    1.66 +
    1.67 +hide_const (open) fork join map exists forall
    1.68 +
    1.69 +end
    1.70 +