# Theory 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 ⟷ (∀x∈set xs. P x)"

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

lemma exists_ex [simp]:
"exists P xs ⟷ (∃x∈set xs. P x)"

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

```