60 definition |
60 definition |
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 |
|
66 lemma finite_range_image: |
|
67 assumes "finite (range f)" |
|
68 shows "finite (f ` A)" |
|
69 using assms unfolding image_def |
|
70 by (rule_tac finite_subset) (auto) |
|
71 |
|
72 lemma finite_eq_tag_rel: |
65 lemma finite_eq_tag_rel: |
73 assumes rng_fnt: "finite (range tag)" |
66 assumes rng_fnt: "finite (range tag)" |
74 shows "finite (UNIV // =tag=)" |
67 shows "finite (UNIV // =tag=)" |
75 proof - |
68 proof - |
76 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
69 let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)" |
77 -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *} |
70 -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *} |
78 have "finite (?f ` ?A)" |
71 have "finite (?f ` ?A)" |
79 proof - |
72 proof - |
80 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def) |
73 have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto |
81 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
74 moreover |
82 ultimately have "finite (range ?f)" |
75 have "finite (Pow (range tag))" using rng_fnt by simp |
83 by (auto simp only:image_def intro:finite_subset) |
76 ultimately |
84 from finite_range_image [OF this] show ?thesis . |
77 have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset) |
|
78 moreover |
|
79 have "?f ` ?A \<subseteq> range ?f" by auto |
|
80 ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset) |
85 qed |
81 qed |
86 moreover |
82 moreover |
87 -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *} |
83 -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *} |
88 have "inj_on ?f ?A" |
84 have "inj_on ?f ?A" |
89 proof - |
85 proof - |
90 { fix X Y |
86 { fix X Y |
91 assume X_in: "X \<in> ?A" |
87 assume X_in: "X \<in> ?A" |
92 and Y_in: "Y \<in> ?A" |
88 and Y_in: "Y \<in> ?A" |
93 and tag_eq: "?f X = ?f Y" |
89 and tag_eq: "?f X = ?f Y" |
|
90 then |
|
91 obtain x y |
|
92 where "x \<in> X" "y \<in> Y" "tag x = tag y" |
|
93 unfolding quotient_def Image_def image_def tag_eq_rel_def |
|
94 by (simp) (blast) |
|
95 with X_in Y_in |
94 have "X = Y" |
96 have "X = Y" |
95 proof - |
97 unfolding quotient_def tag_eq_rel_def by auto |
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 |
98 } then show "inj_on ?f ?A" unfolding inj_on_def by auto |
106 qed |
99 qed |
107 ultimately |
100 ultimately |
108 show "finite (UNIV // =tag=)" by (rule finite_imageD) |
101 show "finite (UNIV // =tag=)" by (rule finite_imageD) |
109 qed |
102 qed |
144 qed |
137 qed |
145 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
138 ultimately show "finite (UNIV // R2)" by (rule finite_imageD) |
146 qed |
139 qed |
147 |
140 |
148 lemma tag_finite_imageD: |
141 lemma tag_finite_imageD: |
149 fixes tag |
|
150 assumes rng_fnt: "finite (range tag)" |
142 assumes rng_fnt: "finite (range tag)" |
151 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |
143 and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>A n" |
152 and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" |
144 shows "finite (UNIV // \<approx>A)" |
153 -- {* And strings with same tag are equivalent *} |
145 proof (rule_tac refined_partition_finite [of "=tag="]) |
154 shows "finite (UNIV // (\<approx>Lang))" |
146 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) |
155 proof - |
147 next |
156 let ?R1 = "(=tag=)" |
148 from same_tag_eqvt |
157 show ?thesis |
149 show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def |
158 proof(rule_tac refined_partition_finite [of ?R1]) |
150 by auto |
159 from finite_eq_tag_rel [OF rng_fnt] |
151 next |
160 show "finite (UNIV // =tag=)" . |
152 show "equiv UNIV =tag=" |
161 next |
153 unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def |
162 from same_tag_eqvt |
154 by auto |
163 show "(=tag=) \<subseteq> (\<approx>Lang)" |
155 next |
164 by (auto simp:tag_eq_rel_def str_eq_def) |
156 show "equiv UNIV (\<approx>A)" |
165 next |
157 unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def |
166 show "equiv UNIV (=tag=)" |
158 by blast |
167 unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def |
159 qed |
168 by auto |
160 |
169 next |
|
170 show "equiv UNIV (\<approx>Lang)" |
|
171 unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def |
|
172 by blast |
|
173 qed |
|
174 qed |
|
175 |
|
176 text {* |
|
177 A more concise, but less intelligible argument for @{text "tag_finite_imageD"} |
|
178 is given as the following. The basic idea is still using standard library |
|
179 lemma @{thm [source] "finite_imageD"}: |
|
180 \[ |
|
181 @{thm "finite_imageD" [no_vars]} |
|
182 \] |
|
183 which says: if the image of injective function @{text "f"} over set @{text "A"} is |
|
184 finite, then @{text "A"} must be finte, as we did in the lemmas above. |
|
185 *} |
|
186 |
|
187 lemma |
|
188 fixes tag |
|
189 assumes rng_fnt: "finite (range tag)" |
|
190 -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} |
|
191 and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" |
|
192 -- {* And strings with same tag are equivalent *} |
|
193 shows "finite (UNIV // (\<approx>Lang))" |
|
194 -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *} |
|
195 proof - |
|
196 -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*} |
|
197 let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>Lang)" |
|
198 show ?thesis |
|
199 proof (rule_tac f = "?f" and A = ?A in finite_imageD) |
|
200 -- {* |
|
201 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
|
202 *} |
|
203 show "finite (?f ` ?A)" |
|
204 proof - |
|
205 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def) |
|
206 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
|
207 ultimately have "finite (range ?f)" |
|
208 by (auto simp only:image_def intro:finite_subset) |
|
209 from finite_range_image [OF this] show ?thesis . |
|
210 qed |
|
211 next |
|
212 -- {* |
|
213 The injectivity of @{text "f"} is the consequence of assumption @{text "same_tag_eqvt"}: |
|
214 *} |
|
215 show "inj_on ?f ?A" |
|
216 proof- |
|
217 { fix X Y |
|
218 assume X_in: "X \<in> ?A" |
|
219 and Y_in: "Y \<in> ?A" |
|
220 and tag_eq: "?f X = ?f Y" |
|
221 have "X = Y" |
|
222 proof - |
|
223 from X_in Y_in tag_eq |
|
224 obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
|
225 unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def |
|
226 apply simp by blast |
|
227 from same_tag_eqvt [OF eq_tg] have "x \<approx>Lang y" . |
|
228 with X_in Y_in x_in y_in |
|
229 show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def) |
|
230 qed |
|
231 } thus ?thesis unfolding inj_on_def by auto |
|
232 qed |
|
233 qed |
|
234 qed |
|
235 |
161 |
236 subsection {* The proof*} |
162 subsection {* The proof*} |
237 |
163 |
238 text {* |
164 text {* |
239 Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by |
165 Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by |
332 subsubsection {* The inductive case for @{const ALT} *} |
258 subsubsection {* The inductive case for @{const ALT} *} |
333 |
259 |
334 definition |
260 definition |
335 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
261 tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)" |
336 where |
262 where |
337 "tag_str_ALT L1 L2 \<equiv> (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))" |
263 "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))" |
338 |
264 |
339 lemma quot_union_finiteI [intro]: |
265 lemma quot_union_finiteI [intro]: |
340 fixes L1 L2::"lang" |
266 fixes L1 L2::"lang" |
341 assumes finite1: "finite (UNIV // \<approx>L1)" |
267 assumes finite1: "finite (UNIV // \<approx>A)" |
342 and finite2: "finite (UNIV // \<approx>L2)" |
268 and finite2: "finite (UNIV // \<approx>B)" |
343 shows "finite (UNIV // \<approx>(L1 \<union> L2))" |
269 shows "finite (UNIV // \<approx>(A \<union> B))" |
344 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD) |
270 proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD) |
345 show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y" |
271 have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" |
|
272 using finite1 finite2 by auto |
|
273 then show "finite (range (tag_str_ALT A B))" |
|
274 unfolding tag_str_ALT_def quotient_def |
|
275 by (rule rev_finite_subset) (auto) |
|
276 next |
|
277 show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y" |
346 unfolding tag_str_ALT_def |
278 unfolding tag_str_ALT_def |
347 unfolding str_eq_def |
279 unfolding str_eq_def |
348 unfolding Image_def |
|
349 unfolding str_eq_rel_def |
280 unfolding str_eq_rel_def |
350 by auto |
|
351 next |
|
352 have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" |
|
353 using finite1 finite2 by auto |
|
354 show "finite (range (tag_str_ALT L1 L2))" |
|
355 unfolding tag_str_ALT_def |
|
356 apply(rule finite_subset[OF _ *]) |
|
357 unfolding quotient_def |
|
358 by auto |
281 by auto |
359 qed |
282 qed |
360 |
283 |
361 subsubsection {* The inductive case for @{text "SEQ"}*} |
284 subsubsection {* The inductive case for @{text "SEQ"}*} |
362 |
285 |