# HG changeset patch
# User paulson
# Date 952707119 -3600
# Node ID 09db77a084aa9a6e8466f27faad2d90523be3f75
# Parent  65f9089f6f711d06d46e8f6d40d19bf2ba982727
tidied, and new thm perm_append2_eq

diff -r 65f9089f6f71 -r 09db77a084aa src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Fri Mar 10 17:14:56 2000 +0100
+++ b/src/HOL/Induct/Perm.ML	Fri Mar 10 17:51:59 2000 +0100
@@ -53,12 +53,6 @@
 by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
 qed "perm_append_Cons";
 
-(*single steps
-by (rtac perm.trans 1);
-by (rtac perm.swap 1);
-by (rtac perm.Cons 1);
-*)
-
 Goal "xs@ys <~~> ys@xs";
 by (induct_tac "xs" 1);
 by (ALLGOALS Simp_tac);
@@ -115,19 +109,16 @@
 Goal "ys <~~> xs ==> xs=[y] --> ys=[y]";
 by (etac perm.induct 1);
 by Auto_tac;
-qed "perm_one_elem_imp";
+qed_spec_mp "perm_sing_imp";
 
 Goal "(ys <~~> [y]) = (ys = [y])"; 
-by Safe_tac;
-by (rtac mp 1);
-by (rtac perm_one_elem_imp 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [perm_refl])));
+by (blast_tac (claset() addIs [perm_sing_imp]) 1);
 qed "perm_sing_eq";
 AddIffs [perm_sing_eq];
 
 Goal "([y] <~~> ys) = (ys = [y])"; 
 by Auto_tac;
-bd perm_sym 1;
+by (dtac perm_sym 1);
 by Auto_tac;
 qed "perm_sing_eq2";
 AddIffs [perm_sing_eq2];
@@ -174,3 +165,12 @@
 by (blast_tac (claset() addIs [append_perm_imp_perm, perm_append1]) 1);
 qed "perm_append1_eq";
 AddIffs [perm_append1_eq];
+
+Goal "(xs@zs <~~> ys@zs) = (xs <~~> ys)";
+by (safe_tac (claset() addSIs [perm_append2]));
+by (rtac append_perm_imp_perm 1);
+by (rtac (perm_append_swap RS perm.trans) 1);
+(*Not clear why this blast_tac alone can't find the proof.*)
+by (blast_tac (claset() addIs [perm_append_swap, perm.trans]) 1);
+qed "perm_append2_eq";
+AddIffs [perm_append2_eq];