(*
 The Isabelle/HOL proof script accompanying the paper
 "The Laws of Programming Unify Process Calculi"
*)

theory LawsOfProgrammingUnifyProcessCalculi
  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 \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
  and 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"
  and iteration :: "'a \<Rightarrow> 'a" ("_\<^sup>\<star>" [101] 100)
  assumes refinement_reflexive: "x\<sqsubseteq>x"
  and refinement_transitive: "x\<sqsubseteq>y \<Longrightarrow> y\<sqsubseteq>z \<Longrightarrow> x\<sqsubseteq>z"
  and refinement_antisymmetric: "x\<sqsubseteq>y \<Longrightarrow> y\<sqsubseteq>x \<Longrightarrow> x=y"
  and disj_increasing1: "x \<sqsubseteq> x\<squnion>y"
  and disj_increasing2: "y \<sqsubseteq> x\<squnion>y"
  and disj_lub: "x\<sqsubseteq>z \<Longrightarrow> y\<sqsubseteq>z \<Longrightarrow> x\<squnion>y \<sqsubseteq> z"
  and conj_decreasing1: "x\<sqinter>y \<sqsubseteq> x"
  and conj_decreasing2: "x\<sqinter>y \<sqsubseteq> y"
  and conj_glb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y\<sqinter>z"
  (* The table *)
  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>"
  (* Distribution laws *)
  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)))"
  assumes disj_distr_through_disj: "distr_through_disj_p (op \<squnion>)"
  and conj_distr_through_disj: "distr_through_disj_p (op \<sqinter>)"
  and semicolon_distr_through_disj: "distr_through_disj_p (op ;)"
  and concurrency_distr_through_disj: "distr_through_disj_p (op \<parallel>)"
  and exchange: "(p\<parallel>q);(r\<parallel>s) \<sqsubseteq> (p;r)\<parallel>(q;s)"
  (* Kleene star laws *)
  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"
  and iter3: "skip \<squnion> (p\<^sup>\<star>;p) \<sqsubseteq> p\<^sup>\<star>"
  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 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

text {* Simple consequences of the laws. *}
lemma conj_disj_relationship: "q=p\<squnion>q \<longleftrightarrow> p=p\<sqinter>q"
  by (metis conj_decreasing1 conj_decreasing2 conj_glb disj_increasing1 disj_increasing2 disj_lub refinement_antisymmetric refinement_reflexive)

lemma refinement_disj: "x\<sqsubseteq>y \<longleftrightarrow> y=x\<squnion>y"
  by (metis disj_increasing1 disj_increasing2 disj_lub refinement_antisymmetric refinement_reflexive)
lemma refinement_conj: "x\<sqsubseteq>y \<longleftrightarrow> x=x\<sqinter>y"
  by (metis conj_decreasing2 conj_disj_relationship refinement_disj)

lemma bottom_least: "\<bottom>\<sqsubseteq>x"
  by (metis disj_increasing2 disjunction_right_unit)
lemma top_greatest: "x\<sqsubseteq>\<top>"
  by (metis conj_decreasing1 conjunction_left_unit)

lemma iter_unfold1: "skip \<sqsubseteq> p\<^sup>\<star>"
  by (metis disj_increasing1 iter1 refinement_transitive)
lemma iter_unfold2: "p;p\<^sup>\<star> \<sqsubseteq> p\<^sup>\<star>"
  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 \<Longrightarrow> 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 \<squnion>)"
  by (metis disj_distr_through_disj distr_through_disj_implies_monotone)
lemma conj_monotone: "monotone_p (op \<sqinter>)"
  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 \<parallel>)"
  by (metis concurrency_distr_through_disj distr_through_disj_implies_monotone)

text {* Lemmas that aid automation. *}
lemma disj_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x\<squnion>z \<sqsubseteq> y\<squnion>z"
  by (metis monotone_p_def disj_monotone)
lemma conj_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x\<sqinter>z \<sqsubseteq> y\<sqinter>z"
  by (metis monotone_p_def conj_monotone)
lemma semicolon_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x;z \<sqsubseteq> y;z"
  by (metis monotone_p_def semicolon_monotone)
lemma concurrency_monotone1: "x \<sqsubseteq> y \<Longrightarrow> x\<parallel>z \<sqsubseteq> y\<parallel>z"
  by (metis monotone_p_def concurrency_monotone)
lemma disj_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x\<squnion>y \<sqsubseteq> x\<squnion>z"
  by (metis monotone_p_def disj_monotone)
lemma conj_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x\<sqinter>y \<sqsubseteq> x\<sqinter>z"
  by (metis monotone_p_def conj_monotone)
lemma semicolon_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x;y \<sqsubseteq> x;z"
  by (metis monotone_p_def semicolon_monotone)
lemma concurrency_monotone2: "y \<sqsubseteq> z \<Longrightarrow> x\<parallel>y \<sqsubseteq> x\<parallel>z"
  by (metis monotone_p_def concurrency_monotone)

text {* The small exchange laws hold. *}
lemma small_exchange1: "x;(y\<parallel>z) \<sqsubseteq> (x;y)\<parallel>z"
  by (metis concurrency_right_unit exchange semicolon_left_unit)
lemma small_exchange2: "(x\<parallel>y);z \<sqsubseteq> x\<parallel>(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 \<sqsubseteq> x\<parallel>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 \<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_decreasing1 refinement_transitive)
  have b: "f (w \<sqinter> x) (y \<sqinter> z) \<sqsubseteq> 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\<sqinter>x);(y\<sqinter>z) \<sqsubseteq> (w;y)\<sqinter>(x;z)"
  by (metis monotone_op_exchanges_with_conj semicolon_monotone)

text {* The dual property says that a monotone operator reverse-exchanges with disjunction. *}
lemma monotone_op_reverse_exchanges_with_disj: "monotone_p f \<Longrightarrow> (f w y)\<squnion>(f x z) \<sqsubseteq> f (w \<squnion> x) (y \<squnion> z)"
proof -
  assume ap: "monotone_p f"
  have a: " f w y \<sqsubseteq> f (w \<squnion> x) (y \<squnion> z)" by (metis monotone_p_def ap disj_increasing1 refinement_transitive)
  have b: "f x z \<sqsubseteq> f (w \<squnion> x) (y \<squnion> z)" by (metis monotone_p_def ap disjunction_commutative disj_increasing1 refinement_transitive)
  from a b show ?thesis by (metis disjunction_associative refinement_disj)
qed

text {* Time reversal duality (opposition). *}
lemma time_reversal: "basicalgebra (op \<sqsubseteq>) (op \<squnion>) (op \<sqinter>) (\<lambda> x y . y;x) (op \<parallel>) \<bottom> \<top> 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 is_partial_order: "class.order (op \<sqsubseteq>) (op \<sqsubset>)"
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 \<sqinter>) (op \<sqsubseteq>) (op \<sqsubset>) (op \<squnion>)"
apply (rule class.lattice.intro)
apply (rule class.semilattice_inf.intro)
apply (rule is_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 is_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 \<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 is_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 is_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 \<sqsubseteq>)" "(op \<squnion>)" "(op \<sqinter>)" "(\<lambda> x y . y;x)" "(op \<parallel>)" "\<bottom>" "\<top>" "skip" "iteration"
apply (rule time_reversal)
apply (rule distr_through_disj_p_def)
apply (rule lessthan_def)
by (rule monotone_p_def)


section {* Hoare logic *}
locale hoarelogic = basicalgebra
begin

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

theorem Hskip: "p\<lbrace>skip\<rbrace>p"
  by (metis refinement_reflexive semicolon_right_unit)
theorem Hseq: "p\<lbrace>q\<rbrace>r \<Longrightarrow> r\<lbrace>q'\<rbrace>s \<Longrightarrow> p\<lbrace>q;q'\<rbrace>s"
  by (metis refinement_transitive semicolon_associative semicolon_monotone1)
theorem Hchoice: "p\<lbrace>q\<rbrace>r \<Longrightarrow> p\<lbrace>q'\<rbrace>r \<Longrightarrow> p\<lbrace>q\<squnion>q'\<rbrace>r"
  by (metis disj_lub distr_through_disj_p_def semicolon_distr_through_disj)
theorem Hconj': "p\<lbrace>q\<rbrace>r \<Longrightarrow> p'\<lbrace>q'\<rbrace>r' \<Longrightarrow> p\<sqinter>p'\<lbrace>q\<sqinter>q'\<rbrace>r\<sqinter>r'"
  by (metis conj_decreasing1 conj_decreasing2 conj_glb conjunction_exchange refinement_transitive)
theorem Hiter: "p\<lbrace>q\<rbrace>p \<Longrightarrow> p\<lbrace>q\<^sup>\<star>\<rbrace>p"
  by (metis disjunction_commutative iter4 refinement_disj refinement_reflexive)
theorem Hcons: "p'\<sqsubseteq>p \<Longrightarrow> p\<lbrace>q\<rbrace>r \<Longrightarrow> r\<sqsubseteq>r' \<Longrightarrow> p'\<lbrace>q\<rbrace>r'"
  by (metis refinement_transitive semicolon_monotone1)
theorem Hconj: "p\<lbrace>q\<rbrace>r \<Longrightarrow> p'\<lbrace>q\<rbrace>r' \<Longrightarrow> p\<sqinter>p'\<lbrace>q\<rbrace>r\<sqinter>r'"
  by (metis Hconj' conjunction_idempotent)
theorem Hdisj: "p\<lbrace>q\<rbrace>r \<Longrightarrow> p'\<lbrace>q\<rbrace>r' \<Longrightarrow> p\<squnion>p'\<lbrace>q\<rbrace>r\<squnion>r'"
  by (smt disjunction_associative disjunction_commutative distr_through_disj_p_def refinement_disj semicolon_distr_through_disj)
theorem Hconc: "p\<lbrace>q\<rbrace>r \<Longrightarrow> p'\<lbrace>q'\<rbrace>r' \<Longrightarrow> p\<parallel>p'\<lbrace>q\<parallel>q'\<rbrace>r\<parallel>r'"
  by (metis concurrency_monotone2 concurrency_monotone1 refinement_transitive exchange)
theorem Hframe: "p\<lbrace>q\<rbrace>r \<Longrightarrow> f\<parallel>p\<lbrace>q\<rbrace>f\<parallel>r"
  by (metis concurrency_monotone2 refinement_transitive small_exchange2)
theorem Hseqframe: "p\<lbrace>q\<rbrace>r \<Longrightarrow> f;p\<lbrace>q\<rbrace>f;r"
  by (metis semicolon_associative semicolon_monotone2)

end

text {* Make the time reversed versions of the theorems available. *}
sublocale hoarelogic < time_reverse!: hoarelogic "(op \<sqsubseteq>)" "(op \<squnion>)" "(op \<sqinter>)" "(\<lambda> x y . y;x)" "(op \<parallel>)" "\<bottom>" "\<top>" "skip" "iteration"
apply (rule hoarelogic.intro)
apply (rule time_reversal)
apply (rule distr_through_disj_p_def)
apply (rule lessthan_def)
by (rule monotone_p_def)

text {* Time-reversing the Hoare calculus yields another calculus. *}
locale newcalculus = hoarelogic
begin
theorem HseqTimeReverse: "q';r \<sqsubseteq> s \<Longrightarrow> q;p \<sqsubseteq> r \<Longrightarrow> (q';q);p \<sqsubseteq> s"
  by (metis time_reverse.Hseq)
end

section {* Milner-style semantics *}
locale milner = hoarelogic
begin

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

theorem Maction: "p-p\<rightarrow>skip"
  by (metis Hskip)
theorem Mseq1: "p-q\<rightarrow>r \<Longrightarrow> p;p'-q\<rightarrow>r;p'"
  by (metis time_reverse.Hseqframe)
theorem Mseq2: "p-q\<rightarrow>skip \<Longrightarrow> p;p'-q\<rightarrow>p'"
  by (metis Mseq1 semicolon_left_unit)
theorem Mprefixing: "p;p'-p\<rightarrow>p'"
  by (metis Maction Mseq2)

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

lemma rearrangement: "p-\<rightarrow>q \<longleftrightarrow> q \<sqsubseteq> p"
  by (metis semicolon_left_unit)

theorem Mchoice: "p\<squnion>p'-\<rightarrow>p"
  by (metis disj_increasing1 rearrangement)
theorem Mchoice2: "p\<squnion>p'-\<rightarrow>p'"
  by (metis Mchoice disjunction_commutative)
theorem Miter1: "p\<^sup>\<star>-\<rightarrow>skip"
  by (metis iter_unfold1 rearrangement)
theorem Miter2: "p\<^sup>\<star>-\<rightarrow>p;p\<^sup>\<star>"
  by (metis iter_unfold2 rearrangement)
theorem Mconc1: "p-q\<rightarrow>r \<Longrightarrow> p\<parallel>p'-q\<rightarrow>r\<parallel>p'"
  by (metis concurrency_commutative time_reverse.Hframe)
theorem Mconc2: "p-q\<rightarrow>skip \<Longrightarrow> p\<parallel>p'-q\<rightarrow>p'"
  by (metis Mconc1 concurrency_left_unit)
theorem Mconc3: "p-q\<rightarrow>r \<Longrightarrow> p'\<parallel>p-q\<rightarrow>p'\<parallel>r"
  by (metis Mconc1 concurrency_commutative)
theorem Mconc4: "p-q\<rightarrow>skip \<Longrightarrow> p'\<parallel>p-q\<rightarrow>p'"
  by (metis Mconc2 concurrency_commutative)
theorem Mseq: "p-q\<rightarrow>r \<Longrightarrow> r-q'\<rightarrow>s \<Longrightarrow> p-q;q'\<rightarrow>s"
  by (metis time_reverse.Hseq)
theorem Mchoice': "p-q\<rightarrow>r \<Longrightarrow> p\<squnion>p'-q\<rightarrow>r"
  by (metis Mseq Mchoice semicolon_left_unit)
theorem Mcons: "p-\<rightarrow>p' \<Longrightarrow> p'-q\<rightarrow>r \<Longrightarrow> r-\<rightarrow>r' \<Longrightarrow> p-q\<rightarrow>r'"
  by (metis rearrangement time_reverse.Hcons)

end


text {* Make the time reversed versions of the theorems available. *}
sublocale milner < time_reverse!: milner "(op \<sqsubseteq>)" "(op \<squnion>)" "(op \<sqinter>)" "(\<lambda> x y . y;x)" "(op \<parallel>)" "\<bottom>" "\<top>" "skip" "iteration"
apply (rule milner.intro)
apply (rule hoarelogic.intro)
apply (rule time_reversal)
apply (rule distr_through_disj_p_def)
apply (rule lessthan_def)
by (rule monotone_p_def)


section {* Kahn's natural semantics *}
locale kahn = milner
begin

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

lemma  Kimprovement: "p \<sqsubseteq> p' \<Longrightarrow> <p,s>\<rightarrow>s' \<Longrightarrow> <p',s>\<rightarrow>s'"
  by (metis refinement_transitive semicolon_monotone2)

theorem Kskip: "<skip,s>\<rightarrow>s"
  by (metis refinement_reflexive semicolon_right_unit)
theorem Kseq: "<p,s>\<rightarrow>s' \<Longrightarrow> <p',s'>\<rightarrow>s'' \<Longrightarrow> <p;p',s>\<rightarrow>s''"
  by (metis refinement_transitive semicolon_associative semicolon_monotone1)
theorem Kchoice: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis disj_increasing1 refinement_transitive semicolon_monotone2)
theorem Kchoice': "<p',s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis Kchoice disjunction_commutative)
theorem Kiter1: "<p\<^sup>\<star>,s>\<rightarrow>s"
  by (metis Kimprovement iter_unfold1 refinement_reflexive semicolon_right_unit)
theorem Kiter2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<^sup>\<star>,s'>\<rightarrow>s'' \<Longrightarrow> <p\<^sup>\<star>,s>\<rightarrow>s''"
proof -
  assume a: "<p,s>\<rightarrow>s'"
  assume b: "<p\<^sup>\<star>,s'>\<rightarrow>s''"
  from a b have c: "<p;p\<^sup>\<star>,s>\<rightarrow>s''" by (rule Kseq)
  from iter_unfold2 c show "<p\<^sup>\<star>,s>\<rightarrow>s''" by (rule Kimprovement)
qed
theorem Kconc1: "<p,s>\<rightarrow>s' \<Longrightarrow> <p',s'>\<rightarrow>s'' \<Longrightarrow> <p\<parallel>p',s>\<rightarrow>s''"
  by (metis Kimprovement Kseq seq_refines_conc)
theorem Kconc2: "<p',s>\<rightarrow>s' \<Longrightarrow> <p,s'>\<rightarrow>s'' \<Longrightarrow> <p\<parallel>p',s>\<rightarrow>s''"
  by (metis Kconc1 concurrency_commutative)

end