equal
deleted
inserted
replaced
169 shows "L (ders s r) = Ders s (L r)" |
169 shows "L (ders s r) = Ders s (L r)" |
170 apply(induct s arbitrary: r) |
170 apply(induct s arbitrary: r) |
171 apply(simp_all add: Ders_def der_correctness Der_def) |
171 apply(simp_all add: Ders_def der_correctness Der_def) |
172 done |
172 done |
173 |
173 |
|
174 |
|
175 section {* Lemmas about ders *} |
|
176 |
174 lemma ders_ZERO: |
177 lemma ders_ZERO: |
175 shows "ders s (ZERO) = ZERO" |
178 shows "ders s (ZERO) = ZERO" |
176 apply(induct s) |
179 apply(induct s) |
177 apply(simp_all) |
180 apply(simp_all) |
178 done |
181 done |
182 apply(induct s) |
185 apply(induct s) |
183 apply(simp_all add: ders_ZERO) |
186 apply(simp_all add: ders_ZERO) |
184 done |
187 done |
185 |
188 |
186 lemma ders_CHAR: |
189 lemma ders_CHAR: |
187 shows "ders s (CHAR c) = (if s = [c] then ONE else |
190 shows "ders s (CHAR c) = |
188 (if s = [] then (CHAR c) else ZERO))" |
191 (if s = [c] then ONE else |
|
192 (if s = [] then (CHAR c) else ZERO))" |
189 apply(induct s) |
193 apply(induct s) |
190 apply(simp_all add: ders_ZERO ders_ONE) |
194 apply(simp_all add: ders_ZERO ders_ONE) |
191 done |
195 done |
192 |
196 |
193 lemma ders_ALT: |
197 lemma ders_ALT: |