src/HOL/Library/Parallel.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 48427 571cb1df0768
child 58249 180f1b3508ed
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann@48427
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@48427
     2
haftmann@48427
     3
header {* Futures and parallel lists for code generated towards Isabelle/ML *}
haftmann@48427
     4
haftmann@48427
     5
theory Parallel
haftmann@48427
     6
imports Main
haftmann@48427
     7
begin
haftmann@48427
     8
haftmann@48427
     9
subsection {* Futures *}
haftmann@48427
    10
haftmann@48427
    11
datatype 'a future = fork "unit \<Rightarrow> 'a"
haftmann@48427
    12
haftmann@48427
    13
primrec join :: "'a future \<Rightarrow> 'a" where
haftmann@48427
    14
  "join (fork f) = f ()"
haftmann@48427
    15
haftmann@48427
    16
lemma future_eqI [intro!]:
haftmann@48427
    17
  assumes "join f = join g"
haftmann@48427
    18
  shows "f = g"
haftmann@48427
    19
  using assms by (cases f, cases g) (simp add: ext)
haftmann@48427
    20
haftmann@52435
    21
code_printing
haftmann@52435
    22
  type_constructor future \<rightharpoonup> (Eval) "_ future"
haftmann@52435
    23
| constant fork \<rightharpoonup> (Eval) "Future.fork"
haftmann@52435
    24
| constant join \<rightharpoonup> (Eval) "Future.join"
haftmann@48427
    25
haftmann@48427
    26
code_reserved Eval Future future
haftmann@48427
    27
haftmann@48427
    28
haftmann@48427
    29
subsection {* Parallel lists *}
haftmann@48427
    30
haftmann@48427
    31
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
haftmann@48427
    32
  [simp]: "map = List.map"
haftmann@48427
    33
haftmann@48427
    34
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
haftmann@48427
    35
  "forall = list_all"
haftmann@48427
    36
haftmann@48427
    37
lemma forall_all [simp]:
haftmann@48427
    38
  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
haftmann@48427
    39
  by (simp add: forall_def list_all_iff)
haftmann@48427
    40
haftmann@48427
    41
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
haftmann@48427
    42
  "exists = list_ex"
haftmann@48427
    43
haftmann@48427
    44
lemma exists_ex [simp]:
haftmann@48427
    45
  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
haftmann@48427
    46
  by (simp add: exists_def list_ex_iff)
haftmann@48427
    47
haftmann@52435
    48
code_printing
haftmann@52435
    49
  constant map \<rightharpoonup> (Eval) "Par'_List.map"
haftmann@52435
    50
| constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
haftmann@52435
    51
| constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
haftmann@48427
    52
haftmann@48427
    53
code_reserved Eval Par_List
haftmann@48427
    54
haftmann@48427
    55
haftmann@48427
    56
hide_const (open) fork join map exists forall
haftmann@48427
    57
haftmann@48427
    58
end
haftmann@48427
    59