more theorems
authorhaftmann
Thu Feb 18 17:53:09 2016 +0100 (2016-02-18)
changeset 6236695c6cf433c91
parent 62365 8a105c235b1f
child 62367 d2bc8a7e5fec
more theorems
src/HOL/Library/Multiset.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Power.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Feb 18 17:52:53 2016 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Feb 18 17:53:09 2016 +0100
     1.3 @@ -1164,6 +1164,15 @@
     1.4    "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
     1.5    by (induct xs) auto
     1.6  
     1.7 +lemma replicate_mset_eq_empty_iff [simp]:
     1.8 +  "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
     1.9 +  by (induct n) simp_all
    1.10 +
    1.11 +lemma replicate_mset_eq_iff:
    1.12 +  "replicate_mset m a = replicate_mset n b \<longleftrightarrow>
    1.13 +    m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
    1.14 +  by (auto simp add: multiset_eq_iff)
    1.15 +
    1.16  
    1.17  subsection \<open>Big operators\<close>
    1.18  
    1.19 @@ -1237,6 +1246,12 @@
    1.20        (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
    1.21  qed
    1.22  
    1.23 +syntax (ASCII)
    1.24 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
    1.25 +syntax
    1.26 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    1.27 +translations
    1.28 +  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
    1.29  
    1.30  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
    1.31    where "\<Union># MM \<equiv> msetsum MM"
    1.32 @@ -1247,12 +1262,14 @@
    1.33  lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
    1.34    by (induct MM) auto
    1.35  
    1.36 -syntax (ASCII)
    1.37 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
    1.38 -syntax
    1.39 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    1.40 -translations
    1.41 -  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
    1.42 +lemma count_setsum:
    1.43 +  "count (setsum f A) x = setsum (\<lambda>a. count (f a) x) A"
    1.44 +  by (induct A rule: infinite_finite_induct) simp_all
    1.45 +
    1.46 +lemma setsum_eq_empty_iff:
    1.47 +  assumes "finite A"
    1.48 +  shows "setsum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
    1.49 +  using assms by induct simp_all
    1.50  
    1.51  context comm_monoid_mult
    1.52  begin
    1.53 @@ -1302,6 +1319,10 @@
    1.54    then show ?thesis by simp
    1.55  qed
    1.56  
    1.57 +lemma (in semidom) msetprod_zero_iff:
    1.58 +  "msetprod A = 0 \<longleftrightarrow> (\<exists>a\<in>set_mset A. a = 0)"
    1.59 +  by (induct A) auto
    1.60 +
    1.61  
    1.62  subsection \<open>Alternative representations\<close>
    1.63  
     2.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Feb 18 17:52:53 2016 +0100
     2.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Feb 18 17:53:09 2016 +0100
     2.3 @@ -8,27 +8,6 @@
     2.4  imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
     2.5  begin
     2.6  
     2.7 -context algebraic_semidom
     2.8 -begin
     2.9 -
    2.10 -lemma is_unit_mult_iff:
    2.11 -  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
    2.12 -  by (auto dest: dvd_mult_left dvd_mult_right)
    2.13 -
    2.14 -lemma is_unit_power_iff:
    2.15 -  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
    2.16 -  by (induct n) (auto simp add: is_unit_mult_iff)
    2.17 -  
    2.18 -lemma subset_divisors_dvd:
    2.19 -  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
    2.20 -  by (auto simp add: subset_iff intro: dvd_trans)
    2.21 -
    2.22 -lemma strict_subset_divisors_dvd:
    2.23 -  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
    2.24 -  by (auto simp add: subset_iff intro: dvd_trans)
    2.25 -
    2.26 -end
    2.27 -
    2.28  class factorial_semiring = normalization_semidom +
    2.29    assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
    2.30    fixes is_prime :: "'a \<Rightarrow> bool"
     3.1 --- a/src/HOL/Power.thy	Thu Feb 18 17:52:53 2016 +0100
     3.2 +++ b/src/HOL/Power.thy	Thu Feb 18 17:53:09 2016 +0100
     3.3 @@ -331,6 +331,10 @@
     3.4    shows "(a div b) ^ n = a ^ n div b ^ n"
     3.5    using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
     3.6  
     3.7 +lemma is_unit_power_iff:
     3.8 +  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
     3.9 +  by (induct n) (auto simp add: is_unit_mult_iff)
    3.10 +
    3.11  end
    3.12  
    3.13  context normalization_semidom
     4.1 --- a/src/HOL/Rings.thy	Thu Feb 18 17:52:53 2016 +0100
     4.2 +++ b/src/HOL/Rings.thy	Thu Feb 18 17:53:09 2016 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  section \<open>Rings\<close>
     4.5  
     4.6  theory Rings
     4.7 -imports Groups
     4.8 +imports Groups Set
     4.9  begin
    4.10  
    4.11  class semiring = ab_semigroup_add + semigroup_mult +
    4.12 @@ -155,6 +155,14 @@
    4.13    then show ?thesis ..
    4.14  qed
    4.15  
    4.16 +lemma subset_divisors_dvd:
    4.17 +  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
    4.18 +  by (auto simp add: subset_iff intro: dvd_trans)
    4.19 +
    4.20 +lemma strict_subset_divisors_dvd:
    4.21 +  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
    4.22 +  by (auto simp add: subset_iff intro: dvd_trans)
    4.23 +
    4.24  lemma one_dvd [simp]:
    4.25    "1 dvd a"
    4.26    by (auto intro!: dvdI)
    4.27 @@ -847,6 +855,10 @@
    4.28    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
    4.29    by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
    4.30  
    4.31 +lemma is_unit_mult_iff:
    4.32 +  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
    4.33 +  by (auto dest: dvd_mult_left dvd_mult_right)
    4.34 +
    4.35  lemma unit_div [intro]:
    4.36    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
    4.37    by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)