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  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
```