src/HOL/Library/Parallel.thy

tuned window position;

(* Author: Florian Haftmann, TU Muenchen *)

header {* Futures and parallel lists for code generated towards Isabelle/ML *}

theory Parallel
imports Main
begin

subsection {* Futures *}

datatype 'a future = fork "unit \<Rightarrow> 'a"

primrec join :: "'a future \<Rightarrow> '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_type future
  (Eval "_ future")

code_const fork
  (Eval "Future.fork")

code_const join
  (Eval "Future.join")

code_reserved Eval Future future


subsection {* Parallel lists *}

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

definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "forall = list_all"

lemma forall_all [simp]:
  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
  by (simp add: forall_def list_all_iff)

definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "exists = list_ex"

lemma exists_ex [simp]:
  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
  by (simp add: exists_def list_ex_iff)

code_const map
  (Eval "Par'_List.map")

code_const forall
  (Eval "Par'_List.forall")

code_const exists
  (Eval "Par'_List.exists")

code_reserved Eval Par_List


hide_const (open) fork join map exists forall

end