(*
 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 \<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 {* 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 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 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 \<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_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 {* General operational calculus *}
locale generalcalculus = basicalgebra +
  fixes Actions :: "'a set"
  assumes skip_in_Actions: "skip \<in> Actions"
  fixes quintuple :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("<_,_>-_\<rightarrow><_,_>" [54,54,54,54,54] 53)
  defines "<p,s>-q\<rightarrow><p',s'> \<equiv> (q \<in> Actions) \<and> (q;p' \<sqsubseteq> p) \<and> (s' \<sqsubseteq> s;q)"
begin

theorem Grearrange: "p' \<sqsubseteq> p \<Longrightarrow> <p,s>-skip\<rightarrow><p',s>"
  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 \<in> Actions \<Longrightarrow> <p,s>-p\<rightarrow><skip,s;p>"
  by (metis quintuple_def refinement_reflexive semicolon_right_unit)
theorem Gskip: "<skip,s>-skip\<rightarrow><skip,s>"
  by (metis skip_in_Actions Gaction semicolon_right_unit)
theorem Gchoice1: "<p,s>-q\<rightarrow><p',s'> \<Longrightarrow> <p\<squnion>p'',s>-q\<rightarrow><p',s'>"
  by (metis quintuple_def disj_increasing1 refinement_transitive)
theorem Gchoice2: "<p',s>-q\<rightarrow><p'',s'> \<Longrightarrow> <p\<squnion>p',s>-q\<rightarrow><p'',s'>"
  by (metis Gchoice1 disjunction_commutative)
theorem Giter: "<p\<^sup>\<star>,s>-skip\<rightarrow><skip,s>"
  by (metis Grearrange iter_unfold1)

text {* Small step theorems *}
theorem GSseq1: "<p,s>-q\<rightarrow><p',s'> \<Longrightarrow> <p;p'',s>-q\<rightarrow><p';p'',s'>"
  by (metis quintuple_def semicolon_associative semicolon_monotone1)
theorem GSseq2: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p;p',s>-q\<rightarrow><p',s'>"
  by (metis GSseq1 semicolon_left_unit)
theorem GSchoice1: "<p\<squnion>p',s>-skip\<rightarrow><p,s>"
  by (metis skip_in_Actions quintuple_def disj_increasing1 refinement_reflexive semicolon_left_unit semicolon_right_unit)
theorem GSchoice2: "<p\<squnion>p',s>-skip\<rightarrow><p',s>"
  by (metis GSchoice1 disjunction_commutative)
theorem GSiter: "<p\<^sup>\<star>,s>-skip\<rightarrow><p;p\<^sup>\<star>,s>"
  by (metis Grearrange iter_unfold2)
theorem GSiterAlt1: "<p,s>-q\<rightarrow><p',s'> \<Longrightarrow> <p\<^sup>\<star>,s>-q\<rightarrow><p';p\<^sup>\<star>,s'>"
  by (metis quintuple_def iter_unfold2 refinement_transitive semicolon_monotone1 semicolon_associative)
theorem GSiterAlt2: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p\<^sup>\<star>,s>-q\<rightarrow><p\<^sup>\<star>,s'>"
  by (metis GSiterAlt1 semicolon_left_unit)
theorem GSconc1: "<p,s>-q\<rightarrow><p',s'> \<Longrightarrow> <p\<parallel>p'',s>-q\<rightarrow><p'\<parallel>p'',s'>"
  by (metis quintuple_def concurrency_monotone1 refinement_transitive small_exchange1)
theorem GSconc2: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p\<parallel>p',s>-q\<rightarrow><p',s'>"
  by (metis GSconc1 concurrency_left_unit)
theorem GSconc3: "<p,s>-q\<rightarrow><p',s'> \<Longrightarrow> <p''\<parallel>p,s>-q\<rightarrow><p''\<parallel>p',s'>"
  by (metis GSconc1 concurrency_commutative)
theorem GSconc4: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p'\<parallel>p,s>-q\<rightarrow><p',s'>"
  by (metis GSconc2 concurrency_commutative)

text {* Big step theorems *}
theorem GBseq: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p',s'>-q'\<rightarrow><skip,s''> \<Longrightarrow> (q;q') \<in> Actions \<Longrightarrow> <p;p',s>-q;q'\<rightarrow><skip,s''>"
proof -
  assume a: "<p,s>-q\<rightarrow><skip,s'>"
  assume b: "<p',s'>-q'\<rightarrow><skip,s''>"
  assume c: "(q;q') \<in> Actions"
  from a b have d: "q;q' \<sqsubseteq> p;p'" by (metis quintuple_def refinement_transitive semicolon_monotone2 semicolon_right_unit semicolon_monotone1)
  from a b have e: "s'' \<sqsubseteq> s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1)
  from c d e show "<p;p',s>-q;q'\<rightarrow><skip,s''>" by (metis quintuple_def semicolon_right_unit)
qed
theorem GBiter: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p\<^sup>\<star>,s'>-q'\<rightarrow><skip,s''> \<Longrightarrow> (q;q') \<in> Actions \<Longrightarrow> <p\<^sup>\<star>,s>-q;q'\<rightarrow><skip,s''>"
proof -
  assume a: "<p,s>-q\<rightarrow><skip,s'>"
  assume b: "<p\<^sup>\<star>,s'>-q'\<rightarrow><skip,s''>"
  assume c: "(q;q') \<in> Actions"
  from a b have d: "q;q' \<sqsubseteq> p\<^sup>\<star>" by (metis quintuple_def GSiterAlt2 refinement_transitive semicolon_monotone2 semicolon_right_unit)
  from a b have e: "s'' \<sqsubseteq> s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1)
  from c d e show "<p\<^sup>\<star>,s>-q;q'\<rightarrow><skip,s''>" by (metis quintuple_def semicolon_right_unit)
qed
theorem GBconc1: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p',s'>-q'\<rightarrow><skip,s''> \<Longrightarrow> (q;q') \<in> Actions \<Longrightarrow> <p\<parallel>p',s>-q;q'\<rightarrow><skip,s''>"
proof -
  assume a: "<p,s>-q\<rightarrow><skip,s'>"
  assume b: "<p',s'>-q'\<rightarrow><skip,s''>"
  assume c: "(q;q') \<in> Actions"
  from a b have d: "q;q' \<sqsubseteq> p\<parallel>p'" by (metis quintuple_def GSconc2 concurrency_monotone2 refinement_transitive semicolon_right_unit)
  from a b have e: "s'' \<sqsubseteq> s;(q;q')" by (metis quintuple_def refinement_transitive semicolon_associative semicolon_monotone1)
  from c d e show "<p\<parallel>p',s>-q;q'\<rightarrow><skip,s''>" by (metis quintuple_def semicolon_right_unit)
qed
theorem GBconc2: "<p,s>-q\<rightarrow><skip,s'> \<Longrightarrow> <p',s'>-q'\<rightarrow><skip,s''> \<Longrightarrow> (q;q') \<in> Actions \<Longrightarrow> <p'\<parallel>p,s>-q;q'\<rightarrow><skip,s''>"
  by (metis GBconc1 concurrency_commutative)

end

section {* Plotkin's SOS *}
locale plotkin = generalcalculus +
  fixes ptransition4 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("<_,_>\<rightarrow><_,_>" [54,54,54,54] 53)
  defines "<p,s>\<rightarrow><p',s'> \<equiv> \<exists>q. <p,s>-q\<rightarrow><p',s'>"
  fixes ptransition3 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("<_,_>\<rightarrow>_" [54,54,54] 53)
  defines "<p,s>\<rightarrow>s' \<equiv> <p,s>\<rightarrow><skip,s'>"
begin

theorem Paction: "p \<in> Actions \<Longrightarrow> <p,s>\<rightarrow>s;p"
  by (metis Gaction ptransition4_def ptransition3_def)
theorem Pskip: "<skip,s>\<rightarrow>s"
  by (metis Gskip ptransition4_def ptransition3_def)
theorem Pseq1: "<p,s>\<rightarrow><p',s'> \<Longrightarrow> <p;p'',s>\<rightarrow><p';p'',s'>"
  by (metis GSseq1 ptransition4_def)
theorem Pseq2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p;p',s>\<rightarrow><p',s'>"
  by (metis GSseq2 ptransition4_def ptransition3_def)
theorem Pchoice1: "<p\<squnion>p',s>\<rightarrow><p,s>"
  by (metis GSchoice1 ptransition4_def)
theorem Pchoice2: "<p\<squnion>p',s>\<rightarrow><p',s>"
  by (metis GSchoice2 ptransition4_def)
theorem Pchoice1Alt_1: "<p,s>\<rightarrow><p',s'> \<Longrightarrow> <p\<squnion>p'',s>\<rightarrow><p',s'>"
  by (metis Gchoice1 ptransition4_def)
theorem Pchoice1Alt_2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis Pchoice1Alt_1 ptransition3_def)
theorem Pchoice2Alt_1: "<p',s>\<rightarrow><p'',s'> \<Longrightarrow> <p\<squnion>p',s>\<rightarrow><p'',s'>"
  by (metis Gchoice2 ptransition4_def)
theorem Pchoice2Alt_2: "<p',s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis Pchoice2Alt_1 ptransition3_def)
theorem Piter1: "<p\<^sup>\<star>,s>\<rightarrow>s"
  by (metis Giter ptransition4_def ptransition3_def)
theorem Piter2: "<p\<^sup>\<star>,s>\<rightarrow><p;p\<^sup>\<star>,s>"
  by (metis GSiter ptransition4_def)
theorem Piter2Alt1: "<p,s>\<rightarrow><p',s'> \<Longrightarrow> <p\<^sup>\<star>,s>\<rightarrow><p';p\<^sup>\<star>,s'>"
  by (metis GSiterAlt1 ptransition4_def)
theorem Piter2Alt2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<^sup>\<star>,s>\<rightarrow><p\<^sup>\<star>,s'>"
  by (metis GSiterAlt2 ptransition4_def ptransition3_def)
theorem Pconc1: "<p,s>\<rightarrow><p',s'> \<Longrightarrow> <p\<parallel>p'',s>\<rightarrow><p'\<parallel>p'',s'>"
  by (metis GSconc1 ptransition4_def)
theorem Pconc2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<parallel>p',s>\<rightarrow><p',s'>"
  by (metis GSconc2 ptransition4_def ptransition3_def)

end

section {* Milner's process calculus semantics *}
locale milner = generalcalculus +
  fixes mtransition :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("_-_\<rightarrow>_" [54,54,54] 53)
  defines "p-q\<rightarrow>r \<equiv> \<forall>s. \<exists>s'. <p,s>-q\<rightarrow><r,s'>"
begin

lemma mtransition_equivalence: "p-q\<rightarrow>r \<longleftrightarrow> (q \<in> Actions \<and> q;r \<sqsubseteq> p)"
  by (metis bottom_least mtransition_def quintuple_def)

lemma mtransition_alt_def: "p-q\<rightarrow>r \<longleftrightarrow> (\<exists>s s'. <p,s>-q\<rightarrow><r,s'>)"
  by (metis mtransition_def mtransition_equivalence quintuple_def)

theorem Maction: "p \<in> Actions \<Longrightarrow> p-p\<rightarrow>skip"
  by (metis Gaction mtransition_def)
theorem Mskip: "skip-skip\<rightarrow>skip"
  by (metis Gskip mtransition_def)
theorem Mseq1: "p-q\<rightarrow>r \<Longrightarrow> p;p'-q\<rightarrow>r;p'"
  by (smt GSseq1 mtransition_def)
theorem Mseq2: "p-q\<rightarrow>skip \<Longrightarrow> p;p'-q\<rightarrow>p'"
  by (smt GSseq2 mtransition_def)
  
theorem Mprefixing: "p \<in> Actions \<Longrightarrow> 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_equivalence: "p-\<rightarrow>q \<longleftrightarrow> q \<sqsubseteq> p"
  by (metis mtransition_equivalence semicolon_left_unit skip_in_Actions)

theorem Mchoice1: "p\<squnion>p'-\<rightarrow>p"
  by (metis GSchoice1 mtransition_def)
theorem Mchoice2: "p\<squnion>p'-\<rightarrow>p'"
  by (metis GSchoice2 mtransition_def)
theorem Mchoice1Alt: "p-q\<rightarrow>r \<Longrightarrow> p\<squnion>p'-q\<rightarrow>r"
  by (smt Gchoice1 mtransition_def)
theorem Mchoice2Alt: "p'-q\<rightarrow>r \<Longrightarrow> p\<squnion>p'-q\<rightarrow>r"
  by (smt Gchoice2 mtransition_def)
theorem Miter1: "p\<^sup>\<star>-\<rightarrow>skip"
  by (metis Giter mtransition_def)
theorem Miter2: "p\<^sup>\<star>-\<rightarrow>p;p\<^sup>\<star>"
  by (metis GSiter mtransition_def)
theorem Miter2Alt_1: "p-q\<rightarrow>r \<Longrightarrow> p\<^sup>\<star>-q\<rightarrow>r;p\<^sup>\<star>"
  by (smt GSiterAlt1 mtransition_def)
theorem Miter2Alt_2: "p-q\<rightarrow>skip \<Longrightarrow> p\<^sup>\<star>-q\<rightarrow>p\<^sup>\<star>"
  by (smt GSiterAlt2 mtransition_def)
theorem Mconc1: "p-q\<rightarrow>r \<Longrightarrow> p\<parallel>p'-q\<rightarrow>r\<parallel>p'"
  by (smt GSconc1 mtransition_def)
theorem Mconc2: "p-q\<rightarrow>skip \<Longrightarrow> p\<parallel>p'-q\<rightarrow>p'"
  by (smt GSconc2 mtransition_def)
theorem Mconc3: "p-q\<rightarrow>p' \<Longrightarrow> p''\<parallel>p-q\<rightarrow>p''\<parallel>p'"
  by (smt GSconc3 mtransition_def)
theorem Mconc4: "p-q\<rightarrow>skip \<Longrightarrow> p'\<parallel>p-q\<rightarrow>p'"
  by (smt GSconc4 mtransition_def)

theorem GeneralCommunication: "p-q\<rightarrow>p' \<Longrightarrow> r-q'\<rightarrow>r' \<Longrightarrow> q'' \<in> Actions \<Longrightarrow> q'' \<sqsubseteq> q\<parallel>q' \<Longrightarrow> p\<parallel>r-q''\<rightarrow>p'\<parallel>r'"
proof -
  assume a: "p-q\<rightarrow>p'"
  assume b: "r-q'\<rightarrow>r'"
  assume c: "q''  \<in> Actions"
  assume d: "q'' \<sqsubseteq> q\<parallel>q'"
  have e: "\<And>a b c a' b' c'. a;b \<sqsubseteq> c \<Longrightarrow> a';b' \<sqsubseteq> c' \<Longrightarrow> (a\<parallel>a');(b\<parallel>b') \<sqsubseteq> c\<parallel>c'"
    by (metis concurrency_monotone1 concurrency_monotone2 refinement_transitive exchange)
  from a b e have f: "(q\<parallel>q');(p'\<parallel>r') \<sqsubseteq> p\<parallel>r" by (metis mtransition_equivalence)
  from f d have g: "q'';(p'\<parallel>r') \<sqsubseteq> p\<parallel>r" by (metis refinement_transitive semicolon_monotone1)
  from c g show "p\<parallel>r-q''\<rightarrow>p'\<parallel>r'" by (metis mtransition_equivalence)
qed

end

section {* Reduction semantics with evaluation contexts. *}
locale reduction = plotkin + milner +
  fixes program_context :: "('a \<Rightarrow> 'a) \<Rightarrow> bool"
  defines "program_context pc \<equiv> (\<forall>p q p'.  p-q\<rightarrow>p' \<longrightarrow> pc(p)-q\<rightarrow>pc(p'))"
begin

theorem empty_context: "program_context (\<lambda>x. x)"
  by (metis program_context_def)
theorem semicolon_context: "program_context (\<lambda>x. x;P)"
  by (metis Mseq1 program_context_def)
theorem concurrency_context1: "program_context (\<lambda>x. x\<parallel>P)"
  by (metis Mconc1 program_context_def)
theorem concurrency_context2: "program_context (\<lambda>x. P\<parallel>x)"
  by (metis Mconc3 program_context_def)

theorem program_contexts_compose: "program_context pc \<Longrightarrow> program_context pc' \<Longrightarrow> program_context (pc' \<circ> pc)"
  by (metis o_def program_context_def)
corollary example_program_context: "program_context (\<lambda>x. (P\<parallel>(x\<parallel>P'));P'')"
proof -
  have a: "program_context (\<lambda>x. x\<parallel>P')" by (metis concurrency_context1)
  have b: "program_context (\<lambda>y. P\<parallel>y)" by (metis concurrency_context2)
  have c: "program_context (\<lambda>z. z;P'')" by (metis semicolon_context)
  have d: "(\<lambda>y. P\<parallel>y)\<circ>(\<lambda>x. x\<parallel>P') = (\<lambda>x. P\<parallel>(x\<parallel>P'))" by (metis o_def)
  from a b d program_contexts_compose have e: "program_context (\<lambda>x. P\<parallel>(x\<parallel>P'))" by metis
  have f: "(\<lambda>z. z;P'')\<circ>(\<lambda>x. P\<parallel>(x\<parallel>P')) = (\<lambda>x. (P\<parallel>(x\<parallel>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 \<Longrightarrow> p-\<rightarrow>p' \<Longrightarrow> pc(p)-\<rightarrow>pc(p')"
  by (metis program_context_def)
theorem Rmain_configuration_context: "program_context pc \<Longrightarrow> p-\<rightarrow>p' \<Longrightarrow> <pc(p),s>\<rightarrow><pc(p'),s>"
  by (metis Grearrange program_context_def ptransition4_def rearrangement_equivalence)

theorem Rseq: "skip;p-\<rightarrow>p"
  by (metis Mprefixing skip_in_Actions)
theorem Rconc1: "skip\<parallel>p-\<rightarrow>p"
  by (metis Mskip Mconc2)
theorem Rconc2: "p\<parallel>skip-\<rightarrow>p"
  by (metis Mskip Mconc4)

corollary example1: "<(P\<parallel>((P1\<squnion>P2)\<parallel>P'));P'',s>\<rightarrow><(P\<parallel>(P1\<parallel>P'));P'',s>"
  by (metis example_program_context Mchoice1 Rmain_configuration_context)
corollary example2: "<(P\<parallel>((P\<^sup>\<star>)\<parallel>P'));P'',s>\<rightarrow><(P\<parallel>((P;P\<^sup>\<star>)\<parallel>P'));P'',s>"
  by (metis example_program_context Miter2 Rmain_configuration_context)
corollary example3: "<(P\<parallel>((skip;P1)\<parallel>P'));P'',s>\<rightarrow><(P\<parallel>(P1\<parallel>P'));P'',s>"
  by (metis example_program_context Rseq Rmain_configuration_context)

theorem GeneralResult1: "<p,s>-q\<rightarrow><p',s'> \<longleftrightarrow> (\<forall>pc. program_context pc \<longrightarrow> <pc(p),s>-q\<rightarrow><pc(p'),s'>)"
  by (metis empty_context mtransition_equivalence program_context_def quintuple_def)

theorem GeneralResult2: "p-q\<rightarrow>p' \<and> <q,s>\<rightarrow>s' \<longleftrightarrow> (\<forall>pc. program_context pc \<longrightarrow> <pc(p),s>-q\<rightarrow><pc(p'),s'>)"
proof -
  have "p-q\<rightarrow>p' \<and> <q,s>\<rightarrow>s' \<longleftrightarrow> q \<in> Actions \<and> q;p'\<sqsubseteq>p \<and> (\<exists>a. <q,s>-a\<rightarrow><skip,s'>)" by (metis mtransition_equivalence ptransition3_def ptransition4_def)
  also have "\<dots> \<longleftrightarrow> q \<in> Actions \<and> q;p'\<sqsubseteq>p \<and> (\<exists>a. a \<in> Actions \<and> a\<sqsubseteq>q \<and> s'\<sqsubseteq>s;a)" by (metis quintuple_def semicolon_right_unit)
  also have "\<dots> \<longleftrightarrow> q \<in> Actions \<and> q;p'\<sqsubseteq>p \<and> s'\<sqsubseteq>s;q" by (metis monotone_p_def refinement_reflexive refinement_transitive semicolon_monotone)
  also have "\<dots> \<longleftrightarrow> <p,s>-q\<rightarrow><p',s'>" by (metis quintuple_def)
  finally show ?thesis by (metis GeneralResult1)
qed

theorem GeneralResult3: "p-q\<rightarrow>p' \<Longrightarrow> <q,s>\<rightarrow>s' \<Longrightarrow> program_context pc \<Longrightarrow> <pc(p),s>\<rightarrow><pc(p'),s'>"
  by (metis GeneralResult2 ptransition4_def)

theorem Ractions: "q \<in> Actions \<Longrightarrow> <q,s>\<rightarrow>s' \<Longrightarrow> program_context pc \<Longrightarrow> <pc(q),s>\<rightarrow><pc(skip),s'>"
  by (metis GeneralResult3 Maction)

theorem GeneralRelationship: "<p,s>-q\<rightarrow><p',s'> \<longleftrightarrow> p-q\<rightarrow>p' \<and> <q,s>\<rightarrow>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 \<Rightarrow> 'a \<Rightarrow> bool"    ("_\<rightarrow>_" [54,54] 53)
  defines "p\<rightarrow>q \<equiv> \<forall>s. \<exists>s'. <p,s>\<rightarrow><q,s'>"
begin

lemma otransition_alt_def1: "p\<rightarrow>q \<longleftrightarrow> (\<exists>s s'. <p,s>\<rightarrow><q,s'>)"
proof -
  have "(\<exists>s s'. <p,s>\<rightarrow><q,s'>) \<Longrightarrow> p\<rightarrow>q"
    proof -
      assume "\<exists>s s'. <p,s>\<rightarrow><q,s'>"
      hence "\<exists>a s s'. <p,s>-a\<rightarrow><q,s'>" by (metis ptransition4_def)
      hence "\<exists>a. \<forall>s. \<exists>s'. <p,s>-a\<rightarrow><q,s'>" by (metis mtransition_alt_def mtransition_def)
      hence "\<forall>s. \<exists>s'. <p,s>\<rightarrow><q,s'>" by (metis ptransition4_def)
      thus "p\<rightarrow>q" by (metis otransition_def)
    qed
  thus ?thesis by (metis otransition_def)
qed

no_notation
  minus  (infixl "-" 65)

lemma otransition_alt_def2: "p\<rightarrow>q \<longleftrightarrow> (\<exists>a. p-a\<rightarrow>q)"
proof -
  have "p\<rightarrow>q \<Longrightarrow> (\<exists>a. p-a\<rightarrow>q)"
    proof -
      assume "p\<rightarrow>q"
      hence "\<exists>s s'. <p,s>\<rightarrow><q,s'>" by (metis otransition_def)
      thus "\<exists>a. p-a\<rightarrow>q" by (metis ptransition4_def mtransition_alt_def)
    qed
  thus ?thesis by (metis mtransition_def otransition_alt_def1 ptransition4_def)
qed

theorem Oaction: "p \<in> Actions \<Longrightarrow> p\<rightarrow>skip"
  by (metis Paction otransition_def ptransition3_def)
(*  by (metis Maction otransition_alt_def2) *)
theorem Oseq1: "p\<rightarrow>r \<Longrightarrow> p;p'\<rightarrow>r;p'"
  by (metis Pseq1 otransition_def)
(*  by (metis Mseq1 otransition_alt_def2) *)
theorem Oseq2: "p\<rightarrow>skip \<Longrightarrow> p;p'\<rightarrow>p'"
  by (metis Pseq2 otransition_def ptransition3_def)
(*  by (metis Mseq2 otransition_alt_def2) *)
theorem Oprefixing: "p \<in> Actions \<Longrightarrow> p;p'\<rightarrow>p'"
  by (metis Oaction Oseq2)
(*  by (metis Mprefixing otransition_alt_def2) *)
theorem Ochoice1: "p\<squnion>p'\<rightarrow>p"
  by (metis Pchoice1 otransition_def)
(*  by (metis Mchoice1 otransition_alt_def2) *)
theorem Ochoice2: "p\<squnion>p'\<rightarrow>p'"
  by (metis Pchoice2 otransition_def)
(*  by (metis Mchoice2 otransition_alt_def2) *)
theorem Ochoice1Alt: "p\<rightarrow>r \<Longrightarrow> p\<squnion>p'\<rightarrow>r"
  by (metis Pchoice1Alt_1 otransition_def)
(*  by (metis Mchoice1Alt otransition_alt_def2) *)
theorem Ochoice2Alt: "p'\<rightarrow>r \<Longrightarrow> p\<squnion>p'\<rightarrow>r"
  by (metis Pchoice2Alt_1 otransition_def)
(*  by (metis Mchoice2Alt otransition_alt_def2) *)
theorem Oiter1: "p\<^sup>\<star>\<rightarrow>skip"
  by (metis Piter1 otransition_def ptransition3_def)
(*  by (metis Miter1 otransition_alt_def2) *)
theorem Oiter2: "p\<^sup>\<star>\<rightarrow>p;p\<^sup>\<star>"
  by (metis Piter2 otransition_def)
(*  by (metis Miter2 otransition_alt_def2) *)
theorem Oiter2Alt_1: "p\<rightarrow>r \<Longrightarrow> p\<^sup>\<star>\<rightarrow>r;p\<^sup>\<star>"
  by (metis Piter2Alt1 otransition_def)
(*  by (metis Miter2Alt_1 otransition_alt_def2) *)
theorem Oiter2Alt_2: "p\<rightarrow>skip \<Longrightarrow> p\<^sup>\<star>\<rightarrow>p\<^sup>\<star>"
  by (metis Piter2Alt2 otransition_def ptransition3_def)
(*  by (metis Miter2Alt_2 otransition_alt_def2) *)
theorem Oconc1: "p\<rightarrow>r \<Longrightarrow> p\<parallel>p'\<rightarrow>r\<parallel>p'"
  by (metis Pconc1 otransition_def)
(*  by (metis Mconc1 otransition_alt_def2) *)
theorem Oconc2: "p\<rightarrow>skip \<Longrightarrow> p\<parallel>p'\<rightarrow>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 \<Rightarrow> 'a \<Rightarrow> bool"    ("_\<rightharpoonup>_" [54,54] 53)
  defines "p\<rightharpoonup>p' \<equiv> p-\<rightarrow>p'"
  fixes cool :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    ("_\<rightharpoondown>_" [54,54] 53)
  defines "p\<rightharpoondown>p' \<equiv> p-\<rightarrow>p'"
  fixes heatcool :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    ("_\<rightleftharpoons>_" [54,54] 53)
  defines "p\<rightleftharpoons>p' \<equiv> p\<rightharpoonup>p' \<and> p'\<rightharpoondown>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 \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"    (infixr "\<bullet>" 60)
  defines "p \<bullet> pc \<equiv> pc(p)"
  fixes standard_airlock :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<triangleleft>" 60)
  defines "p \<triangleleft> p' \<equiv> p \<bullet> (\<lambda>x. x\<parallel>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"      ("\<lbrace>\<rbrace>") where
  "\<lbrace>\<rbrace> \<equiv> skip"

abbreviation (input)
  singleton_solution :: "'a \<Rightarrow> 'a"     ("\<lbrace>_\<rbrace>") where
  "\<lbrace>p\<rbrace> \<equiv> p"

abbreviation (input)
  pair_solution :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    ("\<lbrace>_,_\<rbrace>") where
  "\<lbrace>p,q\<rbrace> \<equiv> p\<parallel>q"

abbreviation (input)
  solution_union :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<uplus>" 80) where
  "p\<uplus>q \<equiv> p\<parallel>q"

lemma heatcool_equivalence: "p\<rightleftharpoons>p' \<longleftrightarrow> p=p'"
  by (metis cool_def heat_def heatcool_def rearrangement_equivalence refinement_antisymmetric refinement_reflexive)

lemma heating_is_special_reaction: "p\<rightharpoonup>p' \<Longrightarrow> p\<rightarrow>p'"
  by (metis heat_def otransition_alt_def2)
lemma cooling_is_special_reaction: "p\<rightharpoondown>p' \<Longrightarrow> p\<rightarrow>p'"
  by (metis cool_def otransition_alt_def2)

theorem Cchemical_heat: "p\<rightharpoonup>p' \<Longrightarrow> (p\<uplus>p'')\<rightharpoonup>(p'\<uplus>p'')"
  by (metis program_context_def heat_def concurrency_context1)
theorem Cchemical_cool: "p\<rightharpoondown>p' \<Longrightarrow> (p\<uplus>p'')\<rightharpoondown>(p'\<uplus>p'')"
  by (metis Mconc1 cool_def)
theorem Cchemical_heatcool: "p\<rightleftharpoons>p' \<Longrightarrow> (p\<uplus>p'')\<rightleftharpoons>(p'\<uplus>p'')"
  by (metis Cchemical_heat Cchemical_cool heatcool_def)
theorem Cchemical_react: "p\<rightarrow>p' \<Longrightarrow> (p\<uplus>p'')\<rightarrow>(p'\<uplus>p'')"
  by (metis Oconc1)

theorem Csolution_heat: "p\<rightharpoonup>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>pc(p)\<rbrace>\<rightharpoonup>\<lbrace>pc(p')\<rbrace>"
  by (metis program_context_def heat_def)
theorem Csolution_cool: "p\<rightharpoondown>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>pc(p)\<rbrace>\<rightharpoondown>\<lbrace>pc(p')\<rbrace>"
  by (metis program_context_def cool_def)
theorem Csolution_heatcool: "p\<rightleftharpoons>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>pc(p)\<rbrace>\<rightleftharpoons>\<lbrace>pc(p')\<rbrace>"
  by (metis Csolution_heat Csolution_cool heatcool_def)
theorem Csolution_react: "p\<rightarrow>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>pc(p)\<rbrace>\<rightarrow>\<lbrace>pc(p')\<rbrace>"
  by (metis GeneralResult1 otransition_def ptransition4_def)
(* Alternative:  by (metis otransition_alt_def2 program_context_def) *)

theorem (in generalcalculus) GskipAction: "<p,s>-skip\<rightarrow><p,s>"
  by (metis Grearrange refinement_reflexive)
theorem (in milner) MskipAction: "p-\<rightarrow>p"
  by (metis GskipAction mtransition_def)

theorem CgeneralAirlock: "\<lbrace>pc(p)\<rbrace>\<rightleftharpoons>\<lbrace>p \<bullet> pc\<rbrace>"
  by (metis MskipAction general_airlock_def heatcool_def heat_def cool_def)
(* Alternative:  by (metis general_airlock_def heatcool_equivalence) *)

lemma ExposedMoleculesFreely_heat: "p\<rightharpoonup>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>p \<bullet> pc\<rbrace>\<rightharpoonup>\<lbrace>p' \<bullet> pc\<rbrace>"
  by (metis Csolution_heat general_airlock_def)
lemma ExposedMoleculesFreely_cool: "p\<rightharpoondown>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>p \<bullet> pc\<rbrace>\<rightharpoondown>\<lbrace>p' \<bullet> pc\<rbrace>"
  by (metis Csolution_cool general_airlock_def)
lemma ExposedMoleculesFreely_heatcool: "p\<rightleftharpoons>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>p \<bullet> pc\<rbrace>\<rightleftharpoons>\<lbrace>p' \<bullet> pc\<rbrace>"
  by (metis Csolution_heatcool general_airlock_def)
lemma ExposedMoleculesFreely_react: "p\<rightarrow>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>p \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p' \<bullet> pc\<rbrace>"
  by (metis Csolution_react general_airlock_def)

lemma standard_airlock_equivalence: "p \<triangleleft> p' = p \<parallel> p'"
  by (metis general_airlock_def standard_airlock_def)
lemma standard_airlock_associative: "(p \<triangleleft> p') \<triangleleft> p'' = p \<triangleleft> (p' \<triangleleft> p'')"
  by (metis concurrency_associative standard_airlock_equivalence)

theorem Cairlock: "\<lbrace>p\<rbrace> \<uplus> p' \<rightleftharpoons> \<lbrace>p \<triangleleft> p'\<rbrace>"
  by (metis CgeneralAirlock general_airlock_def standard_airlock_equivalence)

lemma SolutionUnderAirlockFreely_heat: "p'\<rightharpoonup>p'' \<Longrightarrow> \<lbrace>p \<triangleleft> p'\<rbrace>\<rightharpoonup>\<lbrace>p \<triangleleft> p''\<rbrace>"
  by (metis Csolution_heat concurrency_context2 standard_airlock_equivalence)
lemma SolutionUnderAirlockFreely_cool: "p'\<rightharpoondown>p'' \<Longrightarrow> \<lbrace>p \<triangleleft> p'\<rbrace>\<rightharpoondown>\<lbrace>p \<triangleleft> p''\<rbrace>"
  by (metis Csolution_cool concurrency_context2 standard_airlock_equivalence)
lemma SolutionUnderAirlockFreely_heatcool: "p'\<rightleftharpoons>p'' \<Longrightarrow> \<lbrace>p \<triangleleft> p'\<rbrace>\<rightleftharpoons>\<lbrace>p \<triangleleft> p''\<rbrace>"
  by (metis Csolution_heatcool concurrency_context2 standard_airlock_equivalence)
lemma SolutionUnderAirlockFreely_react: "p'\<rightarrow>p'' \<Longrightarrow> \<lbrace>p \<triangleleft> p'\<rbrace>\<rightarrow>\<lbrace>p \<triangleleft> p''\<rbrace>"
  by (metis Csolution_react concurrency_context2 standard_airlock_equivalence)

lemma context_with_airlock: "program_context pc \<Longrightarrow> program_context (\<lambda>x. pc(x) \<triangleleft> p)"
  by (metis concurrency_context1 program_context_def standard_airlock_equivalence)

lemma ExposeIon: "\<lbrace>pc(p) \<triangleleft> p'\<rbrace> \<rightleftharpoons> \<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p')\<rbrace>"
  by (metis CgeneralAirlock)

lemma RemainderSolutionFreely_heat: "p'\<rightharpoonup>p'' \<Longrightarrow> \<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p')\<rbrace>\<rightharpoonup>\<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p'')\<rbrace>"
  by (metis SolutionUnderAirlockFreely_heat general_airlock_def)
lemma RemainderSolutionFreely_cool: "p'\<rightharpoondown>p'' \<Longrightarrow> \<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p')\<rbrace>\<rightharpoondown>\<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p'')\<rbrace>"
  by (metis SolutionUnderAirlockFreely_cool general_airlock_def)
lemma RemainderSolutionFreely_heatcool: "p'\<rightleftharpoons>p'' \<Longrightarrow> \<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p')\<rbrace>\<rightleftharpoons>\<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p'')\<rbrace>"
  by (metis SolutionUnderAirlockFreely_heatcool general_airlock_def)
lemma RemainderSolutionFreely_react: "p'\<rightarrow>p'' \<Longrightarrow> \<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p')\<rbrace>\<rightarrow>\<lbrace>p \<bullet> (\<lambda>x. pc(x) \<triangleleft> p'')\<rbrace>"
  by (metis SolutionUnderAirlockFreely_react general_airlock_def)

lemma valid_context_for_Cseq: "program_context (\<lambda>x. x;p' \<triangleleft> p'')"
  by (metis context_with_airlock semicolon_context)

theorem Cseq: "\<lbrace>p;p' \<triangleleft> p''\<rbrace> \<rightleftharpoons> \<lbrace>p \<bullet> (\<lambda>x. x;p' \<triangleleft> p'')\<rbrace>"
  by (metis CgeneralAirlock)
theorem Cconc: "\<lbrace>p\<parallel>p'\<rbrace> \<rightleftharpoons> \<lbrace>p, p'\<rbrace>"
  by (metis CgeneralAirlock general_airlock_def)

lemma ReactionFromRearrangement: "p-\<rightarrow>p' \<Longrightarrow> program_context pc \<Longrightarrow> \<lbrace>p \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p' \<bullet> pc\<rbrace>"
  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 \<Longrightarrow> \<lbrace>p\<squnion>p' \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p \<bullet> pc\<rbrace>"
  by (metis Mchoice1 ReactionFromRearrangement)
theorem Cchoice2: "program_context pc \<Longrightarrow> \<lbrace>p\<squnion>p' \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p' \<bullet> pc\<rbrace>"
  by (metis Mchoice2 ReactionFromRearrangement)
theorem Citer1: "program_context pc \<Longrightarrow> \<lbrace>p\<^sup>\<star> \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>skip \<bullet> pc\<rbrace>"
  by (metis Miter1 ReactionFromRearrangement)
theorem Citer2: "program_context pc \<Longrightarrow> \<lbrace>p\<^sup>\<star> \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p;p\<^sup>\<star> \<bullet> pc\<rbrace>"
  by (metis Miter2 ReactionFromRearrangement)
theorem Cdropskip: "program_context pc \<Longrightarrow> \<lbrace>skip;p \<bullet> pc\<rbrace>\<rightarrow>\<lbrace>p \<bullet> pc\<rbrace>"
  by (metis Rseq ReactionFromRearrangement)

lemma Citer1_with_empty_context: "\<lbrace>p\<^sup>\<star>\<rbrace>\<rightarrow>\<lbrace>skip\<rbrace>"
  by (metis Citer1 empty_context general_airlock_def)
lemma Citer1_with_concurrency_context1: "\<lbrace>p\<^sup>\<star> \<triangleleft> p'\<rbrace>\<rightarrow>\<lbrace>skip \<triangleleft> p'\<rbrace>"
  by (metis Citer1 concurrency_context1 standard_airlock_def)
lemma Cdropskip_with_concurrency_context1: "\<lbrace>skip;p \<triangleleft> p'\<rbrace>\<rightarrow>\<lbrace>p \<triangleleft> p'\<rbrace>"
  by (metis Cdropskip concurrency_context1 standard_airlock_def)

theorem Cskip: "\<lbrace>skip\<rbrace>\<rightharpoonup>\<lbrace>\<rbrace>"
  by (metis Mskip heat_def)

text {* The example derivation: *}

lemma "(\<And>pc. program_context pc \<Longrightarrow> \<lbrace>q \<bullet> pc\<rbrace> \<rightarrow> \<lbrace>skip \<bullet> pc\<rbrace>) \<Longrightarrow> True"
proof -
  assume a: "\<And>pc. program_context pc \<Longrightarrow> \<lbrace>q \<bullet> pc\<rbrace> \<rightarrow> \<lbrace>skip \<bullet> pc\<rbrace>"
  have b: "program_context (\<lambda>x. x;p \<triangleleft> \<lbrace>skip\<rbrace>)" by (metis semicolon_context context_with_airlock)
  have "\<lbrace>q;p \<parallel> p\<^sup>\<star>\<rbrace> \<rightharpoonup> \<lbrace>q;p, p\<^sup>\<star>\<rbrace>" by (metis heatcool_def Cconc)
  have "\<dots> \<rightharpoonup> \<lbrace>q;p \<triangleleft> \<lbrace>p\<^sup>\<star>\<rbrace>\<rbrace>" by (metis heatcool_def Cairlock)
  have "\<dots> \<rightharpoonup> \<lbrace>q \<bullet> (\<lambda>x. x;p \<triangleleft> \<lbrace>p\<^sup>\<star>\<rbrace>)\<rbrace>" by (metis heatcool_def Cseq)
  have "\<dots> \<rightarrow> \<lbrace>q \<bullet> (\<lambda>x. x;p \<triangleleft> \<lbrace>skip\<rbrace>)\<rbrace>" by (metis Citer1_with_empty_context RemainderSolutionFreely_react) 
  have "\<dots> \<rightarrow> \<lbrace>skip \<bullet> (\<lambda>x. x;p \<triangleleft> \<lbrace>skip\<rbrace>)\<rbrace>" by (metis a b)
  have "\<dots> \<rightharpoondown> \<lbrace>skip;p \<triangleleft> \<lbrace>skip\<rbrace>\<rbrace>" by (metis heatcool_def Cseq)
  have "\<dots> \<rightarrow> \<lbrace>p \<triangleleft> \<lbrace>skip\<rbrace>\<rbrace>" by (metis Cdropskip_with_concurrency_context1)
  have "\<dots> \<rightharpoondown> \<lbrace>p,skip\<rbrace>" by (metis heatcool_def Cairlock)
  have "\<dots> \<rightharpoonup> \<lbrace>p\<rbrace>" by (metis Cskip Cchemical_heat concurrency_right_unit concurrency_commutative)
  show ?thesis by metis
qed

(* In jEdit, start to type "right" for \<rightharpoonup>, \<rightharpoondown>, \<rightleftharpoons>.    *)
(* "lbrace" \<lbrace>, "rbrace" \<rbrace>, "uplus" \<uplus>, "triangle" \<triangleleft>   *)

end


section {* Kahn's natural semantics *}
locale kahn = generalcalculus +
  assumes big_steps_possible: "\<forall>x. x \<in> Actions"
  fixes kreduction :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("<_,_>\<rightarrow>_" [54,54,54] 53)
  defines "<p,s>\<rightarrow>s' \<equiv> \<exists>q. <p,s>-q\<rightarrow><skip,s'>"
begin

theorem Kskip: "<skip,s>\<rightarrow>s"
  by (metis Gskip kreduction_def)
theorem Kseq: "<p,s>\<rightarrow>s' \<Longrightarrow> <p',s'>\<rightarrow>s'' \<Longrightarrow> <p;p',s>\<rightarrow>s''"
  by (metis GBseq big_steps_possible kreduction_def)
theorem Kchoice: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis Gchoice1 kreduction_def)
theorem Kchoice': "<p',s>\<rightarrow>s' \<Longrightarrow> <p\<squnion>p',s>\<rightarrow>s'"
  by (metis Gchoice2 kreduction_def)
theorem Kiter1: "<p\<^sup>\<star>,s>\<rightarrow>s"
  by (metis Giter kreduction_def)
theorem Kiter2: "<p,s>\<rightarrow>s' \<Longrightarrow> <p\<^sup>\<star>,s'>\<rightarrow>s'' \<Longrightarrow> <p\<^sup>\<star>,s>\<rightarrow>s''"
  by (metis GBiter big_steps_possible kreduction_def)
theorem Kconc1: "<p,s>\<rightarrow>s' \<Longrightarrow> <p',s'>\<rightarrow>s'' \<Longrightarrow> <p\<parallel>p',s>\<rightarrow>s''"
  by (metis GBconc1 big_steps_possible kreduction_def)
theorem Kconc2: "<p',s>\<rightarrow>s' \<Longrightarrow> <p,s'>\<rightarrow>s'' \<Longrightarrow> <p\<parallel>p',s>\<rightarrow>s''"
  by (metis GBconc2 big_steps_possible kreduction_def)

lemma kahn_equivalence: "<p,s>\<rightarrow>s' \<longleftrightarrow> s' \<sqsubseteq> s;p"
proof -
  have "<p,s>\<rightarrow>s' \<Longrightarrow> s' \<sqsubseteq> s;p"
    proof -
      assume "<p,s>\<rightarrow>s'"
      hence "\<exists>q. q \<sqsubseteq> p \<and> s' \<sqsubseteq> s;q" by (metis kreduction_def quintuple_def semicolon_right_unit)
      thus "s' \<sqsubseteq> 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
