equal
deleted
inserted
replaced
12 | CH char |
12 | CH char |
13 | SEQ rexp rexp |
13 | SEQ rexp rexp |
14 | ALT rexp rexp |
14 | ALT rexp rexp |
15 | STAR rexp |
15 | STAR rexp |
16 |
16 |
|
17 | AND rexp rexp |
17 | NOT rexp |
18 | NOT rexp |
18 | PLUS rexp |
19 | PLUS rexp |
19 | OPT rexp |
20 | OPT rexp |
20 | NTIMES rexp nat |
21 | NTIMES rexp nat |
21 | BETWEEN rexp nat nat |
22 | BETWEEN rexp nat nat |
133 "L (ZERO) = {}" |
134 "L (ZERO) = {}" |
134 | "L (ONE) = {[]}" |
135 | "L (ONE) = {[]}" |
135 | "L (CH c) = {[c]}" |
136 | "L (CH c) = {[c]}" |
136 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
137 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
137 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
138 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
139 | "L (AND r1 r2) = (L r1) \<inter> (L r2)" |
138 | "L (STAR r) = (L r)\<star>" |
140 | "L (STAR r) = (L r)\<star>" |
139 | "L (NOT r) = UNIV - (L r)" |
141 | "L (NOT r) = UNIV - (L r)" |
140 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
142 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
141 | "L (OPT r) = (L r) \<union> {[]}" |
143 | "L (OPT r) = (L r) \<union> {[]}" |
142 | "L (NTIMES r n) = (L r) \<up> n" |
144 | "L (NTIMES r n) = (L r) \<up> n" |
154 where |
156 where |
155 "nullable (ZERO) = False" |
157 "nullable (ZERO) = False" |
156 | "nullable (ONE) = True" |
158 | "nullable (ONE) = True" |
157 | "nullable (CH c) = False" |
159 | "nullable (CH c) = False" |
158 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
160 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
161 | "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)" |
159 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
162 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
160 | "nullable (STAR r) = True" |
163 | "nullable (STAR r) = True" |
161 | "nullable (NOT r) = (\<not>(nullable r))" |
164 | "nullable (NOT r) = (\<not>(nullable r))" |
162 | "nullable (PLUS r) = (nullable r)" |
165 | "nullable (PLUS r) = (nullable r)" |
163 | "nullable (OPT r) = True" |
166 | "nullable (OPT r) = True" |
170 where |
173 where |
171 "der c (ZERO) = ZERO" |
174 "der c (ZERO) = ZERO" |
172 | "der c (ONE) = ZERO" |
175 | "der c (ONE) = ZERO" |
173 | "der c (CH d) = (if c = d then ONE else ZERO)" |
176 | "der c (CH d) = (if c = d then ONE else ZERO)" |
174 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
177 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
178 | "der c (AND r1 r2) = AND (der c r1) (der c r2)" |
175 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else ZERO)" |
179 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else ZERO)" |
176 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
180 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
177 | "der c (NOT r) = NOT(der c r)" |
181 | "der c (NOT r) = NOT(der c r)" |
178 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
182 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
179 | "der c (OPT r) = der c r" |
183 | "der c (OPT r) = der c r" |
227 by auto |
231 by auto |
228 |
232 |
229 lemma Der_union [simp]: |
233 lemma Der_union [simp]: |
230 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
234 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
231 unfolding Der_def |
235 unfolding Der_def |
232 by auto |
236 by auto |
|
237 |
|
238 lemma Der_inter [simp]: |
|
239 shows "Der c (A \<inter> B) = Der c A \<inter> Der c B" |
|
240 unfolding Der_def |
|
241 by auto |
233 |
242 |
234 lemma Der_insert_nil [simp]: |
243 lemma Der_insert_nil [simp]: |
235 shows "Der c (insert [] A) = Der c A" |
244 shows "Der c (insert [] A) = Der c A" |
236 unfolding Der_def |
245 unfolding Der_def |
237 by auto |
246 by auto |
326 then show ?case |
335 then show ?case |
327 by (simp add: nullable_correctness) |
336 by (simp add: nullable_correctness) |
328 next |
337 next |
329 case (ALT r1 r2) |
338 case (ALT r1 r2) |
330 then show ?case by simp |
339 then show ?case by simp |
|
340 next |
|
341 case (AND r1 r2) |
|
342 then show ?case by(simp) |
331 next |
343 next |
332 case (STAR r) |
344 case (STAR r) |
333 then show ?case |
345 then show ?case |
334 by simp |
346 by simp |
335 next |
347 next |
381 lemma matcher_correctness: |
393 lemma matcher_correctness: |
382 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
394 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
383 by (induct s arbitrary: r) |
395 by (induct s arbitrary: r) |
384 (simp_all add: nullable_correctness der_correctness Der_def) |
396 (simp_all add: nullable_correctness der_correctness Der_def) |
385 |
397 |
|
398 |
|
399 lemma |
|
400 "L(AND r ZERO) = {}" and |
|
401 "L(AND r r) = L(r)" |
|
402 by(auto) |
|
403 |
|
404 |
386 end |
405 end |