author haftmann Thu Feb 18 17:53:09 2016 +0100 (2016-02-18) changeset 62366 95c6cf433c91 parent 62365 8a105c235b1f child 62367 d2bc8a7e5fec
more theorems
 src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Number_Theory/Factorial_Ring.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions
```     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.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)
```