211 |
210 |
212 |
211 |
213 subsection {* Non-regularity for languages *} |
212 subsection {* Non-regularity for languages *} |
214 |
213 |
215 lemma continuation_lemma: |
214 lemma continuation_lemma: |
216 fixes A B::"('a::finite list) set" |
215 fixes A B::"'a::finite lang" |
217 assumes reg: "regular A" |
216 assumes reg: "regular A" |
218 and inf: "infinite B" |
217 and inf: "infinite B" |
219 shows "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
218 shows "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
220 proof - |
219 proof - |
221 def eqfun \<equiv> "\<lambda>A x::('a::finite list). (\<approx>A) `` {x}" |
220 def eqfun \<equiv> "\<lambda>A x::('a::finite list). (\<approx>A) `` {x}" |
242 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
241 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
243 by blast |
242 by blast |
244 qed |
243 qed |
245 |
244 |
246 |
245 |
247 |
246 subsubsection {* The language @{text "a ^ n b ^ n"} is not regular *} |
248 (* tests *) |
247 |
|
248 abbreviation |
|
249 replicate_rev ("_ ^^^ _" [100, 100] 100) |
|
250 where |
|
251 "a ^^^ n \<equiv> replicate n a" |
|
252 |
249 definition |
253 definition |
250 "quot A B \<equiv> {x. \<exists>y \<in> B. x @ y \<in> A}" |
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
251 |
255 |
252 definition |
256 lemma [simp]: |
253 "quot1 A B \<equiv> {x. \<exists>y \<in> B. y @ x \<in> A}" |
257 assumes "i \<noteq> j" "a \<noteq> b" |
254 |
258 shows "length_test ((a ^^^ i) @ (b ^^^ j)) a b \<noteq> length_test ((a ^^^ n) @ (b ^^^ n)) a b" |
255 lemma |
259 using assms unfolding length_test_def by auto |
256 "quot1 A B \<subseteq> Deriv_lang B A" |
260 |
257 unfolding quot1_def Derivs_def |
261 lemma [simp]: |
258 apply(auto) |
262 assumes "a \<noteq> b" |
259 done |
263 shows "filter (op= a) ((a ^^^ i) @ (b ^^^ j)) = a ^^^ i" |
260 |
264 and "filter (op= b) ((a ^^^ i) @ (b ^^^ j)) = b ^^^ j" |
261 lemma |
265 using assms by simp_all |
262 "rev ` quot1 A B \<subseteq> quot (rev ` A) (rev ` B)" |
266 |
263 unfolding quot_def quot1_def |
267 lemma length_test: |
264 apply(auto) |
268 "x = y \<Longrightarrow> length_test x a b = length_test y a b" |
265 unfolding image_def |
269 by simp |
266 apply(auto) |
270 |
267 apply(rule_tac x="y" in bexI) |
271 lemma an_bn_not_regular: |
268 apply(rule_tac x="y @ xa" in bexI) |
272 shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})" |
269 apply(auto) |
273 proof |
270 done |
274 def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}" |
271 |
275 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
|
276 |
|
277 assume as: "regular A" |
|
278 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
|
279 have b: "infinite B" |
|
280 unfolding infinite_iff_countable_subset |
|
281 apply(rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) |
|
282 apply(auto simp add: inj_on_def B_def) |
|
283 done |
|
284 moreover |
|
285 have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" |
|
286 apply(auto simp add: B_def A_def) |
|
287 apply(auto simp add: str_eq_def) |
|
288 apply(drule_tac x="CHR ''b'' ^^^ aa" in spec) |
|
289 (*apply(auto simp add: f_def dest: l3)*) |
|
290 apply(auto) |
|
291 apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test) |
|
292 apply(simp add: length_test_def) |
|
293 done |
|
294 ultimately |
|
295 show "False" using continuation_lemma[OF as] by blast |
|
296 qed |
272 |
297 |
273 |
298 |
274 end |
299 end |