src/HOL/Induct/Perm.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Perm.ML	Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,98 @@
+(*  Title:      HOL/ex/Perm.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+Permutations: example of an inductive definition
+*)
+
+(*It would be nice to prove
+    xs <~~> ys = (!x. count xs x = count ys x)
+See mset on HOL/ex/Sorting.thy
+*)
+
+open Perm;
+
+goal Perm.thy "l <~~> l";
+by (list.induct_tac "l" 1);
+by (REPEAT (ares_tac perm.intrs 1));
+qed "perm_refl";
+
+
+(** 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);
+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);
+qed "perm_length";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
+by (etac perm.induct 1);
+by (REPEAT (ares_tac perm.intrs 1));
+qed "perm_sym";
+
+goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
+by (etac perm.induct 1);
+by (Fast_tac 4);
+by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+val perm_mem_lemma = result();
+
+bind_thm ("perm_mem", perm_mem_lemma RS mp);
+
+(** Ways of making new permutations **)
+
+(*We can insert the head anywhere in the list*)
+goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+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 Perm.thy "xs@ys <~~> ys@xs";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
+qed "perm_append_swap";
+
+
+goal Perm.thy "a # xs <~~> xs @ [a]";
+by (rtac perm.trans 1);
+by (rtac perm_append_swap 2);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+qed "perm_append_single";
+
+goal Perm.thy "rev xs <~~> xs";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
+by (etac perm.Cons 1);
+qed "perm_rev";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
+by (list.induct_tac "l" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
+qed "perm_append1";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
+by (rtac (perm_append_swap RS perm.trans) 1);
+by (etac (perm_append1 RS perm.trans) 1);
+by (rtac perm_append_swap 1);
+qed "perm_append2";
+