42 have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z]) |
42 have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z]) |
43 with P show ?thesis unfolding proj_def[abs_def] by auto |
43 with P show ?thesis unfolding proj_def[abs_def] by auto |
44 qed |
44 qed |
45 |
45 |
46 (* Operators: *) |
46 (* Operators: *) |
47 definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}" |
|
48 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
47 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
49 |
48 |
50 lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A" |
49 |
51 unfolding diag_def by simp |
50 lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b" |
52 |
51 unfolding Id_on_def by simp |
53 lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b" |
52 |
54 unfolding diag_def by simp |
53 lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x" |
55 |
54 unfolding Id_on_def by auto |
56 lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x" |
55 |
57 unfolding diag_def by auto |
56 lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A" |
58 |
57 unfolding Id_on_def by auto |
59 lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A" |
58 |
60 unfolding diag_def by auto |
59 lemma Id_on_UNIV: "Id_on UNIV = Id" |
61 |
60 unfolding Id_on_def by auto |
62 lemma diag_UNIV: "diag UNIV = Id" |
61 |
63 unfolding diag_def by auto |
62 lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A" |
64 |
63 unfolding Id_on_def by auto |
65 lemma diag_converse: "diag A = (diag A) ^-1" |
64 |
66 unfolding diag_def by auto |
65 lemma Id_on_Gr: "Id_on A = Gr A id" |
67 |
66 unfolding Id_on_def Gr_def by auto |
68 lemma diag_Comp: "diag A = diag A O diag A" |
67 |
69 unfolding diag_def by auto |
68 lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV" |
70 |
69 unfolding Id_on_def by auto |
71 lemma diag_Gr: "diag A = Gr A id" |
|
72 unfolding diag_def Gr_def by simp |
|
73 |
|
74 lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV" |
|
75 unfolding diag_def by auto |
|
76 |
70 |
77 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
71 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
78 unfolding image2_def by auto |
72 unfolding image2_def by auto |
79 |
73 |
80 lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}" |
74 lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}" |
120 |
114 |
121 lemma relInvImage_mono: |
115 lemma relInvImage_mono: |
122 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
116 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
123 unfolding relInvImage_def by auto |
117 unfolding relInvImage_def by auto |
124 |
118 |
125 lemma relInvImage_diag: |
119 lemma relInvImage_Id_on: |
126 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id" |
120 "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id" |
127 unfolding relInvImage_def diag_def by auto |
121 unfolding relInvImage_def Id_on_def by auto |
128 |
122 |
129 lemma relInvImage_UNIV_relImage: |
123 lemma relInvImage_UNIV_relImage: |
130 "R \<subseteq> relInvImage UNIV (relImage R f) f" |
124 "R \<subseteq> relInvImage UNIV (relImage R f) f" |
131 unfolding relInvImage_def relImage_def by auto |
125 unfolding relInvImage_def relImage_def by auto |
132 |
126 |
133 lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})" |
127 lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})" |
134 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) |
128 unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) |
135 |
129 |
136 lemma relImage_proj: |
130 lemma relImage_proj: |
137 assumes "equiv A R" |
131 assumes "equiv A R" |
138 shows "relImage R (proj R) \<subseteq> diag (A//R)" |
132 shows "relImage R (proj R) \<subseteq> Id_on (A//R)" |
139 unfolding relImage_def diag_def apply safe |
133 unfolding relImage_def Id_on_def |
140 using proj_iff[OF assms] |
134 using proj_iff[OF assms] equiv_class_eq_iff[OF assms] |
141 by (metis assms equiv_Image proj_def proj_preserves) |
135 by (auto simp: proj_preserves) |
142 |
136 |
143 lemma relImage_relInvImage: |
137 lemma relImage_relInvImage: |
144 assumes "R \<subseteq> f ` A <*> f ` A" |
138 assumes "R \<subseteq> f ` A <*> f ` A" |
145 shows "relImage (relInvImage A R f) f = R" |
139 shows "relImage (relInvImage A R f) f = R" |
146 using assms unfolding relImage_def relInvImage_def by fastforce |
140 using assms unfolding relImage_def relInvImage_def by fastforce |