src/HOL/Library/Parallel.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 48427 571cb1df0768
child 52435 6646bb548c6b
permissions -rw-r--r--
tuned headers;
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@48427
    21
code_type future
haftmann@48427
    22
  (Eval "_ future")
haftmann@48427
    23
haftmann@48427
    24
code_const fork
haftmann@48427
    25
  (Eval "Future.fork")
haftmann@48427
    26
haftmann@48427
    27
code_const join
haftmann@48427
    28
  (Eval "Future.join")
haftmann@48427
    29
haftmann@48427
    30
code_reserved Eval Future future
haftmann@48427
    31
haftmann@48427
    32
haftmann@48427
    33
subsection {* Parallel lists *}
haftmann@48427
    34
haftmann@48427
    35
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
haftmann@48427
    36
  [simp]: "map = List.map"
haftmann@48427
    37
haftmann@48427
    38
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
haftmann@48427
    39
  "forall = list_all"
haftmann@48427
    40
haftmann@48427
    41
lemma forall_all [simp]:
haftmann@48427
    42
  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
haftmann@48427
    43
  by (simp add: forall_def list_all_iff)
haftmann@48427
    44
haftmann@48427
    45
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
haftmann@48427
    46
  "exists = list_ex"
haftmann@48427
    47
haftmann@48427
    48
lemma exists_ex [simp]:
haftmann@48427
    49
  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
haftmann@48427
    50
  by (simp add: exists_def list_ex_iff)
haftmann@48427
    51
haftmann@48427
    52
code_const map
haftmann@48427
    53
  (Eval "Par'_List.map")
haftmann@48427
    54
haftmann@48427
    55
code_const forall
haftmann@48427
    56
  (Eval "Par'_List.forall")
haftmann@48427
    57
haftmann@48427
    58
code_const exists
haftmann@48427
    59
  (Eval "Par'_List.exists")
haftmann@48427
    60
haftmann@48427
    61
code_reserved Eval Par_List
haftmann@48427
    62
haftmann@48427
    63
haftmann@48427
    64
hide_const (open) fork join map exists forall
haftmann@48427
    65
haftmann@48427
    66
end
haftmann@48427
    67