author | haftmann |
Sun, 22 Jul 2012 09:56:34 +0200 | |
changeset 49442 | 571cb1df0768 |
child 53572 | 6646bb548c6b |
permissions | -rw-r--r-- |
haftmann@49442 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
haftmann@49442 | 2 |
|
haftmann@49442 | 3 |
header {* Futures and parallel lists for code generated towards Isabelle/ML *} |
haftmann@49442 | 4 |
|
haftmann@49442 | 5 |
theory Parallel |
haftmann@49442 | 6 |
imports Main |
haftmann@49442 | 7 |
begin |
haftmann@49442 | 8 |
|
haftmann@49442 | 9 |
subsection {* Futures *} |
haftmann@49442 | 10 |
|
haftmann@49442 | 11 |
datatype 'a future = fork "unit \<Rightarrow> 'a" |
haftmann@49442 | 12 |
|
haftmann@49442 | 13 |
primrec join :: "'a future \<Rightarrow> 'a" where |
haftmann@49442 | 14 |
"join (fork f) = f ()" |
haftmann@49442 | 15 |
|
haftmann@49442 | 16 |
lemma future_eqI [intro!]: |
haftmann@49442 | 17 |
assumes "join f = join g" |
haftmann@49442 | 18 |
shows "f = g" |
haftmann@49442 | 19 |
using assms by (cases f, cases g) (simp add: ext) |
haftmann@49442 | 20 |
|
haftmann@49442 | 21 |
code_type future |
haftmann@49442 | 22 |
(Eval "_ future") |
haftmann@49442 | 23 |
|
haftmann@49442 | 24 |
code_const fork |
haftmann@49442 | 25 |
(Eval "Future.fork") |
haftmann@49442 | 26 |
|
haftmann@49442 | 27 |
code_const join |
haftmann@49442 | 28 |
(Eval "Future.join") |
haftmann@49442 | 29 |
|
haftmann@49442 | 30 |
code_reserved Eval Future future |
haftmann@49442 | 31 |
|
haftmann@49442 | 32 |
|
haftmann@49442 | 33 |
subsection {* Parallel lists *} |
haftmann@49442 | 34 |
|
haftmann@49442 | 35 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where |
haftmann@49442 | 36 |
[simp]: "map = List.map" |
haftmann@49442 | 37 |
|
haftmann@49442 | 38 |
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
haftmann@49442 | 39 |
"forall = list_all" |
haftmann@49442 | 40 |
|
haftmann@49442 | 41 |
lemma forall_all [simp]: |
haftmann@49442 | 42 |
"forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)" |
haftmann@49442 | 43 |
by (simp add: forall_def list_all_iff) |
haftmann@49442 | 44 |
|
haftmann@49442 | 45 |
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
haftmann@49442 | 46 |
"exists = list_ex" |
haftmann@49442 | 47 |
|
haftmann@49442 | 48 |
lemma exists_ex [simp]: |
haftmann@49442 | 49 |
"exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)" |
haftmann@49442 | 50 |
by (simp add: exists_def list_ex_iff) |
haftmann@49442 | 51 |
|
haftmann@49442 | 52 |
code_const map |
haftmann@49442 | 53 |
(Eval "Par'_List.map") |
haftmann@49442 | 54 |
|
haftmann@49442 | 55 |
code_const forall |
haftmann@49442 | 56 |
(Eval "Par'_List.forall") |
haftmann@49442 | 57 |
|
haftmann@49442 | 58 |
code_const exists |
haftmann@49442 | 59 |
(Eval "Par'_List.exists") |
haftmann@49442 | 60 |
|
haftmann@49442 | 61 |
code_reserved Eval Par_List |
haftmann@49442 | 62 |
|
haftmann@49442 | 63 |
|
haftmann@49442 | 64 |
hide_const (open) fork join map exists forall |
haftmann@49442 | 65 |
|
haftmann@49442 | 66 |
end |
haftmann@49442 | 67 |