function "remove" and new lemmas for Factorization

--- a/src/HOL/Induct/Perm.ML	Wed Mar 08 16:14:12 2000 +0100
+++ b/src/HOL/Induct/Perm.ML	Wed Mar 08 16:15:41 2000 +0100
@@ -15,7 +15,7 @@
 by (induct_tac "l" 1);
 by (REPEAT (ares_tac perm.intrs 1));
 qed "perm_refl";
-
+AddIffs [perm_refl];
 
 (** Some examples of rule induction on permutations **)
 
@@ -36,7 +36,7 @@
 by (REPEAT (ares_tac perm.intrs 1));
 qed "perm_sym";
 
-Goal "[| xs <~~> ys |] ==> x mem xs --> x mem ys";
+Goal "xs <~~> ys ==> x mem xs --> x mem ys";
 by (etac perm.induct 1);
 by (Fast_tac 4);
 by (ALLGOALS Asm_simp_tac);
@@ -49,8 +49,7 @@
 (*We can insert the head anywhere in the list*)
 Goal "a # xs @ ys <~~> xs @ a # ys";
 by (induct_tac "xs" 1);
-by (simp_tac (simpset() addsimps [perm_refl]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
 qed "perm_append_Cons";
 
@@ -62,8 +61,7 @@
 
 Goal "xs@ys <~~> ys@xs";
 by (induct_tac "xs" 1);
-by (simp_tac (simpset() addsimps [perm_refl]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
 qed "perm_append_swap";
 
@@ -71,13 +69,12 @@
 Goal "a # xs <~~> xs @ [a]";
 by (rtac perm.trans 1);
 by (rtac perm_append_swap 2);
-by (simp_tac (simpset() addsimps [perm_refl]) 1);
+by (Simp_tac 1);
 qed "perm_append_single";
 
 Goal "rev xs <~~> xs";
 by (induct_tac "xs" 1);
-by (simp_tac (simpset() addsimps [perm_refl]) 1);
-by (Simp_tac 1);
+by (ALLGOALS Simp_tac);
 by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
 by (etac perm.Cons 1);
 qed "perm_rev";
@@ -94,3 +91,86 @@
 by (rtac perm_append_swap 1);
 qed "perm_append2";
 
+(** Further results mostly by Thomas Marthedal Rasmussen **)
+
+val perm_rules = [perm.trans, perm.swap, perm.Cons];
+
+Goal "[] <~~> xs ==> xs = []";
+by (rtac mp 1);
+by (res_inst_tac [("ys","xs"),("xs","[]")] perm_Nil_lemma 1);
+by Auto_tac;
+qed "perm_empty_imp";
+
+Goal "([] <~~> xs) = (xs = [])";
+by (blast_tac (claset() addIs [perm_empty_imp]) 1);
+qed "perm_empty";
+AddIffs [perm_empty];
+
+Goal "(xs <~~> []) = (xs = [])";
+by Auto_tac;
+by (etac (perm_sym RS perm_empty_imp) 1);
+qed "perm_empty2";
+AddIffs [perm_empty2];
+
+Goal "ys <~~> xs ==> xs=[y] --> ys=[y]";
+by (etac perm.induct 1);
+by Auto_tac;
+qed "perm_one_elem_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])));
+qed "perm_sing_eq";
+AddIffs [perm_sing_eq];
+
+Goal "([y] <~~> ys) = (ys = [y])"; 
+by Auto_tac;
+bd perm_sym 1;
+by Auto_tac;
+qed "perm_sing_eq2";
+AddIffs [perm_sing_eq2];
+
+Goal "x:set ys --> ys <~~> x#(remove x ys)";
+by (induct_tac "ys" 1);
+by (auto_tac (claset() addIs perm_rules, simpset()));
+qed_spec_mp "perm_remove"; 
+
+Goal "remove x (remove y l) = remove y (remove x l)";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed "remove_commute";
+
+(*Congruence rule*)
+Goal "xs <~~> ys ==> remove z xs <~~> remove z ys";
+by (etac perm.induct 1);
+by (auto_tac (claset() addIs perm_rules, simpset()));
+by Auto_tac;
+qed "perm_remove_perm";
+
+Goal "remove z (z#xs) = xs";
+by Auto_tac;
+qed "remove_hd";
+Addsimps [remove_hd];
+
+Goal "z#xs <~~> z#ys ==> xs <~~> ys";
+by (dres_inst_tac [("z","z")] perm_remove_perm 1);
+by Auto_tac;
+qed "cons_perm_imp_perm";
+
+Goal "(z#xs <~~> z#ys) = (xs <~~> ys)";
+by (blast_tac (claset() addIs [cons_perm_imp_perm, perm.Cons]) 1);
+qed "cons_perm_eq";
+AddIffs [cons_perm_eq];
+
+Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys";
+by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (ALLGOALS Full_simp_tac);
+by (blast_tac (claset() addSDs [spec]) 1);
+qed_spec_mp "append_perm_imp_perm";
+
+Goal "(zs@xs <~~> zs@ys) = (xs <~~> ys)";
+by (blast_tac (claset() addIs [append_perm_imp_perm, perm_append1]) 1);
+qed "perm_append1_eq";
+AddIffs [perm_append1_eq];

--- a/src/HOL/Induct/Perm.thy	Wed Mar 08 16:14:12 2000 +0100
+++ b/src/HOL/Induct/Perm.thy	Wed Mar 08 16:15:41 2000 +0100
@@ -21,4 +21,12 @@
     Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
     trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
 
+
+consts
+  remove  :: ['a, 'a list] => 'a list
+
+primrec 
+  "remove x []     = []"
+  "remove x (y#ys) = (if x=y then ys else y#remove x ys)"
+
 end