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