# HG changeset patch
# User nipkow
# Date 792239651 -3600
# Node ID 1a3d3b5b5d15704068479333b6d3bc2930d24b64
# Parent  cc7ad90039b92ad453996bf9cbe788b63b0b377b
More rewrite rules.

diff -r cc7ad90039b9 -r 1a3d3b5b5d15 List.ML
--- a/List.ML	Fri Feb 03 16:21:45 1995 +0100
+++ b/List.ML	Wed Feb 08 11:34:11 1995 +0100
@@ -55,6 +55,12 @@
 by(ALLGOALS(asm_simp_tac list_ss));
 qed "append_is_Nil";
 
+goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
+by (list.induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+qed "same_append_eq";
+
+
 (** mem **)
 
 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -96,6 +102,13 @@
 by(fast_tac HOL_cs 1);
 qed "expand_list_case";
 
+goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
+by(list.induct_tac "xs" 1);
+by(fast_tac HOL_cs 1);
+by(fast_tac HOL_cs 1);
+bind_thm("list_eq_cases",
+  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
+
 (** nth **)
 
 val [nth_0,nth_Suc] = nat_recs nth_def; 
@@ -120,7 +133,7 @@
 qed "map_compose";
 
 val list_ss = list_ss addsimps
-  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil,
+  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
    mem_append, mem_filter,
    map_ident, map_append, map_compose,
    list_all_True, list_all_conj, nth_0, nth_Suc];