1.1 --- a/src/HOL/Library/Permutation.thy	Wed May 12 22:33:10 2010 -0700
     1.2 +++ b/src/HOL/Library/Permutation.thy	Thu May 13 14:34:05 2010 +0200
     1.3 @@ -93,29 +93,16 @@
     1.4  
     1.5  subsection {* Removing elements *}
     1.6  
     1.7 -primrec remove :: "'a => 'a list => 'a list" where
     1.8 -    "remove x [] = []"
     1.9 -  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    1.10 -
    1.11 -lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
    1.12 +lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys"
    1.13    by (induct ys) auto
    1.14  
    1.15 -lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
    1.16 -  by (induct l) auto
    1.17 -
    1.18 -lemma multiset_of_remove [simp]:
    1.19 -    "multiset_of (remove a x) = multiset_of x - {#a#}"
    1.20 -  apply (induct x)
    1.21 -   apply (auto simp: multiset_eq_conv_count_eq)
    1.22 -  done
    1.23 -
    1.24  
    1.25  text {* \medskip Congruence rule *}
    1.26  
    1.27 -lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
    1.28 +lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys"
    1.29    by (induct pred: perm) auto
    1.30  
    1.31 -lemma remove_hd [simp]: "remove z (z # xs) = xs"
    1.32 +lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
    1.33    by auto
    1.34  
    1.35  lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
    1.36 @@ -146,7 +133,7 @@
    1.37    apply (erule_tac [2] perm.induct, simp_all add: union_ac)
    1.38    apply (erule rev_mp, rule_tac x=ys in spec)
    1.39    apply (induct_tac xs, auto)
    1.40 -  apply (erule_tac x = "remove a x" in allE, drule sym, simp)
    1.41 +  apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
    1.42    apply (subgoal_tac "a \<in> set x")
    1.43    apply (drule_tac z=a in perm.Cons)
    1.44    apply (erule perm.trans, rule perm_sym, erule perm_remove)