(* Title: HOL/HOLCF/ex/Concurrency_Monad.thy Author: Brian Huffman *) theory Concurrency_Monad 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" 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 {* Resumption-state-nondeterminism monad *} 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 {* 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 (no_asm) add: mapN_mapN) apply simp done subsection {* Monadic bind function *} 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 {* 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 @{text 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 *) 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 {* Other miscellaneous properties about @{text 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 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 {* 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 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 = `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