--- a/src/HOL/Number_Theory/UniqueFactorization.thy Tue Mar 26 22:09:39 2013 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Mar 27 10:55:05 2013 +0100
@@ -36,102 +36,6 @@
"ALL i :# M. P i"?
*)
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
-locale comm_monoid_mset = comm_monoid
-begin
-
-definition F :: "'a multiset \<Rightarrow> 'a"
-where
- eq_fold: "F M = Multiset.fold f 1 M"
-
-lemma empty [simp]:
- "F {#} = 1"
- by (simp add: eq_fold)
-
-lemma singleton [simp]:
- "F {#x#} = x"
-proof -
- interpret comp_fun_commute
- by default (simp add: fun_eq_iff left_commute)
- show ?thesis by (simp add: eq_fold)
-qed
-
-lemma union [simp]:
- "F (M + N) = F M * F N"
-proof -
- interpret comp_fun_commute f
- by default (simp add: fun_eq_iff left_commute)
- show ?thesis by (induct N) (simp_all add: left_commute eq_fold)
-qed
-
-end
-
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
-definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
-where
- "msetprod = comm_monoid_mset.F times 1"
-
-sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1
-where
- "comm_monoid_mset.F times 1 = msetprod"
-proof -
- show "comm_monoid_mset times 1" ..
- from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" by rule
-qed
-
-context comm_monoid_mult
-begin
-
-lemma msetprod_empty:
- "msetprod {#} = 1"
- by (fact msetprod.empty)
-
-lemma msetprod_singleton:
- "msetprod {#x#} = x"
- by (fact msetprod.singleton)
-
-lemma msetprod_Un:
- "msetprod (A + B) = msetprod A * msetprod B"
- by (fact msetprod.union)
-
-lemma msetprod_multiplicity:
- "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
- by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
-
-abbreviation msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
-where
- "msetprod_image f M \<equiv> msetprod (image_mset f M)"
-
-end
-
-syntax
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3PROD _:#_. _)" [0, 51, 10] 10)
-
-syntax (xsymbols)
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
-
-syntax (HTML output)
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
-
-translations
- "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
-
-lemma (in comm_semiring_1) dvd_msetprod:
- assumes "x \<in># A"
- shows "x dvd msetprod A"
-proof -
- from assms have "A = (A - {#x#}) + {#x#}" by simp
- then obtain B where "A = B + {#x#}" ..
- then show ?thesis by simp
-qed
-
subsection {* unique factorization: multiset version *}