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