Theory Power_Allegories_Multirelations

section ‹Multirelational Properties of Power Allegories›

theory Power_Allegories_Multirelations

imports Multirelations_Basics

begin

text ‹We start with random little properties.›

lemma eta_s_id: "η = s_id"
  unfolding s_id_def eta_set by force

lemma Lambda_empty [simp]: "Λ {} = p_id"
  unfolding Lambda_def p_id_def by blast

lemma alpha_pid [simp]: "α p_id = {}"
  unfolding alpha_def epsiloff_def p_id_def by force


subsection ‹Peleg lifting›

definition plift :: "('a,'b) mrel ⇒ ('a set,'b set) rel" (‹_⇩*› [1000] 999) where
  "R⇩* = {(A,B). ∃f. (∀a ∈ A. (a,f(a)) ∈ R) ∧ B = ⋃(f ` A)}"

lemma pcomp_plift: "R ⋅ S = R ; S⇩*"
  unfolding s_prod_def plift_def relcomp_unfold by simp

lemma det_plift_klift: "deterministic R ⟹ R⇩* = (R)⇩𝒫"
  unfolding deterministic_set plift_def klift_set_var
  apply (simp add: set_eq_iff)
  apply safe
  by metis+

lemma plift_ext2 [simp]: "η ; R⇩* = R"
  by (metis eta_s_id pcomp_plift s_prod_idl)

lemma pliftext_3 [simp]: "η⇩* = Id"
  by (simp add: det_eta det_plift_klift)

lemma d_dom_plift: "(Dom R)⇩* = dom (R⇩*)"
  unfolding Dom_def dom_set plift_def
  apply clarsimp
  apply safe
  apply (metis (full_types) UN_singleton image_cong)
  by (metis UN_singleton)

lemma d_pid_plift: "(Dom R)⇩* ⊆ Id"
  by (metis d_dom_plift d_idem dom_subid inf.absorb_iff2)

lemma d_plift_sub: "A ⊆ B ⟹ (B,B) ∈ (Dom R)⇩* ⟹ (A,A) ∈ (Dom R)⇩*"
  by (smt (z3) Pair_inject UN_singleton Dom_def mem_Collect_eq plift_def split_conv subsetD)

lemma plift_empty: "({},A) ∈ R⇩* ⟷ A = {}"
  using plift_def by auto

lemma univ_plift_klift:
  assumes "univalent R"
  shows "R⇩* = (Dom R)⇩* ; (R)⇩𝒫"
proof -
  have "∀A B . (A,B) ∈ R⇩* ⟷ (A,B) ∈ (Dom R)⇩* ; (R)⇩𝒫"
  proof (intro allI, rule iffI)
    fix A B
    assume 1: "(A,B) ∈ R⇩*"
    hence "(A,B) ∈ (R)⇩𝒫"
      unfolding klift_set_var
      apply clarsimp
      by (smt (z3) Collect_cong Pair_inject Union_eq assms case_prodE image_iff mem_Collect_eq plift_def univalent_set)
    thus "(A,B) ∈ (Dom R)⇩* ; (R)⇩𝒫"
      using 1 d_dom_plift dom_set by fastforce
  next
    fix A B
    assume "(A,B) ∈ (Dom R)⇩* ; (R)⇩𝒫"
    from this obtain C where 2: "(A,C) ∈ (Dom R)⇩* ∧ (C,B) ∈ (R)⇩𝒫"
      by auto
    from this obtain f where 3: "(∀a ∈ A. (a,f(a)) ∈ Dom R) ∧ C = ⋃(f ` A)"
      by (smt (verit) Pair_inject case_prodE mem_Collect_eq plift_def)
    hence "∀a ∈ A . ∃D . (a,D) ∈ R"
      by (simp add: Dom_def)
    from this obtain g where 4: "∀a ∈ A . (a,g(a)) ∈ R"
      by metis
    hence "∀a ∈ A. f(a) = {a}"
      using 3 by (simp add: Dom_def)
    hence "A = C"
      using 2 3 by (smt (verit) Pair_inject UN_singleton case_prodE image_cong mem_Collect_eq plift_def)
    hence "(A,B) ∈ (R)⇩𝒫"
      using 2 by simp
    thus "(A,B) ∈ R⇩*"
      unfolding plift_def klift_set_var
      apply clarsimp
      apply (rule exI[where ?x="g"])
      using 4 by (smt (verit, ccfv_SIG) Collect_cong assms image_def univalent_set)
  qed
  thus "R⇩* = (Dom R)⇩* ; (R)⇩𝒫"
    by force
qed

lemma plift_ext1:
  assumes "univalent f"
  shows "(R ; f⇩*)⇩* = R⇩* ; f⇩*"
proof -
  have "∀A B . (A,B) ∈ (R ; (Dom f)⇩* ; (f)⇩𝒫)⇩* ⟷ (A,B) ∈ R⇩* ; (Dom f)⇩* ; (f)⇩𝒫"
  proof (intro allI, rule iffI)
    fix A B
    assume 1: "(A,B) ∈ (R ; (Dom f)⇩* ; (f)⇩𝒫)⇩*"
    from this obtain g where 2: "(∀a ∈ A. (a,g(a)) ∈ R ; (Dom f)⇩* ; (f)⇩𝒫) ∧ B = ⋃(g ` A)"
      by (smt (verit) Pair_inject case_prodE mem_Collect_eq plift_def)
    hence "∀a ∈ A . ∃C D . (a,C) ∈ R ∧ (C,D) ∈ (Dom f)⇩* ∧ (D,g(a)) ∈ (f)⇩𝒫"
      by (meson relcompEpair)
    hence "∀a ∈ A . ∃C . (a,C) ∈ R ∧ (C,C) ∈ (Dom f)⇩* ∧ (C,g(a)) ∈ (f)⇩𝒫"
      using d_pid_plift by fastforce
    from this obtain h where 3: "∀a ∈ A . (a,h a) ∈ R ∧ (h a,h a) ∈ (Dom f)⇩* ∧ (h a,g(a)) ∈ (f)⇩𝒫"
      by metis
    let ?h = "⋃(h ` A)"
    have 4: "(A,?h) ∈ R⇩*"
      using 3 plift_def by fastforce
    have 5: "(?h,?h) ∈ (Dom f)⇩*"
      using 3
      unfolding plift_def Dom_def
      apply clarsimp
      by (metis UN_extend_simps(9) UN_singleton)
    have "(?h,B) ∈ (f)⇩𝒫"
      using 2 3
      unfolding klift_set
      by auto
    thus "(A,B) ∈ R⇩* ; (Dom f)⇩* ; (f)⇩𝒫"
      using 4 5 by blast
  next
    fix A B
    assume "(A,B) ∈ R⇩* ; (Dom f)⇩* ; (f)⇩𝒫"
    from this obtain C D where 6: "(A,C) ∈ R⇩* ∧ (C,D) ∈ (Dom f)⇩* ∧ (D,B) ∈ (f)⇩𝒫"
      by blast
    hence 7: "C = D"
      using d_pid_plift by auto
    from 6 obtain g where 8: "(∀a ∈ A. (a,g(a)) ∈ R) ∧ C = ⋃(g ` A)"
      by (smt (verit) Pair_inject case_prodE mem_Collect_eq plift_def)
    hence 9: "∀a ∈ A. (g(a),g(a)) ∈ (Dom f)⇩*"
      using 6 7 by (metis d_plift_sub UN_iff subsetI)
    let ?h = "λa . ⋃(f `` g a)"
    have "∀a ∈ A. (g(a),?h a) ∈ (f)⇩𝒫"
      using 6 by (simp add: klift_set)
    hence 10: "∀a ∈ A. (a,?h a) ∈ R ; (Dom f)⇩* ; (f)⇩𝒫"
      using 8 9 by blast
    have "B = ⋃(f `` D)"
      using 6 klift_set by fastforce
    hence 11: "B = (⋃a∈A . ?h a)"
      using 7 8 image_empty by blast
    show "(A,B) ∈ (R ; (Dom f)⇩* ; (f)⇩𝒫)⇩*"
      apply (subst plift_def)
      apply clarsimp
      apply (rule exI[where ?x="?h"])
      using 10 11 by simp
  qed
  hence "(R ; (Dom f)⇩* ; (f)⇩𝒫)⇩* = R⇩* ; (Dom f)⇩* ; (f)⇩𝒫"
    by force
  thus ?thesis
    by (metis (no_types, opaque_lifting) assms univ_plift_klift O_assoc)
qed

lemma plift_assoc_univ: "univalent f ⟹ (R ⋅ S) ⋅ f = R ⋅ (S ⋅ f)"
  by (simp add: pcomp_plift O_assoc plift_ext1)

lemma Lambda_funct: "Λ (R ; S) = Λ R ⋅ Λ S"
  by (simp add: Lambda_pow det_lambda det_plift_klift klift_def pcomp_plift)

lemma eta_funct: "R ; S ; η = (R ; η) ⋅ (S ; η)"
proof -
  have "(R ; η) ⋅ (S ; η) = R ; η ; (S ; η)⇩*"
    by (simp add: pcomp_plift)
  also have "… = R ; (η ⋅ (S ; η))"
    by (simp add: O_assoc pcomp_plift)
  also have "… = R ; S ; η"
    by (simp add: O_assoc pcomp_plift)
  finally show ?thesis..
qed

lemma alpha_funct_det: "deterministic R ⟹ deterministic S ⟹ α (R ⋅ S) = α R ; α S"
  by (metis Lambda_epsiloff_up2 Lambda_funct alpha_Lambda_canc)

lemma pcomp_det: "deterministic S ⟹ R ⋅ S = R ; (S)⇩𝒫"
  by (simp add: det_plift_klift pcomp_plift)

lemma pcomp_det2: "deterministic R ⟹ deterministic S ⟹ (R ⋅ S)⇩𝒫 = (R)⇩𝒫 ; (S)⇩𝒫"
  by (simp add: klift_ext1 pcomp_det)

lemma pcomp_alpha: "α (R ⋅ S) = R ; α ((S)⇩*)"
  by (simp add: pcomp_plift)


subsection ‹Fusion and fission›

definition fus :: "('a,'b) mrel ⇒ ('a,'b) mrel" where
  "fus R = Λ (α R)"

definition fis :: "('a,'b) mrel ⇒ ('a,'b) mrel" where
  "fis R = α R ; η"

lemma fus_set: "fus R = {(a,B) |a B. B = ⋃(Image R {a})}"
  unfolding fus_def Lambda_def alpha_set by force

lemma fis_set: "fis R = {(a,{b}) |a b. b ∈ ⋃(Image R {a})}"
  unfolding fis_def alpha_set eta_set relcomp_unfold by force

lemma fis_det_comp: "deterministic R ⟹ deterministic S ⟹ fis (R ⋅ S) = fis R ⋅ fis S"
  by (simp add: alpha_funct_det eta_funct fis_def)

lemma fis_fix_det: "deterministic R = (fus R = R)"
  by (metis Lambda_alpha_canc det_lambda fus_def)


subsection ‹Galois connections for multirelations›

lemma sub_subh: "R ⊆ S ⟹ R ⊆ S ; (epsiloff ⫽ epsiloff)"
  by (metis R_O_Id alpha_def alpha_epsiloff lres_galois order_refl relcomp_mono)

lemma alpha_Lambda_galois: "(α R ⊆ S) = (R ⊆ Λ S ; (epsiloff ⫽ epsiloff))"
proof -
  have a: "(α R ⊆ S) = (R ⊆ S ⫽ epsiloff)"
    by (simp add: alpha_def lres_galois)
  have "S ⫽ epsiloff = (Λ S ; epsiloff) ⫽ epsiloff"
    by (metis alpha_Lambda_canc alpha_def)
  also have "… = Λ S ; (epsiloff ⫽ epsiloff)"
    by (simp add: det_lambda det_lres)
  finally have "S ⫽ epsiloff = Λ S ; (epsiloff ⫽ epsiloff)"
    .
  thus ?thesis
    using a by presburger
qed

lemma alpha_Lambda_galois_set: "(α R ⊆ S) = (R ⊆ {(a,A). ∃B. (a,B) ∈ Λ S ∧ A ⊆ B})"
  unfolding alpha_set Lambda_def by blast

lemma epsiloff_eta_lres: "epsiloff ; η ⊆ epsiloff ⫽ epsiloff"
proof -
  have "epsiloff ; η ; epsiloff = epsiloff ; α (Λ Id)"
    by (simp add: O_assoc alpha_def eta_def)
  also have "… = epsiloff"
    by simp
  finally have "epsiloff ; η ; epsiloff = epsiloff".
  thus ?thesis
    by (smt (verit) lres_galois order_refl)
qed

lemma eta_alpha_galois: "(R ; η ⊆ S ; (epsiloff ⫽ epsiloff)) = (R ⊆ α S)"
proof
  assume "R ; η ⊆ S ; (epsiloff ⫽ epsiloff)"
  hence "R ⊆ S ; (epsiloff ⫽ epsiloff) ; epsiloff"
    by (metis R_O_Id alpha_def alpha_eta alpha_ord_pres alpha_relcomp)
  thus "R ⊆ α S"
    by (simp add: O_assoc alpha_def)
next
  assume "R ⊆ α S"
  hence "R ; η ⊆ α S ; η"
    by (simp add: relcomp_mono)
  hence "R ; η ⊆ S ; epsiloff ; η"
    by (simp add: alpha_def)
  thus "R ; η ⊆ S ; (epsiloff ⫽ epsiloff)"
    using epsiloff_eta_lres in_mono by fastforce
qed

lemma eta_alpha_galois_set: "(R ; η ⊆ {(a,A). ∃B. (a,B) ∈ S ∧ A ⊆ B}) = (R ⊆ α S)"
  unfolding eta_set alpha_set by auto

lemma Lambda_iso: "R ⊆ S ⟹ Λ R ⊆ Λ S ; (epsiloff ⫽ epsiloff)"
  by (metis alpha_Lambda_canc alpha_Lambda_galois)

lemma eta_iso: "R ⊆ S ⟹ R ; η ⊆ S ; η ; (epsiloff ⫽ epsiloff)"
  by (simp add: eta_alpha_galois)

lemma alpha_iso: "R ⊆ S ; (epsiloff ⫽ epsiloff) ⟹ α R ⊆ α S"
  by (metis (no_types, lifting) alpha_def alpha_ord_pres alpha_relcomp conv_Omega conv_Omega_epsiloff)

lemma Lambda_canc_dcl: "R ⊆ Λ (α R) ; (epsiloff ⫽ epsiloff)"
  using alpha_Lambda_galois by blast

lemma eta_canc_dcl: "α R ; η ⊆ R ; (epsiloff ⫽ epsiloff)"
  by (simp add: eta_alpha_galois)

lemma alpha_surj: "surj α"
  using alpha_Lambda_canc by blast

lemma Lambda_inj: "inj Λ"
  by (metis alpha_Lambda_canc injI)

lemma eta_inj: "inj (λx. x ; η)"
  by (metis alpha_eta_id injI)

lemma fus_least_odet:
  assumes "Λ (α S) = S"
  and "R ⊆ S ; (epsiloff ⫽ epsiloff)"
  shows "Λ (α R) ⊆ S ; (epsiloff ⫽ epsiloff)"
proof -
  have "α R ⊆ α S"
    by (simp add: alpha_iso assms(2))
  hence "Λ (α R) ⊆ Λ (α S) ; (epsiloff ⫽ epsiloff)"
    by (simp add: Lambda_iso)
  thus ?thesis
    using assms(1) by auto
qed

lemma fis_greatest_idet:
  assumes "α S ; η = S"
  and "S ⊆ R ; (epsiloff ⫽ epsiloff)"
  shows "S ⊆ α R ; η ; (epsiloff ⫽ epsiloff)"
proof -
  have "α S ⊆ α R"
    by (simp add: alpha_iso assms(2))
  hence "α S ; η ⊆ α R ; η ; (epsiloff ⫽ epsiloff)"
    by (simp add: eta_iso)
  thus ?thesis
    using assms(1) by auto
qed

lemma fis_fus_galois: "(α R ; η ⊆ S ; (epsiloff ⫽ epsiloff)) = (R ⊆ Λ (α S) ; (epsiloff ⫽ epsiloff))"
  by (simp add: alpha_Lambda_galois eta_alpha_galois)


subsection ‹Properties of alpha, fission and fusion›

lemma alpha_lax: "α (R ⋅ S) ⊆ α R ; α S"
  unfolding alpha_def s_prod_def epsiloff_def relcomp_unfold by blast

lemma alpha_down [simp]: "α (R ; Ω⇧⌣) = α R"
  by (metis alpha_def alpha_relcomp conv_Omega_epsiloff)

lemma fis_fis [simp]: "fis ∘ fis = fis"
  unfolding fun_eq_iff fis_def by simp

lemma fus_fus [simp]: "fus ∘ fus = fus"
  unfolding fun_eq_iff fus_def by simp

lemma fis_fus [simp]: "fis ∘ fus = fis"
  unfolding fun_eq_iff fus_def fis_def by simp

lemma fus_fis [simp]: "fus ∘ fis = fus"
  unfolding fun_eq_iff fus_def fis_def by simp

lemma fis_alpha: "fis R ⋅ S = α R ; S"
  by (simp add: O_assoc fis_def pcomp_plift)

lemma fis_lax: "fis (R ⋅ S) ⊆ fis R ⋅ fis S"
  by (metis fis_def alpha_lax eta_funct relcomp_mono subsetI)

lemma klift_fus: "(R)⇩𝒫 = fus (epsiloff ; R)"
  by (simp add: alpha_def fus_def klift_var)

lemma fus_eta_klift: "fus R = η ; (R)⇩𝒫"
  by (metis Id_O_R Lambda_pow eta_def fus_def klift_def)

lemma fus_Lambda_mu: "fus R = Λ R ; μ"
  by (simp add: fus_def lambda_alpha_mu)


subsection ‹Properties of fusion, fission, nu and tau›

lemma alpha_tau [simp]: "α (τ R) = {}"
  by (metis alpha_ord_pres alpha_pid subset_empty tau_le_c)

lemma alpha_nu [simp]: "α (ν R) = α R"
  unfolding alpha_def nu_def epsiloff_def U_def p_id_def relcomp_unfold by force

lemma nu_fis [simp]: "ν (fis R) = fis R"
  by (metis alpha_fp empty_iff equals0I fis_alpha relcompE)

lemma nu_fis_var: "ν (fis R) = fis (ν R)"
  by (metis alpha_nu fis_def nu_fis)

lemma tau_fis [simp]: "τ (fis R) = {}"
  by (metis nu_fis tau_alpha_zero)


text ‹Properties of tests and domain›

lemma subid_plift: "(P ∩ η)⇩* = {(A,A)|A. ∀a ∈ A. (a,{a}) ∈ (P ∩ η)}"
  unfolding plift_def eta_set by safe auto

lemma U_subid: "R ; (P ∩ η)⇩* = R ∩ U ; (P ∩ η)⇩*"
  unfolding plift_def U_def eta_set relcomp_unfold
  apply safe
  apply force
  apply blast
  by force

lemma subid_plift_down: "U ; (P ∩ η)⇩* ; Ω⇧⌣ = U ; (P ∩ η)⇩*"
  unfolding U_def relcomp_unfold plift_def Omega_set eta_set converse_def
  apply safe
  apply clarsimp
  apply (metis IntE UN_singleton inf.orderE)
  by blast

lemma nu_subid_plift: "ν (R ; (P ∩ η)⇩*) = ν R ; ( P ∩ η)⇩*"
  unfolding nu_def relcomp_unfold plift_def U_def p_id_def eta_set by safe fastforce+

lemma dom_fis1: "dom (fis R) = dom (α R)"
  unfolding dom_set fis_set alpha_set by blast

lemma dom_fis2: "dom (fis R) = dom (α (ν R))"
  by (simp add: dom_fis1)

lemma dom_fis3: "dom (fis R) = dom (ν R)"
  unfolding dom_set fis_set nu_def U_def p_id_def by safe fastforce+

lemma dom_fis4: "dom (fis R) = dom (ν (fus R))"
  by (metis comp_eq_dest_lhs dom_fis3 fis_fus)

lemma dom_alpha: "dom (α R ; (P ∩ η)) = dom (ν (R ; Ω⇧⌣) ; (P ∩ η)⇩*)"
  unfolding dom_set alpha_set eta_set Omega_set plift_def nu_def relcomp_unfold U_def p_id_def
  apply safe
  apply (clarsimp, metis empty_iff empty_subsetI insert_subset singletonD singletonI UN_singleton)
  by clarsimp fastforce


subsection ‹Box and diamond›

definition box :: "('a, 'b) mrel ⇒ ('b set, 'a set) rel" where
  "box R = rbox (α R)"

definition dia :: "('a, 'b) mrel ⇒ ('b set, 'a set) rel" where
  "dia R = 𝒫 ((α R)⇧⌣)"

lemma box_set: "box R = {(B, A). A = {a. ∀C. (a, C) ∈ R ⟶ C ⊆ B}}"
  unfolding box_def rbox_set alpha_set by force

lemma dia_set: "dia R = {(B, A). A = {a. ∃C. (a, C) ∈ R ∧ C ∩ B ≠ {}}}"
  unfolding dia_def pow_set Image_def alpha_set converse_def by force

lemma box_Omega: "box R = Λ (Ω⇧⌣ ⫽ R)"
  unfolding box_set Lambda_def lres_def Omega_set by auto

end