(*
 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
  and conjunction :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
  and semicolon :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl ";" 80)
  and concurrency :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<parallel>" 80)
  and bottom :: "'a" ("\<bottom>")
  and top :: "'a" ("\<top>")
  and skip :: "'a"
  assumes disjunction_commutative: "x\<squnion>y = y\<squnion>x"
  and disjunction_associative: "x\<squnion>(y\<squnion>z) = (x\<squnion>y)\<squnion>z"
  and disjunction_idempotent: "x\<squnion>x = x"
  and disjunction_left_unit: "\<bottom>\<squnion>x = x"
  and disjunction_right_unit: "x\<squnion>\<bottom> = x"
  and disjunction_left_zero: "\<top>\<squnion>x = \<top>"
  and disjunction_right_zero: "x\<squnion>\<top> = \<top>"
  and conjunction_commutative: "x\<sqinter>y = y\<sqinter>x"
  and conjunction_associative: "x\<sqinter>(y\<sqinter>z) = (x\<sqinter>y)\<sqinter>z"
  and conjunction_idempotent: "x\<sqinter>x = x"
  and conjunction_left_unit: "\<top>\<sqinter>x = x"
  and conjunction_right_unit: "x\<sqinter>\<top> = x"
  and conjunction_left_zero: "\<bottom>\<sqinter>x = \<bottom>"
  and conjunction_right_zero: "x\<sqinter>\<bottom> = \<bottom>"
  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: "\<bottom>;x = \<bottom>"
  and semicolon_right_zero: "x;\<bottom> = \<bottom>"
  and concurrency_commutative: "x\<parallel>y = y\<parallel>x"
  and concurrency_associative: "x\<parallel>(y\<parallel>z) = (x\<parallel>y)\<parallel>z"
  and concurrency_left_unit: "skip\<parallel>x = x"
  and concurrency_right_unit: "x\<parallel>skip = x"
  and concurrency_left_zero: "\<bottom>\<parallel>x = \<bottom>"
  and concurrency_right_zero: "x\<parallel>\<bottom> = \<bottom>"
  fixes refinement :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
  defines "x\<sqsubseteq>y \<equiv> y=x\<squnion>y"
  assumes semicolon_distr_disj_left: "x;(y\<squnion>z) = x;y \<squnion> x;z"
  and semicolon_distr_disj_right: "(x\<squnion>y);z = x;z \<squnion> y;z"
  and concurrency_distr_disj_left: "x\<parallel>(y\<squnion>z) = x\<parallel>y \<squnion> x\<parallel>z"
  and concurrency_distr_disj_right: "(x\<squnion>y)\<parallel>z = x\<parallel>z \<squnion> y\<parallel>z"
  and conj_disj_relationship1: "q=p\<squnion>q \<Longrightarrow> p=p\<sqinter>q"
  and conj_disj_relationship2: "p=p\<sqinter>q \<Longrightarrow> q=p\<squnion>q"
  and exchange: "(p\<parallel>q);(r\<parallel>s) \<sqsubseteq> (p;r)\<parallel>(q;s)"
  (* Kleene star *)
  fixes iteration :: "'a \<Rightarrow> 'a" ("_\<^sup>\<star>" [101] 100)
  assumes iter1: "skip \<squnion> (p;p\<^sup>\<star>) \<sqsubseteq> p\<^sup>\<star>"
  and iter2: "p \<squnion> (q;r) \<sqsubseteq> r \<Longrightarrow> q\<^sup>\<star>;p \<sqsubseteq> r"
  (* We will prove iter3 as a theorem. *)
  and iter4: "p \<squnion> (r;q) \<sqsubseteq> r \<Longrightarrow> p;q\<^sup>\<star> \<sqsubseteq> r"
(* Auxiliary definitions. They appear here because otherwise the sublocale handling will raise problems later. *)
  fixes lessthan :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<sqsubset>" 50)
  defines "x\<sqsubset>y \<equiv> (x\<sqsubseteq>y) \<and> \<not>(y\<sqsubseteq>x)"
  fixes distr_through_disj_p :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" 
  defines "distr_through_disj_p f \<equiv> (\<forall> x y z . (f x (y\<squnion>z) = (f x y) \<squnion> (f x z)) \<and> (f (x\<squnion>y) z) = ((f x z) \<squnion> (f y z)))"
  fixes monotone_p :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" 
  defines "monotone_p f \<equiv> (\<forall> x y z . (x \<sqsubseteq> y \<longrightarrow> (f x z) \<sqsubseteq> (f y z))) \<and> (\<forall> x y z . (y \<sqsubseteq> z \<longrightarrow> (f x y) \<sqsubseteq> (f x z)))"
  (* Don't define backsemicolon x y \<equiv> y;x explicitly - it will make automation difficult. *)
begin

lemma iter3: "skip \<squnion> (p\<^sup>\<star>;p) \<sqsubseteq> p\<^sup>\<star>"
  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\<sqsubseteq>x"
  by (metis disjunction_idempotent refinement_def)
lemma refinement_transitive: "x\<sqsubseteq>y \<Longrightarrow> y\<sqsubseteq>z \<Longrightarrow> x\<sqsubseteq>z"
  by (metis disjunction_associative refinement_def)
lemma refinement_antisymmetric: "x\<sqsubseteq>y \<Longrightarrow> y\<sqsubseteq>x \<Longrightarrow> x=y"
  by (metis disjunction_commutative refinement_def)

text {* Disjunction is the least upper bound. *}
lemma disj_increasing: "x \<sqsubseteq> x\<squnion>y"
  by (metis disjunction_associative disjunction_idempotent refinement_def)
lemma disj_lub: "x\<sqsubseteq>z \<Longrightarrow> y\<sqsubseteq>z \<Longrightarrow> x\<squnion>y \<sqsubseteq> z"
  by (metis disjunction_associative refinement_def)

text {* Conjunction is the greatest lower bound. *}
lemma conj_decreasing: "x\<sqinter>y \<sqsubseteq> x"
  by (metis conj_disj_relationship2 conjunction_associative conjunction_commutative conjunction_idempotent refinement_def)
lemma conj_glb: "x\<sqsubseteq>y \<Longrightarrow> x\<sqsubseteq>z \<Longrightarrow> x\<sqsubseteq>y\<sqinter>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: "\<bottom>\<sqsubseteq>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 \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> (f x z) \<sqsubseteq> (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 \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> (f x y) \<sqsubseteq> (f x z)"
  by (metis distr_through_disj_p_def disj_increasing refinement_def)
text {* Sequential composition is monotone. *}
lemma semicolon_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x;z \<sqsubseteq> y;z"
  by (metis refinement_def semicolon_distr_disj_right)
lemma semicolon_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x;y \<sqsubseteq> x;z"
  by (metis refinement_def semicolon_distr_disj_left)
text {* Concurrency is monotone. *}
lemma concurrency_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x\<parallel>z \<sqsubseteq> y\<parallel>z"
  by (metis concurrency_distr_disj_right refinement_def)
lemma concurrency_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x\<parallel>y \<sqsubseteq> x\<parallel>z"
  by (metis concurrency_commutative concurrency_monotone1)

text {* The small exchange law holds. *}
lemma small_exchange: "(x\<parallel>y);z \<sqsubseteq> x\<parallel>(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 \<Longrightarrow> f (w \<sqinter> x) (y \<sqinter> z) \<sqsubseteq> (f w y)\<sqinter>(f x z)"
proof -
  assume ap: "monotone_p f"
  have a: "f (w \<sqinter> x) (y \<sqinter> z) \<sqsubseteq> f w y" by (metis monotone_p_def ap conj_decreasing refinement_transitive)
  have b: "f (w \<sqinter> x) (y \<sqinter> z) \<sqsubseteq> 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\<sqinter>x);(y\<sqinter>z) \<sqsubseteq> (w;y)\<sqinter>(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 \<squnion>) (op \<sqinter>) (\<lambda> x y . y;x) (op \<parallel>) \<bottom> \<top> 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 \<sqsubseteq>) (op \<sqsubset>)"
apply (rule class.preorder.intro)
apply (metis lessthan_def)
apply (metis refinement_reflexive)
apply (metis refinement_transitive)
done

lemma partial_order: "class.order (op \<sqsubseteq>) (op \<sqsubset>)"
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 \<sqinter>) (op \<sqsubseteq>) (op \<sqsubset>) (op \<squnion>)"
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 \<sqinter>) (op \<sqsubseteq>) (op \<sqsubset>) (op \<squnion>) \<bottom> \<top>"
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 \<sqsubseteq> r' \<Longrightarrow> r' \<sqsubseteq> r \<Longrightarrow> p;q \<sqsubseteq> r"
  by (rule refinement_transitive)

lemma Hconsequence_pre: "p \<sqsubseteq> p' \<Longrightarrow> p';q \<sqsubseteq> r \<Longrightarrow> p;q \<sqsubseteq> r"
  by (metis refinement_transitive semicolon_monotone1)

lemma Hskip: "p;skip \<sqsubseteq> p"
  by (metis refinement_reflexive semicolon_right_unit)

lemma Hsequential_composition: "p;q \<sqsubseteq> r' \<Longrightarrow> r';q' \<sqsubseteq> r \<Longrightarrow> p;(q;q') \<sqsubseteq> r"
  by (metis refinement_transitive semicolon_associative semicolon_monotone1)

lemma Hnon_determinism: "p;q \<sqsubseteq> r \<Longrightarrow> p;q' \<sqsubseteq> r \<Longrightarrow> p;(q\<squnion>q') \<sqsubseteq> r"
  by (metis disj_lub semicolon_distr_disj_left)

lemma Hiteration: "p;q \<sqsubseteq> p \<Longrightarrow> p;q\<^sup>\<star> \<sqsubseteq> p"
by (metis disj_lub iter4 refinement_reflexive)

lemma Hconcurrency: "p;q \<sqsubseteq> r \<Longrightarrow> p';q' \<sqsubseteq> r' \<Longrightarrow> (p\<parallel>p');(q\<parallel>q') \<sqsubseteq> r\<parallel>r'"
  by (metis concurrency_monotone2 concurrency_monotone1 exchange refinement_transitive)

lemma Hframe: "p;q \<sqsubseteq> r \<Longrightarrow> (p\<parallel>f);q \<sqsubseteq> r\<parallel>f"
  by (metis concurrency_commutative concurrency_monotone2 refinement_transitive small_exchange)

lemma Hdisjunction: "p;q \<sqsubseteq> r \<Longrightarrow> p';q \<sqsubseteq> r' \<Longrightarrow> (p\<squnion>p');q \<sqsubseteq> r\<squnion>r'"
  by (metis disjunction_associative disjunction_commutative refinement_def semicolon_distr_disj_right)

lemma Hconjunction: "p;q \<sqsubseteq> r \<Longrightarrow> p';q' \<sqsubseteq> r' \<Longrightarrow> (p\<sqinter>p');(q\<sqinter>q') \<sqsubseteq> r\<sqinter>r'"
  by (metis conj_decreasing conj_glb conjunction_commutative refinement_transitive semicolon_conjunction_exchange)

lemma Floydconjunction: "p;q \<sqsubseteq> r \<Longrightarrow> p';q \<sqsubseteq> r' \<Longrightarrow> (p\<sqinter>p');q \<sqsubseteq> r\<sqinter>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 \<squnion>)" "(op \<sqinter>)" "(\<lambda> x y . y;x)" "(op \<parallel>)" "\<bottom>" "\<top>" "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 \<sqsubseteq> r \<Longrightarrow> p;(q\<parallel>f) \<sqsubseteq> r\<parallel>f"
  by (rule time_reverse.Hframe)

abbreviation (input) 
  milner_triple :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"    ("_-_\<rightarrow>_" [54,54,54] 53)
  where "r-p\<rightarrow>q \<equiv> p;q \<sqsubseteq> r"

lemma Mconcurrency1: "r-p\<rightarrow>q \<Longrightarrow> (r\<parallel>f)-p\<rightarrow>(q\<parallel>f)"
  by (rule Hframe_time_reverse)

lemma Mconcurrency2: "r-p\<rightarrow>skip \<Longrightarrow> (r\<parallel>f)-p\<rightarrow>f"
  by (metis Mconcurrency1 concurrency_left_unit)

lemma Mconcurrency3: "r-p\<rightarrow>q \<Longrightarrow> r'-p'\<rightarrow>q'  \<Longrightarrow> (r\<parallel>r')-(p\<parallel>p')\<rightarrow>(q\<parallel>q')"
  by (rule Hconcurrency)

text {* Rules for other operators. *}
lemma Mprefixing: "r;r'-r\<rightarrow>r'"
  by (metis refinement_reflexive)

lemma Mseq: "r-p\<rightarrow>q \<Longrightarrow> r;r'-p\<rightarrow>q;r'"
  by (metis semicolon_associative semicolon_monotone1)

lemma Mchoice: "r-p\<rightarrow>q \<Longrightarrow> r\<squnion>r'-p\<rightarrow>q"
  by (metis disj_increasing refinement_transitive)

lemma Miter1: "r\<^sup>\<star>-skip\<rightarrow>skip"
  by (metis disj_increasing iter1 refinement_transitive semicolon_left_unit)

lemma Miter2: "r\<^sup>\<star>-skip\<rightarrow>r;r\<^sup>\<star>"
  by (metis disj_increasing disjunction_commutative iter1 refinement_transitive semicolon_left_unit)

text {* Theorems obtained from time reversing Hoare rules. *}
lemma Mskipaction: "p-skip\<rightarrow>p"
  by (metis time_reverse.Hskip)

lemma Mseqaction: "r-q'\<rightarrow>r' \<Longrightarrow> r'-q\<rightarrow>p \<Longrightarrow> r-q';q\<rightarrow>p"
  by (metis time_reverse.Hsequential_composition)

lemma Mchoiceaction: "r-q\<rightarrow>p \<Longrightarrow> r-q'\<rightarrow>p \<Longrightarrow> r-q\<squnion>q'\<rightarrow>p"
  by (metis time_reverse.Hnon_determinism)

lemma Miteration: "p-q\<rightarrow>p \<Longrightarrow> p-q\<^sup>\<star>\<rightarrow>p"
  by (metis time_reverse.Hiteration)

lemma Mfunnychoice: "r-q\<rightarrow>p \<Longrightarrow> r'-q\<rightarrow>p' \<Longrightarrow> r\<squnion>r'-q\<rightarrow>p\<squnion>p'"
  by (metis time_reverse.Hdisjunction)
end


no_notation
  divide  (infixl "'/" 70)

locale postspecification = hoarelogic +
  fixes Lub :: "'a set \<Rightarrow> 'a"     ("\<Squnion>_" [90] 90)
  fixes postspec :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "'/" 80)
  assumes Lub1: "\<Squnion>A \<sqsubseteq> b \<Longrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
  and Lub2: "(\<forall>a\<in>A. a \<sqsubseteq> b) \<Longrightarrow> \<Squnion>A \<sqsubseteq> b"
  and semicolon_distr_Lub_left: "x;\<Squnion>A = \<Squnion>{r. (\<exists>a\<in>A. r=x;a)}"
  and semicolon_distr_Lub_right: "\<Squnion>A;x = \<Squnion>{r. (\<exists>a\<in>A. r=a;x)}" 
  defines "r/p \<equiv> \<Squnion>{q. p;q \<sqsubseteq> r}"
begin

lemma postspec_semicolon_galois1: "q \<sqsubseteq> r/p \<Longrightarrow> p;q \<sqsubseteq> r"
proof -
  assume a: "q \<sqsubseteq> r/p"
  from a have b: "p;q \<sqsubseteq> p;(r/p)" by (rule semicolon_monotone2)
  have c: "p;(r/p) = \<Squnion>{s. \<exists>q. p;q \<sqsubseteq> r \<and> s = p;q}"
    proof -
      have "p;(r/p) = p;\<Squnion>{q. p;q \<sqsubseteq> r}" by (metis postspec_def)
      also have "\<dots> = \<Squnion>{s. (\<exists>a\<in>{q. p;q \<sqsubseteq> r}. s=p;a)}" by (metis semicolon_distr_Lub_left)
      also have "\<dots> = \<Squnion>{s. \<exists>q. p;q \<sqsubseteq> r \<and> s = p;q}"
        proof -
          have "(\<lambda>s. (\<exists>a\<in>{q. p;q \<sqsubseteq> r}. s=p;a)) = (\<lambda>s. (\<exists>q. p;q \<sqsubseteq> r \<and> 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 \<sqsubseteq> \<Squnion>{s. \<exists>q. p;q \<sqsubseteq> r \<and> s = p;q}" by metis
  have "\<forall>s. (\<exists>q. p;q \<sqsubseteq> r \<and> s = p;q) \<longrightarrow> s \<sqsubseteq> r" by metis
  hence "\<forall>s\<in>{s. (\<exists>q. p;q \<sqsubseteq> r \<and> s = p;q)}. s \<sqsubseteq> r" by (smt Collect_def mem_def)
  hence e: "\<Squnion>{s. \<exists>q. p;q \<sqsubseteq> r \<and> s = p;q} \<sqsubseteq> r" by (rule Lub2)
  from d e show ?thesis by (rule refinement_transitive)
qed

lemma postspec_semicolon_galois2: "p;q \<sqsubseteq> r \<Longrightarrow> q \<sqsubseteq> r/p"
proof -
  assume "p;q \<sqsubseteq> r"
  hence "q \<in> {q. p;q \<sqsubseteq> r}" by (metis Collect_def mem_def)
  thus ?thesis by (metis Lub1 postspec_def refinement_reflexive)
qed

lemma postspec_semicolon_galois: "q \<sqsubseteq> r/p \<longleftrightarrow> p;q \<sqsubseteq> r"
  by (metis postspec_semicolon_galois1 postspec_semicolon_galois2)

lemma postspec_concurrency: "q \<sqsubseteq> r/p \<Longrightarrow> q' \<sqsubseteq> r'/p' \<Longrightarrow> q\<parallel>q' \<sqsubseteq> (r\<parallel>r')/(p\<parallel>p')"
  by (metis Hconcurrency postspec_semicolon_galois)

lemma postspec_exchange: "(r/p)\<parallel>(r'/p') \<sqsubseteq> (r\<parallel>r')/(p\<parallel>p')"
  by (metis postspec_concurrency refinement_reflexive)

lemma postspec_distr_conj: "(r\<sqinter>r')/p = r/p \<sqinter> r'/p"
proof -
  have a: "\<And>q. q \<sqsubseteq> (r\<sqinter>r')/p  \<Longrightarrow>  q \<sqsubseteq> r/p \<sqinter> r'/p" by (smt postspec_semicolon_galois conj_decreasing conj_glb conjunction_commutative refinement_transitive)
  have b: "(r\<sqinter>r')/p \<sqsubseteq> (r\<sqinter>r')/p" by (rule refinement_reflexive)
  from b have c: "(r\<sqinter>r')/p \<sqsubseteq> r/p \<sqinter> r'/p" by (rule a)
  have d: "\<And>q. q \<sqsubseteq> r/p \<sqinter> r'/p \<Longrightarrow> q \<sqsubseteq> (r\<sqinter>r')/p" by (smt postspec_semicolon_galois conj_decreasing conj_glb conjunction_commutative refinement_transitive)
  have e: "r/p \<sqinter> r'/p \<sqsubseteq> r/p \<sqinter> r'/p" by (rule refinement_reflexive)
  from e have f: "r/p \<sqinter> r'/p \<sqsubseteq> (r\<sqinter>r')/p" by (rule d)
  from c f show ?thesis by (rule refinement_antisymmetric)
qed

lemma postspec_left_zero: "\<top>/p = \<top>"
  by (metis disjunction_left_zero disjunction_right_zero postspec_semicolon_galois refinement_def)

lemma postspec_disj_distributivity: "r/(p\<squnion>p') = r/p \<sqinter> r/p'"
proof -
  have a: "\<And>q. q \<sqsubseteq> r/(p\<squnion>p')  \<longleftrightarrow>  q \<sqsubseteq> r/p \<sqinter> r/p'"
    proof -
      fix q
      have "q \<sqsubseteq> r/(p\<squnion>p') \<longleftrightarrow> (p\<squnion>p');q \<sqsubseteq> r" by (metis postspec_semicolon_galois)
      also have "\<dots> \<longleftrightarrow> (p;q)\<squnion>(p';q) \<sqsubseteq> r" by (metis semicolon_distr_disj_right)
      also have "\<dots> \<longleftrightarrow> p;q \<sqsubseteq> r \<and> p';q \<sqsubseteq> r" by (metis Hconsequence_pre disj_increasing disjunction_commutative time_reverse.Hnon_determinism time_reverse.semicolon_distr_disj_left)
      also have "\<dots> \<longleftrightarrow> q \<sqsubseteq> r/p \<and> q \<sqsubseteq> r/p'" by (metis postspec_semicolon_galois)
      also have "\<dots> \<longleftrightarrow> q \<sqsubseteq> r/p \<sqinter> r/p'" by (metis conj_decreasing conj_glb conjunction_commutative refinement_transitive)
      finally show "q \<sqsubseteq> r/(p\<squnion>p')  \<longleftrightarrow>  q \<sqsubseteq> r/p \<sqinter> 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 \<sqsubseteq> r' \<Longrightarrow> r/p \<sqsubseteq> r'/p"
  by (metis conj_decreasing conj_glb conjunction_commutative postspec_distr_conj refinement_antisymmetric refinement_reflexive)

lemma postspec_antimonotone_second: "p \<sqsubseteq> p' \<Longrightarrow> r/p' \<sqsubseteq> r/p "
  by (metis conj_disj_relationship2 disjunction_commutative postspec_disj_distributivity refinement_def)
end


locale prespecification = postspecification +
  fixes prespec :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl  "\<setminus>" 80)  (* Using the "setminus" character... *)
  defines "p\<setminus>r \<equiv> \<Squnion>{q. q;p \<sqsubseteq> r}"


text {* Dualize the theorems. *}
sublocale prespecification < time_reverse!: prespecification "(op \<squnion>)" "(op \<sqinter>)" "(\<lambda> x y . y;x)" "(op \<parallel>)" "\<bottom>" "\<top>" "skip" "(op \<sqsubseteq>)" "iteration" "(op \<sqsubset>)" "distr_through_disj_p" "monotone_p" "Lub" "(\<lambda> x y. y\<setminus>x)" "(\<lambda> 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 \<sqsubseteq> p\<setminus>r \<longleftrightarrow> p \<sqsubseteq> r/q"
  by (metis postspec_semicolon_galois time_reverse.postspec_semicolon_galois)

lemma prespec_exchange: "(p\<setminus>r)\<parallel>(p'\<setminus>r') \<sqsubseteq> (p\<parallel>p')\<setminus>(r\<parallel>r')"
  by (rule time_reverse.postspec_exchange)
end

end
