section ‹ Healthiness Conditions ›

theory utp_healthy
  imports utp_pred_laws
begin

subsection ‹ Main Definitions ›

text ‹ We collect closure laws for healthiness conditions in the following theorem attribute. ›

named_theorems closure
  
type_synonym 'α health = "'α upred → 'α upred"

text ‹ A predicate $P$ is healthy, under healthiness function $H$, if $P$ is a fixed-point of $H$. ›

definition Healthy :: "'α upred → 'α health → bool" (infix ‹is› 30)
where "P is H ≡ (H P = P)"

lemma Healthy_def': "P is H ⟷ (H P = P)"
  unfolding Healthy_def by auto

lemma Healthy_if: "P is H ==> (H P = P)"
  unfolding Healthy_def by auto

lemma Healthy_intro: "H(P) = P ==> P is H"
  by (simp add: Healthy_def)
    
declare Healthy_def' [upred_defs]

abbreviation Healthy_carrier :: "'α health → 'α upred set" (‹[_]_H›)
where "[H]_H ≡ {P. P is H}"

lemma Healthy_carrier_image:
  "A ⊆ [H]_H ==> H ` A = A"
    by (auto simp add: image_def, (metis Healthy_if mem_Collect_eq subsetCE)+)

lemma Healthy_carrier_Collect: "A ⊆ [H]_H ==> A = {H(P) | P. P ∈ A}"
  by (simp add: Healthy_carrier_image Setcompr_eq_image)

lemma Healthy_func:
  "[ F ∈ [H₁]_H → [H₂]_H; P is H₁ ] ==> H₂(F(P)) = F(P)"
  using Healthy_if by blast

lemma Healthy_comp:
  "[ P is H₁; P is H₂ ] ==> P is H₁ ∘ H₂"
  by (simp add: Healthy_def)
    
lemma Healthy_apply_closed:
  assumes "F ∈ [H]_H → [H]_H" "P is H"
  shows "F(P) is H"
  using assms(1) assms(2) by auto

lemma Healthy_set_image_member:
  "[ P ∈ F ` A; ∧ x. F x is H ] ==> P is H"
  by blast

lemma Healthy_case_prod [closure]: 
  "[ ∧ x y. P x y is H ] ==> case_prod P v is H"
  by (simp add: prod.case_eq_if)

lemma Healthy_SUPREMUM:
  "A ⊆ [H]_H ==> Sup (H ` A) = ⊓ A"
  by (drule Healthy_carrier_image, presburger)

lemma Healthy_INFIMUM:
  "A ⊆ [H]_H ==> Inf (H ` A) = ⊔ A"
  by (drule Healthy_carrier_image, presburger)

lemma Healthy_nu [closure]:
  assumes "mono F" "F ∈ [id]_H → [H]_H"
  shows "ν F is H"
  by (metis (mono_tags) Healthy_def Healthy_func assms eq_id_iff lfp_unfold)

lemma Healthy_mu [closure]:
  assumes "mono F" "F ∈ [id]_H → [H]_H"
  shows "μ F is H"
  by (metis (mono_tags) Healthy_def Healthy_func assms eq_id_iff gfp_unfold)

lemma Healthy_subset_member: "[ A ⊆ [H]_H; P ∈ A ] ==> H(P) = P"
  by (meson Ball_Collect Healthy_if)

lemma is_Healthy_subset_member: "[ A ⊆ [H]_H; P ∈ A ] ==> P is H"
  by blast

subsection ‹ Properties of Healthiness Conditions ›

definition Idempotent :: "'α health → bool" where
  "Idempotent(H) ⟷ (∀ P. H(H(P)) = H(P))"

abbreviation Monotonic :: "'α health → bool" where
  "Monotonic(H) ≡ mono H"

definition IMH :: "'α health → bool" where
  "IMH(H) ⟷ Idempotent(H) ∧ Monotonic(H)"

definition Antitone :: "'α health → bool" where
  "Antitone(H) ⟷ (∀ P Q. Q ⊑ P ⟶ (H(P) ⊑ H(Q)))"

definition Conjunctive :: "'α health → bool" where
  "Conjunctive(H) ⟷ (∃ Q. ∀ P. H(P) = (P ∧ Q))"

definition FunctionalConjunctive :: "'α health → bool" where
  "FunctionalConjunctive(H) ⟷ (∃ F. ∀ P. H(P) = (P ∧ F(P)) ∧ Monotonic(F))"

definition WeakConjunctive :: "'α health → bool" where
  "WeakConjunctive(H) ⟷ (∀ P. ∃ Q. H(P) = (P ∧ Q))"

definition Disjunctuous :: "'α health → bool" where
  [upred_defs]: "Disjunctuous H = (∀ P Q. H(P ⊓ Q) = (H(P) ⊓ H(Q)))"

definition Continuous :: "'α health → bool" where
  [upred_defs]: "Continuous H = (∀ A. A ≠ {} ⟶ H (⊓ A) = ⊓ (H ` A))"

lemma Healthy_Idempotent [closure]:
  "Idempotent H ==> H(P) is H"
  by (simp add: Healthy_def Idempotent_def)

lemma Healthy_range: "Idempotent H ==> range H = [H]_H"
  by (auto simp add: image_def Healthy_if Healthy_Idempotent, metis Healthy_if)

lemma Idempotent_id [simp]: "Idempotent id"
  by (simp add: Idempotent_def)

lemma Idempotent_comp [intro]:
  "[ Idempotent f; Idempotent g; f ∘ g = g ∘ f ] ==> Idempotent (f ∘ g)"
  by (auto simp add: Idempotent_def comp_def, metis)

lemma Idempotent_image: "Idempotent f ==> f ` f ` A = f ` A"
  by (metis (mono_tags, lifting) Idempotent_def image_cong image_image)

lemma Monotonic_id [simp]: "Monotonic id"
  by (simp add: monoI)

lemma Monotonic_id' [closure]: 
  "mono (λ X. X)" 
  by (simp add: monoI)
    
lemma Monotonic_const [closure]: 
  "Monotonic (λ x. c)"
  by (simp add: mono_def)
    
lemma Monotonic_comp [intro]:
  "[ Monotonic f; Monotonic g ] ==> Monotonic (f ∘ g)"
  by (simp add: mono_def)

lemma Monotonic_inf [closure]:
  assumes "Monotonic P" "Monotonic Q"
  shows "Monotonic (λ X. P(X) ⊓ Q(X))"
  using assms by (simp add: mono_def, rel_auto)

lemma Monotonic_cond [closure]:
  assumes "Monotonic P" "Monotonic Q"
  shows "Monotonic (λ X. P(X) ◃ b ▹ Q(X))"
  by (simp add: assms cond_monotonic)
    
lemma Conjuctive_Idempotent:
  "Conjunctive(H) ==> Idempotent(H)"
  by (auto simp add: Conjunctive_def Idempotent_def)

lemma Conjunctive_Monotonic:
  "Conjunctive(H) ==> Monotonic(H)"
  unfolding Conjunctive_def mono_def
  using dual_order.trans by fastforce

lemma Conjunctive_conj:
  assumes "Conjunctive(HC)"
  shows "HC(P ∧ Q) = (HC(P) ∧ Q)"
  using assms unfolding Conjunctive_def
  by (metis utp_pred_laws.inf.assoc utp_pred_laws.inf.commute)

lemma Conjunctive_distr_conj:
  assumes "Conjunctive(HC)"
  shows "HC(P ∧ Q) = (HC(P) ∧ HC(Q))"
  using assms unfolding Conjunctive_def
  by (metis Conjunctive_conj assms utp_pred_laws.inf.assoc utp_pred_laws.inf_right_idem)

lemma Conjunctive_distr_disj:
  assumes "Conjunctive(HC)"
  shows "HC(P ∨ Q) = (HC(P) ∨ HC(Q))"
  using assms unfolding Conjunctive_def
  using utp_pred_laws.inf_sup_distrib2 by fastforce

lemma Conjunctive_distr_cond:
  assumes "Conjunctive(HC)"
  shows "HC(P ◃ b ▹ Q) = (HC(P) ◃ b ▹ HC(Q))"
  using assms unfolding Conjunctive_def
  by (metis cond_conj_distr utp_pred_laws.inf_commute)

lemma FunctionalConjunctive_Monotonic:
  "FunctionalConjunctive(H) ==> Monotonic(H)"
  unfolding FunctionalConjunctive_def by (metis mono_def utp_pred_laws.inf_mono)

lemma WeakConjunctive_Refinement:
  assumes "WeakConjunctive(HC)"
  shows "P ⊑ HC(P)"
  using assms unfolding WeakConjunctive_def by (metis utp_pred_laws.inf.cobounded1)

lemma WeakCojunctive_Healthy_Refinement:
  assumes "WeakConjunctive(HC)" and "P is HC"
  shows "HC(P) ⊑ P"
  using assms unfolding WeakConjunctive_def Healthy_def by simp

lemma WeakConjunctive_implies_WeakConjunctive:
  "Conjunctive(H) ==> WeakConjunctive(H)"
  unfolding WeakConjunctive_def Conjunctive_def by pred_auto

declare Conjunctive_def [upred_defs]
declare mono_def [upred_defs]

lemma Disjunctuous_Monotonic: "Disjunctuous H ==> Monotonic H"
  by (metis Disjunctuous_def mono_def semilattice_sup_class.le_iff_sup)

lemma ContinuousD [dest]: "[ Continuous H; A ≠ {} ] ==> H (⊓ A) = (⊓ P∈A. H(P))"
  by (simp add: Continuous_def)

lemma Continuous_Disjunctous: "Continuous H ==> Disjunctuous H"
  apply (auto simp add: Continuous_def Disjunctuous_def)
  apply (rename_tac P Q)
  apply (drule_tac x="{P,Q}" in spec)
  apply (simp)
  done

lemma Continuous_Monotonic [closure]: "Continuous H ==> Monotonic H"
  by (simp add: Continuous_Disjunctous Disjunctuous_Monotonic)

lemma Continuous_comp [intro]:
  "[ Continuous f; Continuous g ] ==> Continuous (f ∘ g)"
  by (simp add: Continuous_def)

lemma Continuous_const [closure]: "Continuous (λ X. P)"
  by pred_auto

lemma Continuous_cond [closure]:
  assumes "Continuous F" "Continuous G"
  shows "Continuous (λ X. F(X) ◃ b ▹ G(X))"
  using assms by (pred_auto)

text ‹ Closure laws derived from continuity ›

lemma Sup_Continuous_closed [closure]:
  "[ Continuous H; ∧ i. i ∈ A ==> P(i) is H; A ≠ {} ] ==> (⊓ i∈A. P(i)) is H"
  by (drule ContinuousD[of H "P ` A"], simp add: UINF_mem_UNIV[THEN sym] UINF_as_Sup[THEN sym])
     (metis (no_types, lifting) Healthy_def' SUP_cong image_image)

lemma UINF_mem_Continuous_closed [closure]:
  "[ Continuous H; ∧ i. i ∈ A ==> P(i) is H; A ≠ {} ] ==> (⊓ i∈A ∙ P(i)) is H"
  by (simp add: Sup_Continuous_closed UINF_as_Sup_collect)

lemma UINF_mem_Continuous_closed_pair [closure]:
  assumes "Continuous H" "∧ i j. (i, j) ∈ A ==> P i j is H" "A ≠ {}"
  shows "(⊓ (i,j)∈A ∙ P i j) is H"
proof -
  have "(⊓ (i,j)∈A ∙ P i j) = (⊓ x∈A ∙ P (fst x) (snd x))"
    by (rel_auto)
  also have "... is H"
    by (metis (mono_tags) UINF_mem_Continuous_closed assms(1) assms(2) assms(3) prod.collapse)
  finally show ?thesis .
qed

lemma UINF_mem_Continuous_closed_triple [closure]:
  assumes "Continuous H" "∧ i j k. (i, j, k) ∈ A ==> P i j k is H" "A ≠ {}"
  shows "(⊓ (i,j,k)∈A ∙ P i j k) is H"
proof -
  have "(⊓ (i,j,k)∈A ∙ P i j k) = (⊓ x∈A ∙ P (fst x) (fst (snd x)) (snd (snd x)))"
    by (rel_auto)
  also have "... is H"
    by (metis (mono_tags) UINF_mem_Continuous_closed assms(1) assms(2) assms(3) prod.collapse)
  finally show ?thesis .
qed

lemma UINF_mem_Continuous_closed_quad [closure]:
  assumes "Continuous H" "∧ i j k l. (i, j, k, l) ∈ A ==> P i j k l is H" "A ≠ {}"
  shows "(⊓ (i,j,k,l)∈A ∙ P i j k l) is H"
proof -
  have "(⊓ (i,j,k,l)∈A ∙ P i j k l) = (⊓ x∈A ∙ P (fst x) (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))))"
    by (rel_auto)
  also have "... is H"
    by (metis (mono_tags) UINF_mem_Continuous_closed assms(1) assms(2) assms(3) prod.collapse)
  finally show ?thesis .
qed

lemma UINF_mem_Continuous_closed_quint [closure]:
  assumes "Continuous H" "∧ i j k l m. (i, j, k, l, m) ∈ A ==> P i j k l m is H" "A ≠ {}"
  shows "(⊓ (i,j,k,l,m)∈A ∙ P i j k l m) is H"
proof -
  have "(⊓ (i,j,k,l,m)∈A ∙ P i j k l m)
         = (⊓ x∈A ∙ P (fst x) (fst (snd x)) (fst (snd (snd x))) (fst (snd (snd (snd x)))) (snd (snd (snd (snd x)))))"
    by (rel_auto)
  also have "... is H"
    by (metis (mono_tags) UINF_mem_Continuous_closed assms(1) assms(2) assms(3) prod.collapse)
  finally show ?thesis .
qed

lemma UINF_ind_closed [closure]:
  assumes "Continuous H" "∧ i. P i = true" "∧ i. Q i is H"
  shows "UINF P Q is H"
proof -
  from assms(2) have "UINF P Q = (⊓ i ∙ Q i)"
    by (rel_auto)
  also have "... is H"
    using UINF_mem_Continuous_closed[of H UNIV P]
    by (simp add: Sup_Continuous_closed UINF_as_Sup_collect' assms)
  finally show ?thesis .
qed

text ‹ All continuous functions are also Scott-continuous ›

lemma sup_continuous_Continuous [closure]: "Continuous F ==> sup_continuous F"
  by (simp add: Continuous_def sup_continuous_def)

lemma USUP_healthy: "A ⊆ [H]_H ==> (⊔ P∈A ∙ F(P)) = (⊔ P∈A ∙ F(H(P)))"
  by (rule USUP_cong, simp add: Healthy_subset_member)

lemma UINF_healthy: "A ⊆ [H]_H ==> (⊓ P∈A ∙ F(P)) = (⊓ P∈A ∙ F(H(P)))"
  by (rule UINF_cong, simp add: Healthy_subset_member)
  
end