theory Orbits_Exercise imports Complex_Main begin text \Equivalence relations are relations on a given set that are reflexive, symmetric, and transitive.\ definition is_relation_on :: "'a set => ('a \ 'a) set => bool" where "is_relation_on X r = (r \ X \ X)" definition is_reflexive :: "'a set => ('a \ 'a) set => bool" where "is_reflexive X r = (\ x \ X. (x,x) \ r)" definition is_symmetric :: "'a set => ('a \ 'a) set => bool" where "is_symmetric X r = (\ x \ X. \ y \ X. (x,y) \ r --> (y,x) \ r)" definition is_transitive :: "'a set => ('a \ 'a) set => bool" where "is_transitive X r = (\ x \ X. \ y \ X. \ z \ X. ((x,y) \ r \ (y,z) \ r) --> (x,z) \ r)" definition is_equivalence_relation :: "'a set => ('a \ 'a) set => bool" where "is_equivalence_relation X r = (is_relation_on X r \ is_reflexive X r \ is_symmetric X r \ is_transitive X r)" text \Small lemmas that help to extract properties of equivalence relations.\ lemma eqrel_symmetric: fixes X r assumes eqrel: "is_equivalence_relation X r" shows "is_symmetric X r" proof - show ?thesis using eqrel is_equivalence_relation_def by auto qed lemma eqrel_symmetric_meta: fixes X r x y assumes eqrel: "is_equivalence_relation X r" and x_rel_y: "(x,y) \ r" shows "(y,x) \ r" proof - have "x \ X" and "y \ X" using x_rel_y eqrel is_equivalence_relation_def by (auto simp add: is_relation_on_def) then show ?thesis using x_rel_y eqrel eqrel_symmetric by (auto simp add: is_symmetric_def) qed lemma eqrel_transitive: fixes X r assumes eqrel: "is_equivalence_relation X r" shows "is_transitive X r" proof - show ?thesis using eqrel is_equivalence_relation_def by auto qed lemma eqrel_transitive_meta: fixes X r x y z assumes eqrel: "is_equivalence_relation X r" and x_rel_y: "(x,y) \ r" and y_rel_z: "(y,z) \ r" shows "(x,z) \ r" proof - have xy_and_yz: "(x,y) \ r \ (y,z) \ r" using x_rel_y y_rel_z by simp have "x \ X" and "y \ X" and "z \ X" using x_rel_y y_rel_z eqrel is_equivalence_relation_def by (auto simp add: is_relation_on_def) then show ?thesis using xy_and_yz eqrel eqrel_transitive is_transitive_def[of X r] by blast qed text \The orbits of an equivalence relation are nothing but its equivalence classes. In the context of measured group theory, we call them orbits.\ definition orbit :: "'a set => ('a \ 'a) set => 'a => 'a set " where "orbit X r x = " (*Complete this definition!*) text \If two elements are related, then their orbits are the same. We first show one inclusion and then show equality by using the inclusion lemma in both directions.\ lemma orbits_inclusion: fixes X r x y assumes eqrel: "is_equivalence_relation X r" and x_rel_y: "(x,y) \ r" shows "orbit X r x \ orbit X r y" proof fix z assume z_in_orbit: "z \ orbit X r x" show "z \ orbit X r y" proof - have y_rel_z: "(y,z) \ r" proof - have y_rel_x: "(y,x) \ r" using eqrel eqrel_symmetric_meta[of X] x_rel_y by simp (* Complete this proof *) qed moreover have "z \ X" using y_rel_z eqrel is_equivalence_relation_def by (auto simp add: is_relation_on_def) ultimately show "z \ orbit X r y" using orbit_def[of X r y] by simp qed qed lemma orbits_equal: fixes X r x y assumes eqrel: "is_equivalence_relation X r" and x_rel_y: "(x,y) \ r" shows "orbit X r x = orbit X r y" proof show "orbit X r x \ orbit X r y" using x_rel_y eqrel orbits_inclusion[of X] by simp show "orbit X r y \ orbit X r x" proof - (* Complete this proof *) qed qed end