changeset 8751 | 9ed0548177fb |
child 8846 | c7d945398677 |
8750:36b165788421 | 8751:9ed0548177fb |
---|---|
1 lemma app_Nil2 [simp]: "xs @ [] = xs"; |
|
2 apply(induct_tac xs); |
|
3 apply(auto).; |
|
4 |
|
5 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
|
6 apply(induct_tac xs); |
|
7 apply(auto).; |
|
8 |
|
9 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
|
10 apply(induct_tac xs); |
|
11 apply(auto).; |
|
12 |
|
13 theorem rev_rev [simp]: "rev(rev xs) = xs"; |
|
14 apply(induct_tac xs); |
|
15 apply(auto).; |
|
16 |
|
17 end |