--- 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];
+