(* Title: HOL/HOLCF/ex/Concurrency_Monad.thy
Author: Brian Huffman
*)
theory Concurrency_Monad
imports HOLCF
begin
text \<open>This file contains the concurrency monad example from
Chapter 7 of the author's PhD thesis.\
subsection \<open>State/nondeterminism monad, as a type synonym\<close>
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"
by (simp add: mapN_def domain_map_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
by (simp add: cfun_map_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 (simp add: convex_map_def)
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 (simp add: bindN_def)
apply (simp add: convex_bind_bind)
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))"
by (simp add: mapN_conv_bindN bindN_bindN)
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)
subsection \<open>Resumption-state-nondeterminism monad\<close>
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 adm: "adm P"
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)
show "adm P" by fact
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)
apply (simp add: bottom)
apply (simp add: Done)
using More [OF Suc]
apply (simp add: mapN_def)
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)"
by (simp add: mapN_def R.take_rews(2))
subsection \<open>Map function\<close>
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 (no_asm) add: mapN_mapN)
apply simp
done
subsection \<open>Monadic bind function\<close>
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)
apply (simp_all add: mapN_mapN)
done
subsection \<open>Zip function\<close>
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\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r)\<cdot>b)"
| zipR_More_Done:
"zipR\f\(More\a)\(Done\y) =
More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y))\<cdot>a)"
| zipR_More_More:
"zipR\f\(More\a)\(More\b) =
More\<cdot>(plusN\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>r)\<cdot>b)
\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(More\<cdot>b))\<cdot>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 \<open>Proofs that \<open>zipR\<close> satisfies the applicative functor laws:\<close>
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 \<open>The associativity rule is the hard one!\<close>
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 *)
by (simp add: mapN_mapN)
qed simp_all
next
case (More p2 c2) thus ?case
proof (induct r3)
case (Done x3) thus ?case (* Done/More/Done *)
by (simp add: mapN_mapN)
next
case (More p3 c3) thus ?case (* Done/More/More *)
by (simp add: mapN_mapN mapN_plusN)
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
by (simp add: mapN_mapN)
next
case (More p3 c3) thus ?case
by (simp add: mapN_mapN)
qed simp_all
next
case (More p2 c2) thus ?case
proof (induct r3)
case (Done x3) thus ?case
by (simp add: mapN_mapN mapN_plusN)
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 \<open>Other miscellaneous properties about \<open>zipR\<close>:\<close>
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
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN mapN_plusN)
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 (simp add: mapN_mapN)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN)
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 (simp add: zipR_Done_left zipR_Done_right)
apply (simp add: mapN_mapN)
apply (induct_tac a)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN)
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)
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_Done_left zipR_Done_right)
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: mapN_mapN)
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
apply (simp add: zipR_mapR_right)
apply (rule allI, rename_tac c)
apply (induct_tac c)
apply simp
apply simp
apply (rename_tac z)
apply (simp add: mapN_mapN)
apply (simp add: zipR_mapR_left gf)
apply (rename_tac pC kC)
apply (simp add: mapN_mapN)
apply (simp add: zipR_mapR_left gf)
apply (rename_tac pB kB)
apply (rule allI, rename_tac c)
apply (induct_tac c)
apply simp
apply simp
apply (simp add: mapN_mapN mapN_plusN)
apply (rename_tac pC kC)
apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
done
text \<open>Alternative proof using take lemma.\<close>
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
by (simp add: zipR_Done_left zipR_Done_right
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 = \<open>a = More\<cdot>nA\<close> \<open>b = More\<cdot>nB\<close> \<open>c = More\<cdot>nC\<close>
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
