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