(* Title: Graphing_Exercise.thy Author: Clara L\"oh *) text \We introduce graphings of equivalence relations (in the non-measurable setting).\ theory Graphing_Exercise imports Complex_Main RelRel_Iso begin section \Generating equivalence relations\ subsection \The equivalence relation generated by a relation\ text \The equivalence relation generated by a relation on a set is the smallest set (i.e., inductive set) that contains the given relation and satisfies the properties of an equivalence relation.\ inductive_set generated_equiv_rel :: "'a set => 'a rel => 'a rel" for X and r where incl: "x \ X ==> y \ X ==> (x,y) \ r ==> (x,y) \ generated_equiv_rel X r" | refl: "x \ X ==> (x,x) \ generated_equiv_rel X r" | symm: "x \ X ==> y \ X ==> (x,y) \ generated_equiv_rel X r ==> (y,x) \ generated_equiv_rel X r" | trans: "x \ X ==> y \ X ==> z \ X ==> (x,y) \ generated_equiv_rel X r ==> (y,z) \ generated_equiv_rel X r ==> (x,z) \ generated_equiv_rel X r" subsection \Basic facts on generated equivalence relations\ text \The generated equivalence relation is a relation on the same base space:\ lemma generated_equiv_rel_on_base: fixes X r assumes r_rel_on_X: "r \ X \ X" shows "(generated_equiv_rel X r) \ X \ X" proof have pair_version: "\ x y. (x,y) \ generated_equiv_rel X r ==> (x,y) \ X \ X" proof - fix x y assume "(x,y) \ generated_equiv_rel X r" then show "(x,y) \ X \ X" proof (induct) case incl fix x y assume "x \ X" "y \ X" "(x,y) \ r" then show "(x,y) \ X \ X" by simp (* alternatively: case (incl x y) then show "(x,y) \ X \ X" by simp *) next case (refl x) then show ?case by simp next case (symm x y) then show ?case by simp next case (trans x y z) then show ?case by simp qed qed (* We can reduce the actual claim to the explicit pair case using fst/snd or using the cases/induction principle for pairs. *) fix xy assume xy_in_genr: "xy \ generated_equiv_rel X r" then show "xy \ X \ X" proof (cases xy) case (Pair x y) then show ?thesis using pair_version[of x y] xy_in_genr by simp qed qed text \Generated equivalence relations are indeed equivalence relations.\ lemma generated_equiv_rel_is_equiv_rel: fixes X r assumes r_rel_on_X: "r \ X \ X" shows "equiv X (generated_equiv_rel X r)" (* equiv: from Equiv_Relations.thy *) proof (intro equivI) define R where "R = generated_equiv_rel X r" show "refl_on X R" proof show "R \ X \ X" using r_rel_on_X generated_equiv_rel_on_base R_def by simp show "\ x. x \ X ==> (x,x) \ R" using generated_equiv_rel.refl R_def by simp qed show "sym R" proof fix x y assume xy_in_R: "(x,y) \ R" then have "x \ X" "y \ X" using generated_equiv_rel_on_base r_rel_on_X R_def by auto then show "(y,x) \ R" using generated_equiv_rel.symm R_def xy_in_R by simp qed show "trans R" proof fix x y z assume xyz_in_R: "(x,y) \ R" "(y,z) \ R" then have "x \ X" "y \ X" "z \ X" using generated_equiv_rel_on_base r_rel_on_X R_def by auto then show "(x,z) \ R" using generated_equiv_rel.trans R_def xyz_in_R by simp qed qed lemma generated_equiv_rel_contains_generator: fixes X r assumes r_rel_on_X: "r \ X \ X" shows "r \ generated_equiv_rel X r" proof fix xy assume xy_in_r: "xy \ r" define x where "x = fst xy" define y where "y = snd xy" have xy_xy: "(x,y) =xy" using x_def y_def prod_eqI by simp have x_in_X: "x \ X" using xy_in_r x_def r_rel_on_X xy_xy by auto have y_in_X: "y \ X" using xy_in_r x_def r_rel_on_X xy_xy by auto show "xy \ generated_equiv_rel X r" using incl[of x X y r] xy_in_r xy_xy x_in_X y_in_X by simp qed text \The construction of generated equivalence relations satisifes monotonicity.\ lemma generated_equiv_rel_mono: fixes X r s assumes r_rel_on_X: "r \ X \ X" and s_rel_on_X: "s \ X \ X" and r_sub_s: "r \ s" shows "generated_equiv_rel X r \ generated_equiv_rel X s" proof have gen_r_sub_s: "\ x y. (x,y) \ generated_equiv_rel X r ==> (x,y) \ generated_equiv_rel X s" proof - fix x y assume "(x,y) \ generated_equiv_rel X r" then show "(x,y) \ generated_equiv_rel X s" proof (induct) case incl fix x y assume "x \ X" "y \ X" "(x,y) \ r" then have "(x,y) \ s" using r_sub_s by auto then show "(x,y) \ generated_equiv_rel X s" using generated_equiv_rel_contains_generator[of s X] s_rel_on_X by auto next case refl fix x assume "x \ X" then show "(x,x) \ generated_equiv_rel X s" using s_rel_on_X generated_equiv_rel_is_equiv_rel[of s X] equiv_def[of X "generated_equiv_rel X s"] refl_onD by auto next case symm fix x y assume "x \ X" "y \ X" "(x,y) \ generated_equiv_rel X s" then show "(y,x) \ generated_equiv_rel X s" using s_rel_on_X generated_equiv_rel_is_equiv_rel[of s X] equiv_def[of X "generated_equiv_rel X s"] sym_def[of "generated_equiv_rel X s"] by auto next case trans fix x y z assume "x \ X" "y \ X" "z \ X" "(x,y) \ generated_equiv_rel X s" "(y,z) \ generated_equiv_rel X s" then show "(x,z) \ generated_equiv_rel X s" using s_rel_on_X generated_equiv_rel_is_equiv_rel[of s X] equiv_def[of X "generated_equiv_rel X s"] trans_def[of "generated_equiv_rel X s"] by auto (* thinks for a bit *) qed qed fix xy assume xy_in_genr: "xy \ generated_equiv_rel X r" then show "xy \ generated_equiv_rel X s" proof (cases xy) case (Pair x y) then show ?thesis using xy_in_genr gen_r_sub_s by simp qed qed text \The equivalence relation generated by an equivalence relation coincides with the given equivalence relation.\ lemma generated_equiv_rel_of_equiv_rel: fixes X r assumes r_erel: "equiv X r" shows "r = generated_equiv_rel X r" proof show "r \ generated_equiv_rel X r" using generated_equiv_rel_contains_generator[of r X] r_erel equiv_def[of X r] refl_on_def[of X r] by auto show "generated_equiv_rel X r \ r" proof have genrel_sub_r: "\ x y. (x,y) \ generated_equiv_rel X r ==> (x,y) \ r" proof - fix x y assume "(x,y) \ generated_equiv_rel X r" then show "(x,y) \ r" text \We prove this claim by showing that \r\ satisfies the inductive properties of the generated equivalence relation. Then minimality (i.e., the associated induction property) gives the claimed inclusion\ proof (induct) case incl fix x y assume "x \ X" "y \ X" "(x,y) \ r" then show "(x,y) \ r" by simp (* alternatively: case (incl x y) then show ?case by simp *) next case (refl x) then show ?case using r_erel equiv_def[of X r] refl_on_def[of X r] by auto next case (symm x y) then show ?case using r_erel equiv_def[of X r] sym_def[of r] by auto next case (trans x y z) then show ?case using r_erel equiv_def[of X r] trans_def[of r] by auto (* thinks for a bit *) qed qed fix xy assume xy_in_genr: "xy \ generated_equiv_rel X r" show "xy \ r" proof (cases xy) case (Pair x y) then show ?thesis using genrel_sub_r[of x y] xy_in_genr by simp qed qed qed section \Graphings of equivalence relations\ subsection \Partial automorphisms of equivalence relations\ text \We model partial isomorphisms of relations as subrelations that are graphs of an isomorphism (in the non-measurable case: bijection).\ definition is_partial_iso_of :: "'a rel => 'a rel => bool" where "is_partial_iso_of r phi = (is_graph_of_iso phi \ phi \ r)" lemma is_graph_of_partial_isoI: fixes r phi f g assumes phi_sub_r: "phi \ r" and phi_partial_iso: "is_graph_of_iso phi" shows "is_partial_iso_of r phi" proof - show ?thesis using is_partial_iso_of_def[of r phi] phi_sub_r phi_partial_iso by simp qed subsection \Graphings\ (* Improve this definition! *) definition is_graphing_of :: "'a set => 'a rel => 'a rel set => bool" where "is_graphing_of X r Phi = (r = generated_equiv_rel X (Union Phi))" subsection \A simple example\ text\The empty set is a graphing of the diagonal relation:\ definition diag :: "'a set => 'a rel" where "diag X = { (x,x) | x . x \ X}" text\The diagonal is an equivalence relation.\ lemma diag_is_equiv_rel: fixes X shows "equiv X (diag X)" proof (intro equivI) show "refl_on X (diag X)" proof show "(diag X) \ X \ X" using diag_def[of X] by auto show "\ x. x\ X ==> (x,x) \ diag X" using diag_def[of X] by auto qed show "sym (diag X)" using diag_def[of X] symI[of "diag X"] by auto show "trans (diag X)" using diag_def[of X] transI[of "diag X"] by auto qed text \Every equivalence relation on a set contains the diagonal on this set because of reflexivity.\ lemma equiv_rel_contains_diag: fixes X r assumes r_equiv_on_X: "equiv X r" shows "diag X \ r" proof have refl_r: "\ x. x \ X ==> (x,x) \ r" using r_equiv_on_X equiv_def refl_onD[of X r] by auto fix xy assume xy_in_diag: "xy \ diag X" define x where "x = fst xy" define y where "y = snd xy" have xy_xy: "xy = (x,y)" using prod_eqI x_def y_def by simp then have "x \ X" "x = y" using x_def y_def xy_in_diag diag_def[of X] by auto then have "(x,y) \ r" using refl_r by auto then show "xy \ r" using xy_xy by simp qed text \We conclude: The equivalence relation generated by the empty graphing is the diagonal on the given set.\ (* Adapt the proof according to your new definition of is_graphing_of ! *) theorem empty_graphing_graphs_diagonal: fixes X shows "is_graphing_of X (diag X) {}" unfolding is_graphing_of_def proof define r where "r = generated_equiv_rel X (Union {})" then have r_simp: "r = generated_equiv_rel X {}" by simp have r_eqrel: "equiv X r" using generated_equiv_rel_is_equiv_rel[of "{}" X] r_def by simp text \The diagonal is contained in the equivalence relation generated by the empty graphing, because the latter one is an equivalence relation and thus must contain the diagonal.\ show "diag X \ r" proof - have "equiv X r" using r_eqrel generated_equiv_rel_on_base[of "{}" X] r_def by simp then show ?thesis using equiv_rel_contains_diag[of X r] by simp qed text \The equivalence relation generated by the empty graphing is contained in the equivalence relation generated by the diagonal (by monotonicity); because the diagonal is already an equivalence relation, the latter equivalence relation is just the diagonal itself.\ show "r \ diag X" proof - have "{} \ diag X" "{} \ X \ X" "diag X \ X \ X" using diag_def[of X] by auto then have "generated_equiv_rel X {} \ generated_equiv_rel X (diag X)" using generated_equiv_rel_mono[of "{}" X "diag X"] by simp then show "r \ diag X" using r_simp diag_is_equiv_rel[of X] generated_equiv_rel_of_equiv_rel[of X "diag X"] by simp qed qed end