Theory Equiv_Relation2

section ‹Some preliminaries on equivalence relations and quotients›

theory Equiv_Relation2 imports Preliminaries Pick
begin


text‹Unary predicates vs. sets:›

definition "S2P A ≡ λ x. x ∈ A"

lemma S2P_app[simp]: "S2P r x ⟷ x ∈ r"
unfolding S2P_def by auto

lemma S2P_Collect[simp]: "S2P (Collect φ) = φ"
apply(rule ext)+ by simp

lemma Collect_S2P[simp]: "Collect (S2P r) = r"
by (metis Collect_mem_eq S2P_Collect)


text‹Binary predicates vs. relatipons:›
definition "P2R φ ≡ {(x,y). φ x y}"
definition "R2P r ≡ λ x y. (x,y) ∈ r"

lemma in_P2R[simp]: "xy ∈ P2R φ ⟷ φ (fst xy) (snd xy)"
unfolding P2R_def by auto

lemma in_P2R_pair[simp]: "(x,y) ∈ P2R φ ⟷ φ x y"
by simp

lemma R2P_app[simp]: "R2P r x y ⟷ (x,y) ∈ r"
unfolding R2P_def by auto

lemma R2P_P2R[simp]: "R2P (P2R φ) = φ"
apply(rule ext)+ by simp

lemma P2R_R2P[simp]: "P2R (R2P r) = r"
using Collect_mem_eq P2R_def R2P_P2R  case_prod_curry by metis

definition "reflP P φ ≡ (∀ x y. φ x y ∨ φ y x ⟶ P x) ∧ (∀ x. P x ⟶ φ x x)"
definition "symP φ ≡ ∀ x y. φ x y ⟶ φ y x"
definition transP where "transP φ ≡ ∀ x y z. φ x y ∧ φ y z ⟶ φ x z"
definition "equivP A φ ≡ reflP A φ ∧ symP φ ∧ transP φ"

lemma refl_on_P2R[simp]: "refl_on (Collect P) (P2R φ) ⟷ reflP P φ"
unfolding reflP_def refl_on_def by force

lemma reflP_R2P[simp]: "reflP (S2P A) (R2P r) ⟷ refl_on A r"
unfolding reflP_def refl_on_def by auto

lemma sym_P2R[simp]: "sym (P2R φ) ⟷ symP φ"
unfolding symP_def sym_def by auto

lemma symP_R2P[simp]: "symP (R2P r) ⟷ sym r"
unfolding symP_def sym_def by auto

lemma trans_P2R[simp]: "trans (P2R φ) ⟷ transP φ"
unfolding transP_def trans_def by auto

lemma transP_R2P[simp]: "transP (R2P r) ⟷ trans r"
unfolding transP_def trans_def by auto

lemma equiv_P2R[simp]: "equiv (Collect P) (P2R φ) ⟷ equivP P φ"
unfolding equivP_def equiv_def by auto

lemma equivP_R2P[simp]: "equivP (S2P A) (R2P r) ⟷ equiv A r"
unfolding equivP_def equiv_def by auto

lemma in_P2R_Im_singl[simp]: "y ∈ P2R φ `` {x} ⟷ φ x y" by simp

definition proj :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set" where
"proj φ x ≡ {y. φ x y}"

lemma proj_P2R: "proj φ x = P2R φ `` {x}" unfolding proj_def by auto

lemma proj_P2R_raw: "proj φ = (λ x. P2R φ `` {x})"
apply(rule ext) unfolding proj_P2R ..

definition univ :: "('a ⇒ 'b) ⇒ ('a set ⇒ 'b)"
where "univ f X == f (SOME x. x ∈ X)"

definition quotientP ::
"('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a set ⇒ bool)"  (infixl "'/'/'/" 90)
where "P /// φ ≡ S2P ((Collect P) // (P2R φ))"

lemma proj_preserves:
"P x ⟹ (P /// φ) (proj φ x)"
unfolding proj_P2R quotientP_def
by (metis S2P_def mem_Collect_eq quotientI)

lemma proj_in_iff:
assumes "equivP P φ"
shows "(P///φ) (proj φ x)  ⟷ P x"
using assms unfolding quotientP_def proj_def 
by (metis (mono_tags) Collect_mem_eq Equiv_Relation2.proj_def 
  Equiv_Relation2.proj_preserves S2P_Collect empty_Collect_eq equivP_def 
  equiv_P2R in_quotient_imp_non_empty quotientP_def reflP_def)

lemma proj_iff[simp]:
"⟦equivP P φ; P x; P y⟧ ⟹ proj φ x = proj φ y ⟷ φ x y"
unfolding proj_P2R
by (metis (full_types) equiv_P2R equiv_class_eq_iff equiv_class_self
          in_P2R_pair mem_Collect_eq proj_P2R proj_def)

lemma in_proj[simp]: "⟦equivP P φ; P x⟧ ⟹ x ∈ proj φ x"
unfolding proj_P2R equiv_def refl_on_def equiv_P2R[symmetric]
by auto

lemma proj_image[simp]: "(proj φ) ` (Collect P) = Collect (P///φ)"
unfolding proj_P2R_raw quotientP_def quotient_def by auto

lemma in_quotientP_imp_non_empty:
assumes "equivP P φ" and "(P///φ) X"
shows "X ≠ {}" 
by (metis R2P_P2R S2P_Collect S2P_def assms equivP_R2P 
in_quotient_imp_non_empty quotientP_def)

lemma in_quotientP_imp_in_rel:
"⟦equivP P φ; (P///φ) X; x ∈ X; y ∈ X⟧ ⟹ φ x y"
unfolding equiv_P2R[symmetric] quotientP_def quotient_eq_iff
by (metis S2P_def in_P2R_pair quotient_eq_iff)

lemma in_quotientP_imp_closed:
"⟦equivP P φ; (P///φ) X; x ∈ X; φ x y⟧ ⟹ y ∈ X"
using S2P_Collect S2P_def equivP_def proj_P2R_raw proj_def
        quotientE quotientP_def transP_def 
by metis 

lemma in_quotientP_imp_subset:
assumes "equivP P φ" and "(P///φ) X"
shows "X ⊆ Collect P"
by (metis (mono_tags, lifting) CollectI assms equivP_def in_quotientP_imp_in_rel reflP_def subsetI)

lemma equivP_pick_in:
assumes  "equivP P φ " and "(P///φ) X"
shows "pick X ∈ X"
by (metis assms in_quotientP_imp_non_empty pick_NE)

lemma equivP_pick_preserves:
assumes  "equivP P φ " and "(P///φ) X"
shows "P (pick X)"
by (metis assms equivP_pick_in in_quotientP_imp_subset mem_Collect_eq set_rev_mp)

lemma proj_pick:
assumes φ: "equivP P φ" and X: "(P///φ) X"
shows "proj φ (pick X) = X"
by (smt (verit) proj_def Equiv_Relation2.proj_iff Equiv_Relation2.proj_image X 
   φ equivP_pick_in equivP_pick_preserves image_iff mem_Collect_eq)
 
lemma pick_proj:
assumes "equivP P φ" and "P x"
shows "φ (pick (proj φ x)) x"
by (metis assms equivP_def in_proj mem_Collect_eq pick proj_def symP_def)

lemma equivP_pick_iff[simp]:
assumes φ: "equivP P φ" and X: "(P///φ) X" and Y: "(P///φ) Y"
shows "φ (pick X) (pick Y) ⟷ X = Y"
by (metis Equiv_Relation2.proj_iff X Y φ equivP_pick_preserves proj_pick)

lemma equivP_pick_inj_on:
assumes "equivP P φ"
shows "inj_on pick (Collect (P///φ))"
using assms unfolding inj_on_def
by (metis assms equivP_pick_iff mem_Collect_eq)

definition congruentP where
"congruentP φ f ≡ ∀ x y. φ x y ⟶ f x = f y"

abbreviation RESPECTS_P (infixr "respectsP" 80) where
"f respectsP r == congruentP r f"

lemma congruent_P2R: "congruent (P2R φ) f = congruentP φ f"
unfolding congruent_def congruentP_def by auto
 
lemma univ_commute[simp]:
assumes "equivP P φ" and "f respectsP φ" and "P x"
shows "(univ f) (proj φ x) = f x"
unfolding congruent_P2R[symmetric]
by (metis (full_types) assms pick_def congruentP_def pick_proj univ_def)

lemma univ_unique:
assumes "equivP P φ" and "f respectsP φ" and "⋀ x. P x ⟹ G (proj φ x) = f x"
shows "∀ X. (P///φ) X ⟶ G X = univ f X"
by (metis assms equivP_pick_preserves proj_pick univ_commute)

lemma univ_preserves:
assumes "equivP P φ " and "f respectsP φ" and "⋀ x. P x ⟹ f x ∈ B"
shows "∀ X. (P///φ) X ⟶ univ f X ∈ B"
by (metis Equiv_Relation2.univ_commute assms  
          equivP_pick_preserves proj_pick) 




end