equal
deleted
inserted
replaced
162 finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq |
162 finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq |
163 by simp |
163 by simp |
164 then show "regular (Deriv_lang B A)" by auto |
164 then show "regular (Deriv_lang B A)" by auto |
165 qed |
165 qed |
166 |
166 |
|
167 |
167 subsection {* Finite and co-finite sets are regular *} |
168 subsection {* Finite and co-finite sets are regular *} |
168 |
169 |
169 lemma singleton_regular: |
170 lemma singleton_regular: |
170 shows "regular {s}" |
171 shows "regular {s}" |
171 proof (induct s) |
172 proof (induct s) |
241 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
242 with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y" |
242 by blast |
243 by blast |
243 qed |
244 qed |
244 |
245 |
245 |
246 |
|
247 |
|
248 (* tests *) |
|
249 definition |
|
250 "quot A B \<equiv> {x. \<exists>y \<in> B. x @ y \<in> A}" |
|
251 |
|
252 definition |
|
253 "quot1 A B \<equiv> {x. \<exists>y \<in> B. y @ x \<in> A}" |
|
254 |
|
255 lemma |
|
256 "quot1 A B \<subseteq> Deriv_lang B A" |
|
257 unfolding quot1_def Derivs_def |
|
258 apply(auto) |
|
259 done |
|
260 |
|
261 lemma |
|
262 "rev ` quot1 A B \<subseteq> quot (rev ` A) (rev ` B)" |
|
263 unfolding quot_def quot1_def |
|
264 apply(auto) |
|
265 unfolding image_def |
|
266 apply(auto) |
|
267 apply(rule_tac x="y" in bexI) |
|
268 apply(rule_tac x="y @ xa" in bexI) |
|
269 apply(auto) |
|
270 done |
|
271 |
|
272 |
|
273 |
246 end |
274 end |