equal
deleted
inserted
replaced
1 theory Matcher |
1 theory Matcher |
2 imports "Main" |
2 imports "Main" |
3 begin |
3 begin |
|
4 |
4 |
5 |
5 section {* Regular Expressions *} |
6 section {* Regular Expressions *} |
6 |
7 |
7 datatype rexp = |
8 datatype rexp = |
8 NULL |
9 NULL |
80 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
81 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
81 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
82 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
82 | "nullable (STAR r) = True" |
83 | "nullable (STAR r) = True" |
83 |
84 |
84 fun |
85 fun |
|
86 noccurs :: "rexp \<Rightarrow> bool" |
|
87 where |
|
88 "noccurs (NULL) = True" |
|
89 | "noccurs (EMPTY) = False" |
|
90 | "noccurs (CHAR c) = False" |
|
91 | "noccurs (ALT r1 r2) = (noccurs r1 \<or> noccurs r2)" |
|
92 | "noccurs (SEQ r1 r2) = (noccurs r1 \<or> noccurs r2)" |
|
93 | "noccurs (STAR r) = (noccurs r)" |
|
94 |
|
95 lemma |
|
96 "\<not> noccurs r \<Longrightarrow> L r \<noteq> {}" |
|
97 apply(induct r) |
|
98 apply(auto simp add: Seq_def) |
|
99 done |
|
100 |
|
101 lemma |
|
102 "L r = {} \<Longrightarrow> noccurs r" |
|
103 apply(induct r) |
|
104 apply(auto simp add: Seq_def) |
|
105 done |
|
106 |
|
107 lemma does_not_hold: |
|
108 "noccurs r \<Longrightarrow> L r = {}" |
|
109 apply(induct r) |
|
110 apply(auto simp add: Seq_def) |
|
111 oops |
|
112 |
|
113 fun |
85 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
114 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
86 where |
115 where |
87 "der c (NULL) = NULL" |
116 "der c (NULL) = NULL" |
88 | "der c (EMPTY) = NULL" |
117 | "der c (EMPTY) = NULL" |
89 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)" |
118 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)" |
106 section {* Correctness Proof of the Matcher *} |
135 section {* Correctness Proof of the Matcher *} |
107 |
136 |
108 lemma nullable_correctness: |
137 lemma nullable_correctness: |
109 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
138 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
110 by (induct r) (auto simp add: Seq_def) |
139 by (induct r) (auto simp add: Seq_def) |
|
140 section {* Left-Quotient of a Set *} |
|
141 |
|
142 fun |
|
143 zeroable :: "rexp \<Rightarrow> bool" |
|
144 where |
|
145 "zeroable (NULL) = True" |
|
146 | "zeroable (EMPTY) = False" |
|
147 | "zeroable (CHAR c) = False" |
|
148 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)" |
|
149 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)" |
|
150 | "zeroable (STAR r) = False" |
|
151 |
|
152 |
|
153 lemma zeroable_correctness: |
|
154 shows "zeroable r \<longleftrightarrow> (L r = {})" |
|
155 apply(induct r) |
|
156 apply(auto simp add: Seq_def)[6] |
|
157 done |
|
158 |
111 section {* Left-Quotient of a Set *} |
159 section {* Left-Quotient of a Set *} |
112 |
160 |
113 definition |
161 definition |
114 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
162 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
115 where |
163 where |