equal
deleted
inserted
replaced
207 then have "regular (-(- A))" by (rule closure_complement) |
207 then have "regular (-(- A))" by (rule closure_complement) |
208 then show "regular A" by simp |
208 then show "regular A" by simp |
209 qed |
209 qed |
210 |
210 |
211 |
211 |
212 subsection {* Non-regularity for languages *} |
212 subsection {* Continuation lemma for showing non-regularity of languages *} |
213 |
213 |
214 lemma continuation_lemma: |
214 lemma continuation_lemma: |
215 fixes A B::"'a::finite lang" |
215 fixes A B::"'a::finite lang" |
216 assumes reg: "regular A" |
216 assumes reg: "regular A" |
217 and inf: "infinite B" |
217 and inf: "infinite B" |
241 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" |
242 by blast |
242 by blast |
243 qed |
243 qed |
244 |
244 |
245 |
245 |
246 subsubsection {* The language @{text "a ^ n b ^ n"} is not regular *} |
246 subsection {* The language @{text "a\<^sup>n b\<^sup>n"} is not regular *} |
247 |
247 |
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" |