Quelle  utp_theory.thy

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" (‹P›) where
"upred_lattice = ( carrier = UNIV, eq = (=), le = (⊑) )"

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

interpretation upred_lattice: complete_lattice P
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 P"
  by (simp add: upred_lattice.weak.weak_complete_lattice_axioms)

lemma upred_lattice_eq [simp]:
  "(.=_<P>) = (=)"
  by (simp add: upred_lattice_def)

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

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

lemma Healthy_fixed_points [simp]: "fps P H = [H]_H"
  by (simp add: fps_def upred_lattice_def Healthy_def)
    
lemma upred_lattice_Idempotent [simp]: "Idem_<P> H = Idempotent H"
  using upred_lattice.weak_partial_order_axioms by (auto simp add: idempotent_def Idempotent_def)

lemma upred_lattice_Monotonic [simp]: "Mono_<P> 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 _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 P 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" (‹H›)
  assumes HCond_Idem: "H(H(P)) = H(P)"
begin

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

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

  sublocale utp_po: partial_order "utp_order H"
    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 H)"
begin

sublocale complete_lattice "utp_order H"
  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 H)"

abbreviation utp_bottom (‹\⊥›)
where "utp_bottom ≡ bottom (utp_order H)"

abbreviation utp_join (infixl ‹\⊔› 65) where
"utp_join ≡ join (utp_order H)"

abbreviation utp_meet (infixl ‹\⊓› 70) where
"utp_meet ≡ meet (utp_order H)"

abbreviation utp_sup (‹\⊔_› [90] 90) where
"utp_sup ≡ Lattice.sup (utp_order H)"

abbreviation utp_inf (‹\⊓_› [90] 90) where
"utp_inf ≡ Lattice.inf (utp_order H)"

abbreviation utp_gfp (‹\ν›) where
"utp_gfp ≡ GREATEST_FP (utp_order H)"

abbreviation utp_lfp (‹\μ›) where
"utp_lfp ≡ LEAST_FP (utp_order H)"

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
  "\<mu> X ∙ P" == "CONST LEAST_FP (CONST utp_order H) (λ X. P)"  
  "\<nu> X ∙ P" == "CONST GREATEST_FP (CONST utp_order H) (λ X. P)"

lemma upred_lattice_inf:
  "Lattice.inf P 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: "\<mu> F = \<mu> (F ∘ H)"
  proof -
    have "{P. (P is H) ∧ F P ⊑ P} = {P. (P is H) ∧ F (H P) ⊑ P}"
      by (auto simp add: Healthy_def)
    thus ?thesis
      by (simp add: LEAST_FP_def)
  qed

  lemma GFP_healthy_comp: "\<nu> F = \<nu> (F ∘ H)"
  proof -
    have "{P. (P is H) ∧ P ⊑ F P} = {P. (P is H) ∧ P ⊑ F (H P)}"
      by (auto simp add: Healthy_def)
    thus ?thesis
      by (simp add: GREATEST_FP_def)
  qed

  lemma top_healthy [closure]: "\<top> is H"
    using weak.top_closed by auto

  lemma bottom_healthy [closure]: "\<bottom> is H"
    using weak.bottom_closed by auto

  lemma utp_top: "P is H ==> P ⊑ \<top>"
    using weak.top_higher by auto

  lemma utp_bottom: "P is H ==> \<bottom> ⊑ P"
    using weak.bottom_lower by auto

end

lemma upred_top: "⊤_<P> = false"
  using ball_UNIV greatest_def by fastforce

lemma upred_bottom: "⊥_<P> = 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 H"

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

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

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

  thus "utp_theory_lattice H"
    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: "\<top> = H(false)"
proof -
  have "\<top> = ⊤ _{P H}"
    by (simp add: utp_order_fpl)
  also have "... = H ⊤_<P>"
    using Knaster_Tarski_idem_extremes(1)[of P H]
    by (simp add: HCond_Idempotent HCond_Mono)
  also have "... = H false"
    by (simp add: upred_top)
  finally show ?thesis .
qed

lemma healthy_bottom: "\<bottom> = H(true)"
proof -
  have "\<bottom> = ⊥ _{P H}"
    by (simp add: utp_order_fpl)
  also have "... = H ⊥_<P>"
    using Knaster_Tarski_idem_extremes(2)[of P H]
    by (simp add: HCond_Idempotent HCond_Mono)
  also have "... = H true"
    by (simp add: upred_bottom)
   finally show ?thesis .
qed

lemma healthy_inf:
  assumes "A ⊆ [H]_H"
  shows "\<Sqinter> A = H (⊓ A)"
  using Knaster_Tarski_idem_inf_eq[OF upred_weak_complete_lattice, of "H"]
  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 H"

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

context utp_theory_continuous
begin

  lemma healthy_inf_cont:
    assumes "A ⊆ [H]_H" "A ≠ {}"
    shows "\<Sqinter> A = ⊓ A"
  proof -
    have "\<Sqinter> A = ⊓ (H`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]_H"
    shows "\<Sqinter> A = (if (A = {}) then \<top> else (⊓ A))"
    using assms healthy_inf_cont weak.weak_inf_empty by auto

  lemma healthy_meet_cont:
    assumes "P is H" "Q is H"
    shows "P \<sqinter> 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 H" "Q is H"
    shows "P ⊓ Q is H"
    by (metis Continuous_Disjunctous Disjunctuous_def HCond_Cont Healthy_def' assms(1) assms(2))

  lemma meet_bottom [simp]:
    assumes "P is H"
    shows "P ⊓ \<bottom> = \<bottom>"
      by (simp add: assms semilattice_sup_class.sup_absorb2 utp_bottom)

  lemma meet_top [simp]:
    assumes "P is H"
    shows "P ⊓ \<top> = 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 → [H]_H"
    shows "\<mu> F = (μ X ∙ F(H(X)))"
  proof (rule antisym)
    have ne: "{P. (P is H) ∧ F P ⊑ P} ≠ {}"
    proof -
      have "F \<top> ⊑ \<top>"
        using assms(2) utp_top weak.top_closed by force
      thus ?thesis
        by (auto, rule_tac x="\<top>" in exI, auto simp add: top_healthy)
    qed
    show "\<mu> F ⊑ (μ X ∙ F (H X))"
    proof -
      have "⊓{P. (P is H) ∧ F(P) ⊑ P} ⊑ ⊓{P. F(H(P)) ⊑ P}"
      proof -
        have 1: "∧ P. F(H(P)) = H(F(H(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 (H P) ⊑ P"
          hence F: "(F (H P)) ⊑ (H P)"
            by (metis 1 HCond_Mono mono_def)
          show "⊓{P. (P is H) ∧ F P ⊑ P} ⊑ P"
          proof (rule Sup_upper2[of "F (H P)"])
            show "F (H P) ∈ {P. (P is H) ∧ F P ⊑ P}"
            proof (auto)
              show "F (H P) is H"
                by (metis 1 Healthy_def)
              show "F (F (H P)) ⊑ F (H P)"
                using F mono_def assms(1) by blast
            qed
            show "F (H 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 (H X)) ⊑ \<mu> 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 H"
    shows "(⊓ i ∙ P(i)) is H"
    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 H; Q is H ] ==> (P ;; Q) is H"
begin

lemma upower_Suc_Healthy [closure]:
  assumes "P is H"
  shows "P ^ Suc n is H"
  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 H" "A ⊆ [H]_H" "A ≠ {}"
    shows "P ;; (\<Sqinter> A) = \<Sqinter> {P ;; Q | Q. Q ∈ A }"
  proof -
    have "{P ;; Q | Q. Q ∈ A } ⊆ [H]_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 H" "A ⊆ [H]_H" "A ≠ {}"
    shows "(\<Sqinter> A) ;; Q = \<Sqinter> {P ;; Q | P. P ∈ A }"
  proof -
    have "{P ;; Q | P. P ∈ A } ⊆ [H]_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 H"  
    shows "P⁺ is H"
    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 (‹II›)
  assumes Healthy_Unit [closure]: "II is H"
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^\<star> ;; II)"

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

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

end

locale utp_theory_left_unital =
  utp_theory_units +
  assumes Unit_Left: "P is H ==> (II ;; P) = P"

locale utp_theory_right_unital =
  utp_theory_units +
  assumes Unit_Right: "P is H ==> (P ;; II) = P"

locale utp_theory_unital =
  utp_theory_left_unital + utp_theory_right_unital
begin

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

lemma utest_intro:
  "II ⊑ P ==> utp_test P"
  by (simp add: utp_test_def)

lemma utest_Unit [closure]:
  "utp_test II"
  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 \<top>"
  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 H ==> \<top> ;; P = \<top>"

locale utp_theory_cont_unital_zerol =
  utp_theory_cont_unital + utp_theory_unital_zerol
begin
  
lemma Top_test_Right_Zero:
  assumes "b is H" "utp_test b"
  shows "b ;; \<top> = \<top>"
proof -
  have "b ⊓ II = II"
    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 <==⟨H₁,H₂⟩==> H2 ≡ ( orderA = utp_order H1, orderB = utp_order H2, lower = H₂, upper = H₁ )"

lemma mk_conn_orderA [simp]: "X _{<==⟨H1,H2⟩==> H2} = utp_order H1"
  by (simp add:mk_conn_def)

lemma mk_conn_orderB [simp]: "Y _{<==⟨H1,H2⟩==> H2} = utp_order H2"
  by (simp add:mk_conn_def)

lemma mk_conn_lower [simp]:  "π_{* <==⟨H1,H2⟩==> H2} = H₁"
  by (simp add: mk_conn_def)

lemma mk_conn_upper [simp]:  "π^* _{<==⟨H1,H2⟩==> H2} = H₂"
  by (simp add: mk_conn_def)

lemma galois_comp: "(H₂ <==⟨H₃,H₄⟩==> H₃) ∘_g (H₁ <==⟨H₁,H₂⟩==> H₂) = H₁ <==⟨H₁∘H₃,H₄∘H₂⟩==> H₃"
  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