equal
deleted
inserted
replaced
161 assumes "s \<in> A \<up> n" |
161 assumes "s \<in> A \<up> n" |
162 shows "s \<in> A\<star>" |
162 shows "s \<in> A\<star>" |
163 using assms |
163 using assms |
164 apply(induct n arbitrary: s) |
164 apply(induct n arbitrary: s) |
165 apply(auto simp add: Sequ_def) |
165 apply(auto simp add: Sequ_def) |
166 done |
166 done |
|
167 |
|
168 lemma |
|
169 assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}" |
|
170 shows "A \<up> (Suc n) = A \<up> n" |
167 |
171 |
168 lemma Der_Pow_0: |
172 lemma Der_Pow_0: |
169 shows "Der c (A \<up> 0) = {}" |
173 shows "Der c (A \<up> 0) = {}" |
170 by(simp add: Der_def) |
174 by(simp add: Der_def) |
171 |
175 |
223 | STAR rexp |
227 | STAR rexp |
224 | UPNTIMES rexp nat |
228 | UPNTIMES rexp nat |
225 | NTIMES rexp nat |
229 | NTIMES rexp nat |
226 | FROMNTIMES rexp nat |
230 | FROMNTIMES rexp nat |
227 | NMTIMES rexp nat nat |
231 | NMTIMES rexp nat nat |
|
232 | NOT rexp |
228 |
233 |
229 section {* Semantics of Regular Expressions *} |
234 section {* Semantics of Regular Expressions *} |
230 |
235 |
231 fun |
236 fun |
232 L :: "rexp \<Rightarrow> string set" |
237 L :: "rexp \<Rightarrow> string set" |
239 | "L (STAR r) = (L r)\<star>" |
244 | "L (STAR r) = (L r)\<star>" |
240 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)" |
245 | "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)" |
241 | "L (NTIMES r n) = (L r) \<up> n" |
246 | "L (NTIMES r n) = (L r) \<up> n" |
242 | "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)" |
247 | "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)" |
243 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
248 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
|
249 | "L (NOT r) = ((UNIV:: string set) - L r)" |
244 |
250 |
245 section {* Nullable, Derivatives *} |
251 section {* Nullable, Derivatives *} |
246 |
252 |
247 fun |
253 fun |
248 nullable :: "rexp \<Rightarrow> bool" |
254 nullable :: "rexp \<Rightarrow> bool" |
255 | "nullable (STAR r) = True" |
261 | "nullable (STAR r) = True" |
256 | "nullable (UPNTIMES r n) = True" |
262 | "nullable (UPNTIMES r n) = True" |
257 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
263 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
258 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
264 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
259 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
265 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
|
266 | "nullable (NOT r) = (\<not> nullable r)" |
260 |
267 |
261 fun |
268 fun |
262 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
269 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
263 where |
270 where |
264 "der c (ZERO) = ZERO" |
271 "der c (ZERO) = ZERO" |
279 | "der c (NMTIMES r n m) = |
286 | "der c (NMTIMES r n m) = |
280 (if m < n then ZERO |
287 (if m < n then ZERO |
281 else (if n = 0 then (if m = 0 then ZERO else |
288 else (if n = 0 then (if m = 0 then ZERO else |
282 SEQ (der c r) (UPNTIMES r (m - 1))) else |
289 SEQ (der c r) (UPNTIMES r (m - 1))) else |
283 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
290 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
|
291 | "der c (NOT r) = NOT (der c r)" |
284 |
292 |
285 lemma |
293 lemma |
286 "L(der c (UPNTIMES r m)) = |
294 "L(der c (UPNTIMES r m)) = |
287 L(if (m = 0) then ZERO else ALT ONE (SEQ(der c r) (UPNTIMES r (m - 1))))" |
295 L(if (m = 0) then ZERO else ALT ONE (SEQ(der c r) (UPNTIMES r (m - 1))))" |
288 apply(case_tac m) |
296 apply(case_tac m) |
291 apply(simp only: der.simps) |
299 apply(simp only: der.simps) |
292 apply(simp add: Sequ_def) |
300 apply(simp add: Sequ_def) |
293 apply(auto) |
301 apply(auto) |
294 defer |
302 defer |
295 apply blast |
303 apply blast |
|
304 oops |
|
305 |
|
306 |
|
307 |
|
308 lemma |
|
309 assumes "der c r = ONE \<or> der c r = ZERO" |
|
310 shows "L (der c (NOT r)) \<noteq> L(if (der c r = ZERO) then ONE else |
|
311 if (der c r = ONE) then ZERO |
|
312 else NOT(der c r))" |
|
313 using assms |
|
314 apply(simp) |
|
315 apply(auto) |
|
316 done |
|
317 |
|
318 lemma |
|
319 "L (der c (NOT r)) = L(if (der c r = ZERO) then ONE else |
|
320 if (der c r = ONE) then ZERO |
|
321 else NOT(der c r))" |
|
322 apply(simp) |
|
323 apply(auto) |
296 oops |
324 oops |
297 |
325 |
298 lemma pow_add: |
326 lemma pow_add: |
299 assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m" |
327 assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m" |
300 shows "s1 @ s2 \<in> A \<up> (n + m)" |
328 shows "s1 @ s2 \<in> A \<up> (n + m)" |
342 L(if n = 0 then ZERO else |
370 L(if n = 0 then ZERO else |
343 ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))" |
371 ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))" |
344 apply(auto simp add: Sequ_def) |
372 apply(auto simp add: Sequ_def) |
345 using SpecExt.Pow_empty by blast |
373 using SpecExt.Pow_empty by blast |
346 |
374 |
|
375 abbreviation "FROM \<equiv> FROMNTIMES" |
|
376 |
|
377 lemma |
|
378 shows "L (der c (FROM r n)) = |
|
379 L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0)) |
|
380 else SEQ (der c r) (ALT ZERO (FROM r (n -1))))" |
|
381 apply(auto simp add: Sequ_def) |
|
382 oops |
|
383 |
|
384 |
347 fun |
385 fun |
348 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
386 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
349 where |
387 where |
350 "ders [] r = r" |
388 "ders [] r = r" |
351 | "ders (c # s) r = ders s (der c r)" |
389 | "ders (c # s) r = ders s (der c r)" |
363 apply(simp add: nullable_correctness del: Der_UNION) |
401 apply(simp add: nullable_correctness del: Der_UNION) |
364 apply(simp add: nullable_correctness del: Der_UNION) |
402 apply(simp add: nullable_correctness del: Der_UNION) |
365 apply(simp add: nullable_correctness del: Der_UNION) |
403 apply(simp add: nullable_correctness del: Der_UNION) |
366 apply(simp add: nullable_correctness del: Der_UNION) |
404 apply(simp add: nullable_correctness del: Der_UNION) |
367 apply(simp add: nullable_correctness del: Der_UNION) |
405 apply(simp add: nullable_correctness del: Der_UNION) |
368 prefer 2 |
406 prefer 2 |
|
407 apply(simp only: der.simps) |
|
408 apply(case_tac "x2 = 0") |
|
409 apply(simp) |
|
410 apply(simp del: Der_Sequ L.simps) |
|
411 apply(subst L.simps) |
|
412 apply(subst (2) L.simps) |
|
413 thm Der_UNION |
|
414 |
369 apply(simp add: nullable_correctness del: Der_UNION) |
415 apply(simp add: nullable_correctness del: Der_UNION) |
370 apply(simp add: nullable_correctness del: Der_UNION) |
416 apply(simp add: nullable_correctness del: Der_UNION) |
371 apply(rule impI) |
417 apply(rule impI) |
372 apply(subst Sequ_Union_in) |
418 apply(subst Sequ_Union_in) |
373 apply(subst Der_Pow_Sequ[symmetric]) |
419 apply(subst Der_Pow_Sequ[symmetric]) |