equal
deleted
inserted
replaced
206 |
206 |
207 lemma genPrefix_append_both: |
207 lemma genPrefix_append_both: |
208 "[| refl r; (xs,ys) : genPrefix r; length xs = length ys |] |
208 "[| refl r; (xs,ys) : genPrefix r; length xs = length ys |] |
209 ==> (xs@zs, ys @ zs) : genPrefix r" |
209 ==> (xs@zs, ys @ zs) : genPrefix r" |
210 apply (drule genPrefix_take_append, assumption) |
210 apply (drule genPrefix_take_append, assumption) |
211 apply (simp add: take_all) |
211 apply simp |
212 done |
212 done |
213 |
213 |
214 |
214 |
215 (*NOT suitable for rewriting since [y] has the form y#ys*) |
215 (*NOT suitable for rewriting since [y] has the form y#ys*) |
216 lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys" |
216 lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys" |
299 |
299 |
300 |
300 |
301 (** recursion equations **) |
301 (** recursion equations **) |
302 |
302 |
303 lemma Nil_prefix [iff]: "[] <= xs" |
303 lemma Nil_prefix [iff]: "[] <= xs" |
304 apply (unfold prefix_def) |
304 by (simp add: prefix_def) |
305 apply (simp add: Nil_genPrefix) |
|
306 done |
|
307 |
305 |
308 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" |
306 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" |
309 apply (unfold prefix_def) |
307 by (simp add: prefix_def) |
310 apply (simp add: genPrefix_Nil) |
|
311 done |
|
312 |
308 |
313 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" |
309 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" |
314 by (simp add: prefix_def) |
310 by (simp add: prefix_def) |
315 |
311 |
316 lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)" |
312 lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)" |