1lemma app_Nil2 [simp]: "xs @ [] = xs" 2apply(induct_tac xs) 3apply(auto) 4done 5 6lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 7apply(induct_tac xs) 8apply(auto) 9done 10 11lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" 12apply(induct_tac xs) 13apply(auto) 14done 15 16theorem rev_rev [simp]: "rev(rev xs) = xs" 17apply(induct_tac xs) 18apply(auto) 19done 20 21end 22