src/HOL/Library/Parallel.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52435 6646bb548c6b
child 58249 180f1b3508ed
permissions -rw-r--r--
more simplification rules on unary and binary minus
     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_printing
    22   type_constructor future \<rightharpoonup> (Eval) "_ future"
    23 | constant fork \<rightharpoonup> (Eval) "Future.fork"
    24 | constant join \<rightharpoonup> (Eval) "Future.join"
    25 
    26 code_reserved Eval Future future
    27 
    28 
    29 subsection {* Parallel lists *}
    30 
    31 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    32   [simp]: "map = List.map"
    33 
    34 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    35   "forall = list_all"
    36 
    37 lemma forall_all [simp]:
    38   "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    39   by (simp add: forall_def list_all_iff)
    40 
    41 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    42   "exists = list_ex"
    43 
    44 lemma exists_ex [simp]:
    45   "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
    46   by (simp add: exists_def list_ex_iff)
    47 
    48 code_printing
    49   constant map \<rightharpoonup> (Eval) "Par'_List.map"
    50 | constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
    51 | constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
    52 
    53 code_reserved Eval Par_List
    54 
    55 
    56 hide_const (open) fork join map exists forall
    57 
    58 end
    59