# HG changeset patch
# User nipkow
# Date 888313493 -3600
# Node ID 42af8ae6e2c146e42108923959a3e24676c6ddb4
# Parent  f6298426f5a758819505d328ce933423b0401935
Added some lemmas.

diff -r f6298426f5a7 -r 42af8ae6e2c1 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Mon Feb 23 11:24:49 1998 +0100
+++ b/src/HOL/Lex/Prefix.ML	Tue Feb 24 10:44:53 1998 +0100
@@ -17,7 +17,7 @@
 goalw thy [prefix_def] "xs <= (xs::'a list)";
 by(Simp_tac 1);
 qed "prefix_refl";
-Addsimps[prefix_refl];
+AddIffs[prefix_refl];
 
 goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
 by(Clarify_tac 1);
@@ -34,7 +34,7 @@
 goalw Prefix.thy [prefix_def] "[] <= xs";
 by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "Nil_prefix";
-Addsimps[Nil_prefix];
+AddIffs[Nil_prefix];
 
 goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
 by (list.induct_tac "xs" 1);
@@ -65,6 +65,15 @@
 qed"Cons_prefix_Cons";
 Addsimps [Cons_prefix_Cons];
 
+goal thy "(xs@ys <= xs@zs) = (ys <= zs)";
+by (induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "same_prefix_prefix";
+Addsimps [same_prefix_prefix];
+
+AddIffs
+ [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
+
 goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
 by(Clarify_tac 1);
 by (Simp_tac 1);
@@ -79,3 +88,13 @@
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "prefix_Cons";
+
+goal thy "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
+by(res_inst_tac [("xs","zs")] snoc_induct 1);
+ by(Simp_tac 1);
+ by(Blast_tac 1);
+by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+                                addsimps [append_assoc RS sym])1);
+by(Simp_tac 1);
+by(Blast_tac 1);
+qed "prefix_append";
diff -r f6298426f5a7 -r 42af8ae6e2c1 src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Feb 23 11:24:49 1998 +0100
+++ b/src/HOL/List.ML	Tue Feb 24 10:44:53 1998 +0100
@@ -180,6 +180,18 @@
 AddSDs
  [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
 
+goal thy "(xs @ ys = ys) = (xs=[])";
+by(cut_inst_tac [("zs","[]")] append_same_eq 1);
+by(Asm_full_simp_tac 1);
+qed "append_self_conv2";
+
+goal thy "(ys = xs @ ys) = (xs=[])";
+by(simp_tac (simpset() addsimps
+     [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
+by(Blast_tac 1);
+qed "self_append_conv2";
+AddIffs [append_self_conv2,self_append_conv2];
+
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);