Theory Reflexive_Relator

✐‹creator "Kevin Kappelmann"›
section ‹Reflexive Relator›
theory Reflexive_Relator
  imports
    Galois_Equivalences
    Galois_Relator
begin

definition "Refl_Rel R x y ≡ R x x ∧ R y y ∧ R x y"

bundle Refl_Rel_syntax begin notation Refl_Rel ("(_⇧⊕)" [1000]) end
bundle no_Refl_Rel_syntax begin no_notation Refl_Rel ("(_⇧⊕)" [1000]) end
unbundle Refl_Rel_syntax

lemma Refl_RelI [intro]:
  assumes "R x x"
  and "R y y"
  and "R x y"
  shows "R⇧⊕ x y"
  using assms unfolding Refl_Rel_def by blast

lemma Refl_Rel_selfI [intro]:
  assumes "R x x"
  shows "R⇧⊕ x x"
  using assms by blast

lemma Refl_RelE [elim]:
  assumes "R⇧⊕ x y"
  obtains "R x x" "R y y" "R x y"
  using assms unfolding Refl_Rel_def by blast

lemma Refl_Rel_reflexive_on_in_field [iff]:
  "reflexive_on (in_field R⇧⊕) R⇧⊕"
  by (rule reflexive_onI) auto

lemma Refl_Rel_le_self [iff]: "R⇧⊕ ≤ R" by blast

lemma Refl_Rel_eq_self_if_reflexive_on [simp]:
  assumes "reflexive_on (in_field R) R"
  shows "R⇧⊕ = R"
  using assms by blast

lemma reflexive_on_in_field_if_Refl_Rel_eq_self:
  assumes "R⇧⊕ = R"
  shows "reflexive_on (in_field R) R"
  by (fact Refl_Rel_reflexive_on_in_field[of R, simplified assms])

corollary Refl_Rel_eq_self_iff_reflexive_on:
  "R⇧⊕ = R ⟷ reflexive_on (in_field R) R"
  using Refl_Rel_eq_self_if_reflexive_on reflexive_on_in_field_if_Refl_Rel_eq_self
  by blast

lemma Refl_Rel_Refl_Rel_eq [simp]: "(R⇧⊕)⇧⊕ = R⇧⊕"
  by (intro ext) auto

lemma rel_inv_Refl_Rel_eq [simp]: "(R⇧⊕)¯ = (R¯)⇧⊕"
  by (intro ext iffI Refl_RelI rel_invI) auto

lemma Refl_Rel_transitive_onI [intro]:
  assumes "transitive_on (P :: 'a ⇒ bool) (R :: 'a ⇒ _)"
  shows "transitive_on P R⇧⊕"
  using assms by (intro transitive_onI) (blast dest: transitive_onD)

corollary Refl_Rel_transitiveI [intro]:
  assumes "transitive R"
  shows "transitive R⇧⊕"
  using assms by blast

corollary Refl_Rel_preorder_onI:
  assumes "transitive_on P R"
  and "P ≤ in_field R⇧⊕"
  shows "preorder_on P R⇧⊕"
  using assms by (intro preorder_onI
    reflexive_on_if_le_pred_if_reflexive_on[where ?P="in_field R⇧⊕" and ?P'=P])
  auto

corollary Refl_Rel_preorder_on_in_fieldI [intro]:
  assumes "transitive R"
  shows "preorder_on (in_field R⇧⊕) R⇧⊕"
  using assms by (intro Refl_Rel_preorder_onI) auto

lemma Refl_Rel_symmetric_onI [intro]:
  assumes "symmetric_on (P :: 'a ⇒ bool) (R :: 'a ⇒ _)"
  shows "symmetric_on P R⇧⊕"
  using assms by (intro symmetric_onI) (auto dest: symmetric_onD)

lemma Refl_Rel_symmetricI [intro]:
  assumes "symmetric R"
  shows "symmetric R⇧⊕"
  by (urule symmetric_on_if_le_pred_if_symmetric_on)
  (use assms in ‹urule Refl_Rel_symmetric_onI›, simp)

lemma Refl_Rel_partial_equivalence_rel_onI [intro]:
  assumes "partial_equivalence_rel_on (P :: 'a ⇒ bool) (R :: 'a ⇒ _)"
  shows "partial_equivalence_rel_on P R⇧⊕"
  using assms by (intro partial_equivalence_rel_onI Refl_Rel_transitive_onI
    Refl_Rel_symmetric_onI) auto

lemma Refl_Rel_partial_equivalence_relI [intro]:
  assumes "partial_equivalence_rel R"
  shows "partial_equivalence_rel R⇧⊕"
  using assms
  by (intro partial_equivalence_relI Refl_Rel_transitiveI Refl_Rel_symmetricI) auto

lemma Refl_Rel_app_leftI:
  assumes "R (f x) y"
  and "in_field S⇧⊕ x"
  and "in_field R⇧⊕ y"
  and "(S ⇛⇩m R) f"
  shows "R⇧⊕ (f x) y"
proof (rule Refl_RelI)
  from ‹in_field R⇧⊕ y› show "R y y" by blast
  from ‹in_field S⇧⊕ x› have "S x x" by blast
  with ‹(S ⇛⇩m R) f› show "R (f x) (f x)" by blast
qed fact

corollary Refl_Rel_app_rightI:
  assumes "R x (f y)"
  and "in_field S⇧⊕ y"
  and "in_field R⇧⊕ x"
  and "(S ⇛⇩m R) f"
  shows "R⇧⊕ x (f y)"
proof -
  from assms have "(R¯)⇧⊕ (f y) x" by (intro Refl_Rel_app_leftI[where ?S="S¯"])
    (auto 5 0 simp flip: rel_inv_Refl_Rel_eq)
  then show ?thesis by blast
qed

lemma mono_wrt_rel_Refl_Rel_Refl_Rel_if_mono_wrt_rel [intro]:
  assumes "(R ⇛⇩m S) f"
  shows "(R⇧⊕ ⇛⇩m S⇧⊕) f"
  using assms by (intro mono_wrt_relI) blast

context galois
begin

interpretation gR : galois "(≤⇘L⇙)⇧⊕" "(≤⇘R⇙)⇧⊕" l r .

lemma Galois_Refl_RelI:
  assumes "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "in_field (≤⇘L⇙)⇧⊕ x"
  and "in_field (≤⇘R⇙)⇧⊕ y"
  and "in_codom (≤⇘R⇙) y ⟹ x ⇘L⇙⪅ y"
  shows "(galois_rel.Galois ((≤⇘L⇙)⇧⊕) ((≤⇘R⇙)⇧⊕) r) x y"
  using assms by (intro gR.left_GaloisI in_codomI Refl_Rel_app_rightI[where ?f=r])
  auto

lemma half_galois_prop_left_Refl_Rel_left_rightI:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ⇩h⊴ (≤⇘R⇙)⇧⊕) l r"
  using assms by (intro gR.half_galois_prop_leftI Refl_RelI)
  (auto elim!: in_codomE gR.left_GaloisE Refl_RelE)

interpretation flip_inv : galois "(≥⇘R⇙)" "(≥⇘L⇙)" r l
  rewrites "((≥⇘R⇙) ⇛⇩m (≥⇘L⇙)) ≡ ((≤⇘R⇙) ⇛⇩m (≤⇘L⇙))"
  and "⋀R. (R¯)⇧⊕ ≡ (R⇧⊕)¯"
  and "⋀R S f g. (R¯ ⇩h⊴ S¯) f g ≡ (S ⊴⇩h R) g f"
  by (simp_all add: galois_prop.half_galois_prop_left_rel_inv_iff_half_galois_prop_right
    mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma half_galois_prop_right_Refl_Rel_right_leftI:
  assumes "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ⊴⇩h (≤⇘R⇙)⇧⊕) l r"
  using assms by (fact flip_inv.half_galois_prop_left_Refl_Rel_left_rightI)

corollary galois_prop_Refl_Rel_left_rightI:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ⊴ (≤⇘R⇙)⇧⊕) l r"
  using assms
  by (intro gR.galois_propI half_galois_prop_left_Refl_Rel_left_rightI
    half_galois_prop_right_Refl_Rel_right_leftI) auto

lemma galois_connection_Refl_Rel_left_rightI:
  assumes "((≤⇘L⇙) ⊣ (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ⊣ (≤⇘R⇙)⇧⊕) l r"
  using assms
  by (intro gR.galois_connectionI galois_prop_Refl_Rel_left_rightI) auto

lemma galois_equivalence_Refl_RelI:
  assumes "((≤⇘L⇙) ≡⇩G (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ≡⇩G (≤⇘R⇙)⇧⊕) l r"
proof -
  interpret flip : galois R L r l .
  show ?thesis using assms by (intro gR.galois_equivalenceI
    galois_connection_Refl_Rel_left_rightI flip.galois_prop_Refl_Rel_left_rightI)
  auto
qed

end

context order_functors
begin

lemma inflationary_on_in_field_Refl_Rel_left:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "inflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "inflationary_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms
  by (intro inflationary_onI Refl_RelI) (auto 0 3 elim!: in_fieldE Refl_RelE)

lemma inflationary_on_in_field_Refl_Rel_left':
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "inflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "inflationary_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms
  by (intro inflationary_onI Refl_RelI) (auto 0 3 elim!: in_fieldE Refl_RelE)

interpretation inv : galois "(≥⇘L⇙)" "(≥⇘R⇙)" l r
  rewrites "((≥⇘L⇙) ⇛⇩m (≥⇘R⇙)) ≡ ((≤⇘L⇙) ⇛⇩m (≤⇘R⇙))"
  and "((≥⇘R⇙) ⇛⇩m (≥⇘L⇙)) ≡ ((≤⇘R⇙) ⇛⇩m (≤⇘L⇙))"
  and "⋀R. (R¯)⇧⊕ ≡ (R⇧⊕)¯"
  and "⋀R. in_dom R¯ ≡ in_codom R"
  and "⋀R. in_codom R¯ ≡ in_dom R"
  and "⋀R. in_field R¯ ≡ in_field R"
  and "⋀(P :: 'c ⇒ bool) (R :: 'd ⇒ 'c ⇒ bool).
    (inflationary_on P R¯ :: ('c ⇒ 'd) ⇒ bool) ≡ deflationary_on P R"
  by (simp_all add: mono_wrt_rel_eq_dep_mono_wrt_rel)

lemma deflationary_on_in_field_Refl_Rel_leftI:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "deflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "deflationary_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms by (fact inv.inflationary_on_in_field_Refl_Rel_left')

lemma deflationary_on_in_field_Refl_RelI_left':
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "deflationary_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "deflationary_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms by (fact inv.inflationary_on_in_field_Refl_Rel_left)

lemma rel_equivalence_on_in_field_Refl_Rel_leftI:
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "rel_equivalence_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_Refl_Rel_left
    deflationary_on_in_field_Refl_Rel_leftI)
  auto

lemma rel_equivalence_on_in_field_Refl_Rel_leftI':
  assumes "((≤⇘L⇙) ⇛⇩m (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇛⇩m (≤⇘L⇙)) r"
  and "rel_equivalence_on (in_codom (≤⇘L⇙)) (≤⇘L⇙) η"
  shows "rel_equivalence_on (in_field (≤⇘L⇙)⇧⊕) (≤⇘L⇙)⇧⊕ η"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_Refl_Rel_left'
    deflationary_on_in_field_Refl_RelI_left')
  auto

interpretation oR : order_functors "(≤⇘L⇙)⇧⊕" "(≤⇘R⇙)⇧⊕" l r .

lemma order_equivalence_Refl_RelI:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  shows "((≤⇘L⇙)⇧⊕ ≡⇩o (≤⇘R⇙)⇧⊕) l r"
proof -
  interpret flip : galois R L r l
    rewrites "flip.unit ≡ ε"
    by (simp only: flip_unit_eq_counit)
  show ?thesis using assms by (intro oR.order_equivalenceI
    mono_wrt_rel_Refl_Rel_Refl_Rel_if_mono_wrt_rel
    rel_equivalence_on_in_field_Refl_Rel_leftI
    flip.rel_equivalence_on_in_field_Refl_Rel_leftI)
    (auto intro: rel_equivalence_on_if_le_pred_if_rel_equivalence_on
      in_field_if_in_dom)
qed

end


end