imports HOLCF
```(*  Title:      HOL/HOLCF/ex/Concurrency_Monad.thy
Author:     Brian Huffman
*)

imports HOLCF
begin

text ‹This file contains the concurrency monad example from
Chapter 7 of the author's PhD thesis.›

subsection ‹State/nondeterminism monad, as a type synonym›

type_synonym ('s, 'a) N = "'s → ('a u ⊗ 's u)♮"

definition mapN :: "('a → 'b) → ('s, 'a) N → ('s, 'b) N"
where "mapN = (Λ f. cfun_map⋅ID⋅(convex_map⋅(sprod_map⋅(u_map⋅f)⋅ID)))"

definition unitN :: "'a → ('s, 'a) N"
where "unitN = (Λ x. (Λ s. convex_unit⋅(:up⋅x, up⋅s:)))"

definition bindN :: "('s, 'a) N → ('a → ('s, 'b) N) → ('s, 'b) N"
where "bindN = (Λ c k. (Λ s. convex_bind⋅(c⋅s)⋅(Λ (:up⋅x, up⋅s':). k⋅x⋅s')))"

definition plusN :: "('s, 'a) N → ('s, 'a) N → ('s, 'a) N"
where "plusN = (Λ a b. (Λ s. convex_plus⋅(a⋅s)⋅(b⋅s)))"

lemma mapN_ID: "mapN⋅ID = ID"

lemma mapN_mapN: "mapN⋅f⋅(mapN⋅g⋅m) = mapN⋅(Λ x. f⋅(g⋅x))⋅m"
unfolding mapN_def ID_def
by (simp add: cfun_map_map convex_map_map sprod_map_map u_map_map eta_cfun)

lemma mapN_unitN: "mapN⋅f⋅(unitN⋅x) = unitN⋅(f⋅x)"
unfolding mapN_def unitN_def

lemma bindN_unitN: "bindN⋅(unitN⋅a)⋅f = f⋅a"
by (simp add: unitN_def bindN_def eta_cfun)

lemma mapN_conv_bindN: "mapN⋅f⋅m = bindN⋅m⋅(unitN oo f)"
apply (simp add: mapN_def bindN_def unitN_def)
apply (rule cfun_eqI, simp)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, simp, rename_tac p)
apply (case_tac p, simp)
apply (case_tac x, simp)
apply (case_tac y, simp)
apply simp
done

lemma bindN_unitN_right: "bindN⋅m⋅unitN = m"
proof -
have "mapN⋅ID⋅m = m" by (simp add: mapN_ID)
thus ?thesis by (simp add: mapN_conv_bindN)
qed

lemma bindN_bindN:
"bindN⋅(bindN⋅m⋅f)⋅g = bindN⋅m⋅(Λ x. bindN⋅(f⋅x)⋅g)"
apply (rule cfun_eqI, rename_tac s)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, rename_tac w)
apply (case_tac w, simp)
apply (case_tac x, simp)
apply (case_tac y, simp)
apply simp
done

lemma mapN_bindN: "mapN⋅f⋅(bindN⋅m⋅g) = bindN⋅m⋅(Λ x. mapN⋅f⋅(g⋅x))"

lemma bindN_mapN: "bindN⋅(mapN⋅f⋅m)⋅g = bindN⋅m⋅(Λ x. g⋅(f⋅x))"
by (simp add: mapN_conv_bindN bindN_bindN bindN_unitN)

lemma mapN_plusN:
"mapN⋅f⋅(plusN⋅a⋅b) = plusN⋅(mapN⋅f⋅a)⋅(mapN⋅f⋅b)"
unfolding mapN_def plusN_def by (simp add: cfun_map_def)

lemma plusN_commute: "plusN⋅a⋅b = plusN⋅b⋅a"
unfolding plusN_def by (simp add: convex_plus_commute)

lemma plusN_assoc: "plusN⋅(plusN⋅a⋅b)⋅c = plusN⋅a⋅(plusN⋅b⋅c)"
unfolding plusN_def by (simp add: convex_plus_assoc)

lemma plusN_absorb: "plusN⋅a⋅a = a"
unfolding plusN_def by (simp add: eta_cfun)

domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")

thm R.take_induct

lemma R_induct [case_names adm bottom Done More, induct type: R]:
fixes P :: "('s, 'a) R ⇒ bool"
assumes bottom: "P ⊥"
assumes Done: "⋀x. P (Done⋅x)"
assumes More: "⋀p c. (⋀r::('s, 'a) R. P (p⋅r)) ⟹ P (More⋅(mapN⋅p⋅c))"
shows "P r"
proof (induct r rule: R.take_induct)
next
fix n
show "P (R_take n⋅r)"
proof (induct n arbitrary: r)
case 0 show ?case by (simp add: bottom)
next
case (Suc n r)
show ?case
apply (cases r)
using More [OF Suc]
done
qed
qed

declare R.take_rews(2) [simp del]

lemma R_take_Suc_More [simp]:
"R_take (Suc n)⋅(More⋅k) = More⋅(mapN⋅(R_take n)⋅k)"

subsection ‹Map function›

fixrec mapR :: "('a → 'b) → ('s, 'a) R → ('s, 'b) R"
where "mapR⋅f⋅(Done⋅a) = Done⋅(f⋅a)"
| "mapR⋅f⋅(More⋅k) = More⋅(mapN⋅(mapR⋅f)⋅k)"

lemma mapR_strict [simp]: "mapR⋅f⋅⊥ = ⊥"
by fixrec_simp

lemma mapR_mapR: "mapR⋅f⋅(mapR⋅g⋅r) = mapR⋅(Λ x. f⋅(g⋅x))⋅r"
by (induct r) (simp_all add: mapN_mapN)

lemma mapR_ID: "mapR⋅ID⋅r = r"
by (induct r) (simp_all add: mapN_mapN eta_cfun)

lemma "mapR⋅f⋅(mapR⋅g⋅r) = mapR⋅(Λ x. f⋅(g⋅x))⋅r"
apply (induct r)
apply simp
apply simp
apply simp
apply (simp (no_asm))
apply simp
done

fixrec bindR :: "('s, 'a) R → ('a → ('s, 'b) R) → ('s, 'b) R"
where "bindR⋅(Done⋅x)⋅k = k⋅x"
| "bindR⋅(More⋅c)⋅k = More⋅(mapN⋅(Λ r. bindR⋅r⋅k)⋅c)"

lemma bindR_strict [simp]: "bindR⋅⊥⋅k = ⊥"
by fixrec_simp

lemma bindR_Done_right: "bindR⋅r⋅Done = r"
by (induct r) (simp_all add: mapN_mapN eta_cfun)

lemma mapR_conv_bindR: "mapR⋅f⋅r = bindR⋅r⋅(Λ x. Done⋅(f⋅x))"
by (induct r) (simp_all add: mapN_mapN)

lemma bindR_bindR: "bindR⋅(bindR⋅r⋅f)⋅g = bindR⋅r⋅(Λ x. bindR⋅(f⋅x)⋅g)"
by (induct r) (simp_all add: mapN_mapN)

lemma "bindR⋅(bindR⋅r⋅f)⋅g = bindR⋅r⋅(Λ x. bindR⋅(f⋅x)⋅g)"
apply (induct r)
done

subsection ‹Zip function›

fixrec zipR :: "('a → 'b → 'c) → ('s, 'a) R → ('s, 'b) R → ('s, 'c) R"
where zipR_Done_Done:
"zipR⋅f⋅(Done⋅x)⋅(Done⋅y) = Done⋅(f⋅x⋅y)"
| zipR_Done_More:
"zipR⋅f⋅(Done⋅x)⋅(More⋅b) =
More⋅(mapN⋅(Λ r. zipR⋅f⋅(Done⋅x)⋅r)⋅b)"
| zipR_More_Done:
"zipR⋅f⋅(More⋅a)⋅(Done⋅y) =
More⋅(mapN⋅(Λ r. zipR⋅f⋅r⋅(Done⋅y))⋅a)"
| zipR_More_More:
"zipR⋅f⋅(More⋅a)⋅(More⋅b) =
More⋅(plusN⋅(mapN⋅(Λ r. zipR⋅f⋅(More⋅a)⋅r)⋅b)
⋅(mapN⋅(Λ r. zipR⋅f⋅r⋅(More⋅b))⋅a))"

lemma zipR_strict1 [simp]: "zipR⋅f⋅⊥⋅r = ⊥"
by fixrec_simp

lemma zipR_strict2 [simp]: "zipR⋅f⋅r⋅⊥ = ⊥"
by (fixrec_simp, cases r, simp_all)

abbreviation apR (infixl "⋄" 70)
where "a ⋄ b ≡ zipR⋅ID⋅a⋅b"

text ‹Proofs that ‹zipR› satisfies the applicative functor laws:›

lemma R_homomorphism: "Done⋅f ⋄ Done⋅x = Done⋅(f⋅x)"
by simp

lemma R_identity: "Done⋅ID ⋄ r = r"
by (induct r, simp_all add: mapN_mapN eta_cfun)

lemma R_interchange: "r ⋄ Done⋅x = Done⋅(Λ f. f⋅x) ⋄ r"
by (induct r, simp_all add: mapN_mapN)

text ‹The associativity rule is the hard one!›

lemma R_associativity: "Done⋅cfcomp ⋄ r1 ⋄ r2 ⋄ r3 = r1 ⋄ (r2 ⋄ r3)"
proof (induct r1 arbitrary: r2 r3)
case (Done x1) thus ?case
proof (induct r2 arbitrary: r3)
case (Done x2) thus ?case
proof (induct r3)
case (More p3 c3) thus ?case (* Done/Done/More *)
qed simp_all
next
case (More p2 c2) thus ?case
proof (induct r3)
case (Done x3) thus ?case (* Done/More/Done *)
next
case (More p3 c3) thus ?case (* Done/More/More *)
qed simp_all
qed simp_all
next
case (More p1 c1) thus ?case
proof (induct r2 arbitrary: r3)
case (Done y) thus ?case
proof (induct r3)
case (Done x3) thus ?case
next
case (More p3 c3) thus ?case
qed simp_all
next
case (More p2 c2) thus ?case
proof (induct r3)
case (Done x3) thus ?case
next
case (More p3 c3) thus ?case
by (simp add: mapN_mapN mapN_plusN plusN_assoc)
qed simp_all
qed simp_all
qed simp_all

text ‹Other miscellaneous properties about ‹zipR›:›

lemma zipR_Done_left:
shows "zipR⋅f⋅(Done⋅x)⋅r = mapR⋅(f⋅x)⋅r"
by (induct r) (simp_all add: mapN_mapN)

lemma zipR_Done_right:
shows "zipR⋅f⋅r⋅(Done⋅y) = mapR⋅(Λ x. f⋅x⋅y)⋅r"
by (induct r) (simp_all add: mapN_mapN)

lemma mapR_zipR: "mapR⋅h⋅(zipR⋅f⋅a⋅b) = zipR⋅(Λ x y. h⋅(f⋅x⋅y))⋅a⋅b"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right mapR_mapR)
apply (induct_tac b)
apply simp
apply simp
done

lemma zipR_mapR_left: "zipR⋅f⋅(mapR⋅h⋅a)⋅b = zipR⋅(Λ x y. f⋅(h⋅x)⋅y)⋅a⋅b"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
apply (induct_tac b)
apply simp
apply simp
done

lemma zipR_mapR_right: "zipR⋅f⋅a⋅(mapR⋅h⋅b) = zipR⋅(Λ x y. f⋅x⋅(h⋅y))⋅a⋅b"
apply (induct b arbitrary: a)
apply simp
apply simp
apply (induct_tac a)
apply simp
apply simp
done

lemma zipR_commute:
assumes f: "⋀x y. f⋅x⋅y = g⋅y⋅x"
shows "zipR⋅f⋅a⋅b = zipR⋅g⋅b⋅a"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right f [symmetric] eta_cfun)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: mapN_mapN mapN_plusN plusN_commute)
done

lemma zipR_assoc:
fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
fixes f :: "'a → 'b → 'd" and g :: "'d → 'c → 'e"
assumes gf: "⋀x y z. g⋅(f⋅x⋅y)⋅z = h⋅x⋅(k⋅y⋅z)"
shows "zipR⋅g⋅(zipR⋅f⋅a⋅b)⋅c = zipR⋅h⋅a⋅(zipR⋅k⋅b⋅c)" (is "?P a b c")
apply (induct a arbitrary: b c)
apply simp
apply simp
apply (simp add: zipR_mapR_left mapR_zipR gf)
apply (rename_tac pA kA b c)
apply (rule_tac x=c in spec)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
apply (rule allI, rename_tac c)
apply (induct_tac c)
apply simp
apply simp
apply (rename_tac z)
apply (rename_tac pC kC)
apply (rename_tac pB kB)
apply (rule allI, rename_tac c)
apply (induct_tac c)
apply simp
apply simp
apply (rename_tac pC kC)
apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
done

text ‹Alternative proof using take lemma.›

lemma
fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
fixes f :: "'a → 'b → 'd" and g :: "'d → 'c → 'e"
assumes gf: "⋀x y z. g⋅(f⋅x⋅y)⋅z = h⋅x⋅(k⋅y⋅z)"
shows "zipR⋅g⋅(zipR⋅f⋅a⋅b)⋅c = zipR⋅h⋅a⋅(zipR⋅k⋅b⋅c)"
(is "?lhs = ?rhs" is "?P a b c")
proof (rule R.take_lemma)
fix n show "R_take n⋅?lhs = R_take n⋅?rhs"
proof (induct n arbitrary: a b c)
case (0 a b c)
show ?case by simp
next
case (Suc n a b c)
note IH = this
let ?P = ?case
show ?case
proof (cases a)
case bottom thus ?P by simp
next
case (Done x) thus ?P
by (simp add: zipR_Done_left zipR_mapR_left mapR_zipR gf)
next
case (More nA) thus ?P
proof (cases b)
case bottom thus ?P by simp
next
case (Done y) thus ?P
zipR_mapR_left zipR_mapR_right gf)
next
case (More nB) thus ?P
proof (cases c)
case bottom thus ?P by simp
next
case (Done z) thus ?P
by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
next
case (More nC)
note H = ‹a = More⋅nA› ‹b = More⋅nB› ‹c = More⋅nC›
show ?P
apply (simp only: H zipR_More_More)
apply (simplesubst zipR_More_More [of f, symmetric])
apply (simplesubst zipR_More_More [of k, symmetric])
apply (simp only: H [symmetric])
apply (simp add: mapN_mapN mapN_plusN plusN_assoc IH)
done
qed
qed
qed
qed
qed

end
```