# HG changeset patch
# User nipkow
# Date 869750729 -7200
# Node ID 5995ab73d79075af5c27a756a569a7b4d6f363fa
# Parent  7544c866315c9c33a0d004629c6f65680d7ae210
Added a few lemmas.

diff -r 7544c866315c -r 5995ab73d790 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Jul 24 11:20:12 1997 +0200
+++ b/src/HOL/List.ML	Thu Jul 24 15:25:29 1997 +0200
@@ -10,7 +10,8 @@
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "not_Cons_self";
-Addsimps [not_Cons_self];
+bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
+Addsimps [not_Cons_self,not_Cons_self2];
 
 goal thy "(xs ~= []) = (? y ys. xs = y#ys)";
 by (induct_tac "xs" 1);
@@ -95,6 +96,18 @@
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
+goal thy "(xs @ ys = xs) = (ys=[])";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "append_self_conv";
+
+goal thy "(xs = xs @ ys) = (ys=[])";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed "self_append_conv";
+AddIffs [append_self_conv,self_append_conv];
+
 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);