src/HOL/Library/Parallel.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 52435 6646bb548c6b child 58249 180f1b3508ed permissions -rw-r--r--
prefer Code.abort over code_abort
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Futures and parallel lists for code generated towards Isabelle/ML *}
5 theory Parallel
6 imports Main
7 begin
9 subsection {* Futures *}
11 datatype 'a future = fork "unit \<Rightarrow> 'a"
13 primrec join :: "'a future \<Rightarrow> 'a" where
14   "join (fork f) = f ()"
16 lemma future_eqI [intro!]:
17   assumes "join f = join g"
18   shows "f = g"
19   using assms by (cases f, cases g) (simp add: ext)
21 code_printing
22   type_constructor future \<rightharpoonup> (Eval) "_ future"
23 | constant fork \<rightharpoonup> (Eval) "Future.fork"
24 | constant join \<rightharpoonup> (Eval) "Future.join"
26 code_reserved Eval Future future
29 subsection {* Parallel lists *}
31 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
32   [simp]: "map = List.map"
34 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
35   "forall = list_all"
37 lemma forall_all [simp]:
38   "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
39   by (simp add: forall_def list_all_iff)
41 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
42   "exists = list_ex"
44 lemma exists_ex [simp]:
45   "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
46   by (simp add: exists_def list_ex_iff)
48 code_printing
49   constant map \<rightharpoonup> (Eval) "Par'_List.map"
50 | constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
51 | constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
53 code_reserved Eval Par_List
56 hide_const (open) fork join map exists forall
58 end