| changeset 48966 | 6e15de7dd871 |
| parent 48965 | 1fead823c7c6 |
| child 48967 | 389e44f9e47a |
| 48965:1fead823c7c6 | 48966:6e15de7dd871 |
|---|---|
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 |