56 is finite (lemma @{text "tag_finite_imageD"}). |
56 is finite (lemma @{text "tag_finite_imageD"}). |
57 \end{enumerate} |
57 \end{enumerate} |
58 *} |
58 *} |
59 |
59 |
60 definition |
60 definition |
61 f_eq_rel ("=_=") |
61 tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=") |
62 where |
62 where |
63 "=f= \<equiv> {(x, y) | x y. f x = f y}" |
63 "=tag= \<equiv> {(x, y) | x y. tag x = tag y}" |
64 |
64 |
65 lemma equiv_f_eq_rel:"equiv UNIV (=f=)" |
65 |
66 by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def) |
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) |
67 |
68 |
68 lemma finite_range_image: |
69 lemma finite_range_image: |
69 assumes "finite (range f)" |
70 assumes "finite (range f)" |
70 shows "finite (f ` A)" |
71 shows "finite (f ` A)" |
71 using assms unfolding image_def |
72 using assms unfolding image_def |
72 by (rule_tac finite_subset) (auto) |
73 by (rule_tac finite_subset) (auto) |
73 |
74 |
74 lemma finite_eq_f_rel: |
75 thm finite_imageD |
|
76 |
|
77 lemma finite_eq_tag_rel: |
75 assumes rng_fnt: "finite (range tag)" |
78 assumes rng_fnt: "finite (range tag)" |
76 shows "finite (UNIV // =tag=)" |
79 shows "finite (UNIV // =tag=)" |
77 proof - |
80 proof - |
78 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
81 let "?f" = "op ` tag" and ?A = "(UNIV // =tag=)" |
79 show ?thesis |
82 show ?thesis |
81 -- {* |
84 -- {* |
82 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
85 The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: |
83 *} |
86 *} |
84 show "finite (?f ` ?A)" |
87 show "finite (?f ` ?A)" |
85 proof - |
88 proof - |
86 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def) |
89 have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp: image_def Pow_def) |
87 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
90 moreover from rng_fnt have "finite (Pow (range tag))" by simp |
88 ultimately have "finite (range ?f)" |
91 ultimately have "finite (range ?f)" |
89 by (auto simp only:image_def intro:finite_subset) |
92 by (auto simp only:image_def intro:finite_subset) |
90 from finite_range_image [OF this] show ?thesis . |
93 from finite_range_image [OF this] show ?thesis . |
91 qed |
94 qed |
92 next |
95 next |
93 -- {* |
96 -- {* |
94 The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: |
97 The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: |
95 *} |
98 *} |
96 show "inj_on ?f ?A" |
99 show "inj_on ?f ?A" |
97 proof- |
100 proof - |
98 { fix X Y |
101 { fix X Y |
99 assume X_in: "X \<in> ?A" |
102 assume X_in: "X \<in> ?A" |
100 and Y_in: "Y \<in> ?A" |
103 and Y_in: "Y \<in> ?A" |
101 and tag_eq: "?f X = ?f Y" |
104 and tag_eq: "?f X = ?f Y" |
102 have "X = Y" |
105 have "X = Y" |
103 proof - |
106 proof - |
104 from X_in Y_in tag_eq |
107 from X_in Y_in tag_eq |
105 obtain x y |
108 obtain x y |
106 where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
109 where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" |
107 unfolding quotient_def Image_def str_eq_rel_def |
110 unfolding quotient_def Image_def str_eq_rel_def |
108 str_eq_def image_def f_eq_rel_def |
111 str_eq_def image_def tag_eq_rel_def |
109 apply simp by blast |
112 apply simp by blast |
110 with X_in Y_in show ?thesis |
113 with X_in Y_in show "X = Y" |
111 by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) |
114 unfolding quotient_def str_eq_rel_def str_eq_def tag_eq_rel_def |
|
115 by auto |
112 qed |
116 qed |
113 } thus ?thesis unfolding inj_on_def by auto |
117 } thus ?thesis unfolding inj_on_def by auto |
114 qed |
118 qed |
115 qed |
119 qed |
116 qed |
120 qed |
186 shows "finite (UNIV // (\<approx>Lang))" |
190 shows "finite (UNIV // (\<approx>Lang))" |
187 proof - |
191 proof - |
188 let ?R1 = "(=tag=)" |
192 let ?R1 = "(=tag=)" |
189 show ?thesis |
193 show ?thesis |
190 proof(rule_tac refined_partition_finite [of _ ?R1]) |
194 proof(rule_tac refined_partition_finite [of _ ?R1]) |
191 from finite_eq_f_rel [OF rng_fnt] |
195 from finite_eq_tag_rel [OF rng_fnt] |
192 show "finite (UNIV // =tag=)" . |
196 show "finite (UNIV // =tag=)" . |
193 next |
197 next |
194 from same_tag_eqvt |
198 from same_tag_eqvt |
195 show "(=tag=) \<subseteq> (\<approx>Lang)" |
199 show "(=tag=) \<subseteq> (\<approx>Lang)" |
196 by (auto simp:f_eq_rel_def str_eq_def) |
200 by (auto simp:tag_eq_rel_def str_eq_def) |
197 next |
201 next |
198 from equiv_f_eq_rel |
202 from equiv_tag_eq_rel |
199 show "equiv UNIV (=tag=)" by blast |
203 show "equiv UNIV (=tag=)" by blast |
200 next |
204 next |
201 from equiv_lang_eq |
205 from equiv_lang_eq |
202 show "equiv UNIV (\<approx>Lang)" by blast |
206 show "equiv UNIV (\<approx>Lang)" by blast |
203 qed |
207 qed |