equal
deleted
inserted
replaced
172 lemma ders_correctness: |
172 lemma ders_correctness: |
173 shows "L (ders s r) = Ders s (L r)" |
173 shows "L (ders s r) = Ders s (L r)" |
174 by (induct s arbitrary: r) |
174 by (induct s arbitrary: r) |
175 (simp_all add: Ders_def der_correctness Der_def) |
175 (simp_all add: Ders_def der_correctness Der_def) |
176 |
176 |
|
177 lemma ders_append: |
|
178 shows "ders (s1 @ s2) r = ders s2 (ders s1 r)" |
|
179 apply(induct s1 arbitrary: s2 r) |
|
180 apply(auto) |
|
181 done |
177 |
182 |
178 |
183 |
179 section {* Values *} |
184 section {* Values *} |
180 |
185 |
181 datatype val = |
186 datatype val = |