equal
deleted
inserted
replaced
298 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
298 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
299 by (induct s arbitrary: r) |
299 by (induct s arbitrary: r) |
300 (simp_all add: nullable_correctness der_correctness Der_def) |
300 (simp_all add: nullable_correctness der_correctness Der_def) |
301 |
301 |
302 |
302 |
303 |
|
304 |
|
305 lemma bb: "A \<up> n ;; A\<star> \<subseteq> A\<star>" |
|
306 apply(induct n) |
|
307 apply(simp) |
|
308 apply(simp) |
|
309 apply(subst aa[symmetric]) |
|
310 apply(subst Seq_def) |
|
311 apply(auto) |
|
312 done |
|
313 |
|
314 lemma cc: "(\<Union>i\<in>{..n}. A \<up> i) ;; A\<star> \<subseteq> A\<star>" |
|
315 apply(induct n) |
|
316 apply(simp) |
|
317 apply(simp add: Suc_Union del: pow.simps) |
|
318 apply(simp only: seq_union) |
|
319 apply(rule Un_least) |
|
320 defer |
|
321 apply(simp) |
|
322 apply(rule bb) |
|
323 done |
|
324 |
|
325 lemma "A\<star> ;; A\<star> = A\<star>" |
|
326 apply(simp add: Seq_def) |
|
327 apply(rule subset_antisym) |
|
328 defer |
|
329 apply(auto)[1] |
|
330 apply(auto simp add: Star_def2) |
|
331 |
|
332 apply(subst (asm) Star_def2) |
|
333 apply(subst (asm) Star_def2) |
|
334 apply(auto) |
|
335 |
|
336 |
|
337 |
|
338 end |
303 end |