new inductive definition: permutations

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Perm.ML	Fri Jun 30 11:34:14 1995 +0200
@@ -0,0 +1,88 @@
+(*  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";
+
+val perm_induct = standard (perm.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+
+(** Two examples of rule induction on permutations **)
+
+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 HOL_cs 4);
+by (ALLGOALS (asm_simp_tac (list_ss 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 (list_ss addsimps [perm_refl]) 1);
+by (simp_tac list_ss 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 (list_ss addsimps [perm_refl]) 1);
+by (simp_tac list_ss 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);
+br perm_append_swap 2;
+by (simp_tac (list_ss addsimps [perm_refl]) 1);
+qed "perm_append_single";
+
+goal Perm.thy "rev xs <~~> xs";
+by (list.induct_tac "xs" 1);
+by (simp_tac (list_ss addsimps [perm_refl]) 1);
+by (simp_tac list_ss 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 list_ss 1);
+by (asm_simp_tac (list_ss 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";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Perm.thy	Fri Jun 30 11:34:14 1995 +0200
@@ -0,0 +1,24 @@
+(*  Title: 	HOL/ex/Perm.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+Permutations: example of an inductive definition
+*)
+
+Perm = List +
+
+consts  perm    :: "('a list * 'a list) set"   
+syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50] 50)
+
+translations
+    "x <~~> y" == "(x,y) : perm"
+
+inductive "perm"
+  intrs
+    Nil   "[] <~~> []"
+    swap  "y#x#l <~~> x#y#l"
+    Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
+    trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
+
+end