src/HOL/Library/Parallel.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Parallel.thy	Sun Jul 22 09:56:34 2012 +0200
@@ -0,0 +1,67 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Futures and parallel lists for code generated towards Isabelle/ML *}
+
+theory Parallel
+imports Main
+begin
+
+subsection {* Futures *}
+
+datatype 'a future = fork "unit \<Rightarrow> 'a"
+
+primrec join :: "'a future \<Rightarrow> 'a" where
+  "join (fork f) = f ()"
+
+lemma future_eqI [intro!]:
+  assumes "join f = join g"
+  shows "f = g"
+  using assms by (cases f, cases g) (simp add: ext)
+
+code_type future
+  (Eval "_ future")
+
+code_const fork
+  (Eval "Future.fork")
+
+code_const join
+  (Eval "Future.join")
+
+code_reserved Eval Future future
+
+
+subsection {* Parallel lists *}
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+  [simp]: "map = List.map"
+
+definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "forall = list_all"
+
+lemma forall_all [simp]:
+  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
+  by (simp add: forall_def list_all_iff)
+
+definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "exists = list_ex"
+
+lemma exists_ex [simp]:
+  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
+  by (simp add: exists_def list_ex_iff)
+
+code_const map
+  (Eval "Par'_List.map")
+
+code_const forall
+  (Eval "Par'_List.forall")
+
+code_const exists
+  (Eval "Par'_List.exists")
+
+code_reserved Eval Par_List
+
+
+hide_const (open) fork join map exists forall
+
+end
+