src/HOL/Library/Permutation.thy
changeset 15072 4861bf6af0b4
parent 15005 546c8e7e28d4
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Library/Permutation.thy	Wed Jul 21 16:35:38 2004 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Thu Jul 22 10:33:26 2004 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4  subsection {* Some examples of rule induction on permutations *}
     1.5  
     1.6  lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
     1.7 -    -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *}
     1.8 +    -- {*the form of the premise lets the induction bind @{term xs} 
     1.9 +         and @{term ys} *}
    1.10    apply (erule perm.induct)
    1.11       apply (simp_all (no_asm_simp))
    1.12    done
    1.13 @@ -69,10 +70,7 @@
    1.14    done
    1.15  
    1.16  lemma perm_append_single: "a # xs <~~> xs @ [a]"
    1.17 -  apply (rule perm.trans)
    1.18 -   prefer 2
    1.19 -   apply (rule perm_append_swap, simp)
    1.20 -  done
    1.21 +  by (rule perm.trans [OF _ perm_append_swap], simp)
    1.22  
    1.23  lemma perm_rev: "rev xs <~~> xs"
    1.24    apply (induct xs, simp_all)
    1.25 @@ -120,6 +118,10 @@
    1.26  lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
    1.27  by (induct l, auto)
    1.28  
    1.29 +lemma multiset_of_remove[simp]: 
    1.30 +  "multiset_of (remove a x) = multiset_of x - {#a#}"
    1.31 +  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
    1.32 +
    1.33  
    1.34  text {* \medskip Congruence rule *}
    1.35  
    1.36 @@ -127,8 +129,7 @@
    1.37  by (erule perm.induct, auto)
    1.38  
    1.39  lemma remove_hd [simp]: "remove z (z # xs) = xs"
    1.40 -  apply auto
    1.41 -  done
    1.42 +  by auto
    1.43  
    1.44  lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
    1.45  by (drule_tac z = z in perm_remove_perm, auto)
    1.46 @@ -153,31 +154,11 @@
    1.47    apply (blast intro: perm_append_swap)
    1.48    done
    1.49  
    1.50 -(****************** Norbert Voelker 17 June 2004 **************) 
    1.51 -
    1.52 -consts 
    1.53 -  multiset_of :: "'a list \<Rightarrow> 'a multiset"
    1.54 -primrec
    1.55 -  "multiset_of [] = {#}"
    1.56 -  "multiset_of (a # x) = multiset_of x + {# a #}"
    1.57 -
    1.58 -lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    1.59 -  by (induct_tac x, auto) 
    1.60 -
    1.61 -lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
    1.62 -  by (induct_tac x, auto)
    1.63 -
    1.64 -lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
    1.65 - by (induct_tac x, auto) 
    1.66 -
    1.67 -lemma multiset_of_remove[simp]: 
    1.68 -  "multiset_of (remove a x) = multiset_of x - {#a#}"
    1.69 -  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
    1.70 -
    1.71 -lemma multiset_of_eq_perm:  "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
    1.72 +lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
    1.73    apply (rule iffI) 
    1.74    apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
    1.75 -  apply (erule rev_mp, rule_tac x=ys in spec, induct_tac xs, auto) 
    1.76 +  apply (erule rev_mp, rule_tac x=ys in spec) 
    1.77 +  apply (induct_tac xs, auto) 
    1.78    apply (erule_tac x = "remove a x" in allE, drule sym, simp) 
    1.79    apply (subgoal_tac "a \<in> set x") 
    1.80    apply (drule_tac z=a in perm.Cons) 
    1.81 @@ -185,15 +166,11 @@
    1.82    apply (drule_tac f=set_of in arg_cong, simp)
    1.83    done
    1.84  
    1.85 -lemma set_count_multiset_of: "set x = {a. 0 < count (multiset_of x) a}"
    1.86 -  by (induct_tac x, auto)  
    1.87 -
    1.88 -lemma distinct_count_multiset_of: 
    1.89 -   "distinct x \<Longrightarrow> count (multiset_of x) a = (if a \<in> set x then 1 else 0)"
    1.90 -  by (erule rev_mp, induct_tac x, auto) 
    1.91 -
    1.92 -lemma distinct_set_eq_iff_multiset_of_eq: 
    1.93 -  "\<lbrakk>distinct x; distinct y\<rbrakk> \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
    1.94 -  by (auto simp: multiset_eq_conv_count_eq distinct_count_multiset_of) 
    1.95 +lemma multiset_of_le_perm_append: 
    1.96 +  "(multiset_of xs \<le># multiset_of ys) = (\<exists> zs. xs @ zs <~~> ys)"; 
    1.97 +  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
    1.98 +  apply (insert surj_multiset_of, drule surjD)
    1.99 +  apply (blast intro: sym)+
   1.100 +  done
   1.101  
   1.102  end