src/HOL/Library/Permutation.thy
 changeset 15072 4861bf6af0b4 parent 15005 546c8e7e28d4 child 15131 c69542757a4d
```--- a/src/HOL/Library/Permutation.thy	Wed Jul 21 16:35:38 2004 +0200
+++ b/src/HOL/Library/Permutation.thy	Thu Jul 22 10:33:26 2004 +0200
@@ -28,7 +28,8 @@
subsection {* Some examples of rule induction on permutations *}

lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
-    -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *}
+    -- {*the form of the premise lets the induction bind @{term xs}
+         and @{term ys} *}
apply (erule perm.induct)
apply (simp_all (no_asm_simp))
done
@@ -69,10 +70,7 @@
done

lemma perm_append_single: "a # xs <~~> xs @ [a]"
-  apply (rule perm.trans)
-   prefer 2
-   apply (rule perm_append_swap, simp)
-  done
+  by (rule perm.trans [OF _ perm_append_swap], simp)

lemma perm_rev: "rev xs <~~> xs"
apply (induct xs, simp_all)
@@ -120,6 +118,10 @@
lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
by (induct l, auto)

+lemma multiset_of_remove[simp]:
+  "multiset_of (remove a x) = multiset_of x - {#a#}"
+  by (induct_tac x, auto simp: multiset_eq_conv_count_eq)
+

text {* \medskip Congruence rule *}

@@ -127,8 +129,7 @@
by (erule perm.induct, auto)

lemma remove_hd [simp]: "remove z (z # xs) = xs"
-  apply auto
-  done
+  by auto

lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
by (drule_tac z = z in perm_remove_perm, auto)
@@ -153,31 +154,11 @@
apply (blast intro: perm_append_swap)
done

-(****************** Norbert Voelker 17 June 2004 **************)
-
-consts
-  multiset_of :: "'a list \<Rightarrow> 'a multiset"
-primrec
-  "multiset_of [] = {#}"
-  "multiset_of (a # x) = multiset_of x + {# a #}"
-
-lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
-  by (induct_tac x, auto)
-
-lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
-  by (induct_tac x, auto)
-
-lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
- by (induct_tac x, auto)
-
-lemma multiset_of_remove[simp]:
-  "multiset_of (remove a x) = multiset_of x - {#a#}"
-  by (induct_tac x, auto simp: multiset_eq_conv_count_eq)
-
-lemma multiset_of_eq_perm:  "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
+lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
apply (rule iffI)
apply (erule_tac [2] perm.induct, simp_all add: union_ac)
-  apply (erule rev_mp, rule_tac x=ys in spec, induct_tac xs, auto)
+  apply (erule rev_mp, rule_tac x=ys in spec)
+  apply (induct_tac xs, auto)
apply (erule_tac x = "remove a x" in allE, drule sym, simp)
apply (subgoal_tac "a \<in> set x")
apply (drule_tac z=a in perm.Cons)
@@ -185,15 +166,11 @@
apply (drule_tac f=set_of in arg_cong, simp)
done

-lemma set_count_multiset_of: "set x = {a. 0 < count (multiset_of x) a}"
-  by (induct_tac x, auto)
-
-lemma distinct_count_multiset_of:
-   "distinct x \<Longrightarrow> count (multiset_of x) a = (if a \<in> set x then 1 else 0)"
-  by (erule rev_mp, induct_tac x, auto)
-
-lemma distinct_set_eq_iff_multiset_of_eq:
-  "\<lbrakk>distinct x; distinct y\<rbrakk> \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
-  by (auto simp: multiset_eq_conv_count_eq distinct_count_multiset_of)
+lemma multiset_of_le_perm_append:
+  "(multiset_of xs \<le># multiset_of ys) = (\<exists> zs. xs @ zs <~~> ys)";
+  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
+  apply (insert surj_multiset_of, drule surjD)
+  apply (blast intro: sym)+
+  done

end```