--- a/src/HOL/Lex/Prefix.ML Thu Sep 10 17:26:53 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML Thu Sep 10 17:27:15 1998 +0200
@@ -71,7 +71,7 @@
qed "same_prefix_prefix";
Addsimps [same_prefix_prefix];
-AddIffs
+AddIffs (* (xs@ys <= xs) = (ys <= []) *)
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
@@ -80,13 +80,10 @@
qed "prefix_prefix";
Addsimps [prefix_prefix];
-(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
Goalw [prefix_def]
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Fast_tac 1);
+by (exhaust_tac "xs" 1);
+by Auto_tac;
qed "prefix_Cons";
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
@@ -94,7 +91,7 @@
by (Simp_tac 1);
by (Blast_tac 1);
by (asm_full_simp_tac (simpset() delsimps [append_assoc]
- addsimps [append_assoc RS sym])1);
+ addsimps [append_assoc RS sym])1);
by (Simp_tac 1);
by (Blast_tac 1);
qed "prefix_append";