equal
deleted
inserted
replaced
113 where |
113 where |
114 "der c (Zero) = Zero" |
114 "der c (Zero) = Zero" |
115 | "der c (One) = Zero" |
115 | "der c (One) = Zero" |
116 | "der c (Atom c') = (if c = c' then One else Zero)" |
116 | "der c (Atom c') = (if c = c' then One else Zero)" |
117 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)" |
117 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)" |
118 | "der c (Times r1 r2) = Plus (Times (der c r1) r2) (if nullable r1 then der c r2 else Zero)" |
118 | "der c (Times r1 r2) = |
|
119 (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)" |
119 | "der c (Star r) = Times (der c r) (Star r)" |
120 | "der c (Star r) = Times (der c r) (Star r)" |
120 |
121 |
121 function |
122 function |
122 ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
123 ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp" |
123 where |
124 where |