251 "a ^^^ n \<equiv> replicate n a" |
251 "a ^^^ n \<equiv> replicate n a" |
252 |
252 |
253 definition |
253 definition |
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
255 |
255 |
256 lemma length_test: |
|
257 "x = y \<Longrightarrow> length_test x a b = length_test y a b" |
|
258 by simp |
|
259 |
|
260 lemma an_bn_not_regular: |
256 lemma an_bn_not_regular: |
261 shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})" |
257 shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})" |
262 proof |
258 proof |
263 def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}" |
259 def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}" |
264 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
260 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
265 |
|
266 assume as: "regular A" |
261 assume as: "regular A" |
267 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
262 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
|
263 |
|
264 have length_test: "\<And>s. s \<in> A \<Longrightarrow> length_test s (CHR ''a'') (CHR ''b'')" |
|
265 unfolding A_def length_test_def by auto |
|
266 |
268 have b: "infinite B" |
267 have b: "infinite B" |
269 unfolding infinite_iff_countable_subset |
268 unfolding infinite_iff_countable_subset |
270 unfolding inj_on_def B_def |
269 unfolding inj_on_def B_def |
271 by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto) |
270 by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto) |
272 moreover |
271 moreover |
273 have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" |
272 have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" |
274 apply(auto simp add: B_def A_def) |
|
275 apply(auto simp add: str_eq_def) |
|
276 apply(drule_tac x="CHR ''b'' ^^^ aa" in spec) |
|
277 apply(auto) |
273 apply(auto) |
278 apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test) |
274 unfolding B_def |
|
275 apply(auto) |
|
276 apply(simp add: str_eq_def) |
|
277 apply(drule_tac x="CHR ''b'' ^^^ n" in spec) |
|
278 apply(subgoal_tac "CHR ''a'' ^^^ na @ CHR ''b'' ^^^ n \<notin> A") |
|
279 apply(subgoal_tac "CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n \<in> A") |
|
280 apply(blast) |
|
281 apply(auto simp add: A_def)[1] |
|
282 apply(rule notI) |
|
283 apply(drule length_test) |
279 apply(simp add: length_test_def) |
284 apply(simp add: length_test_def) |
280 done |
285 done |
281 ultimately |
286 ultimately |
282 show "False" using continuation_lemma[OF as] by blast |
287 show "False" using continuation_lemma[OF as] by blast |
283 qed |
288 qed |