Theory Half_Galois_Property

✐‹creator "Kevin Kappelmann"›
subsection ‹Half Galois Property›
theory Half_Galois_Property
  imports
    Galois_Relator_Base
    Order_Equivalences
begin

text ‹As the definition of the Galois property also works on heterogeneous relations,
we define the concepts in a locale that generalises @{locale galois}.›

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

sublocale galois_rel L R r .

interpretation gr_flip_inv : galois_rel "(≥⇘R⇙)" "(≥⇘L⇙)" l .

abbreviation "right_ge_Galois ≡ gr_flip_inv.Galois"
notation right_ge_Galois (infix ‹⇘R⇙⪆› 50)

abbreviation (input) "Galois_right ≡ gr_flip_inv.ge_Galois_left"
notation Galois_right (infix ‹⪅⇘R⇙› 50)

lemma Galois_rightI [intro]:
  assumes "in_dom (≤⇘L⇙) x"
  and "l x ≤⇘R⇙ y"
  shows "x ⪅⇘R⇙ y"
  using assms by blast

lemma Galois_rightE [elim]:
  assumes "x ⪅⇘R⇙ y"
  obtains "in_dom (≤⇘L⇙) x" "l x ≤⇘R⇙ y"
  using assms by blast

corollary Galois_right_iff_in_dom_and_left_right_rel:
  "x ⪅⇘R⇙ y ⟷ in_dom (≤⇘L⇙) x ∧ l x ≤⇘R⇙ y"
  by blast

text ‹Unlike common literature, we split the definition of the Galois property
into two halves. This has its merits in modularity of proofs and preciser
statement of required assumptions.›

definition "half_galois_prop_left ≡ ∀x y. x ⇘L⇙⪅ y ⟶ l x ≤⇘R⇙ y"

notation galois_prop.half_galois_prop_left (infix ‹⇩h⊴› 50)

lemma half_galois_prop_leftI [intro]:
  assumes "⋀x y. x ⇘L⇙⪅ y ⟹ l x ≤⇘R⇙ y"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  unfolding half_galois_prop_left_def using assms by blast

lemma half_galois_prop_leftD [dest]:
  assumes "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and " x ⇘L⇙⪅ y"
  shows "l x ≤⇘R⇙ y"
  using assms unfolding half_galois_prop_left_def by blast

text‹Observe that the second half can be obtained by creating an appropriately
flipped and inverted interpretation of @{locale galois_prop}. Indeed, many
concepts in our formalisation are "closed" under inversion,
i.e. taking their inversion yields a statement for a related concept.
Many theorems can thus be derived for free by inverting (and flipping) the
concepts at hand. In such cases, we only state those theorems that require some
non-trivial setup. All other theorems can simply be obtained by creating a
suitable locale interpretation.›

interpretation flip_inv : galois_prop "(≥⇘R⇙)" "(≥⇘L⇙)" r l .

definition "half_galois_prop_right ≡ flip_inv.half_galois_prop_left"

notation galois_prop.half_galois_prop_right (infix ‹⊴⇩h› 50)

lemma half_galois_prop_rightI [intro]:
  assumes "⋀x y. x ⪅⇘R⇙ y ⟹ x ≤⇘L⇙ r y"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  unfolding half_galois_prop_right_def using assms by blast

lemma half_galois_prop_rightD [dest]:
  assumes "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "x ⪅⇘R⇙ y"
  shows "x ≤⇘L⇙ r y"
  using assms unfolding half_galois_prop_right_def by blast

interpretation g : galois_prop S T f g for S T f g .

lemma rel_inv_half_galois_prop_right_eq_half_galois_prop_left_rel_inv [simp]:
  "((≤⇘R⇙) ⊴⇩h (≤⇘L⇙))¯ = ((≥⇘L⇙) ⇩h⊴ (≥⇘R⇙))"
  by (intro ext) blast

corollary half_galois_prop_left_rel_inv_iff_half_galois_prop_right [iff]:
  "((≥⇘L⇙) ⇩h⊴ (≥⇘R⇙)) f g ⟷ ((≤⇘R⇙) ⊴⇩h (≤⇘L⇙)) g f"
  by (simp flip: rel_inv_half_galois_prop_right_eq_half_galois_prop_left_rel_inv)

lemma rel_inv_half_galois_prop_left_eq_half_galois_prop_right_rel_inv [simp]:
  "((≤⇘R⇙) ⇩h⊴ (≤⇘L⇙))¯ = ((≥⇘L⇙) ⊴⇩h (≥⇘R⇙))"
  by (intro ext) blast

corollary half_galois_prop_right_rel_inv_iff_half_galois_prop_left [iff]:
  "((≥⇘L⇙) ⊴⇩h (≥⇘R⇙)) f g ⟷ ((≤⇘R⇙) ⇩h⊴ (≤⇘L⇙)) g f"
  by (simp flip: rel_inv_half_galois_prop_left_eq_half_galois_prop_right_rel_inv)

end

context galois
begin

sublocale galois_prop L R l r .

interpretation flip : galois R L r l .

abbreviation "right_Galois ≡ flip.Galois"
notation right_Galois (infix ‹⇘R⇙⪅› 50)

abbreviation (input) "ge_Galois_right ≡ flip.ge_Galois_left"
notation ge_Galois_right (infix ‹⪆⇘R⇙› 50)

abbreviation "left_ge_Galois ≡ flip.right_ge_Galois"
notation left_ge_Galois (infix ‹⇘L⇙⪆› 50)

abbreviation (input) "Galois_left ≡ flip.Galois_right"
notation Galois_left (infix ‹⪅⇘L⇙› 50)

context
begin

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

lemma rel_unit_if_left_rel_if_mono_wrt_relI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "x ⪅⇘R⇙ l x' ⟹ x ≤⇘L⇙ η x'"
  and "x ≤⇘L⇙ x'"
  shows "x ≤⇘L⇙ η x'"
  using assms by blast

corollary rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "x ≤⇘L⇙ x'"
  shows "x ≤⇘L⇙ η x'"
  using assms by (fastforce intro: rel_unit_if_left_rel_if_mono_wrt_relI)

corollary rel_unit_if_reflexive_on_if_half_galois_prop_right_if_mono_wrt_rel:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  and "P x"
  shows "x ≤⇘L⇙ η x"
  using assms by (blast intro: rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel)

corollary inflationary_on_unit_if_reflexive_on_if_half_galois_prop_rightI:
  fixes P :: "'a ⇒ bool"
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘L⇙)"
  shows "inflationary_on P (≤⇘L⇙) η"
  using assms by (intro inflationary_onI)
  (fastforce intro: rel_unit_if_reflexive_on_if_half_galois_prop_right_if_mono_wrt_rel)

interpretation flip : galois_prop R L r l .

lemma right_rel_if_Galois_left_right_if_deflationary_onI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘R⇙) ⊴⇩h (≤⇘L⇙)) r l"
  and "deflationary_on P (≤⇘R⇙) ε"
  and "transitive (≤⇘R⇙)"
  and "y ⪅⇘L⇙ r y'"
  and "P y'"
  shows "y ≤⇘R⇙ y'"
  using assms by force

lemma half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "deflationary_on (in_codom (≤⇘R⇙)) (≤⇘R⇙) ε"
  and "transitive (≤⇘R⇙)"
  shows "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  using assms by (intro half_galois_prop_leftI) fastforce

end

interpretation flip_inv : galois "(≥⇘R⇙)" "(≥⇘L⇙)" r l
  rewrites "flip_inv.unit ≡ ε" and "flip_inv.counit ≡ η"
  and "⋀R S. (R¯ ⇒ S¯) ≡ (R ⇒ S)"
  and "⋀R S f g. (R¯ ⊴⇩h S¯) f g ≡ (S ⇩h⊴ R) g f"
  and "((≥⇘R⇙) ⇩h⊴ (≥⇘L⇙)) r l ≡ ((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  and "⋀R. R¯¯ ≡ R"
  and "⋀(P :: 'c ⇒ bool) (R :: 'c ⇒ 'c ⇒ bool).
    (inflationary_on P R¯ :: ('c ⇒ 'c) ⇒ bool) ≡ deflationary_on P R"
  and "⋀(P :: 'c ⇒ bool) (R :: 'c ⇒ 'c ⇒ bool).
    (deflationary_on P R¯  :: ('c ⇒ 'c) ⇒ bool) ≡ inflationary_on P R"
  and "⋀(P :: 'b ⇒ bool). reflexive_on P (≥⇘R⇙) ≡ reflexive_on P (≤⇘R⇙)"
  and "⋀(R :: 'a ⇒ 'a ⇒ bool). transitive R¯ ≡ transitive R"
  and "⋀R. in_codom R¯ ≡ in_dom R"
  by (simp_all add: flip_unit_eq_counit flip_counit_eq_unit
    galois_prop.half_galois_prop_left_rel_inv_iff_half_galois_prop_right
    galois_prop.half_galois_prop_right_rel_inv_iff_half_galois_prop_left
    mono_wrt_rel_eq_dep_mono_wrt_rel)

corollary counit_rel_if_right_rel_if_mono_wrt_relI:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "r y ⇘L⇙⪅ y' ⟹ ε y ≤⇘R⇙ y'"
  and "y ≤⇘R⇙ y'"
  shows "ε y ≤⇘R⇙ y'"
  using assms
  by (fact flip_inv.rel_unit_if_left_rel_if_mono_wrt_relI
    [simplified rel_inv_iff_rel])

corollary counit_rel_if_right_rel_if_half_galois_prop_left_if_mono_wrt_rel:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "y ≤⇘R⇙ y'"
  shows "ε y ≤⇘R⇙ y'"
  using assms
  by (fact flip_inv.rel_unit_if_left_rel_if_half_galois_prop_right_if_mono_wrt_rel
    [simplified rel_inv_iff_rel])

corollary counit_rel_if_reflexive_on_if_half_galois_prop_left_if_mono_wrt_rel:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘R⇙)"
  and "P y"
  shows "ε y ≤⇘R⇙ y"
  using assms
  by (fact flip_inv.rel_unit_if_reflexive_on_if_half_galois_prop_right_if_mono_wrt_rel
    [simplified rel_inv_iff_rel])

corollary deflationary_on_counit_if_reflexive_on_if_half_galois_prop_leftI:
  fixes P :: "'b ⇒ bool"
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "((≤⇘L⇙) ⇩h⊴ (≤⇘R⇙)) l r"
  and "reflexive_on P (≤⇘R⇙)"
  shows "deflationary_on P (≤⇘R⇙) ε"
  using assms
  by (fact flip_inv.inflationary_on_unit_if_reflexive_on_if_half_galois_prop_rightI)

corollary left_rel_if_left_right_Galois_if_inflationary_onI:
  assumes "((≤⇘L⇙) ⇒ (≤⇘R⇙)) l"
  and "((≤⇘R⇙) ⇩h⊴ (≤⇘L⇙)) r l"
  and "inflationary_on P (≤⇘L⇙) η"
  and "transitive (≤⇘L⇙)"
  and "l x ⇘R⇙⪅ x'"
  and "P x"
  shows "x ≤⇘L⇙ x'"
  using assms by (intro flip_inv.right_rel_if_Galois_left_right_if_deflationary_onI
    [simplified rel_inv_iff_rel])

corollary half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel:
  assumes "((≤⇘R⇙) ⇒ (≤⇘L⇙)) r"
  and "inflationary_on (in_dom (≤⇘L⇙)) (≤⇘L⇙) η"
  and "transitive (≤⇘L⇙)"
  shows "((≤⇘L⇙) ⊴⇩h (≤⇘R⇙)) l r"
  using assms
  by (fact flip_inv.half_galois_prop_left_left_right_if_transitive_if_deflationary_on_if_mono_wrt_rel)

end

context order_functors
begin

interpretation g : galois L R l r .
interpretation flip_g : galois R L r l
  rewrites "flip_g.unit ≡ ε" and "flip_g.counit ≡ η"
  by (simp_all only: flip_unit_eq_counit flip_counit_eq_unit)

lemma left_rel_if_left_right_rel_left_if_order_equivalenceI:
  assumes "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
  and "transitive (≤⇘L⇙)"
  and "l x ≤⇘R⇙ l x'"
  and "in_dom (≤⇘L⇙) x"
  and "in_codom (≤⇘L⇙) x'"
  shows "x ≤⇘L⇙ x'"
  using assms by (auto intro!:
      flip_g.right_rel_if_Galois_left_right_if_deflationary_onI
      g.half_galois_prop_right_left_right_if_transitive_if_inflationary_on_if_mono_wrt_rel
    elim!: rel_equivalence_onE
    intro: inflationary_on_if_le_pred_if_inflationary_on
      in_field_if_in_dom in_field_if_in_codom)

end


end