Theory Refinement

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Viorel Preoteasa
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

section‹\label{sec_Refinement}Refinement Calculus and Monotonic Predicate Transformers›

theory Refinement imports Main
begin
text‹
  In this section we introduce the basics of refinement calculus \cite{back-wright-98}.
  Part of this theory is a reformulation of some definitions from \cite{preoteasa:back:2010a},
  but here they are given for predicates, while \cite{preoteasa:back:2010a} uses
  sets.
›
 
notation
    bot ("⊥") and
    top ("⊤") and
    inf (infixl "⊓" 70)
    and sup (infixl "⊔" 65)

subsection‹Basic predicate transformers›

definition
    demonic :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ bool) => 'a ⇒ bool" ("[: _ :]" [0] 1000) where
    "[:Q:] p s = (Q s ≤ p)"

definition
    assert::"('a ⇒ bool) => ('a ⇒ bool) ⇒ ('a ⇒ bool)" ("{. _ .}" [0] 1000) where
    "{.p.} q ≡  p ⊓ q"

definition
    "assume"::"('a ⇒ bool) ⇒ ('a ⇒ bool) => ('a ⇒ bool)" ("[. _ .]" [0] 1000) where
    "[.p.] q ≡  (-p ⊔ q)"

definition
    angelic :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ bool) ⇒ 'a ⇒ bool" ("{: _ :}" [0] 1000) where
    "{:Q:} p s = (Q s ⊓ p ≠ ⊥)"


syntax
    "_assert" :: "patterns => logic => logic"    ("(1{._._.})")
translations
    "_assert x P" == "CONST assert (_abs x P)"

syntax 
    "_demonic" :: "patterns => patterns => logic => logic" ("([:_↝_._:])")
translations
    "_demonic x y t" == "(CONST demonic (_abs x (_abs y t)))"

syntax 
    "_angelic" :: "patterns => patterns => logic => logic" ("({:_ ↝ _._:})")
translations
    "_angelic x y t" == "(CONST angelic (_abs x (_abs y t)))"

lemma assert_o_def: "{.f o g.} = {.(λ x . f (g x)).}"
  by (simp add: o_def)

lemma demonic_demonic: "[:r:] o [:r':] = [:r OO r':]"
  by (simp add: fun_eq_iff le_fun_def demonic_def, auto)

lemma assert_demonic_comp: "{.p.} o [:r:] o {.p'.} o [:r':] = 
      {.x . p x ∧ (∀ y . r x y ⟶ p' y).} o [:r OO r':]"
  by (auto simp add: fun_eq_iff le_fun_def assert_def demonic_def)


lemma demonic_assert_comp: "[:r:] o {.p.} = {.x.(∀ y . r x y ⟶ p y).} o [:r:]"
  by (auto simp add: fun_eq_iff le_fun_def assert_def demonic_def)

lemma assert_assert_comp: "{.p.} o {.p'.} = {.p ⊓ p'.}"
  by (simp add: fun_eq_iff le_fun_def assert_def demonic_def inf_assoc)

lemma assert_assert_comp_pred: "{.p.} o {.p'.} = {.x . p x ∧ p' x.}"
  by (simp add: fun_eq_iff le_fun_def assert_def demonic_def inf_assoc)
    
lemma demonic_refinement: "r' ≤ r ⟹ [:r:] ≤ [:r':]"
  by (simp add: le_fun_def demonic_def)
  
definition "inpt r x = (∃ y . r x y)"



definition trs ::  "('a => 'b ⇒ bool) => ('b ⇒ bool) => 'a ⇒ bool" ("{: _ :]" [0] 1000) where
  "trs r = {. inpt r.} o [:r:]"

syntax 
    "_trs" :: "patterns => patterns => logic => logic" ("({:_↝_._:])")
translations
    "_trs x y t" == "(CONST trs (_abs x (_abs y t)))"


lemma assert_demonic_prop: "{.p.} o [:r:] = {.p.} o [:(λ x y . p x) ⊓ r:]"
  by (auto simp add: fun_eq_iff assert_def demonic_def)

lemma trs_trs: "(trs r) o (trs r') 
  = trs ((λ s t. (∀ s' . r s s' ⟶ (inpt r' s'))) ⊓ (r OO r'))" (is "?S = ?T")
  by (simp add: trs_def inpt_def fun_eq_iff demonic_def assert_def le_fun_def, blast)

lemma prec_inpt_equiv: "p ≤ inpt r ⟹ r' = (λ x y . p x ∧ r x y) ⟹ {.p.} o [:r:] = {:r':]"
  by (simp add: fun_eq_iff demonic_def assert_def le_fun_def inpt_def trs_def, auto)

lemma assert_demonic_refinement: "({.p.} o [:r:] ≤ {.p'.} o [:r':]) = (p ≤ p' ∧ (∀ x . p x ⟶ r' x ≤ r x))"
  by  (auto simp add: le_fun_def assert_def demonic_def)
    
lemma spec_demonic_refinement: "({.p.} o [:r:] ≤ [:r':]) = (∀ x . p x ⟶ r' x ≤ r x)"
  by  (auto simp add: le_fun_def assert_def demonic_def)    

lemma trs_refinement: "(trs r ≤ trs r') = ((∀ x . inpt r x ⟶ inpt r' x) ∧ (∀ x . inpt r x ⟶ r' x ≤ r x))"
  by (simp add: trs_def assert_demonic_refinement, simp add: le_fun_def)

lemma demonic_choice: "[:r:] ⊓ [:r':] = [:r ⊔ r':]"
  by (simp add: fun_eq_iff demonic_def)

lemma spec_demonic_choice: "({.p.} o [:r:]) ⊓ ({.p'.} o [:r':]) = ({.p ⊓ p'.} o [:r ⊔ r':])"
  by (auto simp add: fun_eq_iff demonic_def assert_def)

lemma trs_demonic_choice: "trs r ⊓ trs r' = trs ((λ x y . inpt r x ∧ inpt r' x) ⊓ (r ⊔ r'))"
  by (simp add: trs_def inpt_def fun_eq_iff demonic_def assert_def le_fun_def, blast)

lemma spec_angelic: "p ⊓ p' = ⊥ ⟹ ({.p.} o [:r:]) ⊔ ({.p'.} o [:r':]) 
    = {.p ⊔ p'.} o [:(λ x y . p x ⟶ r x y) ⊓ ((λ x y . p' x ⟶ r' x y)):]"
  by (simp add: fun_eq_iff assert_def demonic_def, auto)

subsection‹Conjunctive predicate transformers›

definition "conjunctive (S::'a::complete_lattice ⇒ 'b::complete_lattice) = (∀ Q . S (Inf Q) = INFIMUM Q S)"
  
definition "sconjunctive (S::'a::complete_lattice ⇒ 'b::complete_lattice) = (∀ Q . (∃ x . x ∈ Q) ⟶ S (Inf Q) = INFIMUM Q S)"
  

lemma conjunctive_sconjunctive[simp]: "conjunctive S ⟹ sconjunctive S"
  by (simp add: conjunctive_def sconjunctive_def)

lemma [simp]: "conjunctive ⊤"
  by (simp add: conjunctive_def)

lemma conjuncive_demonic [simp]: "conjunctive [:r:]"
  apply (simp add: conjunctive_def demonic_def fun_eq_iff)
  using le_Inf_iff by blast

lemma sconjunctive_assert [simp]: "sconjunctive {.p.}"
  apply (simp add: sconjunctive_def assert_def, safe)
  apply (rule antisym)
   apply (meson inf_le1 inf_le2 le_INF_iff le_Inf_iff le_infI)
  by (metis (mono_tags, lifting) Inf_greatest le_INF_iff le_inf_iff order_refl)

lemma sconjunctive_simp: "x ∈ Q ⟹ sconjunctive S ⟹ S (Inf Q) = INFIMUM Q S"
  by (auto simp add: sconjunctive_def)

lemma sconjunctive_INF_simp: "x ∈ X ⟹ sconjunctive S ⟹ S (INFIMUM X Q) = INFIMUM (Q`X) S"
  by (cut_tac x = "Q x" and Q = "Q ` X" in sconjunctive_simp, auto)

lemma demonic_comp [simp]: "sconjunctive S ⟹ sconjunctive S' ⟹ sconjunctive (S o S')"
proof (subst sconjunctive_def, safe)
  fix X :: "'c set"
  fix a :: 'c
  assume [simp]: "sconjunctive S"
  assume [simp]: "sconjunctive S'"
  assume [simp]: "a ∈ X"
  have C: "(S ` S' ` X)  = (S o S') ` X"
    by (auto simp add: image_def)
  have A: "S' (Inf X) = Inf (S' ` X)"
    by (rule_tac x = a in sconjunctive_simp, auto)
  also have B: "S (Inf (S' ` X)) =  Inf (S ` S' ` X)"
    by (rule_tac x = "S' a" in sconjunctive_simp, auto)
  also have B: "... =  Inf ((S o S') ` X)"
    by (simp add: C)
  finally show "(S o S') (Inf X) =Inf ((S ∘ S') ` X)" by simp
qed

lemma conjunctive_INF[simp]:"conjunctive S ⟹ S (INFIMUM X Q) = (INFIMUM X (S o Q))"
  by (metis INF_image conjunctive_def)

lemma conjunctive_simp: "conjunctive S ⟹  S (Inf Q) = INFIMUM Q S"
  by (metis conjunctive_def)

lemma conjunctive_monotonic [simp]: "sconjunctive S ⟹ mono S"
  proof (rule monoI)
    fix a b :: 'a
    assume [simp]: "a ≤ b"
    assume [simp]: "sconjunctive S"
    have [simp]: "a ⊓ b = a"
      by (rule antisym, auto)
    have A: "S a = S a ⊓ S b"
      by (cut_tac S = S and x = a and Q = "{a, b}" in sconjunctive_simp, auto )
    show "S a ≤ S b"
      by (subst A, simp)
  qed

definition "grd S = - S ⊥"

lemma grd_demonic: "grd [:r:] = inpt r"
  by (simp add: fun_eq_iff grd_def demonic_def le_fun_def inpt_def)
      
lemma "(S::'a::bot ⇒ 'b::boolean_algebra) ≤ S' ⟹ grd S' ≤ grd S"
  by (simp add: grd_def le_fun_def)

lemma [simp]: "inpt (λx y. p x ∧ r x y) = p ⊓ inpt r"
  by (simp add: fun_eq_iff inpt_def)

(*to remove*)
lemma [simp]: "p ≤ inpt r ⟹ p ⊓ inpt r = p"
  by (simp add: fun_eq_iff le_fun_def, auto)

lemma grd_spec: "grd ({.p.} o [:r:]) = -p ⊔ inpt r"
  by (simp add: grd_def fun_eq_iff demonic_def assert_def le_fun_def inpt_def)


definition "fail S = -(S ⊤)"
definition "term S = (S ⊤)"
definition "prec S = - (fail S)"
definition "rel S = (λ x y . ¬ S (λ z . y ≠ z) x)"

lemma rel_spec: "rel ({.p.} o [:r:]) x y = (p x ⟶ r x y)"
  by (simp add: rel_def demonic_def assert_def le_fun_def)

lemma prec_spec: "prec ({.p.} o [:r::'a⇒'b⇒bool:]) = p"
  by (auto simp add: prec_def fail_def demonic_def assert_def le_fun_def fun_eq_iff)

lemma fail_spec: "fail ({.p.} o [: r :]) = -p"
  by (simp add: fail_def fun_eq_iff assert_def demonic_def le_fun_def top_fun_def)

lemma [simp]: "prec ({.p.} o [:r:]) = p"
  by (simp add: prec_def fail_spec)

lemma [simp]: "prec (T::('a::boolean_algebra ⇒ 'b::boolean_algebra)) = ⊤ ⟹ prec (S o T) = prec S"
  by (simp add: prec_def fail_def)

lemma [simp]: "prec [:r:] = ⊤"
  by (simp add: demonic_def prec_def fail_def fun_eq_iff)

lemma prec_rel: "{. p .} ∘ [: λx y. p x ∧ r x y :] = {.p.} o [:r:]"
  by (simp add: fun_eq_iff le_fun_def demonic_def assert_def, auto)

definition "Fail = ⊥"

lemma Fail_assert_demonic: "Fail = {.⊥.} o [:r:]"
  by (simp add: fun_eq_iff Fail_def assert_def)

lemma Fail_assert: "Fail = {.⊥.} o [:⊥:]"
  by (rule Fail_assert_demonic)

lemma fail_comp[simp]: "⊥ o S = ⊥"
  by (simp add: fun_eq_iff)

lemma Fail_fail: "mono (S::'a::boolean_algebra ⇒ 'b::boolean_algebra) ⟹ (S = Fail) = (fail S = ⊤)"
proof auto
  show "fail (Fail::'a ⇒ 'b) = ⊤"
    by (metis Fail_def bot_apply compl_bot_eq fail_def)
next
  assume A: "mono S"
  assume B: "fail S = ⊤"
  show "S = Fail"
  proof (rule antisym)
    show "S ≤ Fail"
      by (metis (hide_lams, no_types) A B bot.extremum_unique compl_le_compl_iff fail_def le_fun_def monoD top_greatest)
    next
      show "Fail ≤ S"
        by (metis Fail_def bot.extremum)
  qed
qed
    
lemma sconjunctive_spec: "sconjunctive S ⟹ S = {.prec S.} o [:rel S:]"
proof (simp add: fun_eq_iff assert_def rel_def demonic_def prec_def fail_def le_fun_def, safe)
  fix x xa
  assume  "sconjunctive S"
  from this have mono: "mono S"
    by (rule conjunctive_monotonic)
  from this have A: "S x ≤ S ⊤"
    by (simp add: monoD)
  assume C: "S x xa"
  from this and A show "S ⊤ xa"
    by blast
  fix xb
  from mono have B: "¬ x xb ⟹ S x ≤ S ((≠) xb)"
    by (rule monoD, blast)
  assume "¬ S ((≠) xb) xa"
  from this B C show "x xb"
    by blast
next
  fix xa x
  assume  sconj: "sconjunctive S"
  assume B: "S ⊤ xa"
  assume D: "∀xb. ¬ S ((≠) xb) xa ⟶ x xb"
  define Q where "Q = { (≠) b | b . ¬ x b}"
  from sconj have A: "(∃x. x ∈ Q) ⟹ S (Inf Q) = (INF x:Q. S x)"
    by (simp add: sconjunctive_def)
  have C: "Inf Q = x"
    apply (simp add: Q_def fun_eq_iff, safe)
    by (drule_tac x = "(≠) xa" in spec, auto)
  show "S x xa"
  proof cases
    assume "x = ⊤"
    from this B show ?thesis by simp
  next
    assume "x ≠ ⊤"
    from this have [simp]: "S x = (INF x:Q. S x)"
      apply (unfold C [symmetric])
      by (rule A, blast)
    show ?thesis
      apply simp
      using D by (simp add: Q_def, blast)
  qed
qed
  
definition "non_magic S = (S ⊥ = ⊥)"
  

lemma non_magic_spec: "non_magic ({.p.} o [:r:]) = (p ≤ inpt r)"
  by (simp add: non_magic_def fun_eq_iff inpt_def demonic_def assert_def le_fun_def)

lemma spec_eq: "p = p' ⟹ (∀ x . p x ⟶ r x = r' x) ⟹ {.p.} o [:r:] = {.p'.} o [:r':]"
  by (auto simp add: fun_eq_iff demonic_def le_fun_def assert_def)


lemma sconjunctive_non_magic: "sconjunctive S ⟹ non_magic S = (prec S ≤ inpt (rel S))"
  apply (subst non_magic_spec [THEN sym])
  apply (subst sconjunctive_spec [THEN sym])
  by simp_all
  
definition "implementable S = (sconjunctive S ∧ non_magic S)"

lemma implementable_spec: "implementable S ⟹ ∃ p r . S = {.p.} o [:r:] ∧ p ≤ inpt r"
  apply (simp add: implementable_def)
  apply (rule_tac x = "prec S" in exI)
  apply (rule_tac x = "rel S" in exI, safe)
  apply (rule sconjunctive_spec, simp)
  by (drule sconjunctive_non_magic, auto)


definition "Skip = (id:: ('a ⇒ bool) ⇒ ('a ⇒ bool))"

lemma assert_true_skip: "{.⊤::'a ⇒ bool.} = Skip"
  by (simp add: fun_eq_iff assert_def Skip_def)

lemma skip_comp [simp]: "Skip o S = S"
  by (simp add: fun_eq_iff assert_def Skip_def)

lemma comp_skip[simp]:"S o Skip = S"
  by (simp add: fun_eq_iff assert_def Skip_def)

lemma assert_rel_skip[simp]: "{. λ (x, y) . True .} = Skip"
  by (simp add: fun_eq_iff Skip_def assert_def)

lemma [simp]: "mono S ⟹ mono S' ⟹ mono (S o S')"
  by (simp add: mono_def)

lemma mono_assert[simp]: "mono {.p.}"
  by simp

lemma [simp]: "mono [:r::('a ⇒ 'b ⇒ bool):]"
  by simp

lemma assert_true_skip_a: "{. x . True .} = Skip"
  by (simp add: fun_eq_iff assert_def Skip_def)
    
lemma assert_false_fail: "{.⊥.}  = ⊥"
  by (simp add: fun_eq_iff assert_def)
    

lemma magoc_comp[simp]: "⊤ o S = ⊤"
  by (simp add: fun_eq_iff)

lemma left_comp: "T o U = T' o U' ⟹ S o T o U = S o T' o U'"
  by (simp add: comp_assoc)

lemma assert_demonic: "{.p.} o [:r:] = {.p.} o [:x  ↝ y . p x ∧ r x y:]"
  by (auto simp add: fun_eq_iff assert_def demonic_def le_fun_def)

lemma "trs r ⊓ trs r' = trs (λ x y . inpt r x ∧ inpt r' x ∧ (r x y ∨ r' x y))"
  by (auto simp add: fun_eq_iff trs_def assert_def demonic_def inpt_def)


lemma mono_assume[simp]: "mono [.p.]"
  by (metis assume_def monoI sup.orderI sup_idem sup_mono)

lemma mono_demonic[simp]: "mono [:r:]"
  by  (auto simp add: mono_def demonic_def le_fun_def)

lemma mono_comp_a[simp]: "mono S ⟹ mono T ⟹ mono (S o T)"
  by simp

lemma mono_demonic_choice[simp]: "mono S ⟹ mono T ⟹ mono (S ⊓ T)"
  apply (simp add: mono_def)
  apply auto
   apply (rule_tac y = "S x" in order_trans, simp_all)
  by (rule_tac y = "T x" in order_trans, simp_all)

lemma mono_Skip[simp]: "mono Skip"
  by (simp add: mono_def Skip_def)

lemma mono_comp: "mono S ⟹ S ≤ S' ⟹ T ≤ T' ⟹ S o T ≤ S' o T'"
  proof (simp add: le_fun_def, safe)
    fix x
    assume A: "mono S"
    assume B: "∀x. S x ≤ S' x"
    assume "∀x. T x ≤ T' x"
    from this have "T x ≤ T' x" by simp
    from A and this have C: "S (T x) ≤ S (T' x)"
      by (simp add: mono_def)
    from B also have "... ≤ S' (T' x)" by simp
    from C and this show "S (T x) ≤ S' (T' x)" by (rule order_trans)
  qed

lemma sconjunctive_simp_a: "sconjunctive S ⟹ prec S = p ⟹ rel S = r ⟹ S = {.p.} o [:r:]"
  by (subst sconjunctive_spec, simp_all)

lemma sconjunctive_simp_b: "sconjunctive S ⟹ prec S = ⊤ ⟹ rel S = r ⟹ S = [:r:]"
  by (subst sconjunctive_spec, simp_all add: assert_true_skip)

lemma sconj_Fail[simp]: "sconjunctive Fail"
  by (metis Fail_def INF_eq_const all_not_in_conv bot_apply sconjunctive_def)

lemma sconjunctive_simp_c: "sconjunctive (S::('a ⇒ bool) ⇒ 'b ⇒ bool) ⟹ prec S = ⊥ ⟹ S = Fail"
  by (drule sconjunctive_spec, simp add: Fail_assert_demonic [THEN sym])

lemma demonic_eq_skip: "[: (=) :] = Skip"
  apply (simp add: fun_eq_iff)
  by (metis (mono_tags) Skip_def demonic_def id_apply predicate1D predicate1I)

definition "Havoc = [:⊤:]"

definition "Magic = [:⊥::'a ⇒ 'b ⇒ bool:]"

lemma Magic_top: "Magic = ⊤"
  by (simp add: fun_eq_iff Magic_def demonic_def)
    
lemma [simp]: "Magic ≠ Fail"
  by (simp add: Magic_top Fail_def fun_eq_iff)
      
lemma Havoc_Fail[simp]: "Havoc o (Fail::'a ⇒ 'b ⇒ bool) = Fail"
  by (simp add: Havoc_def fun_eq_iff Fail_def demonic_def le_fun_def)

lemma demonic_havoc: "[: λx (x', y). True :] = Havoc"
  by (simp add: fun_eq_iff demonic_def le_fun_def top_fun_def Havoc_def)

lemma [simp]: "mono Magic"
  by (simp add: Magic_def)

lemma demonic_false_magic: "[: λ(x, y) (u, v). False :] = Magic"
  by (simp add: fun_eq_iff demonic_def le_fun_def top_fun_def Magic_def)

lemma demonic_magic[simp]: "[:r:] o Magic = Magic"
  by (simp add:  fun_eq_iff demonic_def le_fun_def top_fun_def bot_fun_def Magic_def product_def Skip_def)

lemma magic_comp[simp]: "Magic o S = Magic"
  by (simp add:  fun_eq_iff demonic_def le_fun_def top_fun_def Magic_def product_def Skip_def)
    
lemma hvoc_magic[simp]: "Havoc ∘ Magic = Magic"
  by (simp add: Havoc_def)

lemma "Havoc ⊤ = ⊤"
  by (simp add: Havoc_def fun_eq_iff demonic_def le_fun_def top_fun_def)
    
lemma Skip_id[simp]: "Skip p = p"
  by (simp add: Skip_def)


lemma demonic_pair_skip: "[: x, y ↝ u, v. x = u ∧ y = v :] = Skip"
  by (simp add: fun_eq_iff demonic_def Skip_def le_fun_def)

lemma comp_demonic_demonic: "S o [:r:] o [:r':] = S o [:r OO r':]"
  by (simp add: comp_assoc demonic_demonic)

lemma comp_demonic_assert: "S o [:r:] o {.p.} = S o {. x. ∀y . r x y ⟶ p y .} o [:r:]"
  by (simp add: comp_assoc demonic_assert_comp)

lemma assert_demonic_eq_demonic: "({.p.} o [:r::'a ⇒ 'b ⇒ bool:] = [:r:]) = (∀ x . p x)"
  by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, blast)

lemma trs_inpt_top: "inpt r = ⊤ ⟹ trs r = [:r:]"
  by (simp add: trs_def assert_true_skip)

subsection‹Product and Fusion of predicate transformers›
  
text‹
  In this section we define the fusion and product operators from \cite{back:butler:1995}. 
  The fusion of two programs $S$ and $T$ is intuitively equivalent with the parallel execution 
  of the two programs. If $S$ and $T$ assign nondeterministically some value to some program 
  variable $x$, then the fusion of $S$ and $T$ will assign a value to $x$ which can be assigned 
  by both $S$ and $T$.
›

definition fusion :: "(('a ⇒ bool) ⇒ ('b ⇒ bool)) ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool)) ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool))" (infixl "∥" 70) where
  "(S ∥ S') q x = (∃ (p::'a⇒bool) p' . p ⊓ p' ≤ q ∧ S p x ∧ S' p' x)"

lemma fusion_demonic: "[:r:] ∥ [:r':] = [:r ⊓ r':]"
  by (auto simp add: fun_eq_iff fusion_def demonic_def le_fun_def)

lemma fusion_spec: "({.p.} ∘ [:r:]) ∥ ({.p'.} ∘ [:r':]) = ({.p ⊓ p'.} ∘ [:r ⊓ r':])"
  by (auto simp add: fun_eq_iff fusion_def assert_def demonic_def le_fun_def)

lemma fusion_assoc: "S ∥ (T ∥ U) = (S ∥ T) ∥ U"
proof (rule antisym, auto simp add: fusion_def)
  fix p p' q s s' :: "'a ⇒ bool"
  fix a
  assume A: "p ⊓ p' ≤ q" and B: "s ⊓ s' ≤ p'"
  assume C: "S p a" and D: "T s a" and E: "U s' a"
  from A and B  have F: "(p ⊓ s) ⊓ s' ≤ q"
    by (simp add: le_fun_def)
  have "(∃v v'. v ⊓ v' ≤ (p ⊓ s) ∧ S v a ∧ T v' a)"
    by (metis C D order_refl)
  show "∃u u' . u ⊓ u' ≤ q ∧ (∃v v'. v ⊓ v' ≤ u ∧ S v a ∧ T v' a) ∧ U u' a"
    by (metis F C D E order_refl)
next
  fix p p' q s s' :: "'a ⇒ bool"
  fix a
  assume A: "p ⊓ p' ≤ q" and B: "s ⊓ s' ≤ p"
  assume C: "S s a" and D: "T s' a" and E: "U p' a"
  from A and B  have F: "s ⊓ (s' ⊓ p')  ≤ q"
    by (simp add: le_fun_def)
  have "(∃v v'. v ⊓ v' ≤ s' ⊓ p' ∧ T v a ∧ U v' a)"
    by (metis D E eq_iff)
  show "∃u u'. u ⊓ u' ≤ q ∧ S u a ∧ (∃v v'. v ⊓ v' ≤ u' ∧ T v a ∧ U v' a)"
    by (metis F C D E order_refl)
qed

lemma fusion_refinement: "S ≤ T ⟹ S' ≤ T' ⟹ S ∥ S' ≤ T ∥ T'"
  by (simp add: le_fun_def fusion_def, metis)

lemma "conjunctive S ⟹ S ∥ ⊤ = ⊤"
  by (auto simp add: fun_eq_iff fusion_def le_fun_def conjunctive_def)

lemma fusion_spec_local: "a ∈ init ⟹ ([: x ↝ u, y . u ∈ init ∧ x = y :] ∘ {.p.} ∘ [:r:]) ∥ ({.p'.} ∘ [:r':]) 
    = [: x ↝ u, y . u ∈ init ∧ x = y :] ∘ {.u,x . p (u, x) ∧ p' x.} ∘ [:u, x ↝ y . r (u, x) y ∧ r' x y:]" (is "?p ⟹ ?S = ?T")
proof -
  assume "?p"
  from this have [simp]: "(λx. ∀a. a ∈ init ⟶ p (a, x) ∧ p' x) = (λx. ∀a. a ∈ init ⟶ p (a, x)) ⊓ p'"
     by auto
  have [simp]: "(λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) = (λx (u, y). u ∈ init ∧ x = y) OO r ⊓ r'"
    by auto
  have "?S = 
    ({. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ [: r :]) ∥ ({. p' .} ∘ [: r' :])"
    by (simp add: demonic_assert_comp)
  also have "... =  {. (λx. ∀a. a ∈ init ⟶ p (a, x)) ⊓ p' .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO r ⊓ r' :]"
    by (simp add: comp_assoc demonic_demonic fusion_spec)
  also have "... = ?T"
    by (simp add: demonic_assert_comp comp_assoc demonic_demonic fusion_spec)
  finally show ?thesis by simp
qed
  
lemma fusion_demonic_idemp [simp]: "[:r:] ∥ [:r:] = [:r:]"
  by (simp add: fusion_demonic)


lemma fusion_spec_local_a: "a ∈ init ⟹ ([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]) ∥ [:r':] 
    = ([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:u, x ↝ y . r (u, x) y ∧ r' x y:])"
  by (cut_tac p' = "⊤" and init = init and p = p and r = r and r' = r' in fusion_spec_local, auto simp add:  assert_true_skip)

lemma fusion_local_refinement:
  "a ∈ init ⟹ (⋀ x u y . u ∈ init ⟹ p' x ⟹ r (u, x) y ⟹ r' x y) ⟹ 
    {.p'.} o (([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]) ∥ [:r':]) ≤ [:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]"
proof -
 assume A: "a ∈ init"
 assume [simp]: "(⋀ x u y . u ∈ init ⟹ p' x ⟹ r (u, x) y ⟹ r' x y)"
 have " {. x. p' x ∧ (∀a. a ∈ init ⟶ p (a, x)) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) :]
          ≤ {. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO r :]"
  by (auto simp add: assert_demonic_refinement)
from this have " {. x. p' x ∧ (∀a. a ∈ init ⟶ p (a, x)) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) :]
        ≤ {. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ [: r :]"
  by (simp add: comp_assoc demonic_demonic)
from this have "{. p' .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: λ(u, x) y. r (u, x) y ∧ r' x y :] 
        ≤ [: x ↝ u, y. u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: r :]"
  by (simp add: demonic_assert_comp assert_demonic_comp)
from this have "{. p' .} ∘ ([: x ↝ (u, y) . u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: (u, x) ↝ y . r (u, x) y ∧ r' x y :]) 
      ≤ [: x ↝ (u, y) . u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: r :]"
  by (simp add: comp_assoc [THEN sym])
from A and this show ?thesis 
  by  (unfold fusion_spec_local_a, simp)
qed

lemma fusion_spec_demonic: "({.p.} o [:r:]) ∥ [:r':] = {.p.} o [:r ⊓ r':]"
  by (cut_tac p = p and p' = ⊤ and r = r and r' = r' in fusion_spec, simp add: assert_true_skip)



definition Fusion :: "('c ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool))) ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool))" where
   "Fusion S q x = (∃ (p::'c ⇒ 'a ⇒ bool) . (INF c . p c) ≤ q ∧ (∀ c . (S c) (p c) x))"


lemma Fusion_spec: "Fusion (λ n . {.p n.} ∘ [:r n:]) = ({.INFIMUM UNIV p.} ∘ [:INFIMUM UNIV r:])"
  apply (simp add: fun_eq_iff Fusion_def assert_def demonic_def le_fun_def)
  apply safe
  apply blast
  apply blast
  by (rule_tac x = "λ x y . r x xa y" in exI, auto)
  
lemma Fusion_demonic: "Fusion (λ n . [:r n:]) = [:INF n . r n:]"
  apply (cut_tac r = r and p = ⊤ in Fusion_spec)
  by (simp add: assert_true_skip)

lemma Fusion_refinement: "(⋀ i . S i ≤ T i) ⟹ Fusion S ≤ Fusion T"
  apply (simp add: le_fun_def Fusion_def, safe)
  by (rule_tac x = p in exI, auto)

lemma mono_fusion[simp]: "mono (S ∥ T)"
  apply (auto simp add: mono_def fusion_def)
  using order_trans by auto
    
lemma mono_Fusion: "mono (Fusion S)"
  by (simp add: mono_def Fusion_def le_fun_def, auto)

definition "prod_pred A B = (λ(a, b). A a ∧ B b)"
definition Prod :: "(('a ⇒ bool) ⇒ ('b ⇒ bool)) ⇒ (('c ⇒ bool) ⇒ ('d ⇒ bool)) ⇒ (('a × 'c ⇒ bool) ⇒ ('b × 'd ⇒ bool))"
   (infixr "**" 70)
  where
  "(S ** T) q = (λ (x, y) . ∃ p p' . prod_pred p p' ≤ q ∧ S p x ∧ T p' y)" 

lemma mono_prod[simp]: "mono (S ** T)"
  by (auto simp add: mono_def Prod_def)

lemma Prod_spec: "({.p.} o [:r:]) ** ({.p'.} o [:r':]) = {.x,y . p x ∧ p' y.} o [:x, y ↝ u, v . r x u ∧ r' y v:]"
  apply (simp add: Prod_def fun_eq_iff prod_pred_def demonic_def assert_def le_fun_def)
  apply safe
  apply metis
  by metis

lemma Prod_demonic: "[:r:] ** [:r':] = [:x, y ↝ u, v . r x u ∧ r' y v:]"
  apply (simp add: Prod_def fun_eq_iff prod_pred_def demonic_def le_fun_def)
  apply safe
  apply metis
  by metis

lemma Prod_angelic_demonic: "({:a:} o [:r:]) ** ({:a':} o [:r':]) = {:e,f ↝ u, v . a e u ∧ a' f v:} o [:x, y ↝ u, v . r x u ∧ r' y v:]"
  apply (simp add: Prod_def fun_eq_iff prod_pred_def demonic_def le_fun_def angelic_def)
  apply auto
  by metis


lemma Prod_spec_Skip: "({.p.} o [:r:]) ** Skip = {.x,y . p x.} o [:x, y ↝ u, v . r x u ∧ v = y:]"
  apply (cut_tac p = p and r = r and p' = ⊤ and r' = "λ (x::'b) y . x = y" in Prod_spec)
  apply auto
  apply (subgoal_tac "(λ(x::'c, y::'b) (u::'a, v::'b). r x u ∧ y = v)
     = (λ(x::'c, y::'b) (u::'a, v::'b). r x u ∧ v = y)")
  by (auto simp add: fun_eq_iff assert_true_skip demonic_eq_skip)

lemma Prod_Skip_spec: "Skip ** ({.p.} o [:r:]) = {.x,y . p y.} o [:x, y ↝ u, v . x = u ∧ r y v:]"
  apply (cut_tac p = ⊤ and r = "λ (x::'a) y . x = y" and p' = p and r' = r in Prod_spec)
  by (auto simp add:assert_true_skip demonic_eq_skip)

 lemma Prod_skip_demonic: "Skip ** [:r:] = [:x, y ↝ u, v . x = u ∧ r y v:]"
  by (cut_tac r = "(=)" and r' = r in Prod_demonic, simp add: demonic_eq_skip)    

 lemma Prod_demonic_skip: "[:r:] ** Skip = [:x, y ↝ u, v . r x u ∧  y = v:]"
  by (cut_tac r' = "(=)" and r = r in Prod_demonic, simp add: demonic_eq_skip)

lemma Prod_spec_demonic: "({.p.} o [:r:]) **  [:r':] = {.x, y . p x.} o [:x, y ↝ u, v . r x u ∧ r' y v:]"
  by (cut_tac p = p and p' = ⊤ and r = r and r' = r' in Prod_spec, simp add: assert_true_skip)

lemma Prod_demonic_spec: "[:r:] ** ({.p.} o [:r':]) = {.x, y . p y.} o [:x, y ↝ u, v . r x u ∧ r' y v:]"
  by (cut_tac p = ⊤ and p' = p and r = r and r' = r' in Prod_spec, simp add: assert_true_skip)

lemma pair_eq_demonic_skip: "[: λ(x, y) (u, v). x = u ∧ v = y :] = Skip"
  by (simp add: fun_eq_iff demonic_def le_fun_def assert_def)

lemma Prod_assert_skip: "{.p.} ** Skip = {.x,y . p x.}"
  apply (cut_tac p = p and  r = "(=)" in Prod_spec_Skip)
  by (simp add: demonic_eq_skip pair_eq_demonic_skip)

lemma Prod_skip_assert: "Skip ** {.p.} = {.x,y . p y.}"
  apply (cut_tac p = p and  r = "(=)" in Prod_Skip_spec)
  by (simp add: demonic_eq_skip demonic_pair_skip)
    
lemma fusion_comute: "S ∥ T = T ∥ S"
  by (simp add: fusion_def fun_eq_iff, metis inf_commute)

lemma fusion_mono1: "S ≤ S' ⟹ S ∥ T ≤ S' ∥ T"
  by (auto simp add: le_fun_def fusion_def)

lemma prod_mono1: "S ≤ S' ⟹ S ** T ≤ S' ** T"
  by (auto simp add: Prod_def le_fun_def)

lemma prod_mono2: "S ≤ S' ⟹ T ** S ≤ T ** S'"
  by (auto simp add: Prod_def le_fun_def)

lemma Prod_fusion: "S ** T = ([:x,y ↝ x' . x = x':] o S o [:x ↝ x', y . x = x':]) ∥ ([:x, y ↝ y' . y = y':] o T o [:y ↝ x, y' . y = y':])"
proof (simp add: fun_eq_iff Prod_def prod_pred_def fusion_def demonic_def le_fun_def, safe)
  fix x::"'a × 'b ⇒ bool" fix a :: 'c fix b::'d fix p::"'a ⇒ bool" fix p' :: "'b ⇒ bool"
  assume [simp]: "∀a b. p a ∧ p' b ⟶ x (a, b)"
  assume [simp]: "S p a"
  assume [simp]: "T p' b"
  have [simp]: "[:x↝(x', y).x = x':] (λx. p (fst x)) = p"
    by (simp add: fun_eq_iff demonic_def, auto)
  have [simp]: "[:y↝(x, ya).y = ya:] (λx. p' (snd x)) = p'"
    by (simp add: fun_eq_iff demonic_def, auto)
  show "∃p p'. (∀a b. p (a, b) ∧ p' (a, b) ⟶ x (a, b)) ∧ S ([:x↝(x', y).x = x':] p) a ∧ T ([:y↝(x, ya).y = ya:] p') b"
    apply (rule_tac x = "λ x . p (fst x)" in exI)
    apply (rule_tac x = "λ x . p' (snd x)" in exI)
    by simp
next
  fix x::"'a × 'b ⇒ bool" fix a :: 'c fix b::'d fix p::"'a × 'b ⇒ bool" fix p' :: "'a × 'b ⇒ bool"
  assume [simp]: "  ∀a b. p (a, b) ∧ p' (a, b) ⟶ x (a, b)"
  assume [simp]: "S ([:x↝(x', y).x = x':] p) a"
  assume [simp]: " T ([:y↝(x, ya).y = ya:] p') b"
  have [simp]: "(λa. ∀b. p (a, b)) = [:x↝(x', y).x = x':] p"
    by (simp add: fun_eq_iff demonic_def, auto)
  have [simp]: "(λb. ∀a. p' (a, b)) = [:y↝(x, ya).y = ya:] p'"
    by (simp add: fun_eq_iff demonic_def, auto)
  show "∃p p'. (∀a b. p a ∧ p' b ⟶ x (a, b)) ∧ S p a ∧ T p' b"  
    apply (rule_tac x = "λ a . ∀ b . p (a, b)" in exI)
    apply (rule_tac x = "λ b . ∀ a . p' (a, b)" in exI)
    by simp
qed

lemma refin_comp_right: "(S::'a ⇒ 'b::order) ≤ T ⟹ S o X ≤ T o X"
  by (simp add: le_fun_def)

lemma refin_comp_left: "mono X ⟹ (S::'a ⇒ 'b::order) ≤ T ⟹ X o S  ≤ X o T"
  apply (simp add: le_fun_def)
  by (simp add: monoD)

lemma mono_angelic[simp]: "mono {:r:}"
  apply (simp add: angelic_def mono_def le_fun_def)
  by (metis (no_types, hide_lams) Collect_empty_eq_bot empty_Collect_eq inf1E inf1I)

lemma [simp]: "Skip ** Magic = Magic"
  by (auto simp add: fun_eq_iff demonic_def le_fun_def top_fun_def Magic_def Prod_def prod_pred_def Skip_def)

lemma [simp]: "S ** Fail = Fail"
  by (auto simp add: fun_eq_iff Prod_def prod_pred_def Fail_def)

lemma [simp]: "Fail ** S = Fail"
  by (auto simp add: fun_eq_iff  Prod_def prod_pred_def Fail_def)

lemma demonic_conj: "[:(r::'a ⇒ 'b ⇒ bool):] o (S ⊓ S') = ([:r:] o S) ⊓ ([:r:] o  S')"
  by (simp add: fun_eq_iff demonic_def product_def Skip_def prod_pred_def le_fun_def assert_def, auto)

 lemma demonic_assume: "[:r:] o [.p.] = [:x ↝ y . r x y ∧ p y:]"
    by (simp add: fun_eq_iff demonic_def product_def Skip_def le_fun_def assume_def, auto)
  
lemma assume_demonic: "[.p.] o [:r:] = [:x ↝ y . p x ∧ r x y:]"
  by (simp add: fun_eq_iff demonic_def product_def Skip_def le_fun_def assume_def, auto)

lemma [simp]: "(Fail::'a::boolean_algebra) ≤ S"
  by (simp add: Fail_def)

lemma prod_skip_skip[simp]: "Skip ** Skip = Skip"
  apply (cut_tac r = "(=)" and r' = "(=)" in Prod_demonic)
  by (simp add: demonic_eq_skip demonic_pair_skip)

lemma fusion_prod: "S ∥ T = [:x ↝ y, z . x = y ∧ x = z:] o Prod S T o [:y , z ↝ x . y = x ∧ z = x:]"
  by (simp add: fun_eq_iff fusion_def Prod_def demonic_def prod_pred_def le_fun_def)

lemma fusion_angelic_demonic: "({:a:} o [:r:]) ∥ ({:a':} o [:r':]) =  {:e ↝ u, v . a e u ∧ a' e v :} o [:u, v ↝ x . r u x ∧ r' v x:]"
  apply (simp add: fusion_def fun_eq_iff demonic_def le_fun_def angelic_def)
  apply auto
  by blast

lemma prec_fusion: "mono S ⟹ mono T ⟹ prec (S ∥ T) = prec S ⊓ prec T"
  by (auto simp add: prec_def fusion_def fail_def fun_eq_iff mono_def le_fun_def)
 
lemma [simp]: "prec S = ⊤ ⟹ prec T = ⊤ ⟹ prec (S ** T) = ⊤"
  apply (simp add: prec_def fail_def Prod_def fun_eq_iff, safe)
  apply (rule_tac x = ⊤ in exI, simp)
  by (rule_tac x = ⊤ in exI, simp)

lemma prec_skip[simp]: "prec Skip = (⊤::'a⇒bool)"
  by (simp add: fun_eq_iff prec_def fail_def Skip_def)

lemma [simp]: "prec S = ⊤ ⟹ prec T = ⊤ ⟹ prec (S ∥ T) = ⊤"
  by (simp add: fusion_prod)

subsection‹Functional Update›

definition update :: "('a ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'a ⇒ bool" ("[-_-]") where
    "[-f-] = [:x ↝ y . y = f x:]"
syntax
    "_update" :: "patterns ⇒ tuple_args ⇒ logic"    ("(1[- _ ↝ _ -])")
translations
    "_update x (_tuple_args f F)" == "CONST update ((_abs x (_tuple f F)))"
    "_update x (_tuple_arg F)" == "CONST update (_abs x F)"

definition "func (S:: ('a ⇒ bool) ⇒ ('b⇒bool)) x = (if prec S x then (SOME y . rel S x y) else undefined)"

lemma rel_demonic: "rel [:r:] = r"
  by (simp add: fun_eq_iff demonic_def rel_def le_fun_def)

lemma func_assert_update: "func ({.p.} o [-f-]) = (λ x . if p x then f x else undefined)"
  by (simp add: fun_eq_iff func_def update_def rel_def demonic_def assert_def le_fun_def)

lemma func_update: "func [-f-] = f"
  by (simp add: fun_eq_iff func_def update_def rel_demonic)

lemma prec_assert_update: "prec ({.p.} o [-f-]) = p"
  by (simp add: update_def demonic_def le_fun_def fun_eq_iff assert_def)

lemma assert_update_comp: "{.p.} o [- f -] o {.p'.} o [- f' -] = 
      {. p ⊓ (p' o f) .} o [- f' o f -]"
  by (auto simp add: fun_eq_iff le_fun_def assert_def demonic_def update_def)

    
lemma update_o_def: "[-f o g-] = [-x ↝ f (g x)-]"
  by (simp add: o_def)
    
lemma update_simp: "[-f-] q = (λ x . q (f x))"
  by (simp add: demonic_def update_def fun_eq_iff, auto)
    

lemma update_assert_comp: "[-f-] o {.p.} = {.p o f.} o [-f-]"
  by (simp add: fun_eq_iff update_def demonic_def assert_def le_fun_def)

lemma update_comp: "[-f-] o [-g-] = [-g o f-]"
  by (simp add: fun_eq_iff update_def demonic_def le_fun_def)

lemma update_demonic_comp: "[-f-] o [:r:] = [:x ↝ y . r (f x) y:]"
  by (simp add: fun_eq_iff update_def demonic_def le_fun_def)    
    
lemma demonic_update_comp: "[:r:] o [-f-] = [:x ↝ y . ∃ z . r x z ∧ y = f z:]"
  by (simp add: fun_eq_iff update_def demonic_def le_fun_def, auto)    

lemma comp_update_demonic: "S o [-f-] o [:r:] = S o [:x ↝ y . r (f x) y:]"
  by (simp add: comp_assoc update_demonic_comp)

lemma comp_demonic_update: "S o [:r:] o [-f-] = S o [:x ↝ y . ∃ z . r x z ∧ y = f z:]"
  by (simp add: comp_assoc demonic_update_comp)
        
lemma convert: "(λ x y . (S::('a ⇒ bool) ⇒ ('b ⇒ bool)) x (f y)) = [-f-] o S"
  by (simp add: fun_eq_iff update_def demonic_def le_fun_def)

lemma prod_update: "[-f-] ** [-g-] = [-x, y ↝ f x, g y -]"
  apply (simp add: update_def Prod_demonic)
  apply (rule_tac f = demonic in  HOL.arg_cong)
  by fast

lemma prod_update_skip: "[-f-] ** Skip = [- x, y ↝ f x, y-]"
  apply (simp add: update_def Prod_demonic_skip)
  apply (rule_tac f = demonic in  HOL.arg_cong)
  by fast

lemma prod_skip_update: "Skip ** [-f-] = [- x, y ↝ x, f y-]"
  apply (simp add: update_def Prod_skip_demonic)
  apply (rule_tac f = demonic in  HOL.arg_cong)
  by fast

lemma prod_assert_update_skip: "({.p.} o [-f-]) ** Skip = {.x,y . p x.} o [- x, y ↝ f x, y-]"
  apply (simp add: update_def Prod_spec_Skip)
  apply (rule_tac f = "(o)  {. λ(x, y). p x .}" in  HOL.arg_cong)
  apply (rule_tac f = "demonic" in  HOL.arg_cong)
  by fast

lemma prod_skip_assert_update: "Skip ** ({.p.} o [-f-]) = {.x,y . p y.} o [-λ (x, y) . (x, f y)-]"
  apply (simp add: update_def Prod_Skip_spec)
  apply (rule_tac f = "(o)  {. λ(x, y). p y .}" in  HOL.arg_cong)
  apply (rule_tac f = "demonic" in  HOL.arg_cong)
  by fast

lemma prod_assert_update: "({.p.} o [-f-]) ** ({.p'.} o [-f'-]) = {.x,y . p x ∧ p' y.} o [-λ (x, y) . (f x, f' y)-]"
  apply (simp add: update_def Prod_spec)
  apply (rule_tac f = "(o)  {. λ(x, y). p x ∧ p' y .}" in  HOL.arg_cong)
  apply (rule_tac f = "demonic" in  HOL.arg_cong)
  by (simp add: fun_eq_iff)

lemma update_id_Skip: "[-id-] = Skip"
  by (simp add: update_def fun_eq_iff demonic_def le_fun_def)

lemma prod_assert_assert_update: "{.p.} ** ({.p'.} o [-f-]) = {.x,y . p x ∧ p' y.} o [- x, y ↝ x, f y-]"
  apply (cut_tac p = p and p' = p' and f = id and f' = f in prod_assert_update)
  by (simp add: update_id_Skip)

lemma prod_assert_update_assert: "({.p.} o [-f-])** {.p'.} = {.x,y . p x ∧ p' y.} o [- x, y ↝ f x, y-]"
  apply (cut_tac p = p and p' = p' and f = f and f' = id in prod_assert_update)
  by (simp add: update_id_Skip)

lemma prod_update_assert_update: "[-f-] ** ({.p.} o [-f'-]) = {.x,y . p y.} o [-x, y ↝ f x, f' y-]"
  apply (cut_tac p = ⊤ and p' = p and f = f and f' = f' in prod_assert_update)
  by (simp add: assert_true_skip)

lemma prod_assert_update_update: "({.p.} o [-f-])** [-f'-] = {.x,y . p x .} o [- x, y ↝ f x, f' y-]"
  apply (cut_tac p = p and p' = ⊤ and f = f and f' = f' in prod_assert_update)
  by (simp add: assert_true_skip)

lemma Fail_assert_update: "Fail = {.⊥.} o [- (Eps ⊤) -]"
  by (simp add: fun_eq_iff Fail_def assert_def)

lemma fail_assert_update: "⊥ = {.⊥.} o [- (Eps ⊤) -]"
  by (simp add: fun_eq_iff assert_def)

lemma update_fail: "[-f-] o ⊥ = ⊥"
  by (simp add: update_def demonic_def fun_eq_iff le_fun_def)

lemma fail_assert_demonic: "⊥ = {.⊥.} o [:⊥:]"
  by (simp add: fun_eq_iff assert_def)

lemma false_update_fail: "{.λx. False.} o [-f-] = ⊥"
  by (simp add: fail_assert_update fun_eq_iff assert_def)

lemma comp_update_update: "S ∘ [-f-] ∘ [-f'-] = S ∘ [- f' o f -]"
  by (simp add: comp_assoc update_comp)

lemma comp_update_assert: "S ∘ [-f-] ∘ {.p.} = S ∘ {.p o f.} o [-f-]"
  by (simp add: comp_assoc update_assert_comp)

lemma prod_fail: "⊥ ** S = ⊥"
  by (simp add: fun_eq_iff Prod_def prod_pred_def)

lemma fail_prod: "S ** ⊥ = ⊥"
  by (simp add: fun_eq_iff Prod_def prod_pred_def)

lemma assert_fail: "{.p.} o ⊥ = ⊥"
  by (simp add: assert_def fun_eq_iff)

lemma angelic_assert: "{:r:} o {.p.} = {:x ↝ y . r x y ∧ p y:}"
  by (simp add: fun_eq_iff angelic_def demonic_def assert_def)

lemma Prod_Skip_angelic_demonic: "Skip ** ({:r:} o [:r':]) = {:s,x ↝ s',y . r x y ∧ s' = s:} o [:s,x ↝ s',y . r' x y ∧ s' = s:]"
  apply (simp add: fun_eq_iff Prod_def Skip_def angelic_def demonic_def le_fun_def prod_pred_def)
  apply safe
  apply metis
  apply (rule_tac x = "λ x . x = a" in exI)
  apply (rule_tac x = "λ b . x (a, b)" in exI)
  by metis

lemma Prod_angelic_demonic_Skip: "({:r:} o [:r':]) ** Skip = {:x, u ↝ y, u' . r x y ∧ u = u':} o  [:x, u ↝ y, u' . r' x y ∧ u = u':]"
  apply (simp add: fun_eq_iff demonic_def angelic_def le_fun_def Skip_def Prod_def prod_pred_def, auto)
  apply (rule_tac x = "λ a . r' aa a" in exI)
  apply (rule_tac x = "λ a . a = b" in exI, simp_all)
  by metis

lemma prec_rel_eq: "p = p' ⟹ r = r' ⟹ {.p.} o [:r:] = {.p'.} o [:r':]"
  by simp

lemma prec_rel_le: "p ≤ p' ⟹ (⋀ x . p x ⟹ r' x ≤ r x) ⟹ {.p.} o [:r:] ≤ {.p'.} o [:r':]"
  by (simp add: le_fun_def demonic_def assert_def)

lemma assert_update_eq: "({.p.} o [-f-] = {.p'.} o [-f'-]) = (p = p' ∧ (∀ x. p x ⟶ f x = f' x))"
  apply (simp add: fun_eq_iff assert_def demonic_def update_def le_fun_def)
  by auto

lemma update_eq: "([-f-] = [-f'-]) = (f = f')"
  apply (simp add: fun_eq_iff assert_def demonic_def update_def le_fun_def)
  by auto

lemma spec_eq_iff: 
  shows spec_eq_iff_1: "p = p' ⟹ f = f' ⟹ {.p.} o [-f-] = {.p'.} o [-f'-]" 
  and spec_eq_iff_2: "f = f' ⟹ [-f-] = [-f'-]"
  and spec_eq_iff_3: "p = (λ x . True) ⟹ f = f' ⟹ {.p.} o [-f-] = [-f'-]"
  and spec_eq_iff_4: "p = (λ x . True) ⟹ f = f' ⟹ [-f-] = {.p.} o [-f'-]"
  by (simp_all add: assert_true_skip_a)

lemma spec_eq_iff_a: 
  shows"(⋀ x . p x = p' x) ⟹ (⋀ x . f x = f' x) ⟹ {.p.} o [-f-] = {.p'.} o [-f'-]" 
  and "(⋀ x . f x = f' x) ⟹ [-f-] = [-f'-]"
  and "(⋀ x . p x) ⟹ (⋀ x . f x = f' x) ⟹ {.p.} o [-f-] = [-f'-]"
  and "(⋀ x . p x) ⟹(⋀ x . f x = f' x) ⟹ [-f-] = {.p.} o [-f'-]"
  apply (subgoal_tac "p = p' ∧ f = f'")
  apply simp
  apply (simp add: fun_eq_iff)
  apply (subgoal_tac "f = f'")
  apply simp
  apply (simp add: fun_eq_iff)

  apply (subgoal_tac "p = (λ x. True) ∧ f = f'")
  apply (simp add: assert_true_skip_a)
  apply (simp add: fun_eq_iff)
  apply (subgoal_tac "p = (λ x. True) ∧ f = f'")
  apply (simp add: assert_true_skip_a)
  by (simp add: fun_eq_iff)

lemma spec_eq_iff_prec: "p = p' ⟹ (⋀ x . p x ⟹ f x = f' x) ⟹ {.p.} o [-f-] = {.p'.} o [-f'-]"
  by (simp add: update_def fun_eq_iff assert_def demonic_def le_fun_def, auto)


lemma trs_prod: "trs r ** trs r' = trs (λ (x,x') (y,y') . r x y ∧ r' x' y')"
  apply (simp add: trs_def)
  apply (simp add: Prod_spec)
  apply (subgoal_tac "(λ (x, y).inpt r x ∧ inpt r' y) = ( inpt (λ(x, x') (y, y'). r x y ∧ r' x' y'))")
  apply (simp_all)
  by (simp add: fun_eq_iff inpt_def)

lemma sconjunctiveE: "sconjunctive S ⟹ (∃ p r . S = {. p .} o [: r ::'a ⇒ 'b ⇒ bool:])"
  by (drule sconjunctive_spec, blast)

lemma sconjunctive_prod [simp]: "sconjunctive S ⟹ sconjunctive S' ⟹ sconjunctive (S ** S')"
  apply (drule sconjunctiveE)
  apply (drule sconjunctiveE)
  apply safe
  by (simp add: Prod_spec)

lemma nonmagic_prod [simp]: "non_magic S ⟹ non_magic S' ⟹ non_magic (S ** S')"
  apply (simp add: non_magic_def)
  apply (simp add: Prod_def)
  apply (simp add: fun_eq_iff prod_pred_def le_fun_def, safe)
  apply (case_tac "p = ⊥", simp_all)
  apply (simp add: fun_eq_iff)
  apply (case_tac "p' = ⊥", simp_all)
  by (simp add: fun_eq_iff)

lemma non_magic_comp [simp]: "non_magic S ⟹ non_magic S' ⟹ non_magic (S o S')"
  by (simp add: non_magic_def)

lemma implementable_pred [simp]: "implementable S ⟹ implementable S' ⟹ implementable (S ** S')"
  by (simp add: implementable_def)

lemma implementable_comp[simp]: "implementable S ⟹ implementable S' ⟹ implementable (S o S')"
  by (simp add: implementable_def)

lemma nonmagic_assert: "non_magic {.p.}"
  by (simp add: non_magic_def assert_def)
    
subsection ‹Control Statements›
  
definition "if_stm p S T = ([.p.] o S) ⊓ ([.-p.] o T)"
  
definition "while_stm p S = lfp (λ X . if_stm p (S o X) Skip)"
  
definition "Sup_less x (w::'b::wellorder) = Sup {(x v)::'a::complete_lattice | v . v < w}"
  
lemma Sup_less_upper: "v < w ⟹ P v ≤ Sup_less P w"
  by (simp add: Sup_less_def, rule Sup_upper, blast)

lemma Sup_less_least: "(⋀ v . v < w ⟹ P v ≤ Q) ⟹ Sup_less P w ≤ Q"
  by (simp add: Sup_less_def, rule Sup_least, blast)

theorem fp_wf_induction:
  "f x  = x ⟹ mono f ⟹ (∀ w . (y w) ≤ f (Sup_less y w)) ⟹ Sup (range y) ≤ x"
  apply (rule Sup_least)
  apply (simp add: image_def, safe, simp)
  apply (rule less_induct, simp_all)
  apply (rule_tac y = "f (Sup_less y xa)" in order_trans, simp)
  apply (drule_tac x = "Sup_less y xa" and y = "x" in monoD)
  by (simp add: Sup_less_least, auto)

theorem lfp_wf_induction: "mono f ⟹ (∀ w . (p w) ≤ f (Sup_less p w)) ⟹ Sup (range p) ≤ lfp f"
  apply (rule fp_wf_induction, simp_all)
  by (drule lfp_unfold, simp)
 
theorem lfp_wf_induction_a: "mono f ⟹ (∀ w . (p w) ≤ f (Sup_less p w)) ⟹ (SUP a. p a) ≤ lfp f"
  apply (rule fp_wf_induction, simp_all)
  by (drule lfp_unfold, simp)

theorem lfp_wf_induction_b: "mono f ⟹ (∀ w . (p w) ≤ f (Sup_less p w)) ⟹ S ≤ (SUP a. p a) ⟹ S ≤ lfp f"
  apply (rule_tac y = "(SUP a. p a)" in order_trans)
   apply simp
    by (rule lfp_wf_induction, simp_all)

lemma [simp]: "mono S ⟹ mono (λX. if_stm b (S ∘ X) T)"
  apply (simp add: if_stm_def mono_def le_fun_def)
  apply auto
  by (metis assume_def sup_apply sup_bool_def)
    
definition  "mono_mono F = (mono F ∧ (∀ f . mono f ⟶ mono (F f)))"

theorem lfp_mono [simp]:
  "mono_mono F ⟹ mono (lfp F)"
  apply (simp add: mono_mono_def)
  apply (rule_tac f="F" and P = "mono" in lfp_ordinal_induct)
  apply (simp_all add: mono_def)
  apply (intro allI impI SUP_least)
  apply (rule_tac y = "f y" in order_trans)
  apply (auto intro: SUP_upper)
  done
    
lemma if_mono[simp]: "mono S ⟹ mono T ⟹ mono (if_stm b S T)"
  by (simp add: if_stm_def)

subsection‹Hoare Total Correctness Rules›

definition "Hoare (p::'a ⇒ bool) S (q::'b⇒bool) = (p ≤ S q)"

definition "post_fun (p:: 'a ⇒ bool) q = (if p ≤ q then ⊤ else ⊥)"

lemma post_mono [simp]: "mono (post_fun p :: (_::{order_bot,order_top}))"
  by (simp add: post_fun_def  mono_def le_fun_def)

lemma post_refin [simp]: "mono S ⟹ ((S p):: 'a ⇒ bool) ⊓ (post_fun p) x ≤ S x"
  apply (simp add: le_fun_def post_fun_def, safe)
  apply (drule_tac f = S in monoD, simp_all add: le_fun_def)
  by auto

lemma post_top [simp]: "post_fun p p = ⊤"
  by (simp add: post_fun_def)
 
  theorem hoare_refinement_post:
    "mono f ⟹  (Hoare x  f y) = ({.x.} o (post_fun y) ≤ f)"
    apply safe
    apply (simp_all add: Hoare_def)
    apply (simp_all add: le_fun_def)
     apply (simp add: assert_def, safe)
     apply (metis (mono_tags, lifting) bot_apply bot_bool_def mono_def post_fun_def predicate1D)
    by (simp add: assert_def)
  
  lemma assert_Sup_range: "{.Sup (range (p::'W ⇒ 'a ⇒ bool)).} = Sup(range (assert o p))"
    by (simp add: fun_eq_iff assert_def SUP_inf)

  lemma Sup_range_comp: "(Sup (range p)) o S = Sup (range (λ w . ((p w) o S)))"
    apply (auto simp add: fun_eq_iff image_def)
    by (rule_tac f = Sup in arg_cong, auto)

 
lemma Sup_less_comp: "(Sup_less P) w o S = Sup_less (λ w . ((P w) o S)) w"
  apply (simp add: Sup_less_def fun_eq_iff, safe)
  apply (rule antisym)
   apply (rule SUP_least, safe, simp)
    apply (rule_tac i = "λ x . f (S x)" in SUP_upper2, blast, simp)
   apply (rule SUP_least, safe, simp)
  by (rule_tac i = "P v" in SUP_upper2, auto)

  lemma assert_Sup: "{.Sup (X::('a⇒bool) set).} = Sup (assert ` X)"
    by (simp add: fun_eq_iff assert_def Sup_inf)

lemma Sup_less_assert: "Sup_less (λw. {. (p w)::'a⇒bool .}) w = {.Sup_less p w.}"
  apply (simp add: Sup_less_def assert_Sup image_def)
    by (rule_tac f = Sup in arg_cong, auto)


lemma [simp]: "Sup_less (λn x. t x = n) n = (λ x . (t x < n))"
  by (simp add: Sup_less_def, auto)
    
lemma [simp]: "Sup_less (λn. {.x. t x = n.} ∘ S) n = {.x. t x < n.} ∘ S"
  apply (simp add: Sup_less_comp [THEN sym])
  by (simp add: Sup_less_assert)

lemma [simp]: "(SUP a. {.x .t x = a.} ∘ S) = S"
  by (simp add: fun_eq_iff assert_def)

 
theorem hoare_fixpoint:
  "mono_mono F ⟹ 
     (∀ f w . mono f ⟶ (Hoare (Sup_less p w) f y ⟶ Hoare ((p w)::'a ⇒ bool) (F f) y)) ⟹ Hoare(Sup (range p)) (lfp F) y"
  apply (simp add: mono_mono_def hoare_refinement_post assert_Sup_range Sup_range_comp del: )
  apply (rule lfp_wf_induction)
  apply auto
  apply (simp add: Sup_less_comp [THEN sym])
  apply (simp add: Sup_less_assert)
  apply (drule_tac x = "{. Sup_less p w .} ∘ post_fun y" in spec, safe)
  apply simp_all
  apply (drule_tac x = "w" in spec, safe)
  by (simp add: le_fun_def)


  theorem hoare_sequential:
    "mono S ⟹ (Hoare p (S o T) r) = ( (∃ q. Hoare p S q ∧ Hoare q T r))"
    by (metis (no_types) Hoare_def monoD o_def order_refl order_trans)

  theorem hoare_choice:
    "Hoare  p (S ⊓ T) q = (Hoare p S q ∧ Hoare p T q)"
    by (simp_all add: Hoare_def inf_fun_def le_fun_def, auto)

  theorem hoare_assume:
    "(Hoare P [.R.] Q) = (P ⊓ R ≤ Q)"
    apply (simp add: Hoare_def assume_def)
    apply safe
    apply (case_tac "(inf P R) ≤ (inf (sup (- R) Q) R)")
    apply (simp add: inf_sup_distrib2 le_fun_def)
    apply (simp add: le_infI1)
    apply (case_tac "(sup (-R) (inf P R)) ≤ sup (- R) Q")
    by (simp add: sup_inf_distrib1 le_fun_def, auto)

  lemma hoare_if: "mono S ⟹ mono T ⟹ Hoare (p ⊓ b) S q ⟹ Hoare (p ⊓ -b) T q ⟹ Hoare p (if_stm b S T) q"
    apply (simp add: if_stm_def)
    apply (simp add: hoare_choice, safe)
    apply (simp_all add:  hoare_sequential)
    apply (rule_tac x = " (p ⊓ b)" in exI, simp)
    apply (simp add: hoare_assume) 
    apply (rule_tac x = " (p ⊓ -b)" in exI, simp)
    by (simp add: hoare_assume)
      
lemma [simp]: "mono x ⟹ mono_mono (λX . if_stm b (x ∘ X) Skip)"
  by (simp add: mono_mono_def)


  lemma hoare_while:
      "mono x ⟹ (∀ w . Hoare ((p w) ⊓ b) x (Sup_less p w)) ⟹  Hoare  (Sup (range p)) (while_stm b x) ((Sup (range p)) ⊓ -b)"
    apply (cut_tac y = " ((SUP x. p x) ⊓ - b)" and p = p and F = "λ X . if_stm b (x o X) Skip" in hoare_fixpoint, simp_all)
      apply safe
    apply (rule hoare_if, simp_all)
    apply (simp_all add:  hoare_sequential)
    apply (rule_tac x = " (Sup_less p w)" in exI, simp_all)
    apply (simp add: Hoare_def Skip_def, auto)
    by (simp add: while_stm_def)

  lemma hoare_prec_post: "mono S ⟹ p ≤ p' ⟹ q' ≤ q ⟹ Hoare p' S q' ⟹ Hoare p S q"
    apply (simp add: Hoare_def)
    apply (rule_tac y = p' in order_trans, simp_all)
    apply (rule_tac y = "S q'" in order_trans, simp_all)
    using monoD by auto

  lemma [simp]: "mono x ⟹  mono (while_stm b x)"
    by (simp add: while_stm_def)

  lemma hoare_while_a:
    "mono x ⟹ (∀ w . Hoare ((p w) ⊓ b) x (Sup_less p w)) ⟹ p' ≤  (Sup (range p)) ⟹ ((Sup (range p)) ⊓ -b) ≤ q 
      ⟹  Hoare p' (while_stm b x) q"
    apply (rule hoare_prec_post, simp_all)
    by (drule hoare_while, simp_all)

  lemma hoare_update: "p ≤ q o f ⟹ Hoare p [-f-] q"
    by (simp add: Hoare_def update_def demonic_def le_fun_def)

  lemma hoare_demonic: "(⋀ x y . p x ⟹ r x y ⟹ q y) ⟹ Hoare p [:r:] q"
    by (simp add: Hoare_def demonic_def le_fun_def)
      
lemma refinement_hoare: "S ≤ T ⟹ Hoare p S q ⟹ Hoare p T q"
  by (simp add: Hoare_def le_fun_def)
 
lemma refinement_hoare_iff: "(S ≤ T) = (∀ p q . Hoare p S (q) ⟶ Hoare p T q)"
  apply safe
   apply (rule refinement_hoare, simp_all)
  by (simp add: Hoare_def le_fun_def, auto)
    
subsection‹Data Refinement›
  
lemma data_refinement: "mono S' ⟹ (∀ x a . ∃ u . R x a u) ⟹
    {:x, a ↝ x', u . x = x' ∧ R x a u:} o S ≤ S' o {:y, b ↝ y', v . y = y' ∧ R' y b v:} ⟹ 
    [:x ↝ x', u . x = x':] o S o [:y, v ↝ y' . y = y' :] 
    ≤ [:x ↝ x', a . x = x':] o S' o [:y, b ↝ y' . y = y' :]"
proof (simp add: fun_eq_iff demonic_def le_fun_def, safe)
  fix x xa b
  assume A: "∀x a. ∃u. R x a u"
  assume B: "∀b. S ([: λ(y, v). (=) y :] x) (xa, b)"
  assume "∀x a b. {:(x, a) ↝ (x', u).x = x' ∧ R x a u:} (S x) (a, b) ⟶
                      S' ({:(y, b) ↝ (y', v).y = y' ∧ R' y b v:} x) (a, b)"
      
  from this have C: "{:(x, a) ↝ (x', u).x = x' ∧ R x a u:} (S ([: λ(y, v). (=) y :] x)) (xa, b) ⟹
                      S' ({:(y, b) ↝ (y', v).y = y' ∧ R' y b v:} ([: λ(y, v). (=) y :] x)) (xa, b)"
        
    by simp
  from A obtain u where "R xa b u"
    by blast
    
  from this and B have "{:(x, a) ↝ (x', u).x = x' ∧ R x a u:} (S ([: λ(y, v). (=) y :] x)) (xa, b)"
    apply (simp add: angelic_def fun_eq_iff)
    by blast
      
  from this and C have D: "S' ({:(y, b) ↝ (y', v).y = y' ∧ R' y b v:} ([: λ(y, v). (=) y :] x)) (xa, b)"
    by simp
      
  have [simp]: "⋀ s t . {:(y, b) ↝ (y', v).y = y' ∧ R' y b v:} ([: λ(y, v). (=) y :] x) (s,t) 
    ⟹ [: λ(y, b). (=) y :] x (s, t)"
    by (simp add: le_fun_def demonic_def angelic_def fun_eq_iff)
        
  assume "mono S'"
  from this have "S' ({:(y, b) ↝ (y', v).y = y' ∧ R' y b v:} ([: λ(y, v). (=) y :] x)) ≤ S' ([: λ(y, b). (=) y :] x)"
    by (rule monoD, simp add: le_fun_def)
    
  from D and this show "S' ([: λ(y, b). (=) y :] x) (xa, b)"
    by (simp add: le_fun_def)
qed

lemma mono_update[simp]: "mono [- f -]"
  by (simp add: update_def)
  
end