equal
deleted
inserted
replaced
10 |
10 |
11 lemma SEQs_eq_image: |
11 lemma SEQs_eq_image: |
12 "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs" |
12 "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs" |
13 by auto |
13 by auto |
14 |
14 |
15 primrec |
15 fun |
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 (CH 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 |
26 primrec |
26 fun |
27 pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set" |
27 pders :: "char list \<Rightarrow> rexp \<Rightarrow> rexp set" |
28 where |
28 where |
29 "pders [] r = {r}" |
29 "pders [] r = {r}" |
30 | "pders (c # s) r = \<Union> (pders s ` pder c r)" |
30 | "pders (c # s) r = \<Union> (pders s ` pder c r)" |
31 |
31 |