src/HOL/Library/Parallel.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60500 903bb1495239
permissions -rw-r--r--
more symbols;
haftmann@48427
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@48427
     2
wenzelm@60500
     3
section \<open>Futures and parallel lists for code generated towards Isabelle/ML\<close>
haftmann@48427
     4
haftmann@48427
     5
theory Parallel
haftmann@48427
     6
imports Main
haftmann@48427
     7
begin
haftmann@48427
     8
wenzelm@60500
     9
subsection \<open>Futures\<close>
haftmann@48427
    10
blanchet@58310
    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
wenzelm@60500
    29
subsection \<open>Parallel lists\<close>
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