(* The Isabelle/HOL proof script accompanying the paper "Algebra Unifies Operational Calculi" *) theory AlgebraUnifiesOperationalCalculi imports Main begin declare [[ smt_solver = remote_z3]] declare [[ smt_timeout = 60 ]] declare [[ z3_options = "-memory:500" ]] section {* The basic algebra *} locale basicalgebra = fixes refinement :: "'a \ 'a \ bool" (infix "\" 50) and disjunction :: "'a \ 'a \ 'a" (infixl "\" 65) and conjunction :: "'a \ 'a \ 'a" (infixl "\" 70) and semicolon :: "'a \ 'a \ 'a" (infixl ";" 80) and concurrency :: "'a \ 'a \ 'a" (infixl "\" 80) and bottom :: "'a" ("\") and top :: "'a" ("\") and skip :: "'a" and iteration :: "'a \ 'a" ("_\<^sup>\" [101] 100) assumes refinement_reflexive: "x\x" and refinement_transitive: "x\y \ y\z \ x\z" and refinement_antisymmetric: "x\y \ y\x \ x=y" and disj_increasing1: "x \ x\y" and disj_increasing2: "y \ x\y" and disj_lub: "x\z \ y\z \ x\y \ z" and conj_decreasing1: "x\y \ x" and conj_decreasing2: "x\y \ y" and conj_glb: "x \ y \ x \ z \ x \ y\z" (* The table *) assumes disjunction_commutative: "x\y = y\x" and disjunction_associative: "x\(y\z) = (x\y)\z" and disjunction_idempotent: "x\x = x" and disjunction_left_unit: "\\x = x" and disjunction_right_unit: "x\\ = x" and disjunction_left_zero: "\\x = \" and disjunction_right_zero: "x\\ = \" and conjunction_commutative: "x\y = y\x" and conjunction_associative: "x\(y\z) = (x\y)\z" and conjunction_idempotent: "x\x = x" and conjunction_left_unit: "\\x = x" and conjunction_right_unit: "x\\ = x" and conjunction_left_zero: "\\x = \" and conjunction_right_zero: "x\\ = \" and semicolon_associative: "x;(y;z) = (x;y);z" and semicolon_left_unit: "skip;x = x" and semicolon_right_unit: "x;skip = x" and semicolon_left_zero: "\;x = \" and semicolon_right_zero: "x;\ = \" and concurrency_commutative: "x\y = y\x" and concurrency_associative: "x\(y\z) = (x\y)\z" and concurrency_left_unit: "skip\x = x" and concurrency_right_unit: "x\skip = x" and concurrency_left_zero: "\\x = \" and concurrency_right_zero: "x\\ = \" (* Distribution laws *) fixes distr_through_disj_p :: "('a \ 'a \ 'a) \ bool" defines "distr_through_disj_p f \ (\ x y z . (f x (y\z) = (f x y) \ (f x z)) \ (f (x\y) z) = ((f x z) \ (f y z)))" assumes disj_distr_through_disj: "distr_through_disj_p (op \)" and conj_distr_through_disj: "distr_through_disj_p (op \)" and semicolon_distr_through_disj: "distr_through_disj_p (op ;)" and concurrency_distr_through_disj: "distr_through_disj_p (op \)" and exchange: "(p\q);(r\s) \ (p;r)\(q;s)" (* Kleene star laws *) assumes iter1: "skip \ (p;p\<^sup>\) \ p\<^sup>\" and iter2: "p \ (q;r) \ r \ q\<^sup>\;p \ r" and iter3: "skip \ (p\<^sup>\;p) \ p\<^sup>\" and iter4: "p \ (r;q) \ r \ p;q\<^sup>\ \ r" (* Auxiliary definitions. They appear here because otherwise the sublocale handling will raise problems later. *) fixes lessthan :: "'a \ 'a \ bool" (infix "\" 50) defines "x\y \ (x\y) \ \(y\x)" fixes monotone_p :: "('a \ 'a \ 'a) \ bool" defines "monotone_p f \ (\ x y z . (x \ y \ (f x z) \ (f y z))) \ (\ x y z . (y \ z \ (f x y) \ (f x z)))" (* Don't define backsemicolon x y \ y;x explicitly - it will make automation difficult. *) begin text {* Simple consequences of the laws. *} lemma conj_disj_relationship: "q=p\q \ p=p\q" by (metis conj_decreasing1 conj_decreasing2 conj_glb disj_increasing1 disj_increasing2 disj_lub refinement_antisymmetric refinement_reflexive) lemma refinement_disj: "x\y \ y=x\y" by (metis disj_increasing1 disj_increasing2 disj_lub refinement_antisymmetric refinement_reflexive) lemma refinement_conj: "x\y \ x=x\y" by (metis conj_decreasing2 conj_disj_relationship refinement_disj) lemma bottom_least: "\\x" by (metis disj_increasing2 disjunction_right_unit) lemma top_greatest: "x\\" by (metis conj_decreasing1 conjunction_left_unit) lemma iter_unfold1: "skip \ p\<^sup>\" by (metis disj_increasing1 iter1 refinement_transitive) lemma iter_unfold2: "p;p\<^sup>\ \ p\<^sup>\" by (metis disj_increasing2 iter1 refinement_transitive) text {* Any operator that distributes through disjunction is monotone. *} lemma distr_through_disj_implies_monotone: "distr_through_disj_p f \ monotone_p f" by (metis (full_types) distr_through_disj_p_def monotone_p_def refinement_disj) text {* The binary operators are therefore monotone. *} lemma disj_monotone: "monotone_p (op \)" by (metis disj_distr_through_disj distr_through_disj_implies_monotone) lemma conj_monotone: "monotone_p (op \)" by (metis conj_distr_through_disj distr_through_disj_implies_monotone) lemma semicolon_monotone: "monotone_p (op ;)" by (metis semicolon_distr_through_disj distr_through_disj_implies_monotone) lemma concurrency_monotone: "monotone_p (op \)" by (metis concurrency_distr_through_disj distr_through_disj_implies_monotone) text {* Lemmas that aid automation. *} lemma disj_monotone1: "x \ y \ x\z \ y\z" by (metis monotone_p_def disj_monotone) lemma conj_monotone1: "x \ y \ x\z \ y\z" by (metis monotone_p_def conj_monotone) lemma semicolon_monotone1: "x \ y \ x;z \ y;z" by (metis monotone_p_def semicolon_monotone) lemma concurrency_monotone1: "x \ y \ x\z \ y\z" by (metis monotone_p_def concurrency_monotone) lemma disj_monotone2: "y \ z \ x\y \ x\z" by (metis monotone_p_def disj_monotone) lemma conj_monotone2: "y \ z \ x\y \ x\z" by (metis monotone_p_def conj_monotone) lemma semicolon_monotone2: "y \ z \ x;y \ x;z" by (metis monotone_p_def semicolon_monotone) lemma concurrency_monotone2: "y \ z \ x\y \ x\z" by (metis monotone_p_def concurrency_monotone) text {* The small exchange laws hold. *} lemma small_exchange1: "x;(y\z) \ (x;y)\z" by (metis concurrency_right_unit exchange semicolon_left_unit) lemma small_exchange2: "(x\y);z \ x\(y;z)" by (metis concurrency_left_unit exchange semicolon_right_unit) text {* Sequential composition is a special case of concurrent composition *} lemma seq_refines_conc: "x;y \ x\y" by (metis concurrency_right_unit semicolon_left_unit small_exchange2) text {* Any monotone operator exchanges with conjunction. *} lemma monotone_op_exchanges_with_conj: "monotone_p f \ f (w \ x) (y \ z) \ (f w y)\(f x z)" proof - assume ap: "monotone_p f" have a: "f (w \ x) (y \ z) \ f w y" by (metis monotone_p_def ap conj_decreasing1 refinement_transitive) have b: "f (w \ x) (y \ z) \ f x z" by (metis monotone_p_def ap conjunction_commutative conj_decreasing1 refinement_transitive) from a b show ?thesis by (metis conj_disj_relationship conjunction_associative refinement_disj) qed text {* In particular, sequential composition exchanges with conjunction. *} lemma conjunction_exchange: "(w\x);(y\z) \ (w;y)\(x;z)" by (metis monotone_op_exchanges_with_conj semicolon_monotone) text {* Time reversal duality (opposition). *} lemma time_reversal: "basicalgebra (op \) (op \) (op \) (\ x y . y;x) (op \) \ \ skip iteration" apply (rule basicalgebra.intro) apply (rule refinement_reflexive) apply (metis refinement_transitive) apply (metis refinement_antisymmetric) apply (rule disj_increasing1) apply (rule disj_increasing2) apply (metis disj_lub) apply (rule conj_decreasing1) apply (rule conj_decreasing2) apply (metis conj_glb) apply (metis disjunction_commutative) apply (metis disjunction_associative) apply (metis disjunction_idempotent) apply (metis disjunction_left_unit) apply (metis disjunction_right_unit) apply (metis disjunction_left_zero) apply (metis disjunction_right_zero) apply (metis conjunction_commutative) apply (metis conjunction_associative) apply (metis conjunction_idempotent) apply (metis conjunction_left_unit) apply (metis conjunction_right_unit) apply (metis conjunction_left_zero) apply (metis conjunction_right_zero) apply (metis semicolon_associative) apply (metis semicolon_right_unit) apply (metis semicolon_left_unit) apply (metis semicolon_right_zero) apply (metis semicolon_left_zero) apply (metis concurrency_commutative) apply (metis concurrency_associative) apply (metis concurrency_left_unit) apply (metis concurrency_right_unit) apply (metis concurrency_left_zero) apply (metis concurrency_right_zero) apply (metis disj_distr_through_disj distr_through_disj_p_def) apply (metis conj_distr_through_disj distr_through_disj_p_def) apply (metis semicolon_distr_through_disj distr_through_disj_p_def) apply (metis concurrency_distr_through_disj distr_through_disj_p_def) apply (metis exchange) apply (metis iter3) apply (metis iter4) apply (metis iter1) by (metis iter2) text {* Familiar algebraic structures. *} lemma partial_order: "class.order (op \) (op \)" apply (rule class.order.intro) apply (rule class.preorder.intro) apply (metis lessthan_def) apply (metis refinement_reflexive) apply (metis refinement_transitive) apply (rule class.order_axioms.intro) apply (metis refinement_antisymmetric) done lemma is_lattice: "class.lattice (op \) (op \) (op \) (op \)" apply (rule class.lattice.intro) apply (rule class.semilattice_inf.intro) apply (rule partial_order) apply (rule class.semilattice_inf_axioms.intro) apply (metis conj_decreasing1) apply (metis conj_decreasing1 conjunction_commutative) apply (metis conj_glb) apply (rule class.semilattice_sup.intro) apply (rule partial_order) apply (rule class.semilattice_sup_axioms.intro) apply (metis disj_increasing1) apply (metis disj_increasing1 disjunction_commutative) by (metis disj_lub) lemma is_bounded_lattice: "class.bounded_lattice (op \) (op \) (op \) (op \) \ \" apply (rule class.bounded_lattice.intro) apply (rule class.bounded_lattice_bot.intro) apply (rule is_lattice) apply (rule class.bot.intro) apply (rule partial_order) apply (rule class.bot_axioms.intro) apply (rule bottom_least) apply (rule class.bounded_lattice_top.intro) apply (rule is_lattice) apply (rule class.top.intro) apply (rule partial_order) apply (rule class.top_axioms.intro) by (metis disjunction_right_zero refinement_disj) end text {* Make the time reversed versions of the theorems available. *} sublocale basicalgebra < time_reverse!: basicalgebra "(op \)" "(op \)" "(op \)" "(\ x y . y;x)" "(op \)" "\" "\" "skip" "iteration" apply (rule time_reversal) apply (rule distr_through_disj_p_def) apply (rule lessthan_def) by (rule monotone_p_def) section {* General operational calculus *} locale generalcalculus = basicalgebra + fixes Actions :: "'a set" assumes skip_in_Actions: "skip \ Actions" fixes quintuple :: "'a \ 'a \ 'a \ 'a \ 'a \ bool" ("<_,_>-_\<_,_>" [54,54,54,54,54] 53) defines "-q\ \ (q \ Actions) \ (q;p' \ p) \ (s' \ s;q)" begin theorem Grearrange: "p' \ p \ -skip\" by (metis skip_in_Actions quintuple_def refinement_reflexive semicolon_left_unit semicolon_right_unit) text {* Theorems shared by small step and big step approaches. *} theorem Gaction: "p \ Actions \ -p\" by (metis quintuple_def refinement_reflexive semicolon_right_unit) theorem Gskip: "-skip\" by (metis skip_in_Actions Gaction semicolon_right_unit) theorem Gchoice1: "-q\ \ p'',s>-q\" by (metis quintuple_def disj_increasing1 refinement_transitive) theorem Gchoice2: "-q\ \ p',s>-q\" by (metis Gchoice1 disjunction_commutative) theorem Giter: "\,s>-skip\" by (metis Grearrange iter_unfold1) text {* Small step theorems *} theorem GSseq1: "-q\ \ -q\" by (metis quintuple_def semicolon_associative semicolon_monotone1) theorem GSseq2: "-q\ \ -q\" by (metis GSseq1 semicolon_left_unit) theorem GSchoice1: "p',s>-skip\" by (metis skip_in_Actions quintuple_def disj_increasing1 refinement_reflexive semicolon_left_unit semicolon_right_unit) theorem GSchoice2: "p',s>-skip\" by (metis GSchoice1 disjunction_commutative) theorem GSiter: "\,s>-skip\\,s>" by (metis Grearrange iter_unfold2) theorem GSiterAlt1: "-q\ \ \,s>-q\\,s'>" by (metis quintuple_def iter_unfold2 refinement_transitive semicolon_monotone1 semicolon_associative) theorem GSiterAlt2: "-q\ \ \,s>-q\\,s'>" by (metis GSiterAlt1 semicolon_left_unit) theorem GSconc1: "-q\ \ p'',s>-q\p'',s'>" by (metis quintuple_def concurrency_monotone1 refinement_transitive small_exchange1) theorem GSconc2: "-q\ \ p',s>-q\" by (metis GSconc1 concurrency_left_unit) theorem GSconc3: "-q\ \ p,s>-q\p',s'>" by (metis GSconc1 concurrency_commutative) theorem GSconc4: "-q\ \ p,s>-q\" by (metis GSconc2 concurrency_commutative) text {* Big step theorems *} theorem GBseq: "-q\ \ -q'\ \ (q;q') \ Actions \ -q;q'\" proof - assume a: "-q\" assume b: "-q'\" assume c: "(q;q') \ Actions" from a b have d: "q;q' \ p;p'" by (metis quintuple_def refinement_transitive semicolon_monotone2 semicolon_right_unit semicolon_monotone1) from a b have e: "s'' \ s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1) from c d e show "-q;q'\" by (metis quintuple_def semicolon_right_unit) qed theorem GBiter: "-q\ \ \,s'>-q'\ \ (q;q') \ Actions \ \,s>-q;q'\" proof - assume a: "-q\" assume b: "\,s'>-q'\" assume c: "(q;q') \ Actions" from a b have d: "q;q' \ p\<^sup>\" by (metis quintuple_def GSiterAlt2 refinement_transitive semicolon_monotone2 semicolon_right_unit) from a b have e: "s'' \ s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1) from c d e show "\,s>-q;q'\" by (metis quintuple_def semicolon_right_unit) qed theorem GBconc1: "-q\ \ -q'\ \ (q;q') \ Actions \ p',s>-q;q'\" proof - assume a: "-q\" assume b: "-q'\" assume c: "(q;q') \ Actions" from a b have d: "q;q' \ p\p'" by (metis quintuple_def GSconc2 concurrency_monotone2 refinement_transitive semicolon_right_unit) from a b have e: "s'' \ s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1) from c d e show "p',s>-q;q'\" by (metis quintuple_def semicolon_right_unit) qed theorem GBconc2: "-q\ \ -q'\ \ (q;q') \ Actions \ p,s>-q;q'\" by (metis GBconc1 concurrency_commutative) end section {* Plotkin's SOS *} locale plotkin = generalcalculus + fixes ptransition4 :: "'a \ 'a \ 'a \ 'a \ bool" ("<_,_>\<_,_>" [54,54,54,54] 53) defines "\ \ \q. -q\" fixes ptransition3 :: "'a \ 'a \ 'a \ bool" ("<_,_>\_" [54,54,54] 53) defines "\s' \ \" begin theorem Paction: "p \ Actions \ \s;p" by (metis Gaction ptransition4_def ptransition3_def) theorem Pskip: "\s" by (metis Gskip ptransition4_def ptransition3_def) theorem Pseq1: "\ \ \" by (metis GSseq1 ptransition4_def) theorem Pseq2: "\s' \ \" by (metis GSseq2 ptransition4_def ptransition3_def) theorem Pchoice1: "p',s>\" by (metis GSchoice1 ptransition4_def) theorem Pchoice2: "p',s>\" by (metis GSchoice2 ptransition4_def) theorem Pchoice1Alt_1: "\ \ p'',s>\" by (metis Gchoice1 ptransition4_def) theorem Pchoice1Alt_2: "\s' \ p',s>\s'" by (metis Pchoice1Alt_1 ptransition3_def) theorem Pchoice2Alt_1: "\ \ p',s>\" by (metis Gchoice2 ptransition4_def) theorem Pchoice2Alt_2: "\s' \ p',s>\s'" by (metis Pchoice2Alt_1 ptransition3_def) theorem Piter1: "\,s>\s" by (metis Giter ptransition4_def ptransition3_def) theorem Piter2: "\,s>\\,s>" by (metis GSiter ptransition4_def) theorem Piter2Alt1: "\ \ \,s>\\,s'>" by (metis GSiterAlt1 ptransition4_def) theorem Piter2Alt2: "\s' \ \,s>\\,s'>" by (metis GSiterAlt2 ptransition4_def ptransition3_def) theorem Pconc1: "\ \ p'',s>\p'',s'>" by (metis GSconc1 ptransition4_def) theorem Pconc2: "\s' \ p',s>\" by (metis GSconc2 ptransition4_def ptransition3_def) end section {* Milner's process calculus semantics *} locale milner = generalcalculus + fixes mtransition :: "'a \ 'a \ 'a \ bool" ("_-_\_" [54,54,54] 53) defines "p-q\r \ \s. \s'. -q\" begin lemma mtransition_equivalence: "p-q\r \ (q \ Actions \ q;r \ p)" by (metis bottom_least mtransition_def quintuple_def) lemma mtransition_alt_def: "p-q\r \ (\s s'. -q\)" by (metis mtransition_def mtransition_equivalence quintuple_def) theorem Maction: "p \ Actions \ p-p\skip" by (metis Gaction mtransition_def) theorem Mskip: "skip-skip\skip" by (metis Gskip mtransition_def) theorem Mseq1: "p-q\r \ p;p'-q\r;p'" by (smt GSseq1 mtransition_def) theorem Mseq2: "p-q\skip \ p;p'-q\p'" by (smt GSseq2 mtransition_def) theorem Mprefixing: "p \ Actions \ p;p'-p\p'" by (metis Maction Mseq2) abbreviation (input) milner_rearrangement :: "'a \ 'a \ bool" ("_-\_" [54,54] 53) where "p-\q \ p-skip\q" lemma rearrangement_equivalence: "p-\q \ q \ p" by (metis mtransition_equivalence semicolon_left_unit skip_in_Actions) theorem Mchoice1: "p\p'-\p" by (metis GSchoice1 mtransition_def) theorem Mchoice2: "p\p'-\p'" by (metis GSchoice2 mtransition_def) theorem Mchoice1Alt: "p-q\r \ p\p'-q\r" by (smt Gchoice1 mtransition_def) theorem Mchoice2Alt: "p'-q\r \ p\p'-q\r" by (smt Gchoice2 mtransition_def) theorem Miter1: "p\<^sup>\-\skip" by (metis Giter mtransition_def) theorem Miter2: "p\<^sup>\-\p;p\<^sup>\" by (metis GSiter mtransition_def) theorem Miter2Alt_1: "p-q\r \ p\<^sup>\-q\r;p\<^sup>\" by (smt GSiterAlt1 mtransition_def) theorem Miter2Alt_2: "p-q\skip \ p\<^sup>\-q\p\<^sup>\" by (smt GSiterAlt2 mtransition_def) theorem Mconc1: "p-q\r \ p\p'-q\r\p'" by (smt GSconc1 mtransition_def) theorem Mconc2: "p-q\skip \ p\p'-q\p'" by (smt GSconc2 mtransition_def) theorem Mconc3: "p-q\p' \ p''\p-q\p''\p'" by (smt GSconc3 mtransition_def) theorem Mconc4: "p-q\skip \ p'\p-q\p'" by (smt GSconc4 mtransition_def) theorem GeneralCommunication: "p-q\p' \ r-q'\r' \ q'' \ Actions \ q'' \ q\q' \ p\r-q''\p'\r'" proof - assume a: "p-q\p'" assume b: "r-q'\r'" assume c: "q'' \ Actions" assume d: "q'' \ q\q'" have e: "\a b c a' b' c'. a;b \ c \ a';b' \ c' \ (a\a');(b\b') \ c\c'" by (metis concurrency_monotone1 concurrency_monotone2 refinement_transitive exchange) from a b e have f: "(q\q');(p'\r') \ p\r" by (metis mtransition_equivalence) from f d have g: "q'';(p'\r') \ p\r" by (metis refinement_transitive semicolon_monotone1) from c g show "p\r-q''\p'\r'" by (metis mtransition_equivalence) qed end section {* Reduction semantics with evaluation contexts. *} locale reduction = plotkin + milner + fixes program_context :: "('a \ 'a) \ bool" defines "program_context pc \ (\p q p'. p-q\p' \ pc(p)-q\pc(p'))" begin theorem empty_context: "program_context (\x. x)" by (metis program_context_def) theorem semicolon_context: "program_context (\x. x;P)" by (metis Mseq1 program_context_def) theorem concurrency_context1: "program_context (\x. x\P)" by (metis Mconc1 program_context_def) theorem concurrency_context2: "program_context (\x. P\x)" by (metis Mconc3 program_context_def) theorem program_contexts_compose: "program_context pc \ program_context pc' \ program_context (pc' \ pc)" by (metis o_def program_context_def) corollary example_program_context: "program_context (\x. (P\(x\P'));P'')" proof - have a: "program_context (\x. x\P')" by (metis concurrency_context1) have b: "program_context (\y. P\y)" by (metis concurrency_context2) have c: "program_context (\z. z;P'')" by (metis semicolon_context) have d: "(\y. P\y)\(\x. x\P') = (\x. P\(x\P'))" by (metis o_def) from a b d program_contexts_compose have e: "program_context (\x. P\(x\P'))" by metis have f: "(\z. z;P'')\(\x. P\(x\P')) = (\x. (P\(x\P'));P'')" by (metis o_def) from e c f program_contexts_compose show ?thesis by metis qed theorem Rmain_program_context: "program_context pc \ p-\p' \ pc(p)-\pc(p')" by (metis program_context_def) theorem Rmain_configuration_context: "program_context pc \ p-\p' \ \" by (metis Grearrange program_context_def ptransition4_def rearrangement_equivalence) theorem Rseq: "skip;p-\p" by (metis Mprefixing skip_in_Actions) theorem Rconc1: "skip\p-\p" by (metis Mskip Mconc2) theorem Rconc2: "p\skip-\p" by (metis Mskip Mconc4) corollary example1: "<(P\((P1\P2)\P'));P'',s>\<(P\(P1\P'));P'',s>" by (metis example_program_context Mchoice1 Rmain_configuration_context) corollary example2: "<(P\((P\<^sup>\)\P'));P'',s>\<(P\((P;P\<^sup>\)\P'));P'',s>" by (metis example_program_context Miter2 Rmain_configuration_context) corollary example3: "<(P\((skip;P1)\P'));P'',s>\<(P\(P1\P'));P'',s>" by (metis example_program_context Rseq Rmain_configuration_context) theorem GeneralResult1: "-q\ \ (\pc. program_context pc \ -q\)" by (metis empty_context mtransition_equivalence program_context_def quintuple_def) theorem GeneralResult2: "p-q\p' \ \s' \ (\pc. program_context pc \ -q\)" proof - have "p-q\p' \ \s' \ q \ Actions \ q;p'\p \ (\a. -a\)" by (metis mtransition_equivalence ptransition3_def ptransition4_def) also have "\ \ q \ Actions \ q;p'\p \ (\a. a \ Actions \ a\q \ s'\s;a)" by (metis quintuple_def semicolon_right_unit) also have "\ \ q \ Actions \ q;p'\p \ s'\s;q" by (metis monotone_p_def refinement_reflexive refinement_transitive semicolon_monotone) also have "\ \ -q\" by (metis quintuple_def) finally show ?thesis by (metis GeneralResult1) qed theorem GeneralResult3: "p-q\p' \ \s' \ program_context pc \ \" by (metis GeneralResult2 ptransition4_def) theorem Ractions: "q \ Actions \ \s' \ program_context pc \ \" by (metis GeneralResult3 Maction) theorem GeneralRelationship: "-q\ \ p-q\p' \ \s'" by (metis GeneralResult1 GeneralResult2) end section {* A small-step semantics with implicit states and implicit actions. *} text {* Plotkin's proposal in `The Origins of Structural Operational Semantics'. *} locale origins = plotkin + milner + fixes otransition :: "'a \ 'a \ bool" ("_\_" [54,54] 53) defines "p\q \ \s. \s'. \" begin lemma otransition_alt_def1: "p\q \ (\s s'. \)" proof - have "(\s s'. \) \ p\q" proof - assume "\s s'. \" hence "\a s s'. -a\" by (metis ptransition4_def) hence "\a. \s. \s'. -a\" by (metis mtransition_alt_def mtransition_def) hence "\s. \s'. \" by (metis ptransition4_def) thus "p\q" by (metis otransition_def) qed thus ?thesis by (metis otransition_def) qed no_notation minus (infixl "-" 65) lemma otransition_alt_def2: "p\q \ (\a. p-a\q)" proof - have "p\q \ (\a. p-a\q)" proof - assume "p\q" hence "\s s'. \" by (metis otransition_def) thus "\a. p-a\q" by (metis ptransition4_def mtransition_alt_def) qed thus ?thesis by (metis mtransition_def otransition_alt_def1 ptransition4_def) qed theorem Oaction: "p \ Actions \ p\skip" by (metis Paction otransition_def ptransition3_def) (* by (metis Maction otransition_alt_def2) *) theorem Oseq1: "p\r \ p;p'\r;p'" by (metis Pseq1 otransition_def) (* by (metis Mseq1 otransition_alt_def2) *) theorem Oseq2: "p\skip \ p;p'\p'" by (metis Pseq2 otransition_def ptransition3_def) (* by (metis Mseq2 otransition_alt_def2) *) theorem Oprefixing: "p \ Actions \ p;p'\p'" by (metis Oaction Oseq2) (* by (metis Mprefixing otransition_alt_def2) *) theorem Ochoice1: "p\p'\p" by (metis Pchoice1 otransition_def) (* by (metis Mchoice1 otransition_alt_def2) *) theorem Ochoice2: "p\p'\p'" by (metis Pchoice2 otransition_def) (* by (metis Mchoice2 otransition_alt_def2) *) theorem Ochoice1Alt: "p\r \ p\p'\r" by (metis Pchoice1Alt_1 otransition_def) (* by (metis Mchoice1Alt otransition_alt_def2) *) theorem Ochoice2Alt: "p'\r \ p\p'\r" by (metis Pchoice2Alt_1 otransition_def) (* by (metis Mchoice2Alt otransition_alt_def2) *) theorem Oiter1: "p\<^sup>\\skip" by (metis Piter1 otransition_def ptransition3_def) (* by (metis Miter1 otransition_alt_def2) *) theorem Oiter2: "p\<^sup>\\p;p\<^sup>\" by (metis Piter2 otransition_def) (* by (metis Miter2 otransition_alt_def2) *) theorem Oiter2Alt_1: "p\r \ p\<^sup>\\r;p\<^sup>\" by (metis Piter2Alt1 otransition_def) (* by (metis Miter2Alt_1 otransition_alt_def2) *) theorem Oiter2Alt_2: "p\skip \ p\<^sup>\\p\<^sup>\" by (metis Piter2Alt2 otransition_def ptransition3_def) (* by (metis Miter2Alt_2 otransition_alt_def2) *) theorem Oconc1: "p\r \ p\p'\r\p'" by (metis Pconc1 otransition_def) (* by (metis Mconc1 otransition_alt_def2) *) theorem Oconc2: "p\skip \ p\p'\p'" by (metis Pconc2 otransition_def ptransition3_def) (* by (metis Mconc2 otransition_alt_def2) *) end section {* The chemical abstract machine. *} locale cham = reduction + origins + (* See the comments in the body about the definition of chemical solutions. *) fixes heat :: "'a \ 'a \ bool" ("_\_" [54,54] 53) defines "p\p' \ p-\p'" fixes cool :: "'a \ 'a \ bool" ("_\_" [54,54] 53) defines "p\p' \ p-\p'" fixes heatcool :: "'a \ 'a \ bool" ("_\_" [54,54] 53) defines "p\p' \ p\p' \ p'\p" (* The second operand of the general airlock is a program context, but Isabelle/HOL *) (* does not support dependent types. So we cannot declare program_context_type, which *) (* would depend on the type parameter 'a of the local context. For details, see: *) (* https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-October/msg00045.html *) (* As a workaround, we prove it separately and require it in theorems whenever needed. *) fixes general_airlock :: "'a \ ('a \ 'a) \ 'a" (infixr "\" 60) defines "p \ pc \ pc(p)" fixes standard_airlock :: "'a \ 'a \ 'a" (infixr "\" 60) defines "p \ p' \ p \ (\x. x\p')" begin (* Isabelle does not currently provide simple and proper syntax for defining chemical solutions. *) (* See the email of 24 February 2012 on the Isabelle/HOL list: *) (* https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-February/msg00102.html *) (* Instead of hacking away, the following abbreviations give the three cases we use explicitly. *) abbreviation (input) empty_solution :: "'a" ("\\") where "\\ \ skip" abbreviation (input) singleton_solution :: "'a \ 'a" ("\_\") where "\p\ \ p" abbreviation (input) pair_solution :: "'a \ 'a \ 'a" ("\_,_\") where "\p,q\ \ p\q" abbreviation (input) solution_union :: "'a \ 'a \ 'a" (infixl "\" 80) where "p\q \ p\q" lemma heatcool_equivalence: "p\p' \ p=p'" by (metis cool_def heat_def heatcool_def rearrangement_equivalence refinement_antisymmetric refinement_reflexive) lemma heating_is_special_reaction: "p\p' \ p\p'" by (metis heat_def otransition_alt_def2) lemma cooling_is_special_reaction: "p\p' \ p\p'" by (metis cool_def otransition_alt_def2) theorem Cchemical_heat: "p\p' \ (p\p'')\(p'\p'')" by (metis program_context_def heat_def concurrency_context1) theorem Cchemical_cool: "p\p' \ (p\p'')\(p'\p'')" by (metis Mconc1 cool_def) theorem Cchemical_heatcool: "p\p' \ (p\p'')\(p'\p'')" by (metis Cchemical_heat Cchemical_cool heatcool_def) theorem Cchemical_react: "p\p' \ (p\p'')\(p'\p'')" by (metis Oconc1) theorem Csolution_heat: "p\p' \ program_context pc \ \pc(p)\\\pc(p')\" by (metis program_context_def heat_def) theorem Csolution_cool: "p\p' \ program_context pc \ \pc(p)\\\pc(p')\" by (metis program_context_def cool_def) theorem Csolution_heatcool: "p\p' \ program_context pc \ \pc(p)\\\pc(p')\" by (metis Csolution_heat Csolution_cool heatcool_def) theorem Csolution_react: "p\p' \ program_context pc \ \pc(p)\\\pc(p')\" by (metis GeneralResult1 otransition_def ptransition4_def) (* Alternative: by (metis otransition_alt_def2 program_context_def) *) theorem (in generalcalculus) GskipAction: "-skip\" by (metis Grearrange refinement_reflexive) theorem (in milner) MskipAction: "p-\p" by (metis GskipAction mtransition_def) theorem CgeneralAirlock: "\pc(p)\\\p \ pc\" by (metis MskipAction general_airlock_def heatcool_def heat_def cool_def) (* Alternative: by (metis general_airlock_def heatcool_equivalence) *) lemma ExposedMoleculesFreely_heat: "p\p' \ program_context pc \ \p \ pc\\\p' \ pc\" by (metis Csolution_heat general_airlock_def) lemma ExposedMoleculesFreely_cool: "p\p' \ program_context pc \ \p \ pc\\\p' \ pc\" by (metis Csolution_cool general_airlock_def) lemma ExposedMoleculesFreely_heatcool: "p\p' \ program_context pc \ \p \ pc\\\p' \ pc\" by (metis Csolution_heatcool general_airlock_def) lemma ExposedMoleculesFreely_react: "p\p' \ program_context pc \ \p \ pc\\\p' \ pc\" by (metis Csolution_react general_airlock_def) lemma standard_airlock_equivalence: "p \ p' = p \ p'" by (metis general_airlock_def standard_airlock_def) lemma standard_airlock_associative: "(p \ p') \ p'' = p \ (p' \ p'')" by (metis concurrency_associative standard_airlock_equivalence) theorem Cairlock: "\p\ \ p' \ \p \ p'\" by (metis CgeneralAirlock general_airlock_def standard_airlock_equivalence) lemma SolutionUnderAirlockFreely_heat: "p'\p'' \ \p \ p'\\\p \ p''\" by (metis Csolution_heat concurrency_context2 standard_airlock_equivalence) lemma SolutionUnderAirlockFreely_cool: "p'\p'' \ \p \ p'\\\p \ p''\" by (metis Csolution_cool concurrency_context2 standard_airlock_equivalence) lemma SolutionUnderAirlockFreely_heatcool: "p'\p'' \ \p \ p'\\\p \ p''\" by (metis Csolution_heatcool concurrency_context2 standard_airlock_equivalence) lemma SolutionUnderAirlockFreely_react: "p'\p'' \ \p \ p'\\\p \ p''\" by (metis Csolution_react concurrency_context2 standard_airlock_equivalence) lemma context_with_airlock: "program_context pc \ program_context (\x. pc(x) \ p)" by (metis concurrency_context1 program_context_def standard_airlock_equivalence) lemma ExposeIon: "\pc(p) \ p'\ \ \p \ (\x. pc(x) \ p')\" by (metis CgeneralAirlock) lemma RemainderSolutionFreely_heat: "p'\p'' \ \p \ (\x. pc(x) \ p')\\\p \ (\x. pc(x) \ p'')\" by (metis SolutionUnderAirlockFreely_heat general_airlock_def) lemma RemainderSolutionFreely_cool: "p'\p'' \ \p \ (\x. pc(x) \ p')\\\p \ (\x. pc(x) \ p'')\" by (metis SolutionUnderAirlockFreely_cool general_airlock_def) lemma RemainderSolutionFreely_heatcool: "p'\p'' \ \p \ (\x. pc(x) \ p')\\\p \ (\x. pc(x) \ p'')\" by (metis SolutionUnderAirlockFreely_heatcool general_airlock_def) lemma RemainderSolutionFreely_react: "p'\p'' \ \p \ (\x. pc(x) \ p')\\\p \ (\x. pc(x) \ p'')\" by (metis SolutionUnderAirlockFreely_react general_airlock_def) lemma valid_context_for_Cseq: "program_context (\x. x;p' \ p'')" by (metis context_with_airlock semicolon_context) theorem Cseq: "\p;p' \ p''\ \ \p \ (\x. x;p' \ p'')\" by (metis CgeneralAirlock) theorem Cconc: "\p\p'\ \ \p, p'\" by (metis CgeneralAirlock general_airlock_def) lemma ReactionFromRearrangement: "p-\p' \ program_context pc \ \p \ pc\\\p' \ pc\" by (metis mtransition_def GeneralResult1 general_airlock_def otransition_def ptransition4_def) (* Alternative: by (metis ExposedMoleculesFreely_react otransition_alt_def2) *) theorem Cchoice1: "program_context pc \ \p\p' \ pc\\\p \ pc\" by (metis Mchoice1 ReactionFromRearrangement) theorem Cchoice2: "program_context pc \ \p\p' \ pc\\\p' \ pc\" by (metis Mchoice2 ReactionFromRearrangement) theorem Citer1: "program_context pc \ \p\<^sup>\ \ pc\\\skip \ pc\" by (metis Miter1 ReactionFromRearrangement) theorem Citer2: "program_context pc \ \p\<^sup>\ \ pc\\\p;p\<^sup>\ \ pc\" by (metis Miter2 ReactionFromRearrangement) theorem Cdropskip: "program_context pc \ \skip;p \ pc\\\p \ pc\" by (metis Rseq ReactionFromRearrangement) lemma Citer1_with_empty_context: "\p\<^sup>\\\\skip\" by (metis Citer1 empty_context general_airlock_def) lemma Citer1_with_concurrency_context1: "\p\<^sup>\ \ p'\\\skip \ p'\" by (metis Citer1 concurrency_context1 standard_airlock_def) lemma Cdropskip_with_concurrency_context1: "\skip;p \ p'\\\p \ p'\" by (metis Cdropskip concurrency_context1 standard_airlock_def) theorem Cskip: "\skip\\\\" by (metis Mskip heat_def) text {* The example derivation: *} lemma "(\pc. program_context pc \ \q \ pc\ \ \skip \ pc\) \ True" proof - assume a: "\pc. program_context pc \ \q \ pc\ \ \skip \ pc\" have b: "program_context (\x. x;p \ \skip\)" by (metis semicolon_context context_with_airlock) have "\q;p \ p\<^sup>\\ \ \q;p, p\<^sup>\\" by (metis heatcool_def Cconc) have "\ \ \q;p \ \p\<^sup>\\\" by (metis heatcool_def Cairlock) have "\ \ \q \ (\x. x;p \ \p\<^sup>\\)\" by (metis heatcool_def Cseq) have "\ \ \q \ (\x. x;p \ \skip\)\" by (metis Citer1_with_empty_context RemainderSolutionFreely_react) have "\ \ \skip \ (\x. x;p \ \skip\)\" by (metis a b) have "\ \ \skip;p \ \skip\\" by (metis heatcool_def Cseq) have "\ \ \p \ \skip\\" by (metis Cdropskip_with_concurrency_context1) have "\ \ \p,skip\" by (metis heatcool_def Cairlock) have "\ \ \p\" by (metis Cskip Cchemical_heat concurrency_right_unit concurrency_commutative) show ?thesis by metis qed (* In jEdit, start to type "right" for \, \, \. *) (* "lbrace" \, "rbrace" \, "uplus" \, "triangle" \ *) end section {* Kahn's natural semantics *} locale kahn = generalcalculus + assumes big_steps_possible: "\x. x \ Actions" fixes kreduction :: "'a \ 'a \ 'a \ bool" ("<_,_>\_" [54,54,54] 53) defines "\s' \ \q. -q\" begin theorem Kskip: "\s" by (metis Gskip kreduction_def) theorem Kseq: "\s' \ \s'' \ \s''" by (metis GBseq big_steps_possible kreduction_def) theorem Kchoice: "\s' \ p',s>\s'" by (metis Gchoice1 kreduction_def) theorem Kchoice': "\s' \ p',s>\s'" by (metis Gchoice2 kreduction_def) theorem Kiter1: "\,s>\s" by (metis Giter kreduction_def) theorem Kiter2: "\s' \ \,s'>\s'' \ \,s>\s''" by (metis GBiter big_steps_possible kreduction_def) theorem Kconc1: "\s' \ \s'' \ p',s>\s''" by (metis GBconc1 big_steps_possible kreduction_def) theorem Kconc2: "\s' \ \s'' \ p',s>\s''" by (metis GBconc2 big_steps_possible kreduction_def) lemma kahn_equivalence: "\s' \ s' \ s;p" proof - have "\s' \ s' \ s;p" proof - assume "\s'" hence "\q. q \ p \ s' \ s;q" by (metis kreduction_def quintuple_def semicolon_right_unit) thus "s' \ s;p" by (metis refinement_transitive semicolon_monotone2) qed thus ?thesis by (metis big_steps_possible kreduction_def quintuple_def refinement_reflexive semicolon_right_unit) qed end end