# HG changeset patch
# User lcp
# Date 806684523 -7200
# Node ID d3a3cae80f0889cc43c76ea22d757fd31a903cbd
# Parent  d7e0c280f261c0e0a14f406b07f5659b048d5da9
Proved perm_length

diff -r d7e0c280f261 -r d3a3cae80f08 src/HOL/ex/Perm.ML
--- a/src/HOL/ex/Perm.ML	Tue Jul 25 17:01:25 1995 +0200
+++ b/src/HOL/ex/Perm.ML	Tue Jul 25 17:02:03 1995 +0200
@@ -21,7 +21,19 @@
 val perm_induct = standard (perm.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
 
-(** Two examples of rule induction on permutations **)
+(** Some examples of rule induction on permutations **)
+
+(*The form of the premise lets the induction bind xs and ys.*)
+goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
+by (etac perm_induct 1);
+by (ALLGOALS (asm_simp_tac (HOL_ss addsimps list.simps)));
+qed "perm_Nil_lemma";
+
+(*A more general version is actually easier to understand!*)
+goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
+by (etac perm_induct 1);
+by (ALLGOALS (asm_simp_tac list_ss));
+qed "perm_length";
 
 goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
 by (etac perm_induct 1);