(* The Isabelle/HOL proof script accompanying the paper "In Praise of Algebra" by Tony Hoare and Stephan van Staden. For more information about using Isabelle/HOL in this way, see the paper "Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL" by Simon Foster, Georg Struth and Tjark Weber (RAMICS 2011: 52-67). *) theory InPraiseOfAlgebra imports Main begin declare [[ smt_solver = remote_z3]] declare [[ smt_timeout = 60 ]] declare [[ z3_options = "-memory:500" ]] section {* The basic algebra *} locale basicalgebra = fixes 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" 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\\ = \" fixes refinement :: "'a \ 'a \ bool" (infix "\" 50) defines "x\y \ y=x\y" assumes semicolon_distr_disj_left: "x;(y\z) = x;y \ x;z" and semicolon_distr_disj_right: "(x\y);z = x;z \ y;z" and concurrency_distr_disj_left: "x\(y\z) = x\y \ x\z" and concurrency_distr_disj_right: "(x\y)\z = x\z \ y\z" and conj_disj_relationship1: "q=p\q \ p=p\q" and conj_disj_relationship2: "p=p\q \ q=p\q" and exchange: "(p\q);(r\s) \ (p;r)\(q;s)" (* Kleene star *) fixes iteration :: "'a \ 'a" ("_\<^sup>\" [101] 100) assumes iter1: "skip \ (p;p\<^sup>\) \ p\<^sup>\" and iter2: "p \ (q;r) \ r \ q\<^sup>\;p \ r" (* We will prove iter3 as a theorem. *) 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 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)))" 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 lemma iter3: "skip \ (p\<^sup>\;p) \ p\<^sup>\" by (smt disjunction_associative disjunction_commutative disjunction_idempotent iter1 iter2 refinement_def semicolon_associative semicolon_distr_disj_left semicolon_right_unit) text {* Refinement is a partial order. *} lemma refinement_reflexive: "x\x" by (metis disjunction_idempotent refinement_def) lemma refinement_transitive: "x\y \ y\z \ x\z" by (metis disjunction_associative refinement_def) lemma refinement_antisymmetric: "x\y \ y\x \ x=y" by (metis disjunction_commutative refinement_def) text {* Disjunction is the least upper bound. *} lemma disj_increasing: "x \ x\y" by (metis disjunction_associative disjunction_idempotent refinement_def) lemma disj_lub: "x\z \ y\z \ x\y \ z" by (metis disjunction_associative refinement_def) text {* Conjunction is the greatest lower bound. *} lemma conj_decreasing: "x\y \ x" by (metis conj_disj_relationship2 conjunction_associative conjunction_commutative conjunction_idempotent refinement_def) lemma conj_glb: "x\y \ x\z \ x\y\z" by (metis conj_decreasing conj_disj_relationship1 conjunction_associative conjunction_commutative refinement_def) text {* The constant `bottom' is the least element. *} lemma bottom_least: "\\x" by (metis disjunction_left_unit refinement_def) text {* Any operator that distributes through disjunction is monotone. *} lemma distr_through_disj_implies_monotone1: "distr_through_disj_p f \ x \ y \ (f x z) \ (f y z)" by (metis distr_through_disj_p_def disj_increasing refinement_def) lemma distr_through_disj_implies_monotone2: "distr_through_disj_p f \ y \ z \ (f x y) \ (f x z)" by (metis distr_through_disj_p_def disj_increasing refinement_def) text {* Sequential composition is monotone. *} lemma semicolon_monotone1: "x \ y \ x;z \ y;z" by (metis refinement_def semicolon_distr_disj_right) lemma semicolon_monotone2: "y \ z \ x;y \ x;z" by (metis refinement_def semicolon_distr_disj_left) text {* Concurrency is monotone. *} lemma concurrency_monotone1: "x \ y \ x\z \ y\z" by (metis concurrency_distr_disj_right refinement_def) lemma concurrency_monotone2: "y \ z \ x\y \ x\z" by (metis concurrency_commutative concurrency_monotone1) text {* The small exchange law holds. *} lemma small_exchange: "(x\y);z \ x\(y;z)" by (metis concurrency_left_unit exchange semicolon_right_unit) 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_decreasing refinement_transitive) have b: "f (w \ x) (y \ z) \ f x z" by (metis monotone_p_def ap conjunction_commutative conj_decreasing refinement_transitive) from a b show ?thesis by (metis conj_disj_relationship1 conj_disj_relationship2 conjunction_associative refinement_def) qed text {* In particular, sequential composition exchanges with conjunction. *} lemma semicolon_conjunction_exchange: "(w\x);(y\z) \ (w;y)\(x;z)" proof - have a: "monotone_p (op ;)" by (metis monotone_p_def semicolon_monotone1 semicolon_monotone2) from a show ?thesis by (rule monotone_op_exchanges_with_conj) qed text {* Time reversal duality (opposition). *} lemma time_reversal: "basicalgebra (op \) (op \) (\ x y . y;x) (op \) \ \ skip iteration" apply (rule basicalgebra.intro) 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 semicolon_distr_disj_right) apply (metis semicolon_distr_disj_left) apply (metis concurrency_distr_disj_left) apply (metis concurrency_distr_disj_right) apply (metis conj_disj_relationship1) apply (metis conj_disj_relationship2) apply (metis exchange refinement_def) apply (metis iter3 refinement_def) apply (metis iter4 refinement_def) by (metis iter2 refinement_def) text {* Familiar algebraic structures. *} lemma pre_order: "class.preorder (op \) (op \)" apply (rule class.preorder.intro) apply (metis lessthan_def) apply (metis refinement_reflexive) apply (metis refinement_transitive) done lemma partial_order: "class.order (op \) (op \)" apply (rule class.order.intro) apply (rule pre_order) 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_decreasing) apply (metis conj_decreasing 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_increasing) apply (metis disj_increasing 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_def) end section {* Hoare logic *} locale hoarelogic = basicalgebra begin lemma Hconsequence_post: "p;q \ r' \ r' \ r \ p;q \ r" by (rule refinement_transitive) lemma Hconsequence_pre: "p \ p' \ p';q \ r \ p;q \ r" by (metis refinement_transitive semicolon_monotone1) lemma Hskip: "p;skip \ p" by (metis refinement_reflexive semicolon_right_unit) lemma Hsequential_composition: "p;q \ r' \ r';q' \ r \ p;(q;q') \ r" by (metis refinement_transitive semicolon_associative semicolon_monotone1) lemma Hnon_determinism: "p;q \ r \ p;q' \ r \ p;(q\q') \ r" by (metis disj_lub semicolon_distr_disj_left) lemma Hiteration: "p;q \ p \ p;q\<^sup>\ \ p" by (metis disj_lub iter4 refinement_reflexive) lemma Hconcurrency: "p;q \ r \ p';q' \ r' \ (p\p');(q\q') \ r\r'" by (metis concurrency_monotone2 concurrency_monotone1 exchange refinement_transitive) lemma Hframe: "p;q \ r \ (p\f);q \ r\f" by (metis concurrency_commutative concurrency_monotone2 refinement_transitive small_exchange) lemma Hdisjunction: "p;q \ r \ p';q \ r' \ (p\p');q \ r\r'" by (metis disjunction_associative disjunction_commutative refinement_def semicolon_distr_disj_right) lemma Hconjunction: "p;q \ r \ p';q' \ r' \ (p\p');(q\q') \ r\r'" by (metis conj_decreasing conj_glb conjunction_commutative refinement_transitive semicolon_conjunction_exchange) lemma Floydconjunction: "p;q \ r \ p';q \ r' \ (p\p');q \ r\r'" by (metis Hconjunction conjunction_idempotent) end text {* Make the time reversed versions of the Hoare logic rules (and basic algebra theorems) available. *} sublocale hoarelogic < time_reverse!: hoarelogic "(op \)" "(op \)" "(\ x y . y;x)" "(op \)" "\" "\" "skip" apply (rule hoarelogic.intro) apply (rule time_reversal) apply (rule refinement_def) apply (rule lessthan_def) apply (rule distr_through_disj_p_def) by (rule monotone_p_def) section {* Other calculi *} locale milner = hoarelogic begin text {* The time reversed versions of the rules are now available, as the following example shows. *} lemma Hframe_time_reverse: "p;q \ r \ p;(q\f) \ r\f" by (rule time_reverse.Hframe) abbreviation (input) milner_triple :: "'a \ 'a \ 'a \ bool" ("_-_\_" [54,54,54] 53) where "r-p\q \ p;q \ r" lemma Mconcurrency1: "r-p\q \ (r\f)-p\(q\f)" by (rule Hframe_time_reverse) lemma Mconcurrency2: "r-p\skip \ (r\f)-p\f" by (metis Mconcurrency1 concurrency_left_unit) lemma Mconcurrency3: "r-p\q \ r'-p'\q' \ (r\r')-(p\p')\(q\q')" by (rule Hconcurrency) text {* Rules for other operators. *} lemma Mprefixing: "r;r'-r\r'" by (metis refinement_reflexive) lemma Mseq: "r-p\q \ r;r'-p\q;r'" by (metis semicolon_associative semicolon_monotone1) lemma Mchoice: "r-p\q \ r\r'-p\q" by (metis disj_increasing refinement_transitive) lemma Miter1: "r\<^sup>\-skip\skip" by (metis disj_increasing iter1 refinement_transitive semicolon_left_unit) lemma Miter2: "r\<^sup>\-skip\r;r\<^sup>\" by (metis disj_increasing disjunction_commutative iter1 refinement_transitive semicolon_left_unit) text {* Theorems obtained from time reversing Hoare rules. *} lemma Mskipaction: "p-skip\p" by (metis time_reverse.Hskip) lemma Mseqaction: "r-q'\r' \ r'-q\p \ r-q';q\p" by (metis time_reverse.Hsequential_composition) lemma Mchoiceaction: "r-q\p \ r-q'\p \ r-q\q'\p" by (metis time_reverse.Hnon_determinism) lemma Miteration: "p-q\p \ p-q\<^sup>\\p" by (metis time_reverse.Hiteration) lemma Mfunnychoice: "r-q\p \ r'-q\p' \ r\r'-q\p\p'" by (metis time_reverse.Hdisjunction) end no_notation divide (infixl "'/" 70) locale postspecification = hoarelogic + fixes Lub :: "'a set \ 'a" ("\_" [90] 90) fixes postspec :: "'a \ 'a \ 'a" (infixl "'/" 80) assumes Lub1: "\A \ b \ (\a\A. a \ b)" and Lub2: "(\a\A. a \ b) \ \A \ b" and semicolon_distr_Lub_left: "x;\A = \{r. (\a\A. r=x;a)}" and semicolon_distr_Lub_right: "\A;x = \{r. (\a\A. r=a;x)}" defines "r/p \ \{q. p;q \ r}" begin lemma postspec_semicolon_galois1: "q \ r/p \ p;q \ r" proof - assume a: "q \ r/p" from a have b: "p;q \ p;(r/p)" by (rule semicolon_monotone2) have c: "p;(r/p) = \{s. \q. p;q \ r \ s = p;q}" proof - have "p;(r/p) = p;\{q. p;q \ r}" by (metis postspec_def) also have "\ = \{s. (\a\{q. p;q \ r}. s=p;a)}" by (metis semicolon_distr_Lub_left) also have "\ = \{s. \q. p;q \ r \ s = p;q}" proof - have "(\s. (\a\{q. p;q \ r}. s=p;a)) = (\s. (\q. p;q \ r \ s = p;q))" by (metis Collect_def mem_def) thus ?thesis by metis qed finally show ?thesis. qed from b c have d: "p;q \ \{s. \q. p;q \ r \ s = p;q}" by metis have "\s. (\q. p;q \ r \ s = p;q) \ s \ r" by metis hence "\s\{s. (\q. p;q \ r \ s = p;q)}. s \ r" by (smt Collect_def mem_def) hence e: "\{s. \q. p;q \ r \ s = p;q} \ r" by (rule Lub2) from d e show ?thesis by (rule refinement_transitive) qed lemma postspec_semicolon_galois2: "p;q \ r \ q \ r/p" proof - assume "p;q \ r" hence "q \ {q. p;q \ r}" by (metis Collect_def mem_def) thus ?thesis by (metis Lub1 postspec_def refinement_reflexive) qed lemma postspec_semicolon_galois: "q \ r/p \ p;q \ r" by (metis postspec_semicolon_galois1 postspec_semicolon_galois2) lemma postspec_concurrency: "q \ r/p \ q' \ r'/p' \ q\q' \ (r\r')/(p\p')" by (metis Hconcurrency postspec_semicolon_galois) lemma postspec_exchange: "(r/p)\(r'/p') \ (r\r')/(p\p')" by (metis postspec_concurrency refinement_reflexive) lemma postspec_distr_conj: "(r\r')/p = r/p \ r'/p" proof - have a: "\q. q \ (r\r')/p \ q \ r/p \ r'/p" by (smt postspec_semicolon_galois conj_decreasing conj_glb conjunction_commutative refinement_transitive) have b: "(r\r')/p \ (r\r')/p" by (rule refinement_reflexive) from b have c: "(r\r')/p \ r/p \ r'/p" by (rule a) have d: "\q. q \ r/p \ r'/p \ q \ (r\r')/p" by (smt postspec_semicolon_galois conj_decreasing conj_glb conjunction_commutative refinement_transitive) have e: "r/p \ r'/p \ r/p \ r'/p" by (rule refinement_reflexive) from e have f: "r/p \ r'/p \ (r\r')/p" by (rule d) from c f show ?thesis by (rule refinement_antisymmetric) qed lemma postspec_left_zero: "\/p = \" by (metis disjunction_left_zero disjunction_right_zero postspec_semicolon_galois refinement_def) lemma postspec_disj_distributivity: "r/(p\p') = r/p \ r/p'" proof - have a: "\q. q \ r/(p\p') \ q \ r/p \ r/p'" proof - fix q have "q \ r/(p\p') \ (p\p');q \ r" by (metis postspec_semicolon_galois) also have "\ \ (p;q)\(p';q) \ r" by (metis semicolon_distr_disj_right) also have "\ \ p;q \ r \ p';q \ r" by (metis Hconsequence_pre disj_increasing disjunction_commutative time_reverse.Hnon_determinism time_reverse.semicolon_distr_disj_left) also have "\ \ q \ r/p \ q \ r/p'" by (metis postspec_semicolon_galois) also have "\ \ q \ r/p \ r/p'" by (metis conj_decreasing conj_glb conjunction_commutative refinement_transitive) finally show "q \ r/(p\p') \ q \ r/p \ r/p'" . qed from a show ?thesis by (metis disjunction_commutative refinement_def semicolon_left_unit time_reverse.Hskip) qed lemma postspec_right_unit: "r/skip = r" by (metis disjunction_commutative postspec_semicolon_galois refinement_def refinement_reflexive semicolon_left_unit) lemma postspec_montone_first: "r \ r' \ r/p \ r'/p" by (metis conj_decreasing conj_glb conjunction_commutative postspec_distr_conj refinement_antisymmetric refinement_reflexive) lemma postspec_antimonotone_second: "p \ p' \ r/p' \ r/p " by (metis conj_disj_relationship2 disjunction_commutative postspec_disj_distributivity refinement_def) end locale prespecification = postspecification + fixes prespec :: "'a \ 'a \ 'a" (infixl "\" 80) (* Using the "setminus" character... *) defines "p\r \ \{q. q;p \ r}" text {* Dualize the theorems. *} sublocale prespecification < time_reverse!: prespecification "(op \)" "(op \)" "(\ x y . y;x)" "(op \)" "\" "\" "skip" "(op \)" "iteration" "(op \)" "distr_through_disj_p" "monotone_p" "Lub" "(\ x y. y\x)" "(\ x y. y/x)" apply (rule prespecification.intro) apply (rule postspecification.intro) apply (rule hoarelogic.intro) apply (rule time_reversal) apply (rule postspecification_axioms.intro) apply (metis Lub1 refinement_def) apply (metis Lub2 refinement_def) apply (rule semicolon_distr_Lub_right) apply (rule semicolon_distr_Lub_left) apply (rule refinement_def) apply (rule lessthan_def) apply (rule distr_through_disj_p_def) apply (rule monotone_p_def) apply (rule prespec_def) by (rule postspec_def) locale prespecification_corollaries = prespecification begin lemma prespec_postspec_galois: "q \ p\r \ p \ r/q" by (metis postspec_semicolon_galois time_reverse.postspec_semicolon_galois) lemma prespec_exchange: "(p\r)\(p'\r') \ (p\p')\(r\r')" by (rule time_reverse.postspec_exchange) end end