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 |
32 |
33 |
33 lemma "atmostempty r \<longrightarrow> (zeroable r \<or> nullable r)" |
|
34 apply(induct r) |
|
35 apply(auto) |
|
36 done |
34 |
37 |
35 fun |
38 fun |
36 somechars :: "rexp \<Rightarrow> bool" |
39 somechars :: "rexp \<Rightarrow> bool" |
37 where |
40 where |
38 "somechars (ZERO) \<longleftrightarrow> False" |
41 "somechars (ZERO) \<longleftrightarrow> False" |
39 | "somechars (ONE) \<longleftrightarrow> False" |
42 | "somechars (ONE) \<longleftrightarrow> False" |
40 | "somechars (CH c) \<longleftrightarrow> True" |
43 | "somechars (CH c) \<longleftrightarrow> True" |
41 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2" |
44 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2" |
42 | "somechars (SEQ r1 r2) \<longleftrightarrow> |
45 | "somechars (SEQ r1 r2) \<longleftrightarrow> |
43 (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> |
46 (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1)" |
44 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
|
45 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
47 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
46 |
48 |
47 lemma somechars_correctness: |
49 lemma somechars_correctness: |
48 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
50 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
49 apply(induct r) |
51 apply(induct r) |