List.ML

 
 goalw List.thy [list_case_def] "list_case(Cons(x,xs),a,f) = f(x,xs)";
 by (rtac list_rec_Cons 1);
 val list_case_Cons = result();
 
+(** @ - append **)
+
+goalw List.thy [append_def] "[]@xs = xs";
+by (rtac list_rec_Nil 1);
+val append_Nil = result();
+
+goalw List.thy [append_def] "Cons(x,xs)@ys = Cons(x,xs@ys)";
+by (rtac list_rec_Cons 1);
+val append_Cons = result();
+
+goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
+by(res_inst_tac [("l","xs")] list_induct 1);
+by(REPEAT(asm_simp_tac (list_ss addsimps [append_Nil,append_Cons]) 1));
+val append_assoc = result();
 
 (** The functional "map" **)
 
 goalw List.thy [map_def] "map(f,Nil) = Nil";
 by (rtac list_rec_Nil 1);