equal
deleted
inserted
replaced
1 lemma app_Nil2 [simp]: "xs @ [] = xs"; |
1 lemma app_Nil2 [simp]: "xs @ [] = xs"; |
2 apply(induct_tac xs); |
2 apply(induct_tac xs); |
3 apply(auto).; |
3 apply(auto);.; |
4 |
4 |
5 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
5 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
6 apply(induct_tac xs); |
6 apply(induct_tac xs); |
7 apply(auto).; |
7 apply(auto);.; |
8 |
8 |
9 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
9 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
10 apply(induct_tac xs); |
10 apply(induct_tac xs); |
11 apply(auto).; |
11 apply(auto);.; |
12 |
12 |
13 theorem rev_rev [simp]: "rev(rev xs) = xs"; |
13 theorem rev_rev [simp]: "rev(rev xs) = xs"; |
14 apply(induct_tac xs); |
14 apply(induct_tac xs); |
15 apply(auto).; |
15 apply(auto);.; |
16 |
16 |
17 end |
17 end; |