| author | wenzelm |
| Fri, 15 Sep 2000 20:35:17 +0200 | |
| changeset 10001 | 79b23dbb4b89 |
| parent 9541 | d17c0b34d5c8 |
| child 10171 | 59d6633835fa |
| permissions | -rw-r--r-- |
| 9541 | 1 |
lemma app_Nil2 [simp]: "xs @ [] = xs" |
2 |
apply(induct_tac xs) |
|
3 |
apply(auto) |
|
4 |
. |
|
| 8751 | 5 |
|
| 9541 | 6 |
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
7 |
apply(induct_tac xs) |
|
8 |
by(auto) |
|
| 8751 | 9 |
|
| 9541 | 10 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
11 |
apply(induct_tac xs) |
|
12 |
by(auto) |
|
| 8751 | 13 |
|
| 9541 | 14 |
theorem rev_rev [simp]: "rev(rev xs) = xs" |
15 |
apply(induct_tac xs) |
|
16 |
by(auto) |
|
| 8751 | 17 |
|
| 9541 | 18 |
end |