Theory HOL-Library.Parallel

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Futures and parallel lists for code generated towards Isabelle/ML›

theory Parallel
imports Main
begin

subsection ‹Futures›

datatype 'a future = fork "unit  'a"

primrec join :: "'a future  'a" where
  "join (fork f) = f ()"

lemma future_eqI [intro!]:
  assumes "join f = join g"
  shows "f = g"
  using assms by (cases f, cases g) (simp add: ext)

code_printing
  type_constructor future  (Eval) "_ future"
| constant fork  (Eval) "Future.fork"
| constant join  (Eval) "Future.join"

code_reserved Eval Future future


subsection ‹Parallel lists›

definition map :: "('a  'b)  'a list  'b list" where
  [simp]: "map = List.map"

definition forall :: "('a  bool)  'a list  bool" where
  "forall = list_all"

lemma forall_all [simp]:
  "forall P xs  (xset xs. P x)"
  by (simp add: forall_def list_all_iff)

definition exists :: "('a  bool)  'a list  bool" where
  "exists = list_ex"

lemma exists_ex [simp]:
  "exists P xs  (xset xs. P x)"
  by (simp add: exists_def list_ex_iff)

code_printing
  constant map  (Eval) "Par'_List.map"
| constant forall  (Eval) "Par'_List.forall"
| constant exists  (Eval) "Par'_List.exists"

code_reserved Eval Par_List


hide_const (open) fork join map exists forall

end