equal
deleted
inserted
replaced
27 | "atmostempty (CHAR c) \<longleftrightarrow> False" |
27 | "atmostempty (CHAR c) \<longleftrightarrow> False" |
28 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2" |
28 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2" |
29 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> |
29 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> |
30 zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)" |
30 zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)" |
31 | "atmostempty (STAR r) = atmostempty r" |
31 | "atmostempty (STAR r) = atmostempty r" |
|
32 |
|
33 |
32 |
34 |
33 fun |
35 fun |
34 somechars :: "rexp \<Rightarrow> bool" |
36 somechars :: "rexp \<Rightarrow> bool" |
35 where |
37 where |
36 "somechars (ZERO) \<longleftrightarrow> False" |
38 "somechars (ZERO) \<longleftrightarrow> False" |
48 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
50 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
49 using Nil_is_append_conv apply blast |
51 using Nil_is_append_conv apply blast |
50 apply blast |
52 apply blast |
51 apply(auto) |
53 apply(auto) |
52 using Star_cstring |
54 using Star_cstring |
53 by (metis concat_eq_Nil_conv) |
55 by (metis concat_eq_Nil_conv) |
54 |
|
55 |
56 |
56 lemma atmostempty_correctness_aux: |
57 lemma atmostempty_correctness_aux: |
57 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
58 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
58 apply(induct r) |
59 apply(induct r) |
59 apply(simp_all) |
60 apply(simp_all) |
61 done |
62 done |
62 |
63 |
63 lemma atmostempty_correctness: |
64 lemma atmostempty_correctness: |
64 shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}" |
65 shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}" |
65 by(auto simp add: atmostempty_correctness_aux somechars_correctness) |
66 by(auto simp add: atmostempty_correctness_aux somechars_correctness) |
|
67 |
|
68 fun |
|
69 leastsinglechar :: "rexp \<Rightarrow> bool" |
|
70 where |
|
71 "leastsinglechar (ZERO) \<longleftrightarrow> False" |
|
72 | "leastsinglechar (ONE) \<longleftrightarrow> False" |
|
73 | "leastsinglechar (CHAR c) \<longleftrightarrow> True" |
|
74 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2" |
|
75 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> |
|
76 (if (zeroable r1 \<or> zeroable r2) then False |
|
77 else ((nullable r1 \<and> leastsinglechar r2) \<or> (nullable r2 \<and> leastsinglechar r1)))" |
|
78 | "leastsinglechar (STAR r) \<longleftrightarrow> leastsinglechar r" |
|
79 |
|
80 lemma leastsinglechar_correctness: |
|
81 "leastsinglechar r \<longleftrightarrow> (\<exists>c. [c] \<in> L r)" |
|
82 apply(induct r) |
|
83 apply(simp) |
|
84 apply(simp) |
|
85 apply(simp) |
|
86 prefer 2 |
|
87 apply(simp) |
|
88 apply(blast) |
|
89 prefer 2 |
|
90 apply(simp) |
|
91 using Star.step Star_decomp apply fastforce |
|
92 apply(simp add: Sequ_def zeroable_correctness nullable_correctness) |
|
93 by (metis append_Nil append_is_Nil_conv butlast_append butlast_snoc) |
66 |
94 |
67 fun |
95 fun |
68 infinitestrings :: "rexp \<Rightarrow> bool" |
96 infinitestrings :: "rexp \<Rightarrow> bool" |
69 where |
97 where |
70 "infinitestrings (ZERO) = False" |
98 "infinitestrings (ZERO) = False" |