61 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
61 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
62 where |
62 where |
63 "=tag= \<equiv> {(x, y) | x y. tag x = tag y}" |
63 "=tag= \<equiv> {(x, y) | x y. tag x = tag y}" |
64 |
64 |
65 |
65 |
66 lemma equiv_tag_eq_rel:"equiv UNIV (=f=)" |
|
67 by (auto simp:equiv_def tag_eq_rel_def refl_on_def sym_def trans_def) |
|
68 |
|
69 lemma finite_range_image: |
66 lemma finite_range_image: |
70 assumes "finite (range f)" |
67 assumes "finite (range f)" |
71 shows "finite (f ` A)" |
68 shows "finite (f ` A)" |
72 using assms unfolding image_def |
69 using assms unfolding image_def |
73 by (rule_tac finite_subset) (auto) |
70 by (rule_tac finite_subset) (auto) |
74 |
71 |
75 thm finite_imageD |
|
76 |
|
77 lemma finite_eq_tag_rel: |
72 lemma finite_eq_tag_rel: |
78 assumes rng_fnt: "finite (range tag)" |
73 assumes rng_fnt: "finite (range tag)" |
79 shows "finite (UNIV // =tag=)" |
74 shows "finite (UNIV // =tag=)" |
80 proof - |
75 proof - |
81 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
76 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
82 show ?thesis |
77 -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *} |
83 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
78 have "finite (?f ` ?A)" |
84 -- {* |
79 proof - |
85 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
80 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def) |
86 *} |
81 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
87 show "finite (?f ` ?A)" |
82 ultimately have "finite (range ?f)" |
88 proof - |
83 by (auto simp only:image_def intro:finite_subset) |
89 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def) |
84 from finite_range_image [OF this] show ?thesis . |
90 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
|
91 ultimately have "finite (range ?f)" |
|
92 by (auto simp only:image_def intro:finite_subset) |
|
93 from finite_range_image [OF this] show ?thesis . |
|
94 qed |
|
95 next |
|
96 -- {* |
|
97 The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: |
|
98 *} |
|
99 show "inj_on ?f ?A" |
|
100 proof - |
|
101 { fix X Y |
|
102 assume X_in: "X \<in> ?A" |
|
103 and Y_in: "Y \<in> ?A" |
|
104 and tag_eq: "?f X = ?f Y" |
|
105 have "X = Y" |
|
106 proof - |
|
107 from X_in Y_in tag_eq |
|
108 obtain x y |
|
109 where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
|
110 unfolding quotient_def Image_def str_eq_rel_def |
|
111 str_eq_def image_def tag_eq_rel_def |
|
112 apply simp by blast |
|
113 with X_in Y_in show "X = Y" |
|
114 unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def |
|
115 by auto |
|
116 qed |
|
117 } thus ?thesis unfolding inj_on_def by auto |
|
118 qed |
|
119 qed |
85 qed |
120 qed |
86 moreover |
121 |
87 -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *} |
122 lemma finite_image_finite: |
88 have "inj_on ?f ?A" |
123 "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)" |
89 proof - |
124 by (rule finite_subset [of _ B], auto) |
90 { fix X Y |
|
91 assume X_in: "X \<in> ?A" |
|
92 and Y_in: "Y \<in> ?A" |
|
93 and tag_eq: "?f X = ?f Y" |
|
94 have "X = Y" |
|
95 proof - |
|
96 from X_in Y_in tag_eq |
|
97 obtain x y |
|
98 where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
|
99 unfolding quotient_def Image_def image_def tag_eq_rel_def |
|
100 by (simp) (blast) |
|
101 with X_in Y_in show "X = Y" |
|
102 unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def |
|
103 by auto |
|
104 qed |
|
105 } then show "inj_on ?f ?A" unfolding inj_on_def by auto |
|
106 qed |
|
107 ultimately |
|
108 show "finite (UNIV // =tag=)" by (rule finite_imageD) |
|
109 qed |
125 |
110 |
126 lemma refined_partition_finite: |
111 lemma refined_partition_finite: |
127 fixes R1 R2 A |
112 assumes fnt: "finite (UNIV // R1)" |
128 assumes fnt: "finite (A // R1)" |
|
129 and refined: "R1 \<subseteq> R2" |
113 and refined: "R1 \<subseteq> R2" |
130 and eq1: "equiv A R1" and eq2: "equiv A R2" |
114 and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2" |
131 shows "finite (A // R2)" |
115 shows "finite (UNIV // R2)" |
132 proof - |
116 proof - |
133 let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" |
117 let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}" |
134 and ?A = "(A // R2)" and ?B = "(A // R1)" |
118 and ?A = "UNIV // R2" and ?B = "UNIV // R1" |
135 show ?thesis |
119 have "?f ` ?A \<subseteq> Pow ?B" |
136 proof(rule_tac f = ?f and A = ?A in finite_imageD) |
120 unfolding image_def Pow_def quotient_def by auto |
137 show "finite (?f ` ?A)" |
121 moreover |
138 proof(rule finite_subset [of _ "Pow ?B"]) |
122 have "finite (Pow ?B)" using fnt by simp |
139 from fnt show "finite (Pow (A // R1))" by simp |
123 ultimately |
140 next |
124 have "finite (?f ` ?A)" by (rule finite_subset) |
141 from eq2 |
125 moreover |
142 show " ?f ` A // R2 \<subseteq> Pow ?B" |
126 have "inj_on ?f ?A" |
143 unfolding image_def Pow_def quotient_def |
127 proof - |
144 apply auto |
128 { fix X Y |
145 by (rule_tac x = xb in bexI, simp, |
129 assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y" |
146 unfold equiv_def sym_def refl_on_def, blast) |
130 from quotientE [OF X_in] |
147 qed |
131 obtain x where "X = R2 `` {x}" by blast |
148 next |
132 with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp |
149 show "inj_on ?f ?A" |
133 then have "R1 ``{x} \<in> ?f X" by auto |
150 proof - |
134 with eq_f have "R1 `` {x} \<in> ?f Y" by simp |
151 { fix X Y |
135 then obtain y |
152 assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" |
136 where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto |
153 and eq_f: "?f X = ?f Y" (is "?L = ?R") |
137 with eq_equiv_class[OF _ eq1] |
154 have "X = Y" using X_in |
138 have "(x, y) \<in> R1" by blast |
155 proof(rule quotientE) |
139 with refined have "(x, y) \<in> R2" by auto |
156 fix x |
140 with quotient_eqI [OF eq2 X_in Y_in x_in y_in] |
157 assume "X = R2 `` {x}" and "x \<in> A" with eq2 |
141 have "X = Y" . |
158 have x_in: "x \<in> X" |
142 } |
159 unfolding equiv_def quotient_def refl_on_def by auto |
143 then show "inj_on ?f ?A" unfolding inj_on_def by blast |
160 with eq_f have "R1 `` {x} \<in> ?R" by auto |
|
161 then obtain y where |
|
162 y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto |
|
163 have "(x, y) \<in> R1" |
|
164 proof - |
|
165 from x_in X_in y_in Y_in eq2 |
|
166 have "x \<in> A" and "y \<in> A" |
|
167 unfolding equiv_def quotient_def refl_on_def by auto |
|
168 from eq_equiv_class_iff [OF eq1 this] and eq_r |
|
169 show ?thesis by simp |
|
170 qed |
|
171 with refined have xy_r2: "(x, y) \<in> R2" by auto |
|
172 from quotient_eqI [OF eq2 X_in Y_in x_in y_in this] |
|
173 show ?thesis . |
|
174 qed |
|
175 } thus ?thesis by (auto simp:inj_on_def) |
|
176 qed |
|
177 qed |
144 qed |
178 qed |
145 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
179 |
146 qed |
180 lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)" |
|
181 unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def |
|
182 by blast |
|
183 |
147 |
184 lemma tag_finite_imageD: |
148 lemma tag_finite_imageD: |
185 fixes tag |
149 fixes tag |
186 assumes rng_fnt: "finite (range tag)" |
150 assumes rng_fnt: "finite (range tag)" |
187 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |
151 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |