src/HOL/Library/Parallel.thy
author Christian Sternagel
Thu, 30 Aug 2012 13:05:11 +0900
changeset 49087 7a17ba4bc997
parent 48427 571cb1df0768
child 52435 6646bb548c6b
permissions -rw-r--r--
added author
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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