248 abbreviation |
248 abbreviation |
249 replicate_rev ("_ ^^^ _" [100, 100] 100) |
249 replicate_rev ("_ ^^^ _" [100, 100] 100) |
250 where |
250 where |
251 "a ^^^ n \<equiv> replicate n a" |
251 "a ^^^ n \<equiv> replicate n a" |
252 |
252 |
253 definition |
|
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
|
255 |
|
256 lemma an_bn_not_regular: |
253 lemma an_bn_not_regular: |
257 shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})" |
254 shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})" |
258 proof |
255 proof |
259 def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}" |
256 def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}" |
260 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
257 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
261 assume as: "regular A" |
258 assume as: "regular A" |
262 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
259 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
263 |
260 |
264 have length_test: "\<And>s. s \<in> A \<Longrightarrow> length_test s (CHR ''a'') (CHR ''b'')" |
261 have sameness: "\<And>i j. CHR ''a'' ^^^ i @ CHR ''b'' ^^^ j \<in> A \<longleftrightarrow> i = j" |
265 unfolding A_def length_test_def by auto |
262 unfolding A_def |
|
263 apply auto |
|
264 apply(drule_tac f="\<lambda>s. length (filter (op= (CHR ''a'')) s) = length (filter (op= (CHR ''b'')) s)" |
|
265 in arg_cong) |
|
266 apply(simp) |
|
267 done |
266 |
268 |
267 have b: "infinite B" |
269 have b: "infinite B" |
268 unfolding infinite_iff_countable_subset |
270 unfolding infinite_iff_countable_subset |
269 unfolding inj_on_def B_def |
271 unfolding inj_on_def B_def |
270 by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto) |
272 by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto) |
273 apply(auto) |
275 apply(auto) |
274 unfolding B_def |
276 unfolding B_def |
275 apply(auto) |
277 apply(auto) |
276 apply(simp add: str_eq_def) |
278 apply(simp add: str_eq_def) |
277 apply(drule_tac x="CHR ''b'' ^^^ n" in spec) |
279 apply(drule_tac x="CHR ''b'' ^^^ n" in spec) |
278 apply(subgoal_tac "CHR ''a'' ^^^ na @ CHR ''b'' ^^^ n \<notin> A") |
280 apply(simp add: sameness) |
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) |
|
284 apply(simp add: length_test_def) |
|
285 done |
281 done |
286 ultimately |
282 ultimately |
287 show "False" using continuation_lemma[OF as] by blast |
283 show "False" using continuation_lemma[OF as] by blast |
288 qed |
284 qed |
289 |
285 |