Theory Galois_Relator

✐‹creator "Kevin Kappelmann"›
subsection ‹Relator For Galois Connections›
theory Galois_Relator
  imports
    Galois_Relator_Base
    Galois_Property
begin

context galois_prop
begin

interpretation flip_inv : galois_rel "(≥R)" "(≥L)" l .

lemma left_Galois_if_Galois_right_if_half_galois_prop_right:
  assumes "((≤L) h (≤R)) l r"
  and "xR y"
  shows "x Ly"
  using assms by (intro left_GaloisI) auto

lemma Galois_right_if_left_Galois_if_half_galois_prop_left:
  assumes "((≤L) h (≤R)) l r"
  and "x Ly"
  shows "xR y"
  using assms by fast

corollary Galois_right_iff_left_Galois_if_galois_prop [iff]:
  assumes "((≤L)  (≤R)) l r"
  shows "xR y  x Ly"
  using assms
    left_Galois_if_Galois_right_if_half_galois_prop_right
    Galois_right_if_left_Galois_if_half_galois_prop_left
  by blast

lemma rel_inv_Galois_eq_flip_Galois_rel_inv_if_galois_prop [simp]:
  assumes "((≤L)  (≤R)) l r"
  shows "(⪆L) = (R⪆)"
  using assms by blast

corollary flip_Galois_rel_inv_iff_Galois_if_galois_prop [iff]:
  assumes "((≤L)  (≤R)) l r"
  shows "y Rx  x Ly"
  using assms by blast

corollary inv_flip_Galois_rel_inv_eq_Galois_if_galois_prop [simp]:
  assumes "((≤L)  (≤R)) l r"
  shows "(⪅R) = (L⪅)" ―‹Note that @{term "(⪅R) = (galois_rel.Galois (≥R) (≥L) l)¯"}
  using assms by (subst rel_inv_eq_iff_eq[symmetric]) simp

end

context galois
begin

interpretation flip_inv : galois "(≥R)" "(≥L)" r l .

context
begin

interpretation flip : galois R L r l .

lemma left_Galois_left_if_left_relI:
  assumes "((≤L)  (≤R)) l"
  and "((≤L) h (≤R)) l r"
  and "xL x'"
  shows "x Ll x'"
  using assms
  by (intro left_Galois_if_Galois_right_if_half_galois_prop_right) (auto 5 0)

corollary left_Galois_left_if_reflexive_on_if_half_galois_prop_rightI:
  assumes "((≤L)  (≤R)) l"
  and "((≤L) h (≤R)) l r"
  and "reflexive_on P (≤L)"
  and "P x"
  shows "x Ll x"
  using assms by (intro left_Galois_left_if_left_relI) auto

lemma left_Galois_left_if_in_codom_if_inflationary_onI:
  assumes "((≤L)  (≤R)) l"
  and "inflationary_on P (≤L) η"
  and "in_codom (≤L) x"
  and "P x"
  shows "x Ll x"
  using assms by (intro left_GaloisI) (auto elim!: in_codomE)

lemma left_Galois_left_if_in_codom_if_inflationary_on_in_codomI:
  assumes "((≤L)  (≤R)) l"
  and "inflationary_on (in_codom (≤L)) (≤L) η"
  and "in_codom (≤L) x"
  shows "x Ll x"
  using assms by (auto intro!: left_Galois_left_if_in_codom_if_inflationary_onI)

lemma left_Galois_left_if_left_rel_if_inflationary_on_in_fieldI:
  assumes "((≤L)  (≤R)) l"
  and "inflationary_on (in_field (≤L)) (≤L) η"
  and "xL x"
  shows "x Ll x"
  using assms by (auto intro!: left_Galois_left_if_in_codom_if_inflationary_onI)

lemma right_left_Galois_if_right_relI:
  assumes "((≤R)  (≤L)) r"
  and "yR y'"
  shows "r y Ly'"
  using assms by (intro left_GaloisI) auto

corollary right_left_Galois_if_reflexive_onI:
  assumes "((≤R)  (≤L)) r"
  and "reflexive_on P (≤R)"
  and "P y"
  shows "r y Ly"
  using assms by (intro right_left_Galois_if_right_relI) auto

lemma left_Galois_if_right_rel_if_left_GaloisI:
  assumes "((≤R)  (≤L)) r"
  and "transitive (≤L)"
  and "x Ly"
  and "yR z"
  shows "x Lz"
  using assms by (intro left_GaloisI) (auto 5 0)

lemma left_Galois_if_left_Galois_if_left_relI:
  assumes "transitive (≤L)"
  and "xL y"
  and "y Lz"
  shows "x Lz"
  using assms by (intro left_GaloisI) auto

lemma left_rel_if_right_Galois_if_left_GaloisI:
  assumes "((≤R) h (≤L)) r l"
  and "transitive (≤L)"
  and "x Ly"
  and "y Rz"
  shows "xL z"
  using assms by auto

lemma Dep_Fun_Rel_left_Galois_right_Galois_if_mono_wrt_rel [intro]:
  assumes "((≤L)  (≤R)) l"
  shows "((L⪅)  (R⪅)) l r"
  using assms by blast

lemma left_ge_Galois_eq_left_Galois_if_in_codom_eq_in_dom_if_symmetric:
  assumes "symmetric (≤L)"
  and "in_codom (≤R) = in_dom (≤R)"
  shows "(L⪆) = (L⪅)" ―‹Note that @{term "(L⪆) = galois_rel.Galois (≥L) (≥R) r"}
  using assms by (intro ext iffI)
  (auto elim!: galois_rel.left_GaloisE intro!: galois_rel.left_GaloisI)

end

interpretation flip : galois R L r l .

lemma ge_Galois_right_eq_left_Galois_if_symmetric_if_in_codom_eq_in_dom_if_galois_prop:
  assumes "((≤L)  (≤R)) l r"
  and "in_codom (≤L) = in_dom (≤L)"
  and "symmetric (≤R)"
  shows "(⪆R) = (L⪅)" ―‹Note that @{term "(⪆R) = (galois_rel.Galois (≤R) (≤L) l)¯"}
  using assms
  by (simp only: inv_flip_Galois_rel_inv_eq_Galois_if_galois_prop
    flip: flip.left_ge_Galois_eq_left_Galois_if_in_codom_eq_in_dom_if_symmetric)

interpretation gp : galois_prop "(L⪅)" "(R⪅)" l l .

lemma half_galois_prop_left_left_Galois_right_Galois_if_half_galois_prop_leftI [intro]:
  assumes "((≤L) h (≤R)) l r"
  shows "((L⪅) h (R⪅)) l l"
  using assms by fast

lemma half_galois_prop_right_left_Galois_right_Galois_if_half_galois_prop_rightI [intro]:
  assumes "((≤L) h (≤R)) l r"
  shows "((L⪅) h (R⪅)) l l"
  using assms by fast

corollary galois_prop_left_Galois_right_Galois_if_galois_prop [intro]:
  assumes "((≤L)  (≤R)) l r"
  shows "((L⪅)  (R⪅)) l l"
  using assms by blast

end


end