equal
deleted
inserted
replaced
69 by (auto simp add: Der_def) |
69 by (auto simp add: Der_def) |
70 |
70 |
71 lemma Der_Sequ [simp]: |
71 lemma Der_Sequ [simp]: |
72 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
72 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
73 unfolding Der_def Sequ_def |
73 unfolding Der_def Sequ_def |
74 by (auto simp add: Cons_eq_append_conv) |
74 by (auto simp add: Cons_eq_append_conv) |
75 |
75 |
76 |
76 |
77 section {* Kleene Star for Languages *} |
77 section {* Kleene Star for Languages *} |
78 |
78 |
79 inductive_set |
79 inductive_set |
235 | "L (ONE) = {[]}" |
235 | "L (ONE) = {[]}" |
236 | "L (CHAR c) = {[c]}" |
236 | "L (CHAR c) = {[c]}" |
237 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
237 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
238 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
238 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
239 | "L (STAR r) = (L r)\<star>" |
239 | "L (STAR r) = (L r)\<star>" |
240 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
240 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)" |
241 | "L (NTIMES r n) = (L r) \<up> n" |
241 | "L (NTIMES r n) = (L r) \<up> n" |
242 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
242 | "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)" |
243 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
243 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
244 |
244 |
245 section {* Nullable, Derivatives *} |
245 section {* Nullable, Derivatives *} |
246 |
246 |
247 fun |
247 fun |
364 |
364 |
365 lemma ders_correctness: |
365 lemma ders_correctness: |
366 shows "L (ders s r) = Ders s (L r)" |
366 shows "L (ders s r) = Ders s (L r)" |
367 by (induct s arbitrary: r) |
367 by (induct s arbitrary: r) |
368 (simp_all add: Ders_def der_correctness Der_def) |
368 (simp_all add: Ders_def der_correctness Der_def) |
369 |
|
370 |
369 |
371 |
370 |
372 section {* Values *} |
371 section {* Values *} |
373 |
372 |
374 datatype val = |
373 datatype val = |
1420 apply(simp) |
1419 apply(simp) |
1421 apply(drule_tac x="va" in meta_spec) |
1420 apply(drule_tac x="va" in meta_spec) |
1422 apply(drule_tac x="vs" in meta_spec) |
1421 apply(drule_tac x="vs" in meta_spec) |
1423 apply(simp) |
1422 apply(simp) |
1424 apply(drule meta_mp) |
1423 apply(drule meta_mp) |
1425 apply (smt L.simps(10) Posix1(1) Posix1(2) Posix_NMTIMES1.hyps(4) UN_E append.right_neutral |
1424 apply(drule Posix1(1)) |
1426 append_eq_append_conv2 diff_Suc_1 val.inject(5)) |
1425 apply(drule Posix1(1)) |
|
1426 apply(drule Posix1(1)) |
|
1427 apply(frule Posix1(1)) |
|
1428 apply(simp) |
|
1429 using Posix_NMTIMES1.hyps(4) apply force |
1427 apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2) |
1430 apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2) |
1428 by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil) |
1431 by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil) |
1429 moreover |
1432 moreover |
1430 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1433 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1431 "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1434 "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |