--- a/List.ML Wed Dec 14 11:17:18 1994 +0100
+++ b/List.ML Thu Jan 26 10:41:21 1995 +0100
@@ -50,6 +50,11 @@
by(ALLGOALS(asm_simp_tac list_ss));
qed "append_Nil2";
+goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+qed "append_is_Nil";
+
(** mem **)
goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -91,6 +96,11 @@
by(fast_tac HOL_cs 1);
qed "expand_list_case";
+(** nth **)
+
+val [nth_0,nth_Suc] = nat_recs nth_def;
+store_thm("nth_0",nth_0);
+store_thm("nth_Suc",nth_Suc);
(** Additional mapping lemmas **)
@@ -110,7 +120,8 @@
qed "map_compose";
val list_ss = list_ss addsimps
- [not_Cons_self, append_assoc, append_Nil2, mem_append, mem_filter,
+ [not_Cons_self, append_assoc, append_Nil2, append_is_Nil,
+ mem_append, mem_filter,
map_ident, map_append, map_compose,
- list_all_True, list_all_conj];
+ list_all_True, list_all_conj, nth_0, nth_Suc];