15 primrec |
15 primrec |
16 pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set" |
16 pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set" |
17 where |
17 where |
18 "pder c ZERO = {}" |
18 "pder c ZERO = {}" |
19 | "pder c ONE = {}" |
19 | "pder c ONE = {}" |
20 | "pder c (CHAR d) = (if c = d then {ONE} else {})" |
20 | "pder c (CH d) = (if c = d then {ONE} else {})" |
21 | "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)" |
21 | "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)" |
22 | "pder c (SEQ r1 r2) = |
22 | "pder c (SEQ r1 r2) = |
23 (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)" |
23 (if nullable r1 then SEQs (pder c r1) r2 \<union> pder c r2 else SEQs (pder c r1) r2)" |
24 | "pder c (STAR r) = SEQs (pder c r) (STAR r)" |
24 | "pder c (STAR r) = SEQs (pder c r) (STAR r)" |
25 |
25 |
52 and "pders s ONE = (if s = [] then {ONE} else {})" |
52 and "pders s ONE = (if s = [] then {ONE} else {})" |
53 and "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))" |
53 and "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))" |
54 by (induct s) (simp_all) |
54 by (induct s) (simp_all) |
55 |
55 |
56 lemma pders_CHAR: |
56 lemma pders_CHAR: |
57 shows "pders s (CHAR c) \<subseteq> {CHAR c, ONE}" |
57 shows "pders s (CH c) \<subseteq> {CH c, ONE}" |
58 by (induct s) (simp_all) |
58 by (induct s) (simp_all) |
59 |
59 |
60 subsection \<open>Relating left-quotients and partial derivatives\<close> |
60 subsection \<open>Relating left-quotients and partial derivatives\<close> |
61 |
61 |
62 lemma Sequ_UNION_distrib: |
62 lemma Sequ_UNION_distrib: |
125 lemma pders_Set_ONE [simp]: |
125 lemma pders_Set_ONE [simp]: |
126 shows "pders_Set UNIV1 ONE = {}" |
126 shows "pders_Set UNIV1 ONE = {}" |
127 unfolding UNIV1_def pders_Set_def by (auto split: if_splits) |
127 unfolding UNIV1_def pders_Set_def by (auto split: if_splits) |
128 |
128 |
129 lemma pders_Set_CHAR [simp]: |
129 lemma pders_Set_CHAR [simp]: |
130 shows "pders_Set UNIV1 (CHAR c) = {ONE}" |
130 shows "pders_Set UNIV1 (CH c) = {ONE}" |
131 unfolding UNIV1_def pders_Set_def |
131 unfolding UNIV1_def pders_Set_def |
132 apply(auto) |
132 apply(auto) |
133 apply(frule rev_subsetD) |
133 apply(frule rev_subsetD) |
134 apply(rule pders_CHAR) |
134 apply(rule pders_CHAR) |
135 apply(simp) |
135 apply(simp) |
280 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close> |
280 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close> |
281 |
281 |
282 fun awidth :: "rexp \<Rightarrow> nat" where |
282 fun awidth :: "rexp \<Rightarrow> nat" where |
283 "awidth ZERO = 0" | |
283 "awidth ZERO = 0" | |
284 "awidth ONE = 0" | |
284 "awidth ONE = 0" | |
285 "awidth (CHAR a) = 1" | |
285 "awidth (CH a) = 1" | |
286 "awidth (ALT r1 r2) = awidth r1 + awidth r2" | |
286 "awidth (ALT r1 r2) = awidth r1 + awidth r2" | |
287 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" | |
287 "awidth (SEQ r1 r2) = awidth r1 + awidth r2" | |
288 "awidth (STAR r1) = awidth r1" |
288 "awidth (STAR r1) = awidth r1" |
289 |
289 |
290 lemma card_SEQs_pders_Set_le: |
290 lemma card_SEQs_pders_Set_le: |
362 |
362 |
363 |
363 |
364 fun subs :: "rexp \<Rightarrow> rexp set" where |
364 fun subs :: "rexp \<Rightarrow> rexp set" where |
365 "subs ZERO = {ZERO}" | |
365 "subs ZERO = {ZERO}" | |
366 "subs ONE = {ONE}" | |
366 "subs ONE = {ONE}" | |
367 "subs (CHAR a) = {CHAR a, ONE}" | |
367 "subs (CH a) = {CH a, ONE}" | |
368 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" | |
368 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" | |
369 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union> SEQs (subs r1) r2)" | |
369 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union> SEQs (subs r1) r2)" | |
370 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))" |
370 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))" |
371 |
371 |
372 lemma subs_finite: |
372 lemma subs_finite: |
423 apply(induct r) |
423 apply(induct r) |
424 apply(simp) |
424 apply(simp) |
425 apply(simp_all) |
425 apply(simp_all) |
426 done |
426 done |
427 |
427 |
|
428 (* |
428 lemma subs_card: |
429 lemma subs_card: |
429 shows "card (subs r) \<le> Suc (size2 r + size2 r)" |
430 shows "card (subs r) \<le> Suc (size2 r + size2 r)" |
430 apply(induct r) |
431 apply(induct r) |
431 apply(auto) |
432 apply(auto) |
432 apply(subst card_insert) |
433 apply(subst card_insert) |
433 apply(simp add: subs_finite) |
434 apply(simp add: subs_finite) |
434 apply(simp add: subs_finite) |
435 apply(simp add: subs_finite) |
435 oops |
436 oops |
|
437 *) |
436 |
438 |
437 lemma subs_size2: |
439 lemma subs_size2: |
438 shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
440 shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
439 apply(induct r) |
441 apply(induct r) |
440 apply(simp) |
442 apply(simp) |
530 qed |
532 qed |
531 |
533 |
532 fun height :: "rexp \<Rightarrow> nat" where |
534 fun height :: "rexp \<Rightarrow> nat" where |
533 "height ZERO = 1" | |
535 "height ZERO = 1" | |
534 "height ONE = 1" | |
536 "height ONE = 1" | |
535 "height (CHAR c) = 1" | |
537 "height (CH c) = 1" | |
536 "height (ALT r1 r2) = Suc (max (height r1) (height r2))" | |
538 "height (ALT r1 r2) = Suc (max (height r1) (height r2))" | |
537 "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" | |
539 "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" | |
538 "height (STAR r1) = Suc (height r1)" |
540 "height (STAR r1) = Suc (height r1)" |
539 |
541 |
540 lemma height_size2: |
542 lemma height_size2: |
553 lemma subs_height: |
555 lemma subs_height: |
554 shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)" |
556 shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)" |
555 apply(induct r) |
557 apply(induct r) |
556 apply(auto)+ |
558 apply(auto)+ |
557 done |
559 done |
558 |
560 |
559 |
561 fun lin_concat :: "(char \<times> rexp) \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp)" (infixl "[.]" 91) |
|
562 where |
|
563 "(c, ZERO) [.] t = (c, ZERO)" |
|
564 | "(c, ONE) [.] t = (c, t)" |
|
565 | "(c, p) [.] t = (c, SEQ p t)" |
|
566 |
|
567 |
|
568 fun circle_concat :: "(char \<times> rexp ) set \<Rightarrow> rexp \<Rightarrow> (char \<times> rexp) set" ( infixl "\<circle>" 90) |
|
569 where |
|
570 "l \<circle> ZERO = {}" |
|
571 | "l \<circle> ONE = l" |
|
572 | "l \<circle> t = ( (\<lambda>p. p [.] t) ` l ) " |
|
573 |
|
574 |
|
575 |
|
576 fun linear_form :: "rexp \<Rightarrow>( char \<times> rexp ) set" |
|
577 where |
|
578 "linear_form ZERO = {}" |
|
579 | "linear_form ONE = {}" |
|
580 | "linear_form (CH c) = {(c, ONE)}" |
|
581 | "linear_form (ALT r1 r2) = (linear_form) r1 \<union> (linear_form r2)" |
|
582 | "linear_form (SEQ r1 r2) = (if (nullable r1) then (linear_form r1) \<circle> r2 \<union> linear_form r2 else (linear_form r1) \<circle> r2) " |
|
583 | "linear_form (STAR r ) = (linear_form r) \<circle> (STAR r)" |
|
584 |
|
585 |
|
586 value "linear_form (SEQ (STAR (CH x)) (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) )" |
|
587 |
|
588 |
|
589 value "linear_form (STAR (ALT (SEQ (CH x) (CH x)) (CH y) )) " |
|
590 |
|
591 fun pdero :: "char \<Rightarrow> rexp \<Rightarrow> rexp set" |
|
592 where |
|
593 "pdero c t = \<Union> ((\<lambda>(d, p). if d = c then {p} else {}) ` (linear_form t) )" |
|
594 |
|
595 fun pderso :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set" |
|
596 where |
|
597 "pderso [] r = {r}" |
|
598 | "pderso (c # s) r = \<Union> ( pderso s ` (pdero c r) )" |
|
599 |
|
600 lemma alternative_pder: |
|
601 shows "pderso s r = pders s r" |
|
602 sledgehammer |
|
603 oops |
|
604 |
|
605 |
|
606 export_code height pders subs pderso in Scala module_name Pders |
|
607 export_code pdero pderso in Scala module_name Pderso |
|
608 export_code pdero pderso in Scala module_name Pderso |
|
609 |
|
610 |
560 |
611 |
561 end |
612 end |