(* 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