Theory utp_theory

section ‹ UTP Theories ›

theory utp_theory
imports utp_rel_laws
begin

text ‹ Here, we mechanise a representation of UTP theories using locales~\<^cite>‹"Ballarin06"›. We also
  link them to the HOL-Algebra library~\<^cite>‹"Ballarin17"›, which allows us to import properties from 
  complete lattices and Galois connections. ›

subsection ‹ Complete lattice of predicates ›

definition upred_lattice :: "('α upred) gorder" (‹𝒫›) where
"upred_lattice = ⦇ carrier = UNIV, eq = (=), le = (⊑) ⦈"

text ‹ @{term "𝒫"} is the complete lattice of alphabetised predicates. All other theories will
  be defined relative to it. ›

interpretation upred_lattice: complete_lattice 𝒫
proof (unfold_locales, simp_all add: upred_lattice_def)
  fix A :: "'α upred set"
  show "∃s. is_lub ⦇carrier = UNIV, eq = (=), le = (⊑)⦈ s A"
    apply (rule_tac x="⨆ A" in exI)
    apply (rule least_UpperI)
       apply (auto intro: Inf_greatest simp add: Inf_lower Upper_def)
    done
  show "∃i. is_glb ⦇carrier = UNIV, eq = (=), le = (⊑)⦈ i A"
    apply (rule_tac x="⨅ A" in exI)
    apply (rule greatest_LowerI)
       apply (auto intro: Sup_least simp add: Sup_upper Lower_def)
    done
qed

lemma upred_weak_complete_lattice [simp]: "weak_complete_lattice 𝒫"
  by (simp add: upred_lattice.weak.weak_complete_lattice_axioms)

lemma upred_lattice_eq [simp]:
  "(.=⇘𝒫⇙) = (=)"
  by (simp add: upred_lattice_def)

lemma upred_lattice_le [simp]:
  "le 𝒫 P Q = (P ⊑ Q)"
  by (simp add: upred_lattice_def)

lemma upred_lattice_carrier [simp]:
  "carrier 𝒫 = UNIV"
  by (simp add: upred_lattice_def)

lemma Healthy_fixed_points [simp]: "fps 𝒫 H = ⟦H⟧⇩H"
  by (simp add: fps_def upred_lattice_def Healthy_def)
    
lemma upred_lattice_Idempotent [simp]: "Idem⇘𝒫⇙ H = Idempotent H"
  using upred_lattice.weak_partial_order_axioms by (auto simp add: idempotent_def Idempotent_def)

lemma upred_lattice_Monotonic [simp]: "Mono⇘𝒫⇙ H = Monotonic H"
  using upred_lattice.weak_partial_order_axioms by (auto simp add: isotone_def mono_def)
    
subsection ‹ UTP theories hierarchy ›

definition utp_order :: "('α × 'α) health ⇒ 'α hrel gorder" where
"utp_order H = ⦇ carrier = {P. P is H}, eq = (=), le = (⊑) ⦈"

text ‹ Constant @{term utp_order} obtains the order structure associated with a UTP theory.
  Its carrier is the set of healthy predicates, equality is HOL equality, and the order is
  refinement. ›

lemma utp_order_carrier [simp]:
  "carrier (utp_order H) = ⟦H⟧⇩H"
  by (simp add: utp_order_def)

lemma utp_order_eq [simp]:
  "eq (utp_order T) = (=)"
  by (simp add: utp_order_def)

lemma utp_order_le [simp]:
  "le (utp_order T) = (⊑)"
  by (simp add: utp_order_def)

lemma utp_partial_order: "partial_order (utp_order T)"
  by (unfold_locales, simp_all add: utp_order_def)

lemma utp_weak_partial_order: "weak_partial_order (utp_order T)"
  by (unfold_locales, simp_all add: utp_order_def)

lemma mono_Monotone_utp_order:
  "mono f ⟹ Monotone (utp_order T) f"
  apply (auto simp add: isotone_def)
   apply (metis partial_order_def utp_partial_order)
  apply (metis monoD)
  done

lemma isotone_utp_orderI: "Monotonic H ⟹ isotone (utp_order X) (utp_order Y) H"
  by (auto simp add: mono_def isotone_def utp_weak_partial_order)

lemma Mono_utp_orderI:
  "⟦ ⋀ P Q. ⟦ P ⊑ Q; P is H; Q is H ⟧ ⟹ F(P) ⊑ F(Q) ⟧ ⟹ Mono⇘utp_order H⇙ F"
  by (auto simp add: isotone_def utp_weak_partial_order)

text ‹ The UTP order can equivalently be characterised as the fixed point lattice, @{const fpl}. ›

lemma utp_order_fpl: "utp_order H = fpl 𝒫 H"
  by (auto simp add: utp_order_def upred_lattice_def fps_def Healthy_def)

subsection ‹ UTP theory hierarchy ›

text ‹ We next define a hierarchy of locales that characterise different classes of UTP theory.
  Minimally we require that a UTP theory's healthiness condition is idempotent. ›

locale utp_theory =
  fixes hcond :: "'α hrel ⇒ 'α hrel" (‹ℋ›)
  assumes HCond_Idem: "ℋ(ℋ(P)) = ℋ(P)"
begin

  abbreviation thy_order :: "'α hrel gorder" where
  "thy_order ≡ utp_order ℋ"

  lemma HCond_Idempotent [closure,intro]: "Idempotent ℋ"
    by (simp add: Idempotent_def HCond_Idem)

  sublocale utp_po: partial_order "utp_order ℋ"
    by (unfold_locales, simp_all add: utp_order_def)

  text ‹ We need to remove some transitivity rules to stop them being applied in calculations ›

  declare utp_po.trans [trans del]

end

locale utp_theory_lattice = utp_theory + 
  assumes uthy_lattice: "complete_lattice (utp_order ℋ)"
begin

sublocale complete_lattice "utp_order ℋ"
  by (simp add: uthy_lattice)

declare top_closed [simp del]
declare bottom_closed [simp del]

text ‹ The healthiness conditions of a UTP theory lattice form a complete lattice, and allows us to make
  use of complete lattice results from HOL-Algebra~\<^cite>‹"Ballarin17"›, such as the Knaster-Tarski theorem. We can also
  retrieve lattice operators as below. ›

abbreviation utp_top (‹❙⊤›)
where "utp_top ≡ top (utp_order ℋ)"

abbreviation utp_bottom (‹❙⊥›)
where "utp_bottom ≡ bottom (utp_order ℋ)"

abbreviation utp_join (infixl ‹❙⊔› 65) where
"utp_join ≡ join (utp_order ℋ)"

abbreviation utp_meet (infixl ‹❙⊓› 70) where
"utp_meet ≡ meet (utp_order ℋ)"

abbreviation utp_sup (‹❙⨆_› [90] 90) where
"utp_sup ≡ Lattice.sup (utp_order ℋ)"

abbreviation utp_inf (‹❙⨅_› [90] 90) where
"utp_inf ≡ Lattice.inf (utp_order ℋ)"

abbreviation utp_gfp (‹❙ν›) where
"utp_gfp ≡ GREATEST_FP (utp_order ℋ)"

abbreviation utp_lfp (‹❙μ›) where
"utp_lfp ≡ LEAST_FP (utp_order ℋ)"

end

syntax
  "_tmu" :: "logic ⇒ pttrn ⇒ logic ⇒ logic" (‹❙μı _ ∙ _› [0, 10] 10)
  "_tnu" :: "logic ⇒ pttrn ⇒ logic ⇒ logic" (‹❙νı _ ∙ _› [0, 10] 10)

syntax_consts
  "_tmu" == LEAST_FP and
  "_tnu" == GREATEST_FP

notation gfp (‹μ›)
notation lfp (‹ν›)

translations
  "❙μ⇘H⇙ X ∙ P" == "CONST LEAST_FP (CONST utp_order H) (λ X. P)"  
  "❙ν⇘H⇙ X ∙ P" == "CONST GREATEST_FP (CONST utp_order H) (λ X. P)"

lemma upred_lattice_inf:
  "Lattice.inf 𝒫 A = ⨅ A"
  by (metis Sup_least Sup_upper UNIV_I antisym_conv subsetI upred_lattice.weak.inf_greatest upred_lattice.weak.inf_lower upred_lattice_carrier upred_lattice_le)

text ‹ We can then derive a number of properties about these operators, as below. ›

context utp_theory_lattice
begin

  lemma LFP_healthy_comp: "❙μ F = ❙μ (F ∘ ℋ)"
  proof -
    have "{P. (P is ℋ) ∧ F P ⊑ P} = {P. (P is ℋ) ∧ F (ℋ P) ⊑ P}"
      by (auto simp add: Healthy_def)
    thus ?thesis
      by (simp add: LEAST_FP_def)
  qed

  lemma GFP_healthy_comp: "❙ν F = ❙ν (F ∘ ℋ)"
  proof -
    have "{P. (P is ℋ) ∧ P ⊑ F P} = {P. (P is ℋ) ∧ P ⊑ F (ℋ P)}"
      by (auto simp add: Healthy_def)
    thus ?thesis
      by (simp add: GREATEST_FP_def)
  qed

  lemma top_healthy [closure]: "❙⊤ is ℋ"
    using weak.top_closed by auto

  lemma bottom_healthy [closure]: "❙⊥ is ℋ"
    using weak.bottom_closed by auto

  lemma utp_top: "P is ℋ ⟹ P ⊑ ❙⊤"
    using weak.top_higher by auto

  lemma utp_bottom: "P is ℋ ⟹ ❙⊥ ⊑ P"
    using weak.bottom_lower by auto

end

lemma upred_top: "⊤⇘𝒫⇙ = false"
  using ball_UNIV greatest_def by fastforce

lemma upred_bottom: "⊥⇘𝒫⇙ = true"
  by fastforce

text ‹ One way of obtaining a complete lattice is showing that the healthiness conditions
  are monotone, which the below locale characterises. ›

locale utp_theory_mono = utp_theory +
  assumes HCond_Mono [closure,intro]: "Monotonic ℋ"

sublocale utp_theory_mono ⊆ utp_theory_lattice
proof -
  interpret weak_complete_lattice "fpl 𝒫 ℋ"
    by (rule Knaster_Tarski, auto)

  have "complete_lattice (fpl 𝒫 ℋ)"
    by (unfold_locales, simp add: fps_def sup_exists, (blast intro: sup_exists inf_exists)+)

  hence "complete_lattice (utp_order ℋ)"
    by (simp add: utp_order_def, simp add: upred_lattice_def)

  thus "utp_theory_lattice ℋ"
    by (simp add: utp_theory_axioms utp_theory_lattice.intro utp_theory_lattice_axioms.intro)
qed

text ‹ In a monotone theory, the top and bottom can always be obtained by applying the healthiness
  condition to the predicate top and bottom, respectively. ›

context utp_theory_mono
begin

lemma healthy_top: "❙⊤ = ℋ(false)"
proof -
  have "❙⊤ = ⊤⇘fpl 𝒫 ℋ⇙"
    by (simp add: utp_order_fpl)
  also have "... = ℋ ⊤⇘𝒫⇙"
    using Knaster_Tarski_idem_extremes(1)[of 𝒫 ℋ]
    by (simp add: HCond_Idempotent HCond_Mono)
  also have "... = ℋ false"
    by (simp add: upred_top)
  finally show ?thesis .
qed

lemma healthy_bottom: "❙⊥ = ℋ(true)"
proof -
  have "❙⊥ = ⊥⇘fpl 𝒫 ℋ⇙"
    by (simp add: utp_order_fpl)
  also have "... = ℋ ⊥⇘𝒫⇙"
    using Knaster_Tarski_idem_extremes(2)[of 𝒫 ℋ]
    by (simp add: HCond_Idempotent HCond_Mono)
  also have "... = ℋ true"
    by (simp add: upred_bottom)
   finally show ?thesis .
qed

lemma healthy_inf:
  assumes "A ⊆ ⟦ℋ⟧⇩H"
  shows "❙⨅ A = ℋ (⨅ A)"
  using Knaster_Tarski_idem_inf_eq[OF upred_weak_complete_lattice, of "ℋ"]
  by (simp, metis HCond_Idempotent HCond_Mono assms partial_object.simps(3) upred_lattice_def upred_lattice_inf utp_order_def)

end

locale utp_theory_continuous = utp_theory +
  assumes HCond_Cont [closure,intro]: "Continuous ℋ"

sublocale utp_theory_continuous ⊆ utp_theory_mono
proof
  show "Monotonic ℋ"
    by (simp add: Continuous_Monotonic HCond_Cont)
qed

context utp_theory_continuous
begin

  lemma healthy_inf_cont:
    assumes "A ⊆ ⟦ℋ⟧⇩H" "A ≠ {}"
    shows "❙⨅ A = ⨅ A"
  proof -
    have "❙⨅ A = ⨅ (ℋ`A)"
      using Continuous_def HCond_Cont assms(1) assms(2) healthy_inf by auto
    also have "... = ⨅ A"
      by (unfold Healthy_carrier_image[OF assms(1)], simp)
    finally show ?thesis .
  qed

  lemma healthy_inf_def:
    assumes "A ⊆ ⟦ℋ⟧⇩H"
    shows "❙⨅ A = (if (A = {}) then ❙⊤ else (⨅ A))"
    using assms healthy_inf_cont weak.weak_inf_empty by auto

  lemma healthy_meet_cont:
    assumes "P is ℋ" "Q is ℋ"
    shows "P ❙⊓ Q = P ⊓ Q"
    using healthy_inf_cont[of "{P, Q}"] assms
    by (simp add: Healthy_if meet_def)

  lemma meet_is_healthy [closure]:
    assumes "P is ℋ" "Q is ℋ"
    shows "P ⊓ Q is ℋ"
    by (metis Continuous_Disjunctous Disjunctuous_def HCond_Cont Healthy_def' assms(1) assms(2))

  lemma meet_bottom [simp]:
    assumes "P is ℋ"
    shows "P ⊓ ❙⊥ = ❙⊥"
      by (simp add: assms semilattice_sup_class.sup_absorb2 utp_bottom)

  lemma meet_top [simp]:
    assumes "P is ℋ"
    shows "P ⊓ ❙⊤ = P"
      by (simp add: assms semilattice_sup_class.sup_absorb1 utp_top)

  text ‹ The UTP theory lfp operator can be rewritten to the alphabetised predicate lfp when
    in a continuous context. ›

  theorem utp_lfp_def:
    assumes "Monotonic F" "F ∈ ⟦ℋ⟧⇩H → ⟦ℋ⟧⇩H"
    shows "❙μ F = (μ X ∙ F(ℋ(X)))"
  proof (rule antisym)
    have ne: "{P. (P is ℋ) ∧ F P ⊑ P} ≠ {}"
    proof -
      have "F ❙⊤ ⊑ ❙⊤"
        using assms(2) utp_top weak.top_closed by force
      thus ?thesis
        by (auto, rule_tac x="❙⊤" in exI, auto simp add: top_healthy)
    qed
    show "❙μ F ⊑ (μ X ∙ F (ℋ X))"
    proof -
      have "⨅{P. (P is ℋ) ∧ F(P) ⊑ P} ⊑ ⨅{P. F(ℋ(P)) ⊑ P}"
      proof -
        have 1: "⋀ P. F(ℋ(P)) = ℋ(F(ℋ(P)))"
          by (metis HCond_Idem Healthy_def assms(2) funcset_mem mem_Collect_eq)
        show ?thesis
        proof (rule Sup_least, auto)
          fix P
          assume a: "F (ℋ P) ⊑ P"
          hence F: "(F (ℋ P)) ⊑ (ℋ P)"
            by (metis 1 HCond_Mono mono_def)
          show "⨅{P. (P is ℋ) ∧ F P ⊑ P} ⊑ P"
          proof (rule Sup_upper2[of "F (ℋ P)"])
            show "F (ℋ P) ∈ {P. (P is ℋ) ∧ F P ⊑ P}"
            proof (auto)
              show "F (ℋ P) is ℋ"
                by (metis 1 Healthy_def)
              show "F (F (ℋ P)) ⊑ F (ℋ P)"
                using F mono_def assms(1) by blast
            qed
            show "F (ℋ P) ⊑ P"
              by (simp add: a)
          qed
        qed
      qed

      with ne show ?thesis
        by (simp add: LEAST_FP_def gfp_def, subst healthy_inf_cont, auto simp add: lfp_def)
    qed
    from ne show "(μ X ∙ F (ℋ X)) ⊑ ❙μ F"
      apply (simp add: LEAST_FP_def gfp_def, subst healthy_inf_cont, auto simp add: lfp_def)
      apply (rule Sup_least)
      apply (auto simp add: Healthy_def Sup_upper)
      done
  qed

  lemma UINF_ind_Healthy [closure]:
    assumes "⋀ i. P(i) is ℋ"
    shows "(⨅ i ∙ P(i)) is ℋ"
    by (simp add: closure assms)

end

text ‹ In another direction, we can also characterise UTP theories that are relational. Minimally
  this requires that the healthiness condition is closed under sequential composition. ›

locale utp_theory_rel =
  utp_theory +
  assumes Healthy_Sequence [closure]: "⟦ P is ℋ; Q is ℋ ⟧ ⟹ (P ;; Q) is ℋ"
begin

lemma upower_Suc_Healthy [closure]:
  assumes "P is ℋ"
  shows "P ❙^ Suc n is ℋ"
  by (induct n, simp_all add: closure assms upred_semiring.power_Suc)

end

locale utp_theory_cont_rel = utp_theory_rel + utp_theory_continuous
begin

  lemma seq_cont_Sup_distl:
    assumes "P is ℋ" "A ⊆ ⟦ℋ⟧⇩H" "A ≠ {}"
    shows "P ;; (❙⨅ A) = ❙⨅ {P ;; Q | Q. Q ∈ A }"
  proof -
    have "{P ;; Q | Q. Q ∈ A } ⊆ ⟦ℋ⟧⇩H"
      using Healthy_Sequence assms(1) assms(2) by (auto)
    thus ?thesis
      by (simp add: healthy_inf_cont seq_Sup_distl setcompr_eq_image assms)
  qed

  lemma seq_cont_Sup_distr:
    assumes "Q is ℋ" "A ⊆ ⟦ℋ⟧⇩H" "A ≠ {}"
    shows "(❙⨅ A) ;; Q = ❙⨅ {P ;; Q | P. P ∈ A }"
  proof -
    have "{P ;; Q | P. P ∈ A } ⊆ ⟦ℋ⟧⇩H"
      using Healthy_Sequence assms(1) assms(2) by (auto)
    thus ?thesis
      by (simp add: healthy_inf_cont seq_Sup_distr setcompr_eq_image assms)
  qed

  lemma uplus_healthy [closure]:
    assumes "P is ℋ"  
    shows "P⇧+ is ℋ"
    by (simp add: uplus_power_def closure assms)

end

text ‹ There also exist UTP theories with units. Not all theories have both a left and a right unit 
  (e.g. H1-H2 designs) and so we split up the locale into two cases. ›

locale utp_theory_units =
  utp_theory_rel +
  fixes utp_unit (‹ℐℐ›)
  assumes Healthy_Unit [closure]: "ℐℐ is ℋ"
begin

text ‹ We can characterise the theory Kleene star by lifting the relational one. ›

definition utp_star (‹_❙⋆› [999] 999) where
[upred_defs]: "utp_star P = (P⇧⋆ ;; ℐℐ)"

text ‹ We can then characterise tests as refinements of units. ›

definition utp_test :: "'a hrel ⇒ bool" where
[upred_defs]: "utp_test b = (ℐℐ ⊑ b)"

end

locale utp_theory_left_unital =
  utp_theory_units +
  assumes Unit_Left: "P is ℋ ⟹ (ℐℐ ;; P) = P"

locale utp_theory_right_unital =
  utp_theory_units +
  assumes Unit_Right: "P is ℋ ⟹ (P ;; ℐℐ) = P"

locale utp_theory_unital =
  utp_theory_left_unital + utp_theory_right_unital
begin

lemma Unit_self [simp]:
  "ℐℐ ;; ℐℐ = ℐℐ"
  by (simp add: Healthy_Unit Unit_Right)

lemma utest_intro:
  "ℐℐ ⊑ P ⟹ utp_test P"
  by (simp add: utp_test_def)

lemma utest_Unit [closure]:
  "utp_test ℐℐ"
  by (simp add: utp_test_def)

end

locale utp_theory_mono_unital = utp_theory_unital + utp_theory_mono
begin

lemma utest_Top [closure]: "utp_test ❙⊤"
  by (simp add: Healthy_Unit utp_test_def utp_top)

end

locale utp_theory_cont_unital = utp_theory_cont_rel + utp_theory_unital

sublocale utp_theory_cont_unital ⊆ utp_theory_mono_unital
  by (simp add: utp_theory_mono_axioms utp_theory_mono_unital_def utp_theory_unital_axioms)

locale utp_theory_unital_zerol =
  utp_theory_unital +
  utp_theory_lattice +
  assumes Top_Left_Zero: "P is ℋ ⟹ ❙⊤ ;; P = ❙⊤"

locale utp_theory_cont_unital_zerol =
  utp_theory_cont_unital + utp_theory_unital_zerol
begin
  
lemma Top_test_Right_Zero:
  assumes "b is ℋ" "utp_test b"
  shows "b ;; ❙⊤ = ❙⊤"
proof -
  have "b ⊓ ℐℐ = ℐℐ"
    by (meson assms(2) semilattice_sup_class.le_iff_sup utp_test_def)
  then show ?thesis
    by (metis (no_types) Top_Left_Zero Unit_Left assms(1) meet_top top_healthy upred_semiring.distrib_right)
qed

end

subsection ‹ Theory of relations ›

interpretation rel_theory: utp_theory_mono_unital id skip_r
  rewrites "rel_theory.utp_top = false"
  and "rel_theory.utp_bottom = true"
  and "carrier (utp_order id) = UNIV"
  and "(P is id) = True"
proof -
  show "utp_theory_mono_unital id II"
    by (unfold_locales, simp_all add: Healthy_def)
  then interpret utp_theory_mono_unital id skip_r
    by simp
  show "utp_top = false" "utp_bottom = true"
    by (simp_all add: healthy_top healthy_bottom)
  show "carrier (utp_order id) = UNIV" "(P is id) = True"
    by (auto simp add: utp_order_def Healthy_def)
qed

thm rel_theory.GFP_unfold

subsection ‹ Theory links ›

text ‹ We can also describe links between theories, such a Galois connections and retractions,
  using the following notation. ›

definition mk_conn (‹_ ⇐⟨_,_⟩⇒ _› [90,0,0,91] 91) where
"H1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H2 ≡ ⦇ orderA = utp_order H1, orderB = utp_order H2, lower = ℋ⇩2, upper = ℋ⇩1 ⦈"

lemma mk_conn_orderA [simp]: "𝒳⇘H1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H2⇙ = utp_order H1"
  by (simp add:mk_conn_def)

lemma mk_conn_orderB [simp]: "𝒴⇘H1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H2⇙ = utp_order H2"
  by (simp add:mk_conn_def)

lemma mk_conn_lower [simp]:  "π⇩*⇘H1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H2⇙ = ℋ⇩1"
  by (simp add: mk_conn_def)

lemma mk_conn_upper [simp]:  "π⇧*⇘H1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H2⇙ = ℋ⇩2"
  by (simp add: mk_conn_def)

lemma galois_comp: "(H⇩2 ⇐⟨ℋ⇩3,ℋ⇩4⟩⇒ H⇩3) ∘⇩g (H⇩1 ⇐⟨ℋ⇩1,ℋ⇩2⟩⇒ H⇩2) = H⇩1 ⇐⟨ℋ⇩1∘ℋ⇩3,ℋ⇩4∘ℋ⇩2⟩⇒ H⇩3"
  by (simp add: comp_galcon_def mk_conn_def)

text ‹ Example Galois connection / retract: Existential quantification ›

lemma Idempotent_ex: "mwb_lens x ⟹ Idempotent (ex x)"
  by (simp add: Idempotent_def exists_twice)

lemma Monotonic_ex: "mwb_lens x ⟹ Monotonic (ex x)"
  by (simp add: mono_def ex_mono)

lemma ex_closed_unrest:
  "vwb_lens x ⟹ ⟦ex x⟧⇩H = {P. x ♯ P}"
  by (simp add: Healthy_def unrest_as_exists)

text ‹ Any theory can be composed with an existential quantification to produce a Galois connection ›

theorem ex_retract:
  assumes "vwb_lens x" "Idempotent H" "ex x ∘ H = H ∘ ex x"
  shows "retract ((ex x ∘ H) ⇐⟨ex x, H⟩⇒ H)"
proof (unfold_locales, simp_all)
  show "H ∈ ⟦ex x ∘ H⟧⇩H → ⟦H⟧⇩H"
    using Healthy_Idempotent assms by blast
  from assms(1) assms(3)[THEN sym] show "ex x ∈ ⟦H⟧⇩H → ⟦ex x ∘ H⟧⇩H"
    by (simp add: Pi_iff Healthy_def fun_eq_iff exists_twice)
  fix P Q
  assume "P is (ex x ∘ H)" "Q is H"
  thus "(H P ⊑ Q) = (P ⊑ (∃ x ∙ Q))"
    by (metis (no_types, lifting) Healthy_Idempotent Healthy_if assms comp_apply dual_order.trans ex_weakens utp_pred_laws.ex_mono vwb_lens_wb)
next
  fix P
  assume "P is (ex x ∘ H)"
  thus "(∃ x ∙ H P) ⊑ P"
    by (simp add: Healthy_def)
qed

corollary ex_retract_id:
  assumes "vwb_lens x"
  shows "retract (ex x ⇐⟨ex x, id⟩⇒ id)"
  using assms ex_retract[where H="id"] by (auto)
end