--- a/src/HOL/BNF/More_BNFs.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Wed Mar 27 21:13:02 2013 +0100
@@ -532,34 +532,6 @@
(* Multisets *)
-(* The cardinal of a mutiset: this, and the following basic lemmas about it,
-should eventually go into Multiset.thy *)
-definition "mcard M \<equiv> setsum (count M) {a. count M a > 0}"
-
-lemma mcard_emp[simp]: "mcard {#} = 0"
-unfolding mcard_def by auto
-
-lemma mcard_emp_iff[simp]: "mcard M = 0 \<longleftrightarrow> M = {#}"
-unfolding mcard_def apply safe
- apply simp_all
- by (metis multi_count_eq zero_multiset.rep_eq)
-
-lemma mcard_singl[simp]: "mcard {#a#} = Suc 0"
-unfolding mcard_def by auto
-
-lemma mcard_Plus[simp]: "mcard (M + N) = mcard M + mcard N"
-proof -
- have "setsum (count M) {a. 0 < count M a + count N a} =
- setsum (count M) {a. a \<in># M}"
- apply (rule setsum_mono_zero_cong_right) by auto
- moreover
- have "setsum (count N) {a. 0 < count M a + count N a} =
- setsum (count N) {a. a \<in># N}"
- apply (rule setsum_mono_zero_cong_right) by auto
- ultimately show ?thesis
- unfolding mcard_def count_union [THEN ext] by (simp add: setsum.distrib)
-qed
-
lemma setsum_gt_0_iff:
fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
@@ -1246,7 +1218,7 @@
using multiset_rel_Zero multiset_rel_Plus by auto
lemma mcard_multiset_map[simp]: "mcard (multiset_map f M) = mcard M"
-proof-
+proof -
def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
let ?B = "{b. 0 < setsum (count M) (A b)}"
have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
@@ -1273,7 +1245,7 @@
also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
setsum (count M) {a. a \<in># M}" .
- thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def)
+ then show ?thesis by (simp add: A_def mcard_unfold_setsum multiset_map_def set_of_def mmap_def)
qed
lemma multiset_rel_mcard:
--- a/src/HOL/Big_Operators.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Big_Operators.thy Wed Mar 27 21:13:02 2013 +0100
@@ -325,12 +325,11 @@
sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0
where
- "setsum.F = setsum"
+ "comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_set plus 0" ..
then interpret setsum!: comm_monoid_set plus 0 .
- show "setsum.F = setsum"
- by (simp only: setsum_def)
+ from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
qed
abbreviation
@@ -1048,12 +1047,11 @@
sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1
where
- "setprod.F = setprod"
+ "comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_set times 1" ..
then interpret setprod!: comm_monoid_set times 1 .
- show "setprod.F = setprod"
- by (simp only: setprod_def)
+ from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
qed
abbreviation
@@ -1743,22 +1741,20 @@
sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
where
- "Inf_fin.F = Inf_fin"
+ "semilattice_set.F inf = Inf_fin"
proof -
show "semilattice_order_set inf less_eq less" ..
then interpret Inf_fin!: semilattice_order_set inf less_eq less.
- show "Inf_fin.F = Inf_fin"
- by (fact Inf_fin_def [symmetric])
+ from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
qed
sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
where
- "Sup_fin.F = Sup_fin"
+ "semilattice_set.F sup = Sup_fin"
proof -
show "semilattice_order_set sup greater_eq greater" ..
then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
- show "Sup_fin.F = Sup_fin"
- by (fact Sup_fin_def [symmetric])
+ from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
qed
@@ -1910,12 +1906,6 @@
subsection {* Minimum and Maximum over non-empty sets *}
-text {*
- This case is already setup by the @{text min_max} sublocale dependency from above. But note
- that this yields irregular prefixes, e.g.~@{text min_max.Inf_fin.insert} instead
- of @{text Max.insert}.
-*}
-
context linorder
begin
--- a/src/HOL/Finite_Set.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Finite_Set.thy Wed Mar 27 21:13:02 2013 +0100
@@ -1107,11 +1107,11 @@
interpretation card!: folding "\<lambda>_. Suc" 0
where
- "card.F = card"
+ "folding.F (\<lambda>_. Suc) 0 = card"
proof -
show "folding (\<lambda>_. Suc)" by default rule
then interpret card!: folding "\<lambda>_. Suc" 0 .
- show "card.F = card" by (simp only: card_def)
+ from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
qed
lemma card_infinite:
--- a/src/HOL/GCD.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/GCD.thy Wed Mar 27 21:13:02 2013 +0100
@@ -1545,24 +1545,30 @@
qed simp
interpretation gcd_lcm_complete_lattice_nat:
- complete_lattice Gcd Lcm gcd "op dvd" "\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m" lcm 1 0
-proof
- case goal1 show ?case by simp
-next
- case goal2 show ?case by simp
-next
- case goal5 thus ?case by (rule dvd_Lcm_nat)
-next
- case goal6 thus ?case by simp
-next
- case goal3 thus ?case by (simp add: Gcd_nat_def)
-next
- case goal4 thus ?case by (simp add: Gcd_nat_def)
+ complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
+where
+ "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)"
+ and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)"
+proof -
+ show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
+ proof
+ case goal1 show ?case by simp
+ next
+ case goal2 show ?case by simp
+ next
+ case goal5 thus ?case by (rule dvd_Lcm_nat)
+ next
+ case goal6 thus ?case by simp
+ next
+ case goal3 thus ?case by (simp add: Gcd_nat_def)
+ next
+ case goal4 thus ?case by (simp add: Gcd_nat_def)
+ qed
+ then interpret gcd_lcm_complete_lattice_nat:
+ complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
+ from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" .
+ from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" .
qed
-(* bh: This interpretation generates many lemmas about
-"complete_lattice.SUPR Lcm" and "complete_lattice.INFI Gcd".
-Should we define binder versions of LCM and GCD to correspond
-with these? *)
lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
@@ -1717,11 +1723,12 @@
using assms by (simp add: Gcd_int_def dvd_int_iff)
lemma Lcm_set_int [code_unfold]:
- "Lcm (set xs) = foldl lcm (1::int) xs"
+ "Lcm (set xs) = fold lcm xs (1::int)"
by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
lemma Gcd_set_int [code_unfold]:
- "Gcd (set xs) = foldl gcd (0::int) xs"
+ "Gcd (set xs) = fold gcd xs (0::int)"
by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
end
+
--- a/src/HOL/Groups.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Groups.thy Wed Mar 27 21:13:02 2013 +0100
@@ -91,8 +91,8 @@
fixes z :: 'a ("1")
assumes comm_neutral: "a * 1 = a"
-sublocale comm_monoid < monoid proof
-qed (simp_all add: commute comm_neutral)
+sublocale comm_monoid < monoid
+ by default (simp_all add: commute comm_neutral)
subsection {* Generic operations *}
@@ -151,14 +151,14 @@
class semigroup_add = plus +
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
-sublocale semigroup_add < add!: semigroup plus proof
-qed (fact add_assoc)
+sublocale semigroup_add < add!: semigroup plus
+ by default (fact add_assoc)
class ab_semigroup_add = semigroup_add +
assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
-sublocale ab_semigroup_add < add!: abel_semigroup plus proof
-qed (fact add_commute)
+sublocale ab_semigroup_add < add!: abel_semigroup plus
+ by default (fact add_commute)
context ab_semigroup_add
begin
@@ -174,14 +174,14 @@
class semigroup_mult = times +
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
-sublocale semigroup_mult < mult!: semigroup times proof
-qed (fact mult_assoc)
+sublocale semigroup_mult < mult!: semigroup times
+ by default (fact mult_assoc)
class ab_semigroup_mult = semigroup_mult +
assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
-sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
-qed (fact mult_commute)
+sublocale ab_semigroup_mult < mult!: abel_semigroup times
+ by default (fact mult_commute)
context ab_semigroup_mult
begin
@@ -198,8 +198,8 @@
assumes add_0_left: "0 + a = a"
and add_0_right: "a + 0 = a"
-sublocale monoid_add < add!: monoid plus 0 proof
-qed (fact add_0_left add_0_right)+
+sublocale monoid_add < add!: monoid plus 0
+ by default (fact add_0_left add_0_right)+
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
by (rule eq_commute)
@@ -207,11 +207,11 @@
class comm_monoid_add = zero + ab_semigroup_add +
assumes add_0: "0 + a = a"
-sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
-qed (insert add_0, simp add: ac_simps)
+sublocale comm_monoid_add < add!: comm_monoid plus 0
+ by default (insert add_0, simp add: ac_simps)
-subclass (in comm_monoid_add) monoid_add proof
-qed (fact add.left_neutral add.right_neutral)+
+subclass (in comm_monoid_add) monoid_add
+ by default (fact add.left_neutral add.right_neutral)+
class comm_monoid_diff = comm_monoid_add + minus +
assumes diff_zero [simp]: "a - 0 = a"
@@ -268,8 +268,8 @@
assumes mult_1_left: "1 * a = a"
and mult_1_right: "a * 1 = a"
-sublocale monoid_mult < mult!: monoid times 1 proof
-qed (fact mult_1_left mult_1_right)+
+sublocale monoid_mult < mult!: monoid times 1
+ by default (fact mult_1_left mult_1_right)+
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
by (rule eq_commute)
@@ -277,11 +277,11 @@
class comm_monoid_mult = one + ab_semigroup_mult +
assumes mult_1: "1 * a = a"
-sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
-qed (insert mult_1, simp add: ac_simps)
+sublocale comm_monoid_mult < mult!: comm_monoid times 1
+ by default (insert mult_1, simp add: ac_simps)
-subclass (in comm_monoid_mult) monoid_mult proof
-qed (fact mult.left_neutral mult.right_neutral)+
+subclass (in comm_monoid_mult) monoid_mult
+ by default (fact mult.left_neutral mult.right_neutral)+
class cancel_semigroup_add = semigroup_add +
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
--- a/src/HOL/Lattices.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Lattices.thy Wed Mar 27 21:13:02 2013 +0100
@@ -471,25 +471,23 @@
class bounded_semilattice_inf_top = semilattice_inf + top
sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+ + inf_top!: semilattice_neutr_order inf top less_eq less
proof
fix x
show "x \<sqinter> \<top> = x"
by (rule inf_absorb1) simp
qed
-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
-
class bounded_semilattice_sup_bot = semilattice_sup + bot
sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+ + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
proof
fix x
show "x \<squnion> \<bottom> = x"
by (rule sup_absorb1) simp
qed
-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
-
class bounded_lattice_bot = lattice + bot
begin
--- a/src/HOL/Library/Multiset.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Mar 27 21:13:02 2013 +0100
@@ -702,7 +702,7 @@
then show ?thesis by simp
qed
-lemma fold_mset_fun_comm:
+lemma fold_mset_fun_left_comm:
"f x (fold f s M) = fold f (f x s) M"
by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
@@ -714,7 +714,7 @@
case (add M x)
have "M + {#x#} + N = (M + N) + {#x#}"
by (simp add: add_ac)
- with add show ?case by (simp add: fold_mset_insert fold_mset_fun_comm)
+ with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
qed
lemma fold_mset_fusion:
@@ -821,9 +821,7 @@
declare image_mset.identity [simp]
-subsection {* Alternative representations *}
-
-subsubsection {* Lists *}
+subsection {* Further conversions *}
primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
"multiset_of [] = {#}" |
@@ -950,6 +948,257 @@
ultimately show ?case by simp
qed
+lemma multiset_of_insort [simp]:
+ "multiset_of (insort x xs) = multiset_of xs + {#x#}"
+ by (induct xs) (simp_all add: ac_simps)
+
+definition multiset_of_set :: "'a set \<Rightarrow> 'a multiset"
+where
+ "multiset_of_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
+
+interpretation multiset_of_set!: folding "\<lambda>x M. {#x#} + M" "{#}"
+where
+ "folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set"
+proof -
+ interpret comp_fun_commute "\<lambda>x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps)
+ show "folding (\<lambda>x M. {#x#} + M)" by default (fact comp_fun_commute)
+ from multiset_of_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" ..
+qed
+
+context linorder
+begin
+
+definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
+where
+ "sorted_list_of_multiset M = fold insort [] M"
+
+lemma sorted_list_of_multiset_empty [simp]:
+ "sorted_list_of_multiset {#} = []"
+ by (simp add: sorted_list_of_multiset_def)
+
+lemma sorted_list_of_multiset_singleton [simp]:
+ "sorted_list_of_multiset {#x#} = [x]"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show ?thesis by (simp add: sorted_list_of_multiset_def)
+qed
+
+lemma sorted_list_of_multiset_insert [simp]:
+ "sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)"
+proof -
+ interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
+ show ?thesis by (simp add: sorted_list_of_multiset_def)
+qed
+
+end
+
+lemma multiset_of_sorted_list_of_multiset [simp]:
+ "multiset_of (sorted_list_of_multiset M) = M"
+ by (induct M) simp_all
+
+lemma sorted_list_of_multiset_multiset_of [simp]:
+ "sorted_list_of_multiset (multiset_of xs) = sort xs"
+ by (induct xs) simp_all
+
+lemma finite_set_of_multiset_of_set:
+ assumes "finite A"
+ shows "set_of (multiset_of_set A) = A"
+ using assms by (induct A) simp_all
+
+lemma infinite_set_of_multiset_of_set:
+ assumes "\<not> finite A"
+ shows "set_of (multiset_of_set A) = {}"
+ using assms by simp
+
+lemma set_sorted_list_of_multiset [simp]:
+ "set (sorted_list_of_multiset M) = set_of M"
+ by (induct M) (simp_all add: set_insort)
+
+lemma sorted_list_of_multiset_of_set [simp]:
+ "sorted_list_of_multiset (multiset_of_set A) = sorted_list_of_set A"
+ by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
+
+
+subsection {* Big operators *}
+
+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_add) msetsum :: "'a multiset \<Rightarrow> 'a"
+where
+ "msetsum = comm_monoid_mset.F plus 0"
+
+definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
+where
+ "msetprod = comm_monoid_mset.F times 1"
+
+sublocale comm_monoid_add < msetsum!: comm_monoid_mset plus 0
+where
+ "comm_monoid_mset.F plus 0 = msetsum"
+proof -
+ show "comm_monoid_mset plus 0" ..
+ from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
+qed
+
+context comm_monoid_add
+begin
+
+lemma setsum_unfold_msetsum:
+ "setsum f A = msetsum (image_mset f (multiset_of_set A))"
+ by (cases "finite A") (induct A rule: finite_induct, simp_all)
+
+abbreviation msetsum_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
+where
+ "msetsum_image f M \<equiv> msetsum (image_mset f M)"
+
+end
+
+syntax
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ ("(3SUM _:#_. _)" [0, 51, 10] 10)
+
+syntax (xsymbols)
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ ("(3\<Sum>_:#_. _)" [0, 51, 10] 10)
+
+syntax (HTML output)
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+
+translations
+ "SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
+
+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" ..
+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 setprod_unfold_msetprod:
+ "setprod f A = msetprod (image_mset f (multiset_of_set A))"
+ by (cases "finite A") (induct A rule: finite_induct, simp_all)
+
+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\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
+
+syntax (HTML output)
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ ("(3\<Prod>_\<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 {* Cardinality *}
+
+definition mcard :: "'a multiset \<Rightarrow> nat"
+where
+ "mcard = msetsum \<circ> image_mset (\<lambda>_. 1)"
+
+lemma mcard_empty [simp]:
+ "mcard {#} = 0"
+ by (simp add: mcard_def)
+
+lemma mcard_singleton [simp]:
+ "mcard {#a#} = Suc 0"
+ by (simp add: mcard_def)
+
+lemma mcard_plus [simp]:
+ "mcard (M + N) = mcard M + mcard N"
+ by (simp add: mcard_def)
+
+lemma mcard_empty_iff [simp]:
+ "mcard M = 0 \<longleftrightarrow> M = {#}"
+ by (induct M) simp_all
+
+lemma mcard_unfold_setsum:
+ "mcard M = setsum (count M) (set_of M)"
+proof (induct M)
+ case empty then show ?case by simp
+next
+ case (add M x) then show ?case
+ by (cases "x \<in> set_of M")
+ (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp)
+qed
+
+
+subsection {* Alternative representations *}
+
+subsubsection {* Lists *}
+
context linorder
begin
--- a/src/HOL/List.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/List.thy Wed Mar 27 21:13:02 2013 +0100
@@ -4338,6 +4338,10 @@
context linorder
begin
+lemma set_insort_key:
+ "set (insort_key f x xs) = insert x (set xs)"
+ by (induct xs) auto
+
lemma length_insort [simp]:
"length (insort_key f x xs) = Suc (length xs)"
by (induct xs) simp_all
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Mar 27 21:13:02 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 *}
--- a/src/HOL/Orderings.thy Wed Mar 27 21:07:10 2013 +0100
+++ b/src/HOL/Orderings.thy Wed Mar 27 21:13:02 2013 +0100
@@ -197,10 +197,7 @@
end
-sublocale order < order!: ordering less_eq less
- by default (auto intro: antisym order_trans simp add: less_le)
-
-sublocale order < dual_order!: ordering greater_eq greater
+sublocale order < order!: ordering less_eq less + dual_order!: ordering greater_eq greater
by default (auto intro: antisym order_trans simp add: less_le)
context order
@@ -210,7 +207,7 @@
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
-- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
-by (simp add: less_le) blast
+by (fact order.order_iff_strict)
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
unfolding less_le by blast
@@ -228,10 +225,10 @@
text {* Transitivity rules for calculational reasoning *}
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
-by (simp add: less_le)
+by (fact order.not_eq_order_implies_strict)
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
-by (simp add: less_le)
+by (rule order.not_eq_order_implies_strict)
text {* Asymmetry. *}
@@ -243,7 +240,7 @@
by (blast intro: antisym)
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
-by (erule contrapos_pn, erule subst, rule less_irrefl)
+by (fact order.strict_implies_not_eq)
text {* Least value operator *}
@@ -1168,7 +1165,6 @@
by (simp add: max_def)
-
subsection {* (Unique) top and bottom elements *}
class bot = order +
@@ -1176,8 +1172,7 @@
assumes bot_least: "\<bottom> \<le> a"
sublocale bot < bot!: ordering_top greater_eq greater bot
-proof
-qed (fact bot_least)
+ by default (fact bot_least)
context bot
begin
@@ -1205,8 +1200,7 @@
assumes top_greatest: "a \<le> \<top>"
sublocale top < top!: ordering_top less_eq less top
-proof
-qed (fact top_greatest)
+ by default (fact top_greatest)
context top
begin
@@ -1316,6 +1310,7 @@
class dense_linorder = inner_dense_linorder + no_top + no_bot
+
subsection {* Wellorders *}
class wellorder = linorder +