Theory Galois_Relator_Base

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

locale galois_rel = orders L R
  for L :: "'a ⇒ 'b ⇒ bool"
  and R :: "'c ⇒ 'd ⇒ bool"
  and r :: "'d ⇒ 'b"
begin

text ‹Morally speaking, the Galois relator characterises when two terms
\<^term>‹x :: 'a› and \<^term>‹y :: 'b› are "similar".›

definition "Galois x y ≡ in_codom (≤⇘R⇙) y ∧ x ≤⇘L⇙ r y"

abbreviation "left_Galois ≡ Galois"
notation left_Galois (infix ‹⇘L⇙⪅› 50)

abbreviation (input) "ge_Galois_left ≡ (⇘L⇙⪅)¯"
notation ge_Galois_left (infix ‹⪆⇘L⇙› 50)

text ‹Here we only introduced the (left) Galois relator @{term "(⇘L⇙⪅)"}.
All other variants can be introduced by considering suitable flipped and inversed
interpretations (see @{file "Half_Galois_Property.thy"}).›

lemma left_GaloisI [intro]:
  assumes "in_codom (≤⇘R⇙) y"
  and "x ≤⇘L⇙ r y"
  shows "x ⇘L⇙⪅ y"
  unfolding Galois_def using assms by blast

lemma left_GaloisE [elim]:
  assumes "x ⇘L⇙⪅ y"
  obtains "in_codom (≤⇘R⇙) y" "x ≤⇘L⇙ r y"
  using assms unfolding Galois_def by blast

corollary in_dom_left_if_left_Galois:
  assumes "x ⇘L⇙⪅ y"
  shows "in_dom (≤⇘L⇙) x"
  using assms by blast

corollary left_Galois_iff_in_codom_and_left_rel_right:
  "x ⇘L⇙⪅ y ⟷ in_codom (≤⇘R⇙) y ∧ x ≤⇘L⇙ r y"
  by blast

lemma left_Galois_restrict_left_eq_left_Galois_left_restrict_left:
  "(⇘L⇙⪅)↾⇘P :: 'a ⇒ bool⇙ = galois_rel.Galois (≤⇘L⇙)↾⇘P⇙ (≤⇘R⇙) r"
  by (intro ext iffI galois_rel.left_GaloisI rel_restrict_leftI)
  (auto elim: galois_rel.left_GaloisE)

lemma left_Galois_restrict_right_eq_left_Galois_right_restrict_right:
  "(⇘L⇙⪅)↿⇘P :: 'd ⇒ bool⇙ = galois_rel.Galois (≤⇘L⇙) (≤⇘R⇙)↿⇘P⇙ r"
  by (intro ext iffI galois_rel.left_GaloisI rel_restrict_rightI)
  (auto elim!: galois_rel.left_GaloisE rel_restrict_rightE)

end


end