equal
deleted
inserted
replaced
7 fun |
7 fun |
8 zeroable :: "rexp \<Rightarrow> bool" |
8 zeroable :: "rexp \<Rightarrow> bool" |
9 where |
9 where |
10 "zeroable (ZERO) \<longleftrightarrow> True" |
10 "zeroable (ZERO) \<longleftrightarrow> True" |
11 | "zeroable (ONE) \<longleftrightarrow> False" |
11 | "zeroable (ONE) \<longleftrightarrow> False" |
12 | "zeroable (CHAR c) \<longleftrightarrow> False" |
12 | "zeroable (CH c) \<longleftrightarrow> False" |
13 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2" |
13 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2" |
14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2" |
14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2" |
15 | "zeroable (STAR r) \<longleftrightarrow> False" |
15 | "zeroable (STAR r) \<longleftrightarrow> False" |
16 |
16 |
17 lemma zeroable_correctness: |
17 lemma zeroable_correctness: |
22 fun |
22 fun |
23 atmostempty :: "rexp \<Rightarrow> bool" |
23 atmostempty :: "rexp \<Rightarrow> bool" |
24 where |
24 where |
25 "atmostempty (ZERO) \<longleftrightarrow> True" |
25 "atmostempty (ZERO) \<longleftrightarrow> True" |
26 | "atmostempty (ONE) \<longleftrightarrow> True" |
26 | "atmostempty (ONE) \<longleftrightarrow> True" |
27 | "atmostempty (CHAR c) \<longleftrightarrow> False" |
27 | "atmostempty (CH 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 |
32 |
35 fun |
35 fun |
36 somechars :: "rexp \<Rightarrow> bool" |
36 somechars :: "rexp \<Rightarrow> bool" |
37 where |
37 where |
38 "somechars (ZERO) \<longleftrightarrow> False" |
38 "somechars (ZERO) \<longleftrightarrow> False" |
39 | "somechars (ONE) \<longleftrightarrow> False" |
39 | "somechars (ONE) \<longleftrightarrow> False" |
40 | "somechars (CHAR c) \<longleftrightarrow> True" |
40 | "somechars (CH c) \<longleftrightarrow> True" |
41 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2" |
41 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2" |
42 | "somechars (SEQ r1 r2) \<longleftrightarrow> |
42 | "somechars (SEQ r1 r2) \<longleftrightarrow> |
43 (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> |
43 (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> |
44 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
44 (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)" |
45 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
45 | "somechars (STAR r) \<longleftrightarrow> somechars r" |
67 fun |
67 fun |
68 leastsinglechar :: "rexp \<Rightarrow> bool" |
68 leastsinglechar :: "rexp \<Rightarrow> bool" |
69 where |
69 where |
70 "leastsinglechar (ZERO) \<longleftrightarrow> False" |
70 "leastsinglechar (ZERO) \<longleftrightarrow> False" |
71 | "leastsinglechar (ONE) \<longleftrightarrow> False" |
71 | "leastsinglechar (ONE) \<longleftrightarrow> False" |
72 | "leastsinglechar (CHAR c) \<longleftrightarrow> True" |
72 | "leastsinglechar (CH c) \<longleftrightarrow> True" |
73 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2" |
73 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2" |
74 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> |
74 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> |
75 (if (zeroable r1 \<or> zeroable r2) then False |
75 (if (zeroable r1 \<or> zeroable r2) then False |
76 else ((nullable r1 \<and> leastsinglechar r2) \<or> (nullable r2 \<and> leastsinglechar r1)))" |
76 else ((nullable r1 \<and> leastsinglechar r2) \<or> (nullable r2 \<and> leastsinglechar r1)))" |
77 | "leastsinglechar (STAR r) \<longleftrightarrow> leastsinglechar r" |
77 | "leastsinglechar (STAR r) \<longleftrightarrow> leastsinglechar r" |
94 fun |
94 fun |
95 infinitestrings :: "rexp \<Rightarrow> bool" |
95 infinitestrings :: "rexp \<Rightarrow> bool" |
96 where |
96 where |
97 "infinitestrings (ZERO) = False" |
97 "infinitestrings (ZERO) = False" |
98 | "infinitestrings (ONE) = False" |
98 | "infinitestrings (ONE) = False" |
99 | "infinitestrings (CHAR c) = False" |
99 | "infinitestrings (CH c) = False" |
100 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)" |
100 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)" |
101 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> |
101 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> |
102 (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)" |
102 (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)" |
103 | "infinitestrings (STAR r) = (\<not> atmostempty r)" |
103 | "infinitestrings (STAR r) = (\<not> atmostempty r)" |
104 |
104 |