equal
deleted
inserted
replaced
134 fun |
134 fun |
135 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
135 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
136 where |
136 where |
137 "der c (ZERO) = ZERO" |
137 "der c (ZERO) = ZERO" |
138 | "der c (ONE) = ZERO" |
138 | "der c (ONE) = ZERO" |
139 | "der c (CHAR c') = (if c = c' then ONE else ZERO)" |
139 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
140 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
140 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
141 | "der c (SEQ r1 r2) = |
141 | "der c (SEQ r1 r2) = |
142 (if nullable r1 |
142 (if nullable r1 |
143 then ALT (SEQ (der c r1) r2) (der c r2) |
143 then ALT (SEQ (der c r1) r2) (der c r2) |
144 else SEQ (der c r1) r2)" |
144 else SEQ (der c r1) r2)" |
397 apply(simp_all)[7] |
397 apply(simp_all)[7] |
398 apply(simp) |
398 apply(simp) |
399 apply(erule Prf.cases) |
399 apply(erule Prf.cases) |
400 apply(simp_all)[7] |
400 apply(simp_all)[7] |
401 apply(simp) |
401 apply(simp) |
402 apply(case_tac "c = c'") |
402 apply(case_tac "c = d") |
403 apply(simp) |
403 apply(simp) |
404 apply(auto)[1] |
404 apply(auto)[1] |
405 apply(erule Prf.cases) |
405 apply(erule Prf.cases) |
406 apply(simp_all)[7] |
406 apply(simp_all)[7] |
407 apply(simp) |
407 apply(simp) |
1166 apply(simp_all)[7] |
1166 apply(simp_all)[7] |
1167 (* ONE case *) |
1167 (* ONE case *) |
1168 apply(erule PMatch.cases) |
1168 apply(erule PMatch.cases) |
1169 apply(simp_all)[7] |
1169 apply(simp_all)[7] |
1170 (* CHAR case *) |
1170 (* CHAR case *) |
1171 apply(case_tac "c = c'") |
1171 apply(case_tac "c = d") |
1172 apply(simp) |
1172 apply(simp) |
1173 apply(erule PMatch.cases) |
1173 apply(erule PMatch.cases) |
1174 apply(simp_all)[7] |
1174 apply(simp_all)[7] |
1175 apply (metis PMatch.intros(2)) |
1175 apply (metis PMatch.intros(2)) |
1176 apply(simp) |
1176 apply(simp) |