| changeset 57083 | 5c26000e1042 |
| parent 48985 | 5386df44a037 |
| 57082:2c1c8b38e3f0 | 57083:5c26000e1042 |
|---|---|
1 lemma app_Nil2 [simp]: "xs @ [] = xs" |
|
2 apply(induct_tac xs) |
|
3 apply(auto) |
|
4 done |
|
5 |
|
6 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
|
7 apply(induct_tac xs) |
|
8 apply(auto) |
|
9 done |
|
10 |
|
11 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
|
12 apply(induct_tac xs) |
|
13 apply(auto) |
|
14 done |
|
15 |
|
16 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
17 apply(induct_tac xs) |
|
18 apply(auto) |
|
19 done |
|
20 |
|
21 end |