diff -r 91614f0eb250 -r ac7b7003f177 List.ML
--- a/List.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/List.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -163,6 +163,13 @@
 val not_Cons_self = result();
 
 
+goal List.thy "(xs ~= []) = (? y ys. xs = Cons(y,ys))";
+by(list_ind_tac "xs" 1);
+by(simp_tac list_free_ss 1);
+by(asm_simp_tac list_free_ss 1);
+by(REPEAT(resolve_tac [exI,refl,conjI] 1));
+val neq_Nil_conv = result();
+
 (** Conversion rules for List_case: case analysis operator **)
 
 goalw List.thy [List_case_def,NIL_def] "List_case(NIL,c,h) = c";
@@ -303,6 +310,7 @@
 val [null_Nil,null_Cons] = list_recs null_def;
 val [_,hd_Cons] = list_recs hd_def;
 val [_,tl_Cons] = list_recs tl_def;
+val [ttl_Nil,ttl_Cons] = list_recs ttl_def;
 val [append_Nil,append_Cons] = list_recs append_def;
 val [mem_Nil, mem_Cons] = list_recs mem_def;
 val [map_Nil,map_Cons] = list_recs map_def;
@@ -313,7 +321,7 @@
 val list_ss = arith_ss addsimps
   [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
    list_rec_Nil, list_rec_Cons,
-   null_Nil, null_Cons, hd_Cons, tl_Cons,
+   null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons,
    mem_Nil, mem_Cons,
    list_case_Nil, list_case_Cons,
    append_Nil, append_Cons,
@@ -329,6 +337,11 @@
 by(ALLGOALS(asm_simp_tac list_ss));
 val append_assoc = result();
 
+goal List.thy "xs @ [] = xs";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+val append_Nil2 = result();
+
 (** mem **)
 
 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -376,6 +389,16 @@
 
 (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
 
+(** list_case **)
+
+goal List.thy
+ "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
+\                         (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss addsimps [list_case_Nil,list_case_Cons])));
+by(fast_tac HOL_cs 1);
+val expand_list_case = result();
+
 
 (** Additional mapping lemmas **)
 
@@ -392,5 +415,6 @@
 val Abs_Rep_map = result();
 
 val list_ss = list_ss addsimps
-  [mem_append, mem_filter, append_assoc, map_ident,
+  [mem_append, mem_filter, append_assoc, append_Nil2, map_ident,
    list_all_True, list_all_conj];
+