(* Title: RelRel_Iso.thy Author: Clara L\"oh *) text \We will prove that the intersection of a graph of a map and an inverse graph is the graph of an invertible map.\ theory RelRel_Iso imports Complex_Main begin section \Basic definitions\ text \First, we introduce basic notions and properties of graphs of functions:\ definition is_graph_of :: "'a rel => ('a => 'a) => bool" where "is_graph_of r f = (r = { (x, y) . x \ Domain r \ y = f x})" definition is_graph_of_fun :: "'a rel => bool" where "is_graph_of_fun r = (\ f. is_graph_of r f)" definition is_graph_of_inv_isos :: "'a rel => ('a => 'a) => ('a => 'a) => bool" where "is_graph_of_inv_isos r f g = (is_graph_of r f \ (\ x \ Domain r. (g o f) x = x) \ (\ x \ Range r. (f o g) x = x ))" definition is_graph_of_iso :: "'a rel => bool" where "is_graph_of_iso r = (\ f g. is_graph_of_inv_isos r f g)" lemma graphs_are_single_valued: fixes r f assumes gf: "is_graph_of r f" shows "single_valued r" proof (intro single_valuedI) fix x y z assume xy_in_r: "(x,y) \ r" and xz_in_r: "(x,z) \ r" show "y = z" proof - have "y = f x" using xy_in_r gf is_graph_of_def[of "r"] by auto moreover have "z = f x" using xz_in_r gf is_graph_of_def[of "r"] by auto ultimately show ?thesis by simp qed qed lemma graph_projection2: fixes r f x y assumes gf: "is_graph_of r f" and xy_in_r: "(x,y) \ r" shows "y = f x" proof - have "(x, f x) \ r" using gf xy_in_r is_graph_of_def[of r f] by auto then show ?thesis using xy_in_r gf graphs_are_single_valued[of r f] single_valuedD by auto qed lemma is_graph_of_inv_isosI: fixes r f g assumes gf: "is_graph_of r f" and gof: "\ x \ Domain r. (g o f) x = x" and fog: "\ x \ Range r. (f o g) x = x" shows "is_graph_of_inv_isos r f g" unfolding is_graph_of_inv_isos_def proof (intro conjI) show "is_graph_of r f" using gf . show "\ x \ Domain r. (g o f) x = x" using gof . show "\ x \ Range r. (f o g) x = x" using fog . qed lemma is_graph_of_isoI: fixes r f g assumes iso: "is_graph_of_inv_isos r f g" shows "is_graph_of_iso r" proof - from iso obtain f' g' where fg_def: "is_graph_of_inv_isos r f' g'" .. then show ?thesis using iso is_graph_of_iso_def[of "r"] by auto qed section \The explicit version\ text\The explicit version of the main claim; making the maps explicit has the advantage that it is easier to use this lemma in the future to establish additional properties of the maps.\ lemma intersections_of_graphs_lead_to_inv_isos: fixes r_1 :: "'a rel" and r_2 :: "'a rel" and r :: "'a rel" and f_1 f_2 assumes r_def: "r = r_1 \ r_2^-1" and graph_1: "is_graph_of r_1 f_1" and graph_2: "is_graph_of r_2 f_2" shows "is_graph_of_inv_isos r f_1 f_2" proof - define D :: "'a set" where "D = Domain r" define R :: "'a set" where "R = Range r" have rr1: "r \ r_1" using r_def by simp have rr2: "r \ r_2^-1" using r_def by simp have r_graph_f: "is_graph_of r f_1" unfolding is_graph_of_def proof define graph_f where "graph_f = {(x,y) . x \ Domain r \ y = f_1 x}" show "r \ graph_f" proof fix xy assume xy_in_r: "xy \ r" show "xy \ graph_f" proof - define x where "x = fst xy" define y where "y = snd xy" have xy_xy: "(x,y) = xy" using x_def y_def by (simp add: prod_eqI) have "y = f_1 x" proof - have "(x,y) \ r_1" using xy_in_r xy_xy rr1 by auto then show "y = f_1 x" using graph_1 is_graph_of_def[of "r_1" "f_1"] by auto qed moreover have "x \ Domain r" using xy_in_r xy_xy Domain_def by auto ultimately show "xy \ graph_f" using xy_xy graph_f_def by (auto simp add: prod_eqI) qed qed show "graph_f \ r" proof fix xy assume xy_in_gf: "xy \ graph_f" show "xy \ r" proof - define x where "x = fst xy" define y where "y = snd xy" have xy_xy: "(x,y) = xy" using x_def y_def by (simp add: prod_eqI) have xy_in_r1: "(x,y) \ r_1" proof - have "y = f_1 x" using xy_in_gf xy_xy graph_f_def by auto moreover have "x \ Domain r_1" using xy_in_gf xy_xy graph_f_def rr1 by auto ultimately show "(x,y) \ r_1" using graph_1 is_graph_of_def by auto qed have "x \ Domain r" using xy_in_gf x_def graph_f_def by auto then obtain "z" where z_def: "(x,z) \ r" using Domain_def by auto have "y = z" proof - have "(x,y) \ r_1" using xy_in_r1 by simp moreover have "(x,z) \ r_1" using z_def rr1 by auto ultimately show "y = z" using graph_1 graphs_are_single_valued[of "r_1"] single_valuedD[of "r_1"] by simp qed then have "(x,y) \ r" using z_def by simp then show "xy \ r" using xy_xy by simp qed qed qed have gof: "\ x \ D. (f_2 o f_1) x = x" proof (intro ballI) fix x :: 'a assume x_in_D: "x \ D" obtain y where y_def: "(x,y) \ r" using x_in_D D_def Domain_def by auto have y_f1_x: "y = f_1 x" proof - have "(x,y) \ r_1" using y_def rr1 by auto then show "y = f_1 x" using y_def rr1 graph_1 graph_projection2[of "r_1" "f_1"] by simp qed have x_f2_y: "x = f_2 y" proof - have "(y,x) \ r_2" using y_def rr2 by auto then show "x = f_2 y" using y_def rr2 graph_2 graph_projection2[of "r_2" "f_2"] by simp qed have "(f_2 o f_1) x = f_2 (f_1 (x))" by simp also have "... = f_2 (y)" using y_f1_x by simp finally show "(f_2 o f_1) x = x" using x_f2_y by simp qed have fog: "\ y \ R. (f_1 o f_2) y = y" proof (intro ballI) fix y :: 'a assume y_in_R: "y \ R" obtain x where x_def: "(x,y) \ r" using y_in_R R_def Range_def by auto have x_f2_y: "x = f_2 y" proof - have "(y,x) \ r_2" using x_def rr2 by auto then show "x = f_2 y" using x_def rr2 graph_2 graph_projection2[of "r_2" "f_2"] by simp qed have y_f1_x: "y = f_1 x" proof - have "(x,y) \ r_1" using x_def rr1 by auto then show "y = f_1 x" using x_def rr1 graph_1 graph_projection2[of "r_1" "f_1"] by simp qed have "(f_1 o f_2) y = f_1 (f_2 (y))" by simp also have "... = f_1 (x)" using x_f2_y by simp finally show "(f_1 o f_2) y = y" using y_f1_x by simp qed show "is_graph_of_inv_isos r f_1 f_2" using r_graph_f D_def R_def gof fog is_graph_of_inv_isosI[of "r" "f_1" "f_2"] by simp qed section \The non-explicit version\ text\The main statement: The intersection of a graph and an inverse graph is the graph of an isomorphism:\ theorem intersections_of_graphs_are_isos: fixes r_1 r_2 assumes graph_1: "is_graph_of_fun r_1" and graph_2: "is_graph_of_fun r_2" shows "is_graph_of_iso (r_1 \ r_2^-1)" proof - from graph_1 obtain f_1 where f1_def: "is_graph_of r_1 f_1" using is_graph_of_fun_def[of "r_1"] by auto from graph_2 obtain f_2 where f2_def: "is_graph_of r_2 f_2" using is_graph_of_fun_def[of "r_2"] by auto define r where "r = r_1 \ r_2^-1" have "is_graph_of_inv_isos r f_1 f_2" using r_def f1_def f2_def intersections_of_graphs_lead_to_inv_isos[of "r" "r_1" "r_2" "f_1" "f_2"] by simp then show ?thesis using is_graph_of_isoI[of "r" "f_1" "f_2"] r_def by auto qed end