equal
deleted
inserted
replaced
197 ultimately have "regular ({s} \<union> A)" by (rule closure_union) |
197 ultimately have "regular ({s} \<union> A)" by (rule closure_union) |
198 then show "regular (insert s A)" by simp |
198 then show "regular (insert s A)" by simp |
199 qed |
199 qed |
200 |
200 |
201 lemma cofinite_regular: |
201 lemma cofinite_regular: |
202 fixes A::"('a::finite list) set" |
202 fixes A::"'a::finite lang" |
203 assumes "finite (- A)" |
203 assumes "finite (- A)" |
204 shows "regular A" |
204 shows "regular A" |
205 proof - |
205 proof - |
206 from assms have "regular (- A)" by (simp add: finite_regular) |
206 from assms have "regular (- A)" by (simp add: finite_regular) |
207 then have "regular (-(- A))" by (rule closure_complement) |
207 then have "regular (-(- A))" by (rule closure_complement) |
276 |
276 |
277 assume as: "regular A" |
277 assume as: "regular A" |
278 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
278 def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}" |
279 have b: "infinite B" |
279 have b: "infinite B" |
280 unfolding infinite_iff_countable_subset |
280 unfolding infinite_iff_countable_subset |
281 apply(rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) |
281 unfolding inj_on_def B_def |
282 apply(auto simp add: inj_on_def B_def) |
282 by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto) |
283 done |
|
284 moreover |
283 moreover |
285 have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" |
284 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) |
285 apply(auto simp add: B_def A_def) |
287 apply(auto simp add: str_eq_def) |
286 apply(auto simp add: str_eq_def) |
288 apply(drule_tac x="CHR ''b'' ^^^ aa" in spec) |
287 apply(drule_tac x="CHR ''b'' ^^^ aa" in spec) |