22 "lang (Atom a) = {[a]}" | |
22 "lang (Atom a) = {[a]}" | |
23 "lang (Plus r s) = (lang r) Un (lang s)" | |
23 "lang (Plus r s) = (lang r) Un (lang s)" | |
24 "lang (Times r s) = conc (lang r) (lang s)" | |
24 "lang (Times r s) = conc (lang r) (lang s)" | |
25 "lang (Star r) = star(lang r)" |
25 "lang (Star r) = star(lang r)" |
26 |
26 |
27 primrec atoms :: "'a rexp \<Rightarrow> 'a set" |
27 primrec atoms :: "'a rexp \<Rightarrow> 'a set" where |
28 where |
|
29 "atoms Zero = {}" | |
28 "atoms Zero = {}" | |
30 "atoms One = {}" | |
29 "atoms One = {}" | |
31 "atoms (Atom a) = {a}" | |
30 "atoms (Atom a) = {a}" | |
32 "atoms (Plus r s) = atoms r \<union> atoms s" | |
31 "atoms (Plus r s) = atoms r \<union> atoms s" | |
33 "atoms (Times r s) = atoms r \<union> atoms s" | |
32 "atoms (Times r s) = atoms r \<union> atoms s" | |
34 "atoms (Star r) = atoms r" |
33 "atoms (Star r) = atoms r" |
35 |
34 |
|
35 primrec nullable :: "'a rexp \<Rightarrow> bool" where |
|
36 "nullable (Zero) = False" | |
|
37 "nullable (One) = True" | |
|
38 "nullable (Atom c) = False" | |
|
39 "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" | |
|
40 "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" | |
|
41 "nullable (Star r) = True" |
|
42 |
|
43 lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang r" |
|
44 by (induct r) (auto simp add: conc_def split: if_splits) |
|
45 |
36 end |
46 end |