--- a/src/Doc/Main/Main_Doc.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Mon Oct 17 19:03:13 2016 +0200
@@ -409,7 +409,7 @@
@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
@{const Groups_Big.sum} & @{term_type_only Groups_Big.sum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\
-@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
+@{const Groups_Big.prod} & @{term_type_only Groups_Big.prod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
\end{supertabular}
--- a/src/HOL/Algebra/IntRing.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy Mon Oct 17 19:03:13 2016 +0200
@@ -73,7 +73,7 @@
qed
interpretation int: comm_monoid \<Z>
- rewrites "finprod \<Z> f A = setprod f A"
+ rewrites "finprod \<Z> f A = prod f A"
proof -
\<comment> "Specification"
show "comm_monoid \<Z>" by standard auto
@@ -83,7 +83,7 @@
{ fix x y have "mult \<Z> x y = x * y" by simp }
note mult = this
have one: "one \<Z> = 1" by simp
- show "finprod \<Z> f A = setprod f A"
+ show "finprod \<Z> f A = prod f A"
by (induct A rule: infinite_finite_induct, auto)
qed
--- a/src/HOL/Analysis/Bochner_Integration.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Mon Oct 17 19:03:13 2016 +0200
@@ -3003,7 +3003,7 @@
finally show ?thesis .
qed
-lemma (in product_sigma_finite) product_integrable_setprod:
+lemma (in product_sigma_finite) product_integrable_prod:
fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
@@ -3014,15 +3014,15 @@
using assms by simp
have "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) =
(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ennreal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
- by (simp add: setprod_norm setprod_ennreal)
+ by (simp add: prod_norm prod_ennreal)
also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ennreal (norm (f i x)) \<partial>M i)"
- using assms by (intro product_nn_integral_setprod) auto
+ using assms by (intro product_nn_integral_prod) auto
also have "\<dots> < \<infinity>"
- using integrable by (simp add: less_top[symmetric] ennreal_setprod_eq_top integrable_iff_bounded)
+ using integrable by (simp add: less_top[symmetric] ennreal_prod_eq_top integrable_iff_bounded)
finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
qed
-lemma (in product_sigma_finite) product_integral_setprod:
+lemma (in product_sigma_finite) product_integral_prod:
fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>L (M i) (f i))"
@@ -3036,10 +3036,10 @@
then have iI: "finite (insert i I)" by auto
then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
- by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
+ by (intro product_integrable_prod insert(4)) (auto intro: finite_subset)
interpret I: finite_product_sigma_finite M I by standard fact
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
- using \<open>i \<notin> I\<close> by (auto intro!: setprod.cong)
+ using \<open>i \<notin> I\<close> by (auto intro!: prod.cong)
show ?case
unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
by (simp add: * insert prod subset_insertI)
--- a/src/HOL/Analysis/Borel_Space.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1348,7 +1348,7 @@
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
-lemma borel_measurable_setprod[measurable (raw)]:
+lemma borel_measurable_prod[measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1652,7 +1652,7 @@
shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
using assms by (induction S rule: infinite_finite_induct) auto
-lemma borel_measurable_ereal_setprod[measurable (raw)]:
+lemma borel_measurable_ereal_prod[measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1728,7 +1728,7 @@
shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel"
unfolding is_borel_def[symmetric] by transfer simp
-lemma borel_measurable_setprod_ennreal[measurable (raw)]:
+lemma borel_measurable_prod_ennreal[measurable (raw)]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
--- a/src/HOL/Analysis/Determinants.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Determinants.thy Mon Oct 17 19:03:13 2016 +0200
@@ -37,20 +37,20 @@
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
"det A =
- sum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
+ sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
{p. p permutes (UNIV :: 'n set)}"
text \<open>A few general lemmas we need below.\<close>
-lemma setprod_permute:
+lemma prod_permute:
assumes p: "p permutes S"
- shows "setprod f S = setprod (f \<circ> p) S"
- using assms by (fact setprod.permute)
+ shows "prod f S = prod (f \<circ> p) S"
+ using assms by (fact prod.permute)
-lemma setproduct_permute_nat_interval:
+lemma product_permute_nat_interval:
fixes m n :: nat
- shows "p permutes {m..n} \<Longrightarrow> setprod f {m..n} = setprod (f \<circ> p) {m..n}"
- by (blast intro!: setprod_permute)
+ shows "p permutes {m..n} \<Longrightarrow> prod f {m..n} = prod (f \<circ> p) {m..n}"
+ by (blast intro!: prod_permute)
text \<open>Basic determinant properties.\<close>
@@ -70,12 +70,12 @@
have pi: "inj_on p ?U"
by (blast intro: subset_inj_on)
from permutes_image[OF pU]
- have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
- setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
+ have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
+ prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
by simp
- also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U"
- unfolding setprod.reindex[OF pi] ..
- also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
+ also have "\<dots> = prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U"
+ unfolding prod.reindex[OF pi] ..
+ also have "\<dots> = prod (\<lambda>i. ?di A i (p i)) ?U"
proof -
{
fix i
@@ -84,12 +84,12 @@
have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)"
unfolding transpose_def by (simp add: fun_eq_iff)
}
- then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U =
- setprod (\<lambda>i. ?di A i (p i)) ?U"
- by (auto intro: setprod.cong)
+ then show "prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U =
+ prod (\<lambda>i. ?di A i (p i)) ?U"
+ by (auto intro: prod.cong)
qed
- finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
- of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)"
+ finally have "of_int (sign (inv p)) * (prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
+ of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)"
using sth by simp
}
then show ?thesis
@@ -104,11 +104,11 @@
lemma det_lowerdiagonal:
fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
- shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
+ shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
proof -
let ?U = "UNIV:: 'n set"
let ?PU = "{p. p permutes ?U}"
- let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
+ let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
have fU: "finite ?U"
by simp
from finite_permutations[OF fU] have fPU: "finite ?PU" .
@@ -123,7 +123,7 @@
by (metis not_le)
from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
by blast
- from setprod_zero[OF fU ex] have "?pp p = 0"
+ from prod_zero[OF fU ex] have "?pp p = 0"
by simp
}
then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
@@ -135,11 +135,11 @@
lemma det_upperdiagonal:
fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
- shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
+ shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
proof -
let ?U = "UNIV:: 'n set"
let ?PU = "{p. p permutes ?U}"
- let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
+ let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
have fU: "finite ?U"
by simp
from finite_permutations[OF fU] have fPU: "finite ?PU" .
@@ -154,7 +154,7 @@
by (metis not_le)
from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
by blast
- from setprod_zero[OF fU ex] have "?pp p = 0"
+ from prod_zero[OF fU ex] have "?pp p = 0"
by simp
}
then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
@@ -166,11 +166,11 @@
lemma det_diagonal:
fixes A :: "'a::comm_ring_1^'n^'n"
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
- shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"
+ shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)"
proof -
let ?U = "UNIV:: 'n set"
let ?PU = "{p. p permutes ?U}"
- let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
+ let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
have fU: "finite ?U" by simp
from finite_permutations[OF fU] have fPU: "finite ?PU" .
have id0: "{id} \<subseteq> ?PU"
@@ -184,7 +184,7 @@
unfolding fun_eq_iff by auto
from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
by blast
- from setprod_zero [OF fU ex] have "?pp p = 0"
+ from prod_zero [OF fU ex] have "?pp p = 0"
by simp
}
then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
@@ -204,23 +204,23 @@
have "?f i i = 1"
using i by (vector mat_def)
}
- then have th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
- by (auto intro: setprod.cong)
+ then have th: "prod (\<lambda>i. ?f i i) ?U = prod (\<lambda>x. 1) ?U"
+ by (auto intro: prod.cong)
{
fix i j
assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
have "?f i j = 0" using i j ij
by (vector mat_def)
}
- then have "det ?A = setprod (\<lambda>i. ?f i i) ?U"
+ then have "det ?A = prod (\<lambda>i. ?f i i) ?U"
using det_diagonal by blast
also have "\<dots> = 1"
- unfolding th setprod.neutral_const ..
+ unfolding th prod.neutral_const ..
finally show ?thesis .
qed
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
- by (simp add: det_def setprod_zero)
+ by (simp add: det_def prod_zero)
lemma det_permute_rows:
fixes A :: "'a::comm_ring_1^'n^'n"
@@ -240,16 +240,16 @@
from p q have pp: "permutation p" and qp: "permutation q"
by (metis fU permutation_permutes)+
from permutes_inv[OF p] have ip: "inv p permutes ?U" .
- have "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U"
- by (simp only: setprod_permute[OF ip, symmetric])
- also have "\<dots> = setprod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U"
+ have "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U"
+ by (simp only: prod_permute[OF ip, symmetric])
+ also have "\<dots> = prod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U"
by (simp only: o_def)
- also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U"
+ also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U"
by (simp only: o_def permutes_inverses[OF p])
- finally have thp: "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U"
+ finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U"
by blast
- show "of_int (sign (q \<circ> p)) * setprod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U =
- of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U"
+ show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U =
+ of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U"
by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult)
qed rule
@@ -341,30 +341,30 @@
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j"
by simp_all
}
- then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
- and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk"
+ then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
+ and th2: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?h i $ p i) ?Uk"
apply -
- apply (rule setprod.cong, simp_all)+
+ apply (rule prod.cong, simp_all)+
done
have th3: "finite ?Uk" "k \<notin> ?Uk"
by auto
- have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
+ have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
unfolding kU[symmetric] ..
- also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
- apply (rule setprod.insert)
+ also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk"
+ apply (rule prod.insert)
apply simp
apply blast
done
- also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)"
+ also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?f i $ p i) ?Uk)"
by (simp add: field_simps)
- also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)"
+ also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?h i $ p i) ?Uk)"
by (metis th1 th2)
- also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
- unfolding setprod.insert[OF th3] by simp
- finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U"
+ also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
+ unfolding prod.insert[OF th3] by simp
+ finally have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?g i $ p i) ?U + prod (\<lambda>i. ?h i $ p i) ?U"
unfolding kU[symmetric] .
- then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
- of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U"
+ then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U =
+ of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U"
by (simp add: field_simps)
qed rule
@@ -391,30 +391,30 @@
from j have "?f j $ p j = ?g j $ p j"
by simp
}
- then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
+ then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
apply -
- apply (rule setprod.cong)
+ apply (rule prod.cong)
apply simp_all
done
have th3: "finite ?Uk" "k \<notin> ?Uk"
by auto
- have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
+ have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
unfolding kU[symmetric] ..
- also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
- apply (rule setprod.insert)
+ also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk"
+ apply (rule prod.insert)
apply simp
apply blast
done
- also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
+ also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk"
by (simp add: field_simps)
- also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
+ also have "\<dots> = c* (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk)"
unfolding th1 by (simp add: ac_simps)
- also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
- unfolding setprod.insert[OF th3] by simp
- finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
+ also have "\<dots> = c* (prod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
+ unfolding prod.insert[OF th3] by simp
+ finally have "prod (\<lambda>i. ?f i $ p i) ?U = c* (prod (\<lambda>i. ?g i $ p i) ?U)"
unfolding kU[symmetric] .
- then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
- c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)"
+ then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U =
+ c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)"
by (simp add: field_simps)
qed rule
@@ -644,8 +644,8 @@
lemma det_rows_mul:
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
- setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
-proof (simp add: det_def sum_distrib_left cong add: setprod.cong, rule sum.cong)
+ prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
+proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong)
let ?U = "UNIV :: 'n set"
let ?PU = "{p. p permutes ?U}"
fix p
@@ -653,10 +653,10 @@
let ?s = "of_int (sign p)"
from pU have p: "p permutes ?U"
by blast
- have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"
- unfolding setprod.distrib ..
+ have "prod (\<lambda>i. c i * a i $ p i) ?U = prod c ?U * prod (\<lambda>i. a i $ p i) ?U"
+ unfolding prod.distrib ..
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
- setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
+ prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
by (simp add: field_simps)
qed rule
@@ -754,17 +754,17 @@
have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
by (simp add: th00 ac_simps sign_idempotent sign_compose)
- have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
- by (rule setprod_permute[OF p])
- have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
- setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U"
- unfolding th001 setprod.distrib[symmetric] o_def permutes_inverses[OF p]
- apply (rule setprod.cong[OF refl])
+ have th001: "prod (\<lambda>i. B$i$ q (inv p i)) ?U = prod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
+ by (rule prod_permute[OF p])
+ have thp: "prod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
+ prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U"
+ unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p]
+ apply (rule prod.cong[OF refl])
using permutes_in_image[OF q]
apply vector
done
- show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
- ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * setprod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)"
+ show "?s q * prod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
+ ?s p * (prod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * prod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)"
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose)
qed rule
@@ -1202,13 +1202,13 @@
text \<open>Explicit formulas for low dimensions.\<close>
-lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1"
+lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1"
by simp
-lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
+lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
-lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
+lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1129,7 +1129,7 @@
lemma negligible_interval:
"negligible (cbox a b) \<longleftrightarrow> box a b = {}" "negligible (box a b) \<longleftrightarrow> box a b = {}"
- by (auto simp: negligible_iff_null_sets null_sets_def setprod_nonneg inner_diff_left box_eq_empty
+ by (auto simp: negligible_iff_null_sets null_sets_def prod_nonneg inner_diff_left box_eq_empty
not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
intro: eq_refl antisym less_imp_le)
@@ -1254,9 +1254,9 @@
then have ufvf: "cbox (uf X) (vf X) = X"
using uvz by blast
have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
- by (rule setprod_constant [symmetric])
+ by (rule prod_constant [symmetric])
also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
- using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: setprod.cong)
+ using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: prod.cong)
finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
@@ -1272,7 +1272,7 @@
have 0: "0 \<le> prj1 (vf X - uf X)"
using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
- apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> setprod_constant)
+ apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> prod_constant)
apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
apply (fastforce simp add: box_ne_empty power_decreasing)
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Mon Oct 17 19:03:13 2016 +0200
@@ -202,7 +202,7 @@
next
case (4 x)
thus ?case using assms
- by (auto intro!: setprod.cong split: if_split_asm)
+ by (auto intro!: prod.cong split: if_split_asm)
qed
@@ -926,12 +926,12 @@
by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
(\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
- using E by (subst insert) (auto intro!: setprod.cong)
+ using E by (subst insert) (auto intro!: prod.cong)
also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
- using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] setprod.cong)
+ using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] prod.cong)
also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
- using insert(1,2) J E by (intro setprod.mono_neutral_right) auto
+ using insert(1,2) J E by (intro prod.mono_neutral_right) auto
finally show "?\<mu> ?p = \<dots>" .
show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))"
@@ -943,7 +943,7 @@
show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
using insert by auto
- qed (auto intro!: setprod.cong)
+ qed (auto intro!: prod.cong)
with insert show ?case
by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
qed simp
@@ -962,7 +962,7 @@
by (simp add: eq emeasure_PiM)
define A where "A n = (\<Pi>\<^sub>E i\<in>I. C i n)" for n
with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)"
- by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_setprod_eq_top)
+ by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top)
qed
qed
@@ -981,7 +981,7 @@
ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
by (intro exI[of _ "PiE I ` PiE I F"])
(auto intro!: countable_PiE sets_PiM_I_finite
- simp: PiE_iff emeasure_PiM finite_index ennreal_setprod_eq_top)
+ simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
qed
sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
@@ -1008,7 +1008,7 @@
from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
(\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
by (subst emeasure_distr)
- (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times setprod.union_disjoint)
+ (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
qed (insert fin, simp_all)
lemma (in product_sigma_finite) product_nn_integral_fold:
@@ -1090,7 +1090,7 @@
apply measurable
done
-lemma (in product_sigma_finite) product_nn_integral_setprod:
+lemma (in product_sigma_finite) product_nn_integral_prod:
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
using assms proof (induction I)
@@ -1099,10 +1099,10 @@
note \<open>finite I\<close>[intro, simp]
interpret I: finite_product_sigma_finite M I by standard auto
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
- using insert by (auto intro!: setprod.cong)
+ using insert by (auto intro!: prod.cong)
have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)"
using sets.sets_into_space insert
- by (intro borel_measurable_setprod_ennreal
+ by (intro borel_measurable_prod_ennreal
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
then show ?case
--- a/src/HOL/Analysis/Gamma_Function.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Mon Oct 17 19:03:13 2016 +0200
@@ -510,15 +510,15 @@
(of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))"
unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_sum)
also from assms have "(\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))) = (\<Prod>k=1..n. z / of_nat k + 1)"
- by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
+ by (intro prod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
also have "... = (\<Prod>k=1..n. z + k) / fact n"
- by (simp add: fact_setprod)
- (subst setprod_dividef [symmetric], simp_all add: field_simps)
+ by (simp add: fact_prod)
+ (subst prod_dividef [symmetric], simp_all add: field_simps)
also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
- by (simp add: setprod.atLeast0_atMost_Suc_shift setprod.atLeast_Suc_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift)
also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)"
- unfolding pochhammer_setprod
- by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+ unfolding pochhammer_prod
+ by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
finally show ?thesis .
@@ -995,10 +995,10 @@
norm (y - z)) (nhds 0) (at z)"
assumes differentiable_rGamma_aux2:
"let z = - of_nat n
- in filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (setprod of_nat {1..n}) * (y - z)) /\<^sub>R
+ in filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (prod of_nat {1..n}) * (y - z)) /\<^sub>R
norm (y - z)) (nhds 0) (at z)"
assumes rGamma_series_aux: "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow>
- let fact' = (\<lambda>n. setprod of_nat {1..n});
+ let fact' = (\<lambda>n. prod of_nat {1..n});
exp = (\<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x^k /\<^sub>R fact k) \<longlonglongrightarrow> e);
pochhammer' = (\<lambda>a n. (\<Prod>n = 0..n. a + of_nat n))
in filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1))))
@@ -1033,7 +1033,7 @@
case False
hence "z \<noteq> - of_nat n" for n by auto
from rGamma_series_aux[OF this] show ?thesis
- by (simp add: rGamma_series_def[abs_def] fact_setprod pochhammer_Suc_setprod
+ by (simp add: rGamma_series_def[abs_def] fact_prod pochhammer_Suc_prod
exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
@@ -1183,7 +1183,7 @@
apply (rule has_field_derivative_at_within)
using differentiable_rGamma_aux2[of n]
unfolding Let_def has_field_derivative_def has_derivative_def netlimit_at
- by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_setprod) simp
+ by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_prod) simp
lemma has_field_derivative_rGamma [derivative_intros]:
"(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>norm z\<rfloor>) * fact (nat \<lfloor>norm z\<rfloor>)
@@ -1387,18 +1387,18 @@
next
fix n :: nat
from has_field_derivative_rGamma_complex_nonpos_Int[of n]
- show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * setprod of_nat {1..n} *
+ show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * prod of_nat {1..n} *
(y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0"
- by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
+ by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
next
fix z :: complex
from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z"
by (simp add: convergent_LIMSEQ_iff rGamma_complex_def)
- thus "let fact' = \<lambda>n. setprod of_nat {1..n};
+ thus "let fact' = \<lambda>n. prod of_nat {1..n};
exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
- by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+ by (simp add: fact_prod pochhammer_Suc_prod rGamma_series_def [abs_def] exp_def
of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
qed
@@ -1517,9 +1517,9 @@
have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
simp: Polygamma_of_real rGamma_real_def [abs_def])
- thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * setprod of_nat {1..n} *
+ thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * prod of_nat {1..n} *
(y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
- by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
+ by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
next
fix x :: real
have "rGamma_series x \<longlonglongrightarrow> rGamma x"
@@ -1527,11 +1527,11 @@
show "(\<lambda>n. Re (rGamma_series (of_real x) n)) \<longlonglongrightarrow> rGamma x" unfolding rGamma_real_def
by (intro tendsto_intros)
qed (insert rGamma_series_real, simp add: eq_commute)
- thus "let fact' = \<lambda>n. setprod of_nat {1..n};
+ thus "let fact' = \<lambda>n. prod of_nat {1..n};
exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
in (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
- by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+ by (simp add: fact_prod pochhammer_Suc_prod rGamma_series_def [abs_def] exp_def
of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
qed
@@ -2575,11 +2575,11 @@
exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))"
by (subst exp_sum [symmetric]) (simp_all add: sum_distrib_left)
also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)"
- by (subst ln_setprod [symmetric]) (auto intro!: add_pos_nonneg)
+ by (subst ln_prod [symmetric]) (auto intro!: add_pos_nonneg)
also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
- by (intro setprod.cong) (simp_all add: divide_simps)
+ by (intro prod.cong) (simp_all add: divide_simps)
also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
- by (induction n) (simp_all add: setprod_nat_ivl_Suc' divide_simps)
+ by (induction n) (simp_all add: prod_nat_ivl_Suc' divide_simps)
finally show ?thesis ..
qed
@@ -2606,11 +2606,11 @@
from n z' have "Gamma_series_euler' z n =
exp (z * of_real (ln (of_nat n + 1))) / (z * (\<Prod>k=1..n. (1 + z / of_nat k)))"
by (subst Gamma_euler'_aux1)
- (simp_all add: Gamma_series_euler'_def setprod.distrib
- setprod_inversef[symmetric] divide_inverse)
+ (simp_all add: Gamma_series_euler'_def prod.distrib
+ prod_inversef[symmetric] divide_inverse)
also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
- by (cases n) (simp_all add: pochhammer_setprod fact_setprod atLeastLessThanSuc_atLeastAtMost
- setprod_dividef [symmetric] field_simps setprod.atLeast_Suc_atMost_Suc_shift)
+ by (cases n) (simp_all add: pochhammer_prod fact_prod atLeastLessThanSuc_atLeastAtMost
+ prod_dividef [symmetric] field_simps prod.atLeast_Suc_atMost_Suc_shift)
also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
qed
@@ -2681,7 +2681,7 @@
case False
have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
- exp_minus divide_inverse setprod_inversef[symmetric] mult_ac)
+ exp_minus divide_inverse prod_inversef[symmetric] mult_ac)
also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
finally show ?thesis by (simp add: Gamma_def)
@@ -2865,7 +2865,7 @@
also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
by (simp add: divide_simps pochhammer_rec
- setprod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
+ prod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
by simp
qed (simp_all add: bounded_bilinear_mult)
@@ -3024,10 +3024,10 @@
have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
- divide_simps setprod.distrib[symmetric] power2_eq_square)
+ divide_simps prod.distrib[symmetric] power2_eq_square)
also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
(\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
- by (intro setprod.cong) (simp_all add: power2_eq_square field_simps)
+ by (intro prod.cong) (simp_all add: power2_eq_square field_simps)
finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \<dots>"
by (simp add: divide_simps)
qed
@@ -3058,10 +3058,10 @@
from tendsto_inverse[OF tendsto_mult[OF
sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
- by (simp add: setprod_inversef [symmetric])
+ by (simp add: prod_inversef [symmetric])
also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
(\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
- by (intro ext setprod.cong refl) (simp add: divide_simps)
+ by (intro ext prod.cong refl) (simp add: divide_simps)
finally show ?thesis .
qed
@@ -3086,7 +3086,7 @@
have "(\<lambda>n. P x n - P x (Suc n)) sums (P x 0 - sin (pi * x) / (pi * x))"
unfolding P_def using x by (intro telescope_sums' sin_product_formula_real')
also have "(\<lambda>n. P x n - P x (Suc n)) = (\<lambda>n. (x^2 / of_nat (Suc n)^2) * P x n)"
- unfolding P_def by (simp add: setprod_nat_ivl_Suc' algebra_simps)
+ unfolding P_def by (simp add: prod_nat_ivl_Suc' algebra_simps)
also have "P x 0 = 1" by (simp add: P_def)
finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" .
from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp
@@ -3104,9 +3104,9 @@
finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k
by (simp_all add: field_simps del: of_nat_Suc)
}
- hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro setprod_mono) simp
+ hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro prod_mono) simp
thus "norm (P x n / (of_nat (Suc n)^2)) \<le> 1 / of_nat (Suc n)^2"
- unfolding P_def by (simp add: field_simps abs_setprod del: of_nat_Suc)
+ unfolding P_def by (simp add: field_simps abs_prod del: of_nat_Suc)
qed (subst summable_Suc_iff, insert inverse_power_summable[of 2], simp add: inverse_eq_divide)
qed (auto simp: P_def intro!: continuous_intros)
hence "isCont f 0" by (subst (asm) continuous_on_eq_continuous_at) simp_all
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Mon Oct 17 19:03:13 2016 +0200
@@ -31,9 +31,9 @@
let ?P = "\<Prod>i=0..<n. a - of_nat i"
from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
(?P / (\<Prod>i=0..n. a - of_nat i))"
- by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+ by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
- by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+ by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
also from assms have "?P / ?P = 1" by auto
also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
@@ -210,7 +210,7 @@
also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
using assms by (subst powr_of_real) simp_all
also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
- by (simp add: gbinomial_setprod_rev)
+ by (simp add: gbinomial_prod_rev)
hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
(\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
finally show ?thesis by (simp only: sums_of_real_iff)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Oct 17 19:03:13 2016 +0200
@@ -56,7 +56,7 @@
where "content s \<equiv> measure lborel s"
lemma content_cbox_cases:
- "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
+ "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then prod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
by (simp add: measure_lborel_cbox_eq inner_diff)
lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
@@ -84,7 +84,7 @@
using not_le by blast
lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
- by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
+ by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)
lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
@@ -93,7 +93,7 @@
unfolding content_eq_0 interior_cbox box_eq_empty by auto
lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
- by (auto simp add: content_cbox_cases less_le setprod_nonneg)
+ by (auto simp add: content_cbox_cases less_le prod_nonneg)
lemma content_empty [simp]: "content {} = 0"
by simp
@@ -110,9 +110,9 @@
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
unfolding measure_lborel_cbox_eq Basis_prod_def
- apply (subst setprod.union_disjoint)
+ apply (subst prod.union_disjoint)
apply (auto simp: bex_Un ball_Un)
- apply (subst (1 2) setprod.reindex_nontrivial)
+ apply (subst (1 2) prod.reindex_nontrivial)
apply auto
done
@@ -138,7 +138,7 @@
apply (subst *(1))
defer
apply (subst *(1))
- unfolding setprod.insert[OF *(2-)]
+ unfolding prod.insert[OF *(2-)]
apply auto
done
assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
@@ -151,7 +151,7 @@
(\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
"(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
(\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
- by (auto intro!: setprod.cong)
+ by (auto intro!: prod.cong)
have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
unfolding not_le
using as[unfolded ,rule_format,of k] assms
@@ -1876,7 +1876,7 @@
by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
using k *
- by (intro setprod_zero bexI[OF _ k])
+ by (intro prod_zero bexI[OF _ k])
(auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
@@ -3472,7 +3472,7 @@
also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
by (intro measure_times) auto
also have "\<dots> = 0"
- by (intro setprod_zero bexI[OF _ k]) auto
+ by (intro prod_zero bexI[OF _ k]) auto
finally show ?thesis
by (subst AE_iff_measurable[OF _ refl]) auto
qed
@@ -3494,13 +3494,13 @@
show ?thesis
using m unfolding eq measure_def
by (subst lborel_affine_euclidean[where c=m and t=0])
- (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
- s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
+ (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_prod nn_integral_cmult
+ s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult prod_nonneg)
next
assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
then obtain k where k: "k \<in> Basis" "m k = 0" by auto
then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
- by (intro setprod_zero) auto
+ by (intro prod_zero) auto
have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
proof (rule emeasure_eq_0_AE)
show "AE x in lborel. x \<notin> s m ` cbox a b"
@@ -3539,7 +3539,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis
by (simp add: image_affinity_cbox True content_cbox'
- setprod.distrib setprod_constant inner_diff_left)
+ prod.distrib prod_constant inner_diff_left)
next
case False
with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
@@ -3552,7 +3552,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis using False
by (simp add: image_affinity_cbox content_cbox'
- setprod.distrib[symmetric] setprod_constant[symmetric] inner_diff_left)
+ prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
qed
qed
@@ -3589,7 +3589,7 @@
assumes "(f has_integral i) (cbox a b)"
and "\<forall>k\<in>Basis. m k \<noteq> 0"
shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
- ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+ ((1/ \<bar>prod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
apply (rule has_integral_twiddle[where f=f])
unfolding zero_less_abs_iff content_image_stretch_interval
unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
@@ -7371,7 +7371,8 @@
subsection \<open>Integration by parts\<close>
lemma integration_by_parts_interior_strong:
- assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes bilinear: "bounded_bilinear (prod)"
assumes s: "finite s" and le: "a \<le> b"
assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
@@ -7389,7 +7390,8 @@
qed
lemma integration_by_parts_interior:
- assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes "bounded_bilinear (prod)" "a \<le> b"
"continuous_on {a..b} f" "continuous_on {a..b} g"
assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
"\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7398,7 +7400,8 @@
by (rule integration_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
lemma integration_by_parts:
- assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes "bounded_bilinear (prod)" "a \<le> b"
"continuous_on {a..b} f" "continuous_on {a..b} g"
assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
"\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7407,7 +7410,8 @@
by (rule integration_by_parts_interior[of _ _ _ f g f' g']) (insert assms, simp_all)
lemma integrable_by_parts_interior_strong:
- assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes bilinear: "bounded_bilinear (prod)"
assumes s: "finite s" and le: "a \<le> b"
assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
@@ -7424,7 +7428,8 @@
qed
lemma integrable_by_parts_interior:
- assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes "bounded_bilinear (prod)" "a \<le> b"
"continuous_on {a..b} f" "continuous_on {a..b} g"
assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
"\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7433,7 +7438,8 @@
by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
lemma integrable_by_parts:
- assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+ fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+ assumes "bounded_bilinear (prod)" "a \<le> b"
"continuous_on {a..b} f" "continuous_on {a..b} g"
assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
"\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Oct 17 19:03:13 2016 +0200
@@ -404,11 +404,11 @@
lemma lborel_eq: "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. lborel) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
by (subst lborel_def) (simp add: lborel_eq_real)
-lemma nn_integral_lborel_setprod:
+lemma nn_integral_lborel_prod:
assumes [measurable]: "\<And>b. b \<in> Basis \<Longrightarrow> f b \<in> borel_measurable borel"
assumes nn[simp]: "\<And>b x. b \<in> Basis \<Longrightarrow> 0 \<le> f b x"
shows "(\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. f b (x \<bullet> b)) \<partial>lborel) = (\<Prod>b\<in>Basis. (\<integral>\<^sup>+x. f b x \<partial>lborel))"
- by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod
+ by (simp add: lborel_def nn_integral_distr product_nn_integral_prod
product_nn_integral_singleton)
lemma emeasure_lborel_Icc[simp]:
@@ -434,13 +434,13 @@
then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
by simp
also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
- by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left)
+ by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
finally show ?thesis .
qed
lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
- by (auto simp add: cbox_sing setprod_constant power_0_left)
+ by (auto simp add: cbox_sing prod_constant power_0_left)
lemma emeasure_lborel_Ioo[simp]:
assumes [simp]: "l \<le> u"
@@ -481,7 +481,7 @@
then have "emeasure lborel (box l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
by simp
also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
- by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left)
+ by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
finally show ?thesis .
qed
@@ -495,7 +495,7 @@
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
using emeasure_lborel_cbox[of x x] nonempty_Basis
- by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
+ by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing prod_constant)
lemma
fixes l u :: real
@@ -510,7 +510,7 @@
assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
- by (simp_all add: measure_def inner_diff_left setprod_nonneg)
+ by (simp_all add: measure_def inner_diff_left prod_nonneg)
lemma measure_lborel_cbox_eq:
"measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
@@ -549,7 +549,7 @@
show ?thesis
unfolding UN_box_eq_UNIV[symmetric]
apply (subst SUP_emeasure_incseq[symmetric])
- apply (auto simp: incseq_def subset_box inner_add_left setprod_constant
+ apply (auto simp: incseq_def subset_box inner_add_left prod_constant
simp del: Sup_eq_top_iff SUP_eq_top_iff
intro!: ennreal_SUP_eq_top)
done
@@ -629,15 +629,15 @@
using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
- field_simps divide_simps ennreal_mult'[symmetric] setprod_nonneg setprod.distrib[symmetric]
- intro!: setprod.cong)
+ field_simps divide_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric]
+ intro!: prod.cong)
qed simp
lemma lborel_affine:
fixes t :: "'a::euclidean_space"
shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
- unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation setprod_constant by simp
+ unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation prod_constant by simp
lemma lborel_real_affine:
"c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
@@ -696,7 +696,7 @@
then have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))) A = 0"
unfolding T_def using c by (subst lborel_affine_euclidean[symmetric]) auto
also have "\<dots> \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0"
- using A c by (simp add: distr_completion emeasure_density nn_integral_cmult setprod_nonneg cong: distr_cong)
+ using A c by (simp add: distr_completion emeasure_density nn_integral_cmult prod_nonneg cong: distr_cong)
finally have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0" . }
then have eq: "null_sets lborel = null_sets (distr lebesgue lborel T)"
by (auto simp: null_sets_def)
@@ -707,7 +707,7 @@
have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))"
using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
also have "\<dots> = density (completion (distr lebesgue lborel T)) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
- using c by (auto intro!: always_eventually setprod_pos completion_density_eq simp: distr_completion cong: distr_cong)
+ using c by (auto intro!: always_eventually prod_pos completion_density_eq simp: distr_completion cong: distr_cong)
also have "\<dots> = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
by (subst completion.completion_distr_eq) (auto simp: eq measurable_completion)
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
@@ -761,7 +761,7 @@
apply (subst lebesgue_affine_euclidean[of "\<lambda>_. m" \<delta>])
apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr
del: space_completion emeasure_completion)
- apply (simp add: vimage_comp s_comp_s setprod_constant)
+ apply (simp add: vimage_comp s_comp_s prod_constant)
done
next
assume "S \<notin> sets lebesgue"
@@ -779,7 +779,7 @@
qed
qed
show ?m
- unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult setprod_nonneg)
+ unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
qed
lemma divideR_right:
@@ -843,9 +843,9 @@
"box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
- ennreal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
- by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint
- setprod.reindex ennreal_mult inner_diff_left setprod_nonneg)
+ ennreal (prod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+ by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint
+ prod.reindex ennreal_mult inner_diff_left prod_nonneg)
qed (simp add: borel_prod[symmetric])
(* FIXME: conversion in measurable prover *)
@@ -860,7 +860,7 @@
then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
by (intro emeasure_mono) auto
then show ?thesis
- by (auto simp: emeasure_lborel_cbox_eq setprod_nonneg less_top[symmetric] top_unique split: if_split_asm)
+ by (auto simp: emeasure_lborel_cbox_eq prod_nonneg less_top[symmetric] top_unique split: if_split_asm)
qed
lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Mon Oct 17 19:03:13 2016 +0200
@@ -192,7 +192,7 @@
lemma sum: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>i \<in> I. f i x) \<in> R"
by (induct I rule: finite_induct; simp add: const add)
- lemma setprod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
+ lemma prod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
by (induct I rule: finite_induct; simp add: const mult)
definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
@@ -467,19 +467,19 @@
by metis
define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x
have pffR: "pff \<in> R"
- unfolding pff_def using subA ff by (auto simp: intro: setprod)
+ unfolding pff_def using subA ff by (auto simp: intro: prod)
moreover
have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x
proof -
have "0 \<le> pff x"
using subA cardp t
apply (simp add: pff_def divide_simps sum_nonneg)
- apply (rule Groups_Big.linordered_semidom_class.setprod_nonneg)
+ apply (rule Groups_Big.linordered_semidom_class.prod_nonneg)
using ff by fastforce
moreover have "pff x \<le> 1"
using subA cardp t
apply (simp add: pff_def divide_simps sum_nonneg)
- apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified])
+ apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
using ff by fastforce
ultimately show ?thesis
by auto
@@ -488,10 +488,10 @@
{ fix v x
assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> S"
from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)"
- unfolding pff_def by (metis setprod.remove)
+ unfolding pff_def by (metis prod.remove)
also have "... \<le> ff v x * 1"
apply (rule Rings.ordered_semiring_class.mult_left_mono)
- apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified])
+ apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
using ff [THEN conjunct2, THEN conjunct1] v subA x
apply auto
apply (meson atLeastAtMost_iff contra_subsetD imageI)
@@ -515,10 +515,10 @@
using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp
by (auto simp: field_simps)
also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)"
- by (simp add: setprod_constant subA(2))
+ by (simp add: prod_constant subA(2))
also have "... < pff x"
apply (simp add: pff_def)
- apply (rule setprod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
+ apply (rule prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
apply (simp_all add: subA(2))
apply (intro ballI conjI)
using e apply (force simp: divide_simps)
--- a/src/HOL/Analysis/ex/Approximations.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Analysis/ex/Approximations.thy Mon Oct 17 19:03:13 2016 +0200
@@ -185,12 +185,12 @@
also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)"
proof (intro sum.cong refl)
fix k assume k: "k \<in> {..n}"
- have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod)
+ have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_prod)
also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto
- also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
- by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto
- also have "\<dots> = fact k" by (simp add: fact_setprod)
- finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp
+ also have "prod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
+ by (subst nonzero_divide_eq_eq, simp, subst prod.union_disjoint [symmetric]) auto
+ also have "\<dots> = fact k" by (simp add: fact_prod)
+ finally show "1 / (fact n / prod real {k + 1..n}) = 1 / fact k" by simp
qed
also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps)
finally show ?thesis by (simp add: euler_approx_aux_def)
--- a/src/HOL/Binomial.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Binomial.thy Mon Oct 17 19:03:13 2016 +0200
@@ -18,45 +18,45 @@
begin
definition fact :: "nat \<Rightarrow> 'a"
- where fact_setprod: "fact n = of_nat (\<Prod>{1..n})"
+ where fact_prod: "fact n = of_nat (\<Prod>{1..n})"
-lemma fact_setprod_Suc: "fact n = of_nat (setprod Suc {0..<n})"
+lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
by (cases n)
- (simp_all add: fact_setprod setprod.atLeast_Suc_atMost_Suc_shift
+ (simp_all add: fact_prod prod.atLeast_Suc_atMost_Suc_shift
atLeastLessThanSuc_atLeastAtMost)
-lemma fact_setprod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
- using setprod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
+lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
+ using prod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
by (cases n)
- (simp_all add: fact_setprod_Suc setprod.atLeast_Suc_atMost_Suc_shift
+ (simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
atLeastLessThanSuc_atLeastAtMost)
lemma fact_0 [simp]: "fact 0 = 1"
- by (simp add: fact_setprod)
+ by (simp add: fact_prod)
lemma fact_1 [simp]: "fact 1 = 1"
- by (simp add: fact_setprod)
+ by (simp add: fact_prod)
lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
- by (simp add: fact_setprod)
+ by (simp add: fact_prod)
lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
- by (simp add: fact_setprod atLeastAtMostSuc_conv algebra_simps)
+ by (simp add: fact_prod atLeastAtMostSuc_conv algebra_simps)
lemma fact_2 [simp]: "fact 2 = 2"
by (simp add: numeral_2_eq_2)
-lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (setprod Suc {n - k..<n}) * fact (n - k)"
- by (simp add: fact_setprod_Suc setprod.union_disjoint [symmetric]
+lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (prod Suc {n - k..<n}) * fact (n - k)"
+ by (simp add: fact_prod_Suc prod.union_disjoint [symmetric]
ivl_disj_un ac_simps of_nat_mult [symmetric])
end
lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
- by (simp add: fact_setprod)
+ by (simp add: fact_prod)
lemma of_int_fact [simp]: "of_int (fact n) = fact n"
- by (simp only: fact_setprod of_int_of_nat_eq)
+ by (simp only: fact_prod of_int_of_nat_eq)
lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
by (cases n) auto
@@ -170,7 +170,7 @@
shows "fact n div fact (n - r) \<le> n ^ r"
proof -
have "r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" for r
- by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
+ by (subst prod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
with assms show ?thesis
by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
qed
@@ -434,7 +434,7 @@
with True have "n = m + 2"
by simp
then have "fact n = n * (n - 1) * fact (n - 2)"
- by (simp add: fact_setprod_Suc atLeast0_lessThan_Suc algebra_simps)
+ by (simp add: fact_prod_Suc atLeast0_lessThan_Suc algebra_simps)
with True show ?thesis
by (simp add: binomial_fact')
qed
@@ -508,29 +508,29 @@
begin
definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
- where pochhammer_setprod: "pochhammer a n = setprod (\<lambda>i. a + of_nat i) {0..<n}"
+ where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"
-lemma pochhammer_setprod_rev: "pochhammer a n = setprod (\<lambda>i. a + of_nat (n - i)) {1..n}"
- using setprod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
- by (simp add: pochhammer_setprod)
+lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
+ using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
+ by (simp add: pochhammer_prod)
-lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat i) {0..n}"
- by (simp add: pochhammer_setprod atLeastLessThanSuc_atLeastAtMost)
+lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
+ by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)
-lemma pochhammer_Suc_setprod_rev: "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat (n - i)) {0..n}"
- by (simp add: pochhammer_setprod_rev setprod.atLeast_Suc_atMost_Suc_shift)
+lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
+ by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift)
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
- by (simp add: pochhammer_setprod)
+ by (simp add: pochhammer_prod)
lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
- by (simp add: pochhammer_setprod lessThan_Suc)
+ by (simp add: pochhammer_prod lessThan_Suc)
lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
- by (simp add: pochhammer_setprod lessThan_Suc)
+ by (simp add: pochhammer_prod lessThan_Suc)
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
- by (simp add: pochhammer_setprod atLeast0_lessThan_Suc ac_simps)
+ by (simp add: pochhammer_prod atLeast0_lessThan_Suc ac_simps)
end
@@ -545,22 +545,22 @@
by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
- by (simp add: pochhammer_setprod)
+ by (simp add: pochhammer_prod)
lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
- by (simp add: pochhammer_setprod)
+ by (simp add: pochhammer_prod)
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
- by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc_shift ac_simps)
+ by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
- by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc ac_simps)
+ by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)
lemma pochhammer_fact: "fact n = pochhammer 1 n"
- by (simp add: pochhammer_setprod fact_setprod_Suc)
+ by (simp add: pochhammer_prod fact_prod_Suc)
lemma pochhammer_of_nat_eq_0_lemma: "k > n \<Longrightarrow> pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
- by (auto simp add: pochhammer_setprod)
+ by (auto simp add: pochhammer_prod)
lemma pochhammer_of_nat_eq_0_lemma':
assumes kn: "k \<le> n"
@@ -571,7 +571,7 @@
next
case (Suc h)
then show ?thesis
- apply (simp add: pochhammer_Suc_setprod)
+ apply (simp add: pochhammer_Suc_prod)
using Suc kn
apply (auto simp add: algebra_simps)
done
@@ -585,7 +585,7 @@
by (auto simp add: not_le[symmetric])
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
- by (auto simp add: pochhammer_setprod eq_neg_iff_add_eq_0)
+ by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)
lemma pochhammer_eq_0_mono:
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
@@ -603,11 +603,11 @@
next
case (Suc h)
have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
- using setprod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
+ using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
by auto
with Suc show ?thesis
- using pochhammer_Suc_setprod_rev [of "b - of_nat k + 1"]
- by (auto simp add: pochhammer_Suc_setprod setprod.distrib [symmetric] eq of_nat_diff)
+ using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
+ by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
qed
lemma pochhammer_minus':
@@ -705,19 +705,19 @@
subsection \<open>Generalized binomial coefficients\<close>
definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
- where gbinomial_setprod_rev: "a gchoose n = setprod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
+ where gbinomial_prod_rev: "a gchoose n = prod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
lemma gbinomial_0 [simp]:
"a gchoose 0 = 1"
"0 gchoose (Suc n) = 0"
- by (simp_all add: gbinomial_setprod_rev setprod.atLeast0_lessThan_Suc_shift)
+ by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift)
-lemma gbinomial_Suc: "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
- by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
+ by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
lemma gbinomial_mult_fact: "fact n * (a gchoose n) = (\<Prod>i = 0..<n. a - of_nat i)"
for a :: "'a::field_char_0"
- by (simp_all add: gbinomial_setprod_rev field_simps)
+ by (simp_all add: gbinomial_prod_rev field_simps)
lemma gbinomial_mult_fact': "(a gchoose n) * fact n = (\<Prod>i = 0..<n. a - of_nat i)"
for a :: "'a::field_char_0"
@@ -727,9 +727,9 @@
for a :: "'a::field_char_0"
by (cases n)
(simp_all add: pochhammer_minus,
- simp_all add: gbinomial_setprod_rev pochhammer_setprod_rev
+ simp_all add: gbinomial_prod_rev pochhammer_prod_rev
power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
- setprod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
+ prod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
lemma gbinomial_pochhammer': "s gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
for s :: "'a::field_char_0"
@@ -749,42 +749,42 @@
by (simp add: not_le)
then have "0 \<in> (op - n) ` {0..<k}"
by auto
- then have "setprod (op - n) {0..<k} = 0"
- by (auto intro: setprod_zero)
+ then have "prod (op - n) {0..<k} = 0"
+ by (auto intro: prod_zero)
with \<open>n < k\<close> show ?thesis
- by (simp add: binomial_eq_0 gbinomial_setprod_rev setprod_zero)
+ by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero)
next
case True
then have "inj_on (op - n) {0..<k}"
by (auto intro: inj_onI)
- then have "\<Prod>(op - n ` {0..<k}) = setprod (op - n) {0..<k}"
- by (auto dest: setprod.reindex)
+ then have "\<Prod>(op - n ` {0..<k}) = prod (op - n) {0..<k}"
+ by (auto dest: prod.reindex)
also have "op - n ` {0..<k} = {Suc (n - k)..n}"
using True by (auto simp add: image_def Bex_def) presburger (* FIXME slow *)
- finally have *: "setprod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
+ finally have *: "prod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
from True have "n choose k = fact n div (fact k * fact (n - k))"
by (rule binomial_fact')
with * show ?thesis
- by (simp add: gbinomial_setprod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+ by (simp add: gbinomial_prod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
qed
lemma of_nat_gbinomial: "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof (cases "k \<le> n")
case False
then show ?thesis
- by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_setprod_rev)
+ by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_prod_rev)
next
case True
define m where "m = n - k"
with True have n: "n = m + k"
by arith
from n have "fact n = ((\<Prod>i = 0..<m + k. of_nat (m + k - i) ):: 'a)"
- by (simp add: fact_setprod_rev)
+ by (simp add: fact_prod_rev)
also have "\<dots> = ((\<Prod>i\<in>{0..<k} \<union> {k..<m + k}. of_nat (m + k - i)) :: 'a)"
by (simp add: ivl_disj_un)
finally have "fact n = (fact m * (\<Prod>i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)"
- using setprod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
- by (simp add: fact_setprod_rev [of m] setprod.union_disjoint of_nat_diff)
+ using prod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
+ by (simp add: fact_prod_rev [of m] prod.union_disjoint of_nat_diff)
then have "fact n / fact (n - k) = ((\<Prod>i = 0..<k. of_nat n - of_nat i) :: 'a)"
by (simp add: n)
with True have "fact k * of_nat (n gchoose k) = (fact k * (of_nat n gchoose k) :: 'a)"
@@ -800,10 +800,10 @@
\<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
lemma gbinomial_1[simp]: "a gchoose 1 = a"
- by (simp add: gbinomial_setprod_rev lessThan_Suc)
+ by (simp add: gbinomial_prod_rev lessThan_Suc)
lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
- by (simp add: gbinomial_setprod_rev lessThan_Suc)
+ by (simp add: gbinomial_prod_rev lessThan_Suc)
lemma gbinomial_mult_1:
fixes a :: "'a::field_char_0"
@@ -833,7 +833,7 @@
next
case (Suc h)
have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
- apply (rule setprod.reindex_cong [where l = Suc])
+ apply (rule prod.reindex_cong [where l = Suc])
using Suc
apply (auto simp add: image_Suc_atMost)
done
@@ -865,7 +865,7 @@
by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost)
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
using eq0
- by (simp add: Suc setprod.atLeast0_atMost_Suc_shift)
+ by (simp add: Suc prod.atLeast0_atMost_Suc_shift)
also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost)
finally show ?thesis
@@ -1003,7 +1003,7 @@
Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}.\<close>
lemma gbinomial_altdef_of_nat: "x gchoose k = (\<Prod>i = 0..<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
for k :: nat and x :: "'a::field_char_0"
- by (simp add: setprod_dividef gbinomial_setprod_rev fact_setprod_rev)
+ by (simp add: prod_dividef gbinomial_prod_rev fact_prod_rev)
lemma gbinomial_ge_n_over_k_pow_k:
fixes k :: nat
@@ -1014,10 +1014,10 @@
have x: "0 \<le> x"
using assms of_nat_0_le_iff order_trans by blast
have "(x / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. x / of_nat k :: 'a)"
- by (simp add: setprod_constant)
+ by (simp add: prod_constant)
also have "\<dots> \<le> x gchoose k" (* FIXME *)
unfolding gbinomial_altdef_of_nat
- apply (safe intro!: setprod_mono)
+ apply (safe intro!: prod_mono)
apply simp_all
prefer 2
subgoal premises for i
@@ -1051,11 +1051,11 @@
next
case (Suc b)
then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
- by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+ by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
- by (simp add: setprod.atLeast0_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift)
also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
- by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+ by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
qed
@@ -1066,11 +1066,11 @@
next
case (Suc b)
then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)"
- by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+ by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
- by (simp add: setprod.atLeast0_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift)
also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
- by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
+ by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
finally show ?thesis
by (simp add: Suc)
qed
@@ -1647,11 +1647,11 @@
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)"
proof -
have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
- by (simp add: fact_setprod)
+ by (simp add: fact_prod)
also have "\<Prod>{1..n} = \<Prod>{2..n}"
- by (intro setprod.mono_neutral_right) auto
+ by (intro prod.mono_neutral_right) auto
also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
- by (simp add: setprod_atLeastAtMost_code)
+ by (simp add: prod_atLeastAtMost_code)
finally show ?thesis .
qed
@@ -1660,7 +1660,7 @@
(if n = 0 then 1
else fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
by (cases n)
- (simp_all add: pochhammer_setprod setprod_atLeastAtMost_code [symmetric]
+ (simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
atLeastLessThanSuc_atLeastAtMost)
lemma gbinomial_code [code]:
@@ -1668,7 +1668,7 @@
(if n = 0 then 1
else fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
by (cases n)
- (simp_all add: gbinomial_setprod_rev setprod_atLeastAtMost_code [symmetric]
+ (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
atLeastLessThanSuc_atLeastAtMost)
(* FIXME *)
@@ -1685,9 +1685,9 @@
assume "k \<le> n"
then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
- by (simp add: setprod.union_disjoint fact_altdef_nat)
+ by (simp add: prod.union_disjoint fact_altdef_nat)
}
- then show ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
+ then show ?thesis by (auto simp: binomial_altdef_nat mult_ac prod_atLeastAtMost_code)
qed
*)
--- a/src/HOL/Complex.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Complex.thy Mon Oct 17 19:03:13 2016 +0200
@@ -486,7 +486,7 @@
lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
by (simp add: complex_eq_iff)
-lemma cnj_setprod [simp]: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
+lemma cnj_prod [simp]: "cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))"
by (induct s rule: infinite_finite_induct) auto
lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Oct 17 19:03:13 2016 +0200
@@ -3972,7 +3972,7 @@
qed
have "\<And>k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
- hence setprod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
+ hence prod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
by auto
have sum_move0: "\<And>k F. sum F {0..<Suc k} = F 0 + sum (\<lambda> k. F (Suc k)) {0..<k}"
unfolding sum_shift_bounds_Suc_ivl[symmetric]
@@ -3994,7 +3994,7 @@
also have "?X (Suc k) f n t * (xs!x - real_of_float c) * inverse (real k) + ?f 0 c =
(\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i c * (xs!x - c)^i) +
inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - c)^Suc n" (is "_ = ?T")
- unfolding funpow_Suc C_def[symmetric] sum_move0 setprod_head_Suc
+ unfolding funpow_Suc C_def[symmetric] sum_move0 prod_head_Suc
by (auto simp add: algebra_simps)
(simp only: mult.left_commute [of _ "inverse (real k)"] sum_distrib_left [symmetric])
finally have "?T \<in> {l .. u}" .
@@ -4003,8 +4003,8 @@
qed
qed
-lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
- by (simp add: fact_setprod atLeastLessThanSuc_atLeastAtMost)
+lemma prod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
+ by (simp add: fact_prod atLeastLessThanSuc_atLeastAtMost)
lemma approx_tse:
assumes "bounded_by xs vs"
@@ -4029,7 +4029,7 @@
(\<Sum> j = 0..<n. inverse(fact j) * F j c * (xs!x - c)^j) +
inverse ((fact n)) * F n t * (xs!x - c)^n
\<in> {l .. u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
- unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact
+ unfolding F_def atLeastAtMost_iff[symmetric] prod_fact
by blast
have bnd_xs: "xs ! x \<in> { lx .. ux }"
--- a/src/HOL/Deriv.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Deriv.thy Mon Oct 17 19:03:13 2016 +0200
@@ -351,7 +351,7 @@
lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
-lemma has_derivative_setprod[simp, derivative_intros]:
+lemma has_derivative_prod[simp, derivative_intros]:
fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
@@ -377,7 +377,7 @@
fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
assumes f: "(f has_derivative f') (at x within s)"
shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
- using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
+ using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps)
lemma has_derivative_inverse':
fixes x :: "'a::real_normed_div_algebra"
--- a/src/HOL/GCD.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/GCD.thy Mon Oct 17 19:03:13 2016 +0200
@@ -859,7 +859,7 @@
lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
by (subst add_commute) simp
-lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
+lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
@@ -1373,7 +1373,7 @@
also have "lcm a \<dots> = lcm a (\<Prod>A)"
by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
also from insert have "gcd a (\<Prod>A) = 1"
- by (subst gcd.commute, intro setprod_coprime) auto
+ by (subst gcd.commute, intro prod_coprime) auto
with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
by (simp add: lcm_coprime)
finally show ?case .
--- a/src/HOL/Groups_Big.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Groups_Big.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1051,34 +1051,34 @@
context comm_monoid_mult
begin
-sublocale setprod: comm_monoid_set times 1
- defines setprod = setprod.F ..
+sublocale prod: comm_monoid_set times 1
+ defines prod = prod.F ..
-abbreviation Setprod ("\<Prod>_" [1000] 999)
- where "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
+abbreviation Prod ("\<Prod>_" [1000] 999)
+ where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
end
syntax (ASCII)
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
syntax
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
- "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A"
+ "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
syntax (ASCII)
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
syntax
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
translations
- "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
+ "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
context comm_monoid_mult
begin
-lemma setprod_dvd_setprod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
+lemma prod_dvd_prod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> prod f A dvd prod g A"
proof (induct A rule: infinite_finite_induct)
case infinite
then show ?case by (auto intro: dvdI)
@@ -1087,18 +1087,18 @@
then show ?case by (auto intro: dvdI)
next
case (insert a A)
- then have "f a dvd g a" and "setprod f A dvd setprod g A"
+ then have "f a dvd g a" and "prod f A dvd prod g A"
by simp_all
- then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s"
+ then obtain r s where "g a = f a * r" and "prod g A = prod f A * s"
by (auto elim!: dvdE)
- then have "g a * setprod g A = f a * setprod f A * (r * s)"
+ then have "g a * prod g A = f a * prod f A * (r * s)"
by (simp add: ac_simps)
with insert.hyps show ?case
by (auto intro: dvdI)
qed
-lemma setprod_dvd_setprod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
- by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
+lemma prod_dvd_prod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> prod f A dvd prod f B"
+ by (auto simp add: prod.subset_diff ac_simps intro: dvdI)
end
@@ -1108,25 +1108,25 @@
context comm_semiring_1
begin
-lemma dvd_setprod_eqI [intro]:
+lemma dvd_prod_eqI [intro]:
assumes "finite A" and "a \<in> A" and "b = f a"
- shows "b dvd setprod f A"
+ shows "b dvd prod f A"
proof -
- from \<open>finite A\<close> have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
- by (intro setprod.insert) auto
+ from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})"
+ by (intro prod.insert) auto
also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A"
by blast
- finally have "setprod f A = f a * setprod f (A - {a})" .
+ finally have "prod f A = f a * prod f (A - {a})" .
with \<open>b = f a\<close> show ?thesis
by simp
qed
-lemma dvd_setprodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd setprod f A"
+lemma dvd_prodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd prod f A"
by auto
-lemma setprod_zero:
+lemma prod_zero:
assumes "finite A" and "\<exists>a\<in>A. f a = 0"
- shows "setprod f A = 0"
+ shows "prod f A = 0"
using assms
proof (induct A)
case empty
@@ -1134,32 +1134,32 @@
next
case (insert a A)
then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
- then have "f a * setprod f A = 0" by rule (simp_all add: insert)
+ then have "f a * prod f A = 0" by rule (simp_all add: insert)
with insert show ?case by simp
qed
-lemma setprod_dvd_setprod_subset2:
+lemma prod_dvd_prod_subset2:
assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
- shows "setprod f A dvd setprod g B"
+ shows "prod f A dvd prod g B"
proof -
- from assms have "setprod f A dvd setprod g A"
- by (auto intro: setprod_dvd_setprod)
- moreover from assms have "setprod g A dvd setprod g B"
- by (auto intro: setprod_dvd_setprod_subset)
+ from assms have "prod f A dvd prod g A"
+ by (auto intro: prod_dvd_prod)
+ moreover from assms have "prod g A dvd prod g B"
+ by (auto intro: prod_dvd_prod_subset)
ultimately show ?thesis by (rule dvd_trans)
qed
end
-lemma (in semidom) setprod_zero_iff [simp]:
+lemma (in semidom) prod_zero_iff [simp]:
fixes f :: "'b \<Rightarrow> 'a"
assumes "finite A"
- shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+ shows "prod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
using assms by (induct A) (auto simp: no_zero_divisors)
-lemma (in semidom_divide) setprod_diff1:
+lemma (in semidom_divide) prod_diff1:
assumes "finite A" and "f a \<noteq> 0"
- shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
+ shows "prod f (A - {a}) = (if a \<in> A then prod f A div f a else prod f A)"
proof (cases "a \<notin> A")
case True
then show ?thesis by simp
@@ -1196,73 +1196,73 @@
for c :: "nat \<Rightarrow> 'a::field"
using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
-lemma (in field) setprod_inversef:
- "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
+lemma (in field) prod_inversef:
+ "finite A \<Longrightarrow> prod (inverse \<circ> f) A = inverse (prod f A)"
by (induct A rule: finite_induct) simp_all
-lemma (in field) setprod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
- using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
+lemma (in field) prod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
+ using prod_inversef [of A g] by (simp add: divide_inverse prod.distrib)
-lemma setprod_Un:
+lemma prod_Un:
fixes f :: "'b \<Rightarrow> 'a :: field"
assumes "finite A" and "finite B"
and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
- shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
+ shows "prod f (A \<union> B) = prod f A * prod f B / prod f (A \<inter> B)"
proof -
- from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
- by (simp add: setprod.union_inter [symmetric, of A B])
+ from assms have "prod f A * prod f B = prod f (A \<union> B) * prod f (A \<inter> B)"
+ by (simp add: prod.union_inter [symmetric, of A B])
with assms show ?thesis
by simp
qed
-lemma (in linordered_semidom) setprod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
+lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
by (induct A rule: infinite_finite_induct) simp_all
-lemma (in linordered_semidom) setprod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
+lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
by (induct A rule: infinite_finite_induct) simp_all
-lemma (in linordered_semidom) setprod_mono:
- "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A"
- by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono)
+lemma (in linordered_semidom) prod_mono:
+ "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
+ by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
-lemma (in linordered_semidom) setprod_mono_strict:
+lemma (in linordered_semidom) prod_mono_strict:
assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
- shows "setprod f A < setprod g A"
+ shows "prod f A < prod g A"
using assms
proof (induct A rule: finite_induct)
case empty
then show ?case by simp
next
case insert
- then show ?case by (force intro: mult_strict_mono' setprod_nonneg)
+ then show ?case by (force intro: mult_strict_mono' prod_nonneg)
qed
-lemma (in linordered_field) abs_setprod: "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
+lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
-lemma setprod_eq_1_iff [simp]: "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
+lemma prod_eq_1_iff [simp]: "finite A \<Longrightarrow> prod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
for f :: "'a \<Rightarrow> nat"
by (induct A rule: finite_induct) simp_all
-lemma setprod_pos_nat_iff [simp]: "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
+lemma prod_pos_nat_iff [simp]: "finite A \<Longrightarrow> prod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
for f :: "'a \<Rightarrow> nat"
- using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
+ using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
-lemma setprod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
+lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
for y :: "'a::comm_monoid_mult"
by (induct A rule: infinite_finite_induct) simp_all
-lemma setprod_power_distrib: "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
+lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
-lemma setprod_gen_delta:
+lemma prod_gen_delta:
fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult"
assumes fin: "finite S"
- shows "setprod (\<lambda>k. if k = a then b k else c) S =
+ shows "prod (\<lambda>k. if k = a then b k else c) S =
(if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)"
proof -
let ?f = "(\<lambda>k. if k=a then b k else c)"
@@ -1270,7 +1270,7 @@
proof (cases "a \<in> S")
case False
then have "\<forall> k\<in> S. ?f k = c" by simp
- with False show ?thesis by (simp add: setprod_constant)
+ with False show ?thesis by (simp add: prod_constant)
next
case True
let ?A = "S - {a}"
@@ -1278,16 +1278,16 @@
from True have eq: "S = ?A \<union> ?B" by blast
have disjoint: "?A \<inter> ?B = {}" by simp
from fin have fin': "finite ?A" "finite ?B" by auto
- have f_A0: "setprod ?f ?A = setprod (\<lambda>i. c) ?A"
- by (rule setprod.cong) auto
+ have f_A0: "prod ?f ?A = prod (\<lambda>i. c) ?A"
+ by (rule prod.cong) auto
from fin True have card_A: "card ?A = card S - 1" by auto
- have f_A1: "setprod ?f ?A = c ^ card ?A"
- unfolding f_A0 by (rule setprod_constant)
- have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
- using setprod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
+ have f_A1: "prod ?f ?A = c ^ card ?A"
+ unfolding f_A0 by (rule prod_constant)
+ have "prod ?f ?A * prod ?f ?B = prod ?f S"
+ using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
by simp
with True card_A show ?thesis
- by (simp add: f_A1 field_simps cong add: setprod.cong cong del: if_weak_cong)
+ by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong)
qed
qed
--- a/src/HOL/Groups_List.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Groups_List.thy Mon Oct 17 19:03:13 2016 +0200
@@ -340,15 +340,15 @@
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
qed
-sublocale setprod: comm_monoid_list_set times 1
+sublocale prod: comm_monoid_list_set times 1
rewrites
"monoid_list.F times 1 = prod_list"
- and "comm_monoid_set.F times 1 = setprod"
+ and "comm_monoid_set.F times 1 = prod"
proof -
show "comm_monoid_list_set times 1" ..
- then interpret setprod: comm_monoid_list_set times 1 .
+ then interpret prod: comm_monoid_list_set times 1 .
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
- from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
+ from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
qed
end
--- a/src/HOL/Int.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Int.thy Mon Oct 17 19:03:13 2016 +0200
@@ -866,7 +866,7 @@
qed
-subsection \<open>@{term sum} and @{term setprod}\<close>
+subsection \<open>@{term sum} and @{term prod}\<close>
lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
by (induct A rule: infinite_finite_induct) auto
@@ -874,14 +874,14 @@
lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
by (induct A rule: infinite_finite_induct) auto
-lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))"
by (induct A rule: infinite_finite_induct) auto
-lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
by (induct A rule: infinite_finite_induct) auto
lemmas int_sum = of_nat_sum [where 'a=int]
-lemmas int_setprod = of_nat_setprod [where 'a=int]
+lemmas int_prod = of_nat_prod [where 'a=int]
text \<open>Legacy theorems\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Oct 17 19:03:13 2016 +0200
@@ -550,12 +550,12 @@
lemma top_power_ennreal: "top ^ n = (if n = 0 then 1 else top :: ennreal)"
by (induction n) (simp_all add: ennreal_mult_eq_top_iff)
-lemma ennreal_setprod_eq_0[simp]:
+lemma ennreal_prod_eq_0[simp]:
fixes f :: "'a \<Rightarrow> ennreal"
- shows "(setprod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
+ shows "(prod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
by (induction A rule: infinite_finite_induct) auto
-lemma ennreal_setprod_eq_top:
+lemma ennreal_prod_eq_top:
fixes f :: "'a \<Rightarrow> ennreal"
shows "(\<Prod>i\<in>I. f i) = top \<longleftrightarrow> (finite I \<and> ((\<forall>i\<in>I. f i \<noteq> 0) \<and> (\<exists>i\<in>I. f i = top)))"
by (induction I rule: infinite_finite_induct) (auto simp: ennreal_mult_eq_top_iff)
@@ -1047,9 +1047,9 @@
lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
by (subst divide_ennreal[symmetric]) auto
-lemma setprod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (setprod f A)"
+lemma prod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (prod f A)"
by (induction A rule: infinite_finite_induct)
- (auto simp: ennreal_mult setprod_nonneg)
+ (auto simp: ennreal_mult prod_nonneg)
lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
apply (cases "0 \<le> c")
--- a/src/HOL/Library/Extended_Real.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1180,7 +1180,7 @@
shows "y \<le> x"
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
-lemma setprod_ereal_0:
+lemma prod_ereal_0:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
proof (cases "finite A")
@@ -1191,7 +1191,7 @@
then show ?thesis by auto
qed
-lemma setprod_ereal_pos:
+lemma prod_ereal_pos:
fixes f :: "'a \<Rightarrow> ereal"
assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
shows "0 \<le> (\<Prod>i\<in>I. f i)"
@@ -1204,7 +1204,7 @@
then show ?thesis by simp
qed
-lemma setprod_PInf:
+lemma prod_PInf:
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
@@ -1213,15 +1213,15 @@
from this assms show ?thesis
proof (induct I)
case (insert i I)
- then have pos: "0 \<le> f i" "0 \<le> setprod f I"
- by (auto intro!: setprod_ereal_pos)
- from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>"
+ then have pos: "0 \<le> f i" "0 \<le> prod f I"
+ by (auto intro!: prod_ereal_pos)
+ from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> prod f I * f i = \<infinity>"
by auto
- also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
- using setprod_ereal_pos[of I f] pos
- by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
+ also have "\<dots> \<longleftrightarrow> (prod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> prod f I \<noteq> 0"
+ using prod_ereal_pos[of I f] pos
+ by (cases rule: ereal2_cases[of "f i" "prod f I"]) auto
also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
- using insert by (auto simp: setprod_ereal_0)
+ using insert by (auto simp: prod_ereal_0)
finally show ?case .
qed simp
next
@@ -1229,7 +1229,7 @@
then show ?thesis by simp
qed
-lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
+lemma prod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (prod f A)"
proof (cases "finite A")
case True
then show ?thesis
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Oct 17 19:03:13 2016 +0200
@@ -2278,11 +2278,11 @@
qed
text \<open>The general form.\<close>
-lemma fps_setprod_nth:
+lemma fps_prod_nth:
fixes m :: nat
and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
- shows "(setprod a {0 .. m}) $ n =
- sum (\<lambda>v. setprod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
+ shows "(prod a {0 .. m}) $ n =
+ sum (\<lambda>v. prod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
(is "?P m n")
proof (induct m arbitrary: n rule: nat_less_induct)
fix m n assume H: "\<forall>m' < m. \<forall>n. ?P m' n"
@@ -2301,8 +2301,8 @@
using Suc by (simp add: set_eq_iff) presburger
have f0: "finite {0 .. k}" "finite {m}" by auto
have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto
- have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n"
- unfolding setprod.union_disjoint[OF f0 d0, unfolded u0] by simp
+ have "(prod a {0 .. m}) $ n = (prod a {0 .. k} * a m) $ n"
+ unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp
also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). \<Prod>j\<in>{0..k}. a j $ v ! j) * a m $ (n - i))"
unfolding fps_mult_nth H[rule_format, OF km] ..
also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)"
@@ -2325,7 +2325,7 @@
apply (rule_tac l = "\<lambda>xs. xs @ [n - x]" in sum.reindex_cong)
apply (simp add: inj_on_def)
apply auto
- unfolding setprod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc]
+ unfolding prod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc]
apply (clarsimp simp add: natpermute_def nth_append)
done
finally show ?thesis .
@@ -2336,18 +2336,18 @@
lemma fps_power_nth_Suc:
fixes m :: nat
and a :: "'a::comm_ring_1 fps"
- shows "(a ^ Suc m)$n = sum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
+ shows "(a ^ Suc m)$n = sum (\<lambda>v. prod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
proof -
- have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}"
- by (simp add: setprod_constant)
- show ?thesis unfolding th0 fps_setprod_nth ..
+ have th0: "a^Suc m = prod (\<lambda>i. a) {0..m}"
+ by (simp add: prod_constant)
+ show ?thesis unfolding th0 fps_prod_nth ..
qed
lemma fps_power_nth:
fixes m :: nat
and a :: "'a::comm_ring_1 fps"
shows "(a ^m)$n =
- (if m=0 then 1$n else sum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
+ (if m=0 then 1$n else sum (\<lambda>v. prod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
by (cases m) (simp_all add: fps_power_nth_Suc del: power_Suc)
lemma fps_nth_power_0:
@@ -2360,10 +2360,10 @@
next
case (Suc n)
then have c: "m = card {0..n}" by simp
- have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
+ have "(a ^m)$0 = prod (\<lambda>i. a$0) {0..n}"
by (simp add: Suc fps_power_nth del: replicate.simps power_Suc)
also have "\<dots> = (a$0) ^ m"
- unfolding c by (rule setprod_constant)
+ unfolding c by (rule prod_constant)
finally show ?thesis .
qed
@@ -2433,10 +2433,10 @@
from j have "{0..m} = insert j ({0..m} - {j})" by auto
also from j have "(\<Prod>i\<in>\<dots>. f $ (v ! i)) = f $ k * (\<Prod>i\<in>{0..m} - {j}. f $ (v ! i))"
- by (subst setprod.insert) auto
+ by (subst prod.insert) auto
also have "(\<Prod>i\<in>{0..m} - {j}. f $ (v ! i)) = (\<Prod>i\<in>{0..m} - {j}. f $ 0)"
- by (intro setprod.cong) (simp_all add: zero)
- also from j have "\<dots> = (f $ 0) ^ m" by (subst setprod_constant) simp_all
+ by (intro prod.cong) (simp_all add: zero)
+ also from j have "\<dots> = (f $ 0) ^ m" by (subst prod_constant) simp_all
finally have "(\<Prod>j = 0..m. f $ (v ! j)) = f $ k * (f $ 0) ^ m" .
} note A = this
@@ -2472,7 +2472,7 @@
using that elem_le_sum_list_nat[of i v] unfolding natpermute_def
by (auto simp: set_conv_nth dest!: spec[of _ i])
hence "?h f = ?h g"
- by (intro sum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
+ by (intro sum.cong refl prod.cong less lessI) (auto simp: natpermute_def)
finally have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) = g $ k * (of_nat (Suc m) * (f $ 0) ^ m)"
by simp
with assms show "f $ k = g $ k"
@@ -2567,7 +2567,7 @@
subsection \<open>Radicals\<close>
-declare setprod.cong [fundef_cong]
+declare prod.cong [fundef_cong]
function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a::field fps \<Rightarrow> nat \<Rightarrow> 'a"
where
@@ -2575,7 +2575,7 @@
| "radical r 0 a (Suc n) = 0"
| "radical r (Suc k) a 0 = r (Suc k) (a$0)"
| "radical r (Suc k) a (Suc n) =
- (a$ Suc n - sum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
+ (a$ Suc n - sum (\<lambda>xs. prod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
{xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) /
(of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
by pat_completeness auto
@@ -2641,14 +2641,14 @@
have eq1: "fps_radical r k a ^ k $ 0 = (\<Prod>j\<in>{0..h}. fps_radical r k a $ (replicate k 0) ! j)"
unfolding fps_power_nth Suc by simp
also have "\<dots> = (\<Prod>j\<in>{0..h}. r k (a$0))"
- apply (rule setprod.cong)
+ apply (rule prod.cong)
apply simp
using Suc
apply (subgoal_tac "replicate k 0 ! x = 0")
apply (auto intro: nth_replicate simp del: replicate.simps)
done
also have "\<dots> = a$0"
- using r Suc by (simp add: setprod_constant)
+ using r Suc by (simp add: prod_constant)
finally show ?thesis
using Suc by simp
qed
@@ -2693,12 +2693,12 @@
unfolding natpermute_contain_maximal by auto
have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) =
(\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
- apply (rule setprod.cong, simp)
+ apply (rule prod.cong, simp)
using i r0
apply (simp del: replicate.simps)
done
also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
- using i r0 by (simp add: setprod_gen_delta)
+ using i r0 by (simp add: prod_gen_delta)
finally show ?ths .
qed rule
then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
@@ -2720,7 +2720,7 @@
by simp
then show ?thesis
unfolding fps_power_nth_Suc
- by (simp add: setprod_constant del: replicate.simps)
+ by (simp add: prod_constant del: replicate.simps)
qed
qed
@@ -2757,10 +2757,10 @@
from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
unfolding natpermute_contain_maximal by auto
have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
- apply (rule setprod.cong, simp)
+ apply (rule prod.cong, simp)
using i r0 by (simp del: replicate.simps)
also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
- unfolding setprod_gen_delta[OF fK] using i r0 by simp
+ unfolding prod_gen_delta[OF fK] using i r0 by simp
finally show ?ths .
qed
then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
@@ -2828,18 +2828,18 @@
unfolding Suc_eq_plus1 natpermute_contain_maximal
by (auto simp del: replicate.simps)
have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
- apply (rule setprod.cong, simp)
+ apply (rule prod.cong, simp)
using i a0
apply (simp del: replicate.simps)
done
also have "\<dots> = a $ n * (?r $ 0)^k"
- using i by (simp add: setprod_gen_delta)
+ using i by (simp add: prod_gen_delta)
finally show ?ths .
qed rule
then have th0: "sum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k"
by (simp add: natpermute_max_card[OF nz, simplified])
have th1: "sum ?g ?Pnknn = sum ?f ?Pnknn"
- proof (rule sum.cong, rule refl, rule setprod.cong, simp)
+ proof (rule sum.cong, rule refl, rule prod.cong, simp)
fix xs i
assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}"
have False if c: "n \<le> xs ! i"
@@ -3380,9 +3380,9 @@
apply (simp add: fps_compose_nth fps_mult_nth sum_distrib_right)
done
-lemma fps_compose_setprod_distrib:
+lemma fps_compose_prod_distrib:
assumes c0: "c$0 = (0::'a::idom)"
- shows "setprod a S oo c = setprod (\<lambda>k. a k oo c) S"
+ shows "prod a S oo c = prod (\<lambda>k. a k oo c) S"
apply (cases "finite S")
apply simp_all
apply (induct S rule: finite_induct)
@@ -3413,10 +3413,10 @@
then show ?thesis by simp
next
case (Suc m)
- have th0: "a^n = setprod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = setprod (\<lambda>k. a oo c) {0..m}"
- by (simp_all add: setprod_constant Suc)
+ have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
+ by (simp_all add: prod_constant Suc)
then show ?thesis
- by (simp add: fps_compose_setprod_distrib[OF c0])
+ by (simp add: fps_compose_prod_distrib[OF c0])
qed
lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
@@ -4155,8 +4155,8 @@
case False
with kn have kn': "k < n"
by simp
- have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
- by (simp_all add: setprod_constant m h)
+ have m1nk: "?m1 n = prod (\<lambda>i. - 1) {..m}" "?m1 k = prod (\<lambda>i. - 1) {0..h}"
+ by (simp_all add: prod_constant m h)
have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
using bn0 kn
unfolding pochhammer_eq_0_iff
@@ -4164,37 +4164,37 @@
apply (erule_tac x= "n - ka - 1" in allE)
apply (auto simp add: algebra_simps of_nat_diff)
done
- have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
- setprod of_nat {Suc (m - h) .. Suc m}"
+ have eq1: "prod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
+ prod of_nat {Suc (m - h) .. Suc m}"
using kn' h m
- by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
+ by (intro prod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
(auto simp: of_nat_diff)
have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
apply (simp add: pochhammer_minus field_simps)
using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n])
- apply (simp add: pochhammer_setprod)
- using setprod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
+ apply (simp add: pochhammer_prod)
+ using prod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
apply (auto simp add: of_nat_diff field_simps)
done
- have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
+ have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}"
apply (simp add: pochhammer_minus field_simps m)
- apply (auto simp add: pochhammer_setprod_rev of_nat_diff setprod.atLeast_Suc_atMost_Suc_shift)
+ apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift)
done
- have th21:"pochhammer (b - of_nat n + 1) k = setprod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
- using kn apply (simp add: pochhammer_setprod_rev m h setprod.atLeast_Suc_atMost_Suc_shift)
- using setprod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
+ have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
+ using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift)
+ using prod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
apply (auto simp add: of_nat_diff field_simps)
done
have "?m1 n * ?p b n =
- setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
+ prod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
using kn' m h unfolding th20 th21 apply simp
- apply (subst setprod.union_disjoint [symmetric])
+ apply (subst prod.union_disjoint [symmetric])
apply auto
- apply (rule setprod.cong)
+ apply (rule prod.cong)
apply auto
done
then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k =
- setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
+ prod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
using nz' by (simp add: field_simps)
have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) =
((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
@@ -4204,7 +4204,7 @@
unfolding th1 th2
using kn' m h
apply (simp add: field_simps gbinomial_mult_fact)
- apply (rule setprod.cong)
+ apply (rule prod.cong)
apply auto
done
finally show ?thesis by simp
--- a/src/HOL/Library/Groups_Big_Fun.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Mon Oct 17 19:03:13 2016 +0200
@@ -283,11 +283,11 @@
sublocale Prod_any: comm_monoid_fun times 1
defines Prod_any = Prod_any.G
- rewrites "comm_monoid_set.F times 1 = setprod"
+ rewrites "comm_monoid_set.F times 1 = prod"
proof -
show "comm_monoid_fun times 1" ..
then interpret Prod_any: comm_monoid_fun times 1 .
- from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
+ from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
qed
end
@@ -308,7 +308,7 @@
from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
- by (simp add: Prod_any.expand_set setprod_zero)
+ by (simp add: Prod_any.expand_set prod_zero)
qed
lemma Prod_any_not_zero:
--- a/src/HOL/Library/Multiset.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Oct 17 19:03:13 2016 +0200
@@ -2269,13 +2269,13 @@
"prod_mset (replicate_mset n a) = a ^ n"
by (induct n) simp_all
-lemma setprod_unfold_prod_mset:
- "setprod f A = prod_mset (image_mset f (mset_set A))"
+lemma prod_unfold_prod_mset:
+ "prod f A = prod_mset (image_mset f (mset_set A))"
by (cases "finite A") (induct A rule: finite_induct, simp_all)
lemma prod_mset_multiplicity:
- "prod_mset M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
- by (simp add: fold_mset_def setprod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
+ "prod_mset M = prod (\<lambda>x. x ^ count M x) (set_mset M)"
+ by (simp add: fold_mset_def prod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
lemma prod_mset_delta: "prod_mset (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
by (induction A) simp_all
--- a/src/HOL/Library/Multiset_Permutations.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy Mon Oct 17 19:03:13 2016 +0200
@@ -161,24 +161,24 @@
context
begin
-private lemma multiset_setprod_fact_insert:
+private lemma multiset_prod_fact_insert:
"(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
(count A x + 1) * (\<Prod>y\<in>set_mset A. fact (count A y))"
proof -
have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
(\<Prod>y\<in>set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))"
- by (intro setprod.cong) simp_all
+ by (intro prod.cong) simp_all
also have "\<dots> = (count A x + 1) * (\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y))"
- by (simp add: setprod.distrib setprod.delta)
+ by (simp add: prod.distrib prod.delta)
also have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y)) = (\<Prod>y\<in>set_mset A. fact (count A y))"
- by (intro setprod.mono_neutral_right) (auto simp: not_in_iff)
+ by (intro prod.mono_neutral_right) (auto simp: not_in_iff)
finally show ?thesis .
qed
-private lemma multiset_setprod_fact_remove:
+private lemma multiset_prod_fact_remove:
"x \<in># A \<Longrightarrow> (\<Prod>y\<in>set_mset A. fact (count A y)) =
count A x * (\<Prod>y\<in>set_mset (A-{#x#}). fact (count (A-{#x#}) y))"
- using multiset_setprod_fact_insert[of "A - {#x#}" x] by simp
+ using multiset_prod_fact_insert[of "A - {#x#}" x] by simp
lemma card_permutations_of_multiset_aux:
"card (permutations_of_multiset A) * (\<Prod>x\<in>set_mset A. fact (count A x)) = fact (size A)"
@@ -199,7 +199,7 @@
have "card (permutations_of_multiset (A - {#x#})) * (\<Prod>y\<in>set_mset A. fact (count A y)) =
count A x * (card (permutations_of_multiset (A - {#x#})) *
(\<Prod>y\<in>set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _")
- by (subst multiset_setprod_fact_remove[OF x]) simp_all
+ by (subst multiset_prod_fact_remove[OF x]) simp_all
also note remove.IH[OF x]
also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset)
finally show "?lhs = count A x * fact (size A - 1)" .
@@ -223,7 +223,7 @@
proof -
note card_permutations_of_multiset_aux[of "A + {#x#}"]
also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp
- also note multiset_setprod_fact_insert[of A x]
+ also note multiset_prod_fact_insert[of A x]
also note card_permutations_of_multiset_aux[of A, symmetric]
finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) *
(\<Prod>y\<in>set_mset A. fact (count A y)) =
--- a/src/HOL/Library/Polynomial.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1054,13 +1054,13 @@
shows "poly (p ^ n) x = poly p x ^ n"
by (induct n) simp_all
-lemma poly_setprod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
+lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
by (induct A rule: infinite_finite_induct) simp_all
-lemma degree_setprod_sum_le: "finite S \<Longrightarrow> degree (setprod f S) \<le> sum (degree o f) S"
+lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree o f) S"
proof (induct S rule: finite_induct)
case (insert a S)
- show ?case unfolding setprod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
+ show ?case unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
by (rule le_trans[OF degree_mult_le], insert insert, auto)
qed simp
@@ -2856,7 +2856,7 @@
by (cases "finite A", induction rule: finite_induct)
(simp_all add: pcompose_1 pcompose_add)
-lemma pcompose_setprod: "pcompose (setprod f A) p = setprod (\<lambda>i. pcompose (f i) p) A"
+lemma pcompose_prod: "pcompose (prod f A) p = prod (\<lambda>i. pcompose (f i) p) A"
by (cases "finite A", induction rule: finite_induct)
(simp_all add: pcompose_1 pcompose_mult)
@@ -3209,9 +3209,9 @@
reflect_poly p ^ n"
by (induction n) (simp_all add: reflect_poly_mult)
-lemma reflect_poly_setprod:
- "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) =
- setprod (\<lambda>x. reflect_poly (f x)) A"
+lemma reflect_poly_prod:
+ "reflect_poly (prod (f :: _ \<Rightarrow> _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) =
+ prod (\<lambda>x. reflect_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
lemma reflect_poly_prod_list:
@@ -3225,7 +3225,7 @@
lemmas reflect_poly_simps =
reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
- reflect_poly_power reflect_poly_setprod reflect_poly_prod_list
+ reflect_poly_power reflect_poly_prod reflect_poly_prod_list
subsection \<open>Derivatives of univariate polynomials\<close>
@@ -3395,11 +3395,11 @@
apply (simp add: algebra_simps)
done
-lemma pderiv_setprod: "pderiv (setprod f (as)) =
- (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
+lemma pderiv_prod: "pderiv (prod f (as)) =
+ (\<Sum>a \<in> as. prod f (as - {a}) * pderiv (f a))"
proof (induct as rule: infinite_finite_induct)
case (insert a as)
- hence id: "setprod f (insert a as) = f a * setprod f as"
+ hence id: "prod f (insert a as) = f a * prod f as"
"\<And> g. sum g (insert a as) = g a + sum g as"
"insert a as - {a} = as"
by auto
@@ -3407,9 +3407,9 @@
fix b
assume "b \<in> as"
hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto
- have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
+ have "prod f (insert a as - {b}) = f a * prod f (as - {b})"
unfolding id2
- by (subst setprod.insert, insert insert, auto)
+ by (subst prod.insert, insert insert, auto)
} note id2 = this
show ?case
unfolding id pderiv_mult insert(3) sum_distrib_left
--- a/src/HOL/Library/Polynomial_FPS.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Mon Oct 17 19:03:13 2016 +0200
@@ -67,7 +67,7 @@
lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
by (induction xs) (simp_all add: fps_of_poly_add)
-lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
+lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A"
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
@@ -144,7 +144,7 @@
lemmas fps_of_poly_simps =
fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
- fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
+ fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
fps_of_poly_divide_numeral
--- a/src/HOL/Library/RBT_Set.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Library/RBT_Set.thy Mon Oct 17 19:03:13 2016 +0200
@@ -88,7 +88,7 @@
"sum = sum" ..
lemma [code, code del]:
- "setprod = setprod" ..
+ "prod = prod" ..
lemma [code, code del]:
"Product_Type.product = Product_Type.product" ..
--- a/src/HOL/Lifting_Set.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Lifting_Set.thy Mon Oct 17 19:03:13 2016 +0200
@@ -286,7 +286,7 @@
qed
lemmas sum_parametric = sum.F_parametric
-lemmas setprod_parametric = setprod.F_parametric
+lemmas prod_parametric = prod.F_parametric
lemma rel_set_UNION:
assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
--- a/src/HOL/Limits.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Limits.thy Mon Oct 17 19:03:13 2016 +0200
@@ -833,20 +833,20 @@
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
unfolding continuous_on_def by (auto intro: tendsto_power)
-lemma tendsto_setprod [tendsto_intros]:
+lemma tendsto_prod [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
shows "(\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F"
by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)
-lemma continuous_setprod [continuous_intros]:
+lemma continuous_prod [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
- unfolding continuous_def by (rule tendsto_setprod)
-
-lemma continuous_on_setprod [continuous_intros]:
+ unfolding continuous_def by (rule tendsto_prod)
+
+lemma continuous_on_prod [continuous_intros]:
fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
- unfolding continuous_on_def by (auto intro: tendsto_setprod)
+ unfolding continuous_on_def by (auto intro: tendsto_prod)
lemma tendsto_of_real_iff:
"((\<lambda>x. of_real (f x) :: 'a::real_normed_div_algebra) \<longlongrightarrow> of_real c) F \<longleftrightarrow> (f \<longlongrightarrow> c) F"
--- a/src/HOL/List.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/List.thy Mon Oct 17 19:03:13 2016 +0200
@@ -4672,7 +4672,7 @@
moreover
have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
- by (subst setprod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
+ by (subst prod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
ultimately show ?case
by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
qed
--- a/src/HOL/Nat_Transfer.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy Mon Oct 17 19:03:13 2016 +0200
@@ -186,33 +186,33 @@
]
-text \<open>sum and setprod\<close>
+text \<open>sum and prod\<close>
(* this handles the case where the *domain* of f is nat *)
lemma transfer_nat_int_sum_prod:
"sum f A = sum (%x. f (nat x)) (int ` A)"
- "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+ "prod f A = prod (%x. f (nat x)) (int ` A)"
apply (subst sum.reindex)
apply (unfold inj_on_def, auto)
- apply (subst setprod.reindex)
+ apply (subst prod.reindex)
apply (unfold inj_on_def o_def, auto)
done
(* this handles the case where the *range* of f is nat *)
lemma transfer_nat_int_sum_prod2:
"sum f A = nat(sum (%x. int (f x)) A)"
- "setprod f A = nat(setprod (%x. int (f x)) A)"
+ "prod f A = nat(prod (%x. int (f x)) A)"
apply (simp only: int_sum [symmetric] nat_int)
- apply (simp only: int_setprod [symmetric] nat_int)
+ apply (simp only: int_prod [symmetric] nat_int)
done
lemma transfer_nat_int_sum_prod_closure:
"nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
unfolding nat_set_def
apply (rule sum_nonneg)
apply auto
- apply (rule setprod_nonneg)
+ apply (rule prod_nonneg)
apply auto
done
@@ -223,28 +223,28 @@
lemma transfer_nat_int_sum_prod_closure:
"(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
unfolding nat_set_def simp_implies_def
apply (rule sum_nonneg)
apply auto
- apply (rule setprod_nonneg)
+ apply (rule prod_nonneg)
apply auto
done
*)
(* Making A = B in this lemma doesn't work. Why not?
- Also, why aren't sum.cong and setprod.cong enough,
+ Also, why aren't sum.cong and prod.cong enough,
with the previously mentioned rule turned on? *)
lemma transfer_nat_int_sum_prod_cong:
"A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
sum f A = sum g B"
"A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- setprod f A = setprod g B"
+ prod f A = prod g B"
unfolding nat_set_def
apply (subst sum.cong, assumption)
apply auto [2]
- apply (subst setprod.cong, assumption, auto)
+ apply (subst prod.cong, assumption, auto)
done
declare transfer_morphism_nat_int [transfer add
@@ -389,29 +389,29 @@
]
-text \<open>sum and setprod\<close>
+text \<open>sum and prod\<close>
(* this handles the case where the *domain* of f is int *)
lemma transfer_int_nat_sum_prod:
"nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
- "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+ "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
apply (subst sum.reindex)
apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
- apply (subst setprod.reindex)
+ apply (subst prod.reindex)
apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
- cong: setprod.cong)
+ cong: prod.cong)
done
(* this handles the case where the *range* of f is int *)
lemma transfer_int_nat_sum_prod2:
"(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
"(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
- setprod f A = int(setprod (%x. nat (f x)) A)"
+ prod f A = int(prod (%x. nat (f x)) A)"
unfolding is_nat_def
by (subst int_sum) auto
declare transfer_morphism_int_nat [transfer add
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
- cong: sum.cong setprod.cong]
+ cong: sum.cong prod.cong]
end
--- a/src/HOL/Number_Theory/Cong.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Mon Oct 17 19:03:13 2016 +0200
@@ -193,7 +193,7 @@
apply (auto intro: cong_add_int)
done
-lemma cong_setprod_nat [rule_format]:
+lemma cong_prod_nat [rule_format]:
"(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
[(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
@@ -201,7 +201,7 @@
apply (auto intro: cong_mult_nat)
done
-lemma cong_setprod_int [rule_format]:
+lemma cong_prod_int [rule_format]:
"(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
[(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
apply (cases "finite A")
@@ -562,22 +562,22 @@
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
by (auto simp add: cong_altdef_int lcm_least) [1]
-lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
- apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime)
+ apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
done
-lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow>
(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
- apply (metis coprime_cong_mult_int gcd.commute setprod_coprime)
+ apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
done
lemma binary_chinese_remainder_aux_nat:
@@ -760,7 +760,7 @@
fix i
assume "i : A"
with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
- by (intro setprod_coprime, auto)
+ by (intro prod_coprime, auto)
then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
by (elim cong_solve_coprime_nat)
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
@@ -769,7 +769,7 @@
(mod (\<Prod>j \<in> A - {i}. m j))"
by (subst mult.commute, rule cong_mult_self_nat)
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
- (mod setprod m (A - {i}))"
+ (mod prod m (A - {i}))"
by blast
qed
@@ -824,7 +824,7 @@
[x = y] (mod (\<Prod>i\<in>A. m i))"
apply (induct set: finite)
apply auto
- apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime)
+ apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
done
lemma chinese_remainder_unique_nat:
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Mon Oct 17 19:03:13 2016 +0200
@@ -1294,12 +1294,12 @@
using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
by simp
-lemma prime_elem_multiplicity_setprod_distrib:
+lemma prime_elem_multiplicity_prod_distrib:
assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
- shows "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
+ shows "multiplicity p (prod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
proof -
- have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
- using assms by (subst setprod_unfold_prod_mset)
+ have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
+ using assms by (subst prod_unfold_prod_mset)
(simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset
multiset.map_comp o_def)
also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
@@ -1352,7 +1352,7 @@
"prime p \<Longrightarrow> prime_factors p = {p}"
by (drule prime_factorization_prime) simp
-lemma setprod_prime_factors:
+lemma prod_prime_factors:
assumes "x \<noteq> 0"
shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
proof -
@@ -1361,7 +1361,7 @@
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
by (subst prod_mset_multiplicity) simp_all
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
- by (intro setprod.cong)
+ by (intro prod.cong)
(simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
finally show ?thesis ..
qed
@@ -1751,12 +1751,12 @@
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
also have "\<dots> = ?rhs1"
by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
- count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
+ count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
finally show "gcd x y = ?rhs1" .
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
also have "\<dots> = ?rhs2"
by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
- count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
+ count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
finally show "lcm x y = ?rhs2" .
qed
--- a/src/HOL/Number_Theory/Gauss.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Mon Oct 17 19:03:13 2016 +0200
@@ -209,8 +209,8 @@
using p_prime A_ncong_p [OF assms]
by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
-lemma A_prod_relprime: "gcd (setprod id A) p = 1"
- by (metis id_def all_A_relprime setprod_coprime)
+lemma A_prod_relprime: "gcd (prod id A) p = 1"
+ by (metis id_def all_A_relprime prod_coprime)
subsection \<open>Relationships Between Gauss Sets\<close>
@@ -242,15 +242,15 @@
lemma C_card_eq_D_plus_E: "card C = card D + card E"
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
-lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
- by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
+lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
+ by (metis C_eq D_E_disj finite_D finite_E inf_commute prod.union_disjoint sup_commute)
-lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
+lemma C_B_zcong_prod: "[prod id C = prod id B] (mod p)"
apply (auto simp add: C_def)
apply (insert finite_B SR_B_inj)
- apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
+ apply (drule prod.reindex [of "\<lambda>x. x mod int p" B id])
apply auto
- apply (rule cong_setprod_int)
+ apply (rule cong_prod_int)
apply (auto simp add: cong_int_def)
done
@@ -295,25 +295,25 @@
using finite_A F_Un_D_subset A_card_eq F_Un_D_card
by (auto simp add: card_seteq)
-lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
- by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
+lemma prod_D_F_eq_prod_A: "(prod id D) * (prod id F) = prod id A"
+ by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F prod.union_disjoint)
-lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
+lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
proof -
- have FE: "setprod id F = setprod (op - p) E"
+ have FE: "prod id F = prod (op - p) E"
apply (auto simp add: F_def)
apply (insert finite_E inj_on_pminusx_E)
- apply (drule setprod.reindex, auto)
+ apply (drule prod.reindex, auto)
done
then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
- then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
+ then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
using finite_E p_ge_2
- cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
+ cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
by auto
- then have two: "[setprod id F = setprod (uminus) E](mod p)"
- by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
- have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
+ then have two: "[prod id F = prod (uminus) E](mod p)"
+ by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
+ have "prod uminus E = (-1) ^ (card E) * (prod id E)"
using finite_E by (induct set: finite) auto
with two show ?thesis
by simp
@@ -322,50 +322,50 @@
subsection \<open>Gauss' Lemma\<close>
-lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
+lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
theorem pre_gauss_lemma:
"[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
- have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong)
- then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
+ have "[prod id A = prod id F * prod id D](mod p)"
+ by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
+ then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
apply (rule cong_trans_int)
apply (metis cong_scalar_int prod_F_zcong)
done
- then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
+ then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
- then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
+ then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
- then have "[setprod id A = ((-1)^(card E) *
- (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
+ then have "[prod id A = ((-1)^(card E) *
+ (prod id ((\<lambda>x. x * a) ` A)))] (mod p)"
by (simp add: B_def)
- then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
+ then have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. x * a) A))]
(mod p)"
- by (simp add: inj_on_xa_A setprod.reindex)
- moreover have "setprod (\<lambda>x. x * a) A =
- setprod (\<lambda>x. a) A * setprod id A"
+ by (simp add: inj_on_xa_A prod.reindex)
+ moreover have "prod (\<lambda>x. x * a) A =
+ prod (\<lambda>x. a) A * prod id A"
using finite_A by (induct set: finite) auto
- ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
- setprod id A))] (mod p)"
+ ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A *
+ prod id A))] (mod p)"
by simp
- then have "[setprod id A = ((-1)^(card E) * a^(card A) *
- setprod id A)](mod p)"
+ then have "[prod id A = ((-1)^(card E) * a^(card A) *
+ prod id A)](mod p)"
apply (rule cong_trans_int)
- apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
+ apply (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
done
- then have a: "[setprod id A * (-1)^(card E) =
- ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
+ then have a: "[prod id A * (-1)^(card E) =
+ ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
by (rule cong_scalar_int)
- then have "[setprod id A * (-1)^(card E) = setprod id A *
+ then have "[prod id A * (-1)^(card E) = prod id A *
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
apply (rule cong_trans_int)
apply (simp add: a mult.commute mult.left_commute)
done
- then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
+ then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
apply (rule cong_trans_int)
- apply (simp add: aux cong del: setprod.strong_cong)
+ apply (simp add: aux cong del: prod.strong_cong)
done
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel_int)
--- a/src/HOL/Number_Theory/Primes.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Mon Oct 17 19:03:13 2016 +0200
@@ -485,11 +485,11 @@
lemma prime_factorization_nat:
"n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
- by (simp add: setprod_prime_factors)
+ by (simp add: prod_prime_factors)
lemma prime_factorization_int:
"n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
- by (simp add: setprod_prime_factors)
+ by (simp add: prod_prime_factors)
lemma prime_factorization_unique_nat:
fixes f :: "nat \<Rightarrow> _"
@@ -524,13 +524,13 @@
by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
(* TODO Move *)
-lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
+lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A"
by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
lemma primes_characterization'_int [rule_format]:
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
- by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
+ by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
lemma multiplicity_characterization_nat:
"S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
@@ -545,7 +545,7 @@
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
- (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
+ (auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
lemma multiplicity_characterization'_int [rule_format]:
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
@@ -583,11 +583,11 @@
unfolding set_mset_def count_A by (auto simp: g_def)
with assms have prime: "prime x" if "x \<in># A" for x using that by auto
from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
- by (intro setprod.cong) (auto simp: g_def)
+ by (intro prod.cong) (auto simp: g_def)
also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
- by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
+ by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
also have "\<dots> = prod_mset A"
- by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: setprod.cong)
+ by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
@@ -601,10 +601,10 @@
shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
using assms by (induct A) (auto simp add: prime_factorization_mult)
-lemma prime_factors_setprod:
+lemma prime_factors_prod:
assumes "finite A" and "0 \<notin> f ` A"
- shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
- using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset)
+ shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
+ using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
lemma prime_factors_fact:
"prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
@@ -621,7 +621,7 @@
by (auto intro: order_trans)
} note * = this
show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
- by (auto simp add: fact_setprod prime_factors_setprod Suc_le_eq dest!: prime_prime_factors intro: *)
+ by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
qed
lemma prime_dvd_fact_iff:
--- a/src/HOL/Number_Theory/Residues.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Mon Oct 17 19:03:13 2016 +0200
@@ -428,10 +428,10 @@
apply auto
done
also have "\<dots> = fact (p - 1) mod p"
- apply (simp add: fact_setprod)
+ apply (simp add: fact_prod)
apply (insert assms)
apply (subst res_prime_units_eq)
- apply (simp add: int_setprod zmod_int setprod_int_eq)
+ apply (simp add: int_prod zmod_int prod_int_eq)
done
finally have "fact (p - 1) mod p = \<ominus> \<one>" .
then show ?thesis
@@ -445,7 +445,7 @@
proof (cases "p = 2")
case True
then show ?thesis
- by (simp add: cong_int_def fact_setprod)
+ by (simp add: cong_int_def fact_prod)
next
case False
then show ?thesis
--- a/src/HOL/Old_Number_Theory/Euler.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Mon Oct 17 19:03:13 2016 +0200
@@ -133,7 +133,7 @@
then show ?thesis by auto
qed
-lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
+lemma SetS_prod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
~(QuadRes p a); x \<in> (SetS a p) |] ==>
[\<Prod>x = a] (mod p)"
apply (auto simp add: SetS_def MultInvPair_def)
@@ -174,21 +174,21 @@
apply (frule d22set_g_1, auto)
done
-lemma Union_SetS_setprod_prop1:
+lemma Union_SetS_prod_prop1:
assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
"~(QuadRes p a)"
shows "[\<Prod>(\<Union>(SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
proof -
- from assms have "[\<Prod>(\<Union>(SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
+ from assms have "[\<Prod>(\<Union>(SetS a p)) = prod (prod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
- MultInvPair_prop1c setprod.Union_disjoint)
- also have "[setprod (setprod (%x. x)) (SetS a p) =
- setprod (%x. a) (SetS a p)] (mod p)"
- by (rule setprod_same_function_zcong)
- (auto simp add: assms SetS_setprod_prop SetS_finite)
- also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
+ MultInvPair_prop1c prod.Union_disjoint)
+ also have "[prod (prod (%x. x)) (SetS a p) =
+ prod (%x. a) (SetS a p)] (mod p)"
+ by (rule prod_same_function_zcong)
+ (auto simp add: assms SetS_prod_prop SetS_finite)
+ also (zcong_trans) have "[prod (%x. a) (SetS a p) =
a^(card (SetS a p))] (mod p)"
- by (auto simp add: assms SetS_finite setprod_constant)
+ by (auto simp add: assms SetS_finite prod_constant)
finally (zcong_trans) show ?thesis
apply (rule zcong_trans)
apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
@@ -197,7 +197,7 @@
done
qed
-lemma Union_SetS_setprod_prop2:
+lemma Union_SetS_prod_prop2:
assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
shows "\<Prod>(\<Union>(SetS a p)) = zfact (p - 1)"
proof -
@@ -219,8 +219,8 @@
lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
[zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
- apply (frule Union_SetS_setprod_prop1)
- apply (auto simp add: Union_SetS_setprod_prop2)
+ apply (frule Union_SetS_prod_prop1)
+ apply (auto simp add: Union_SetS_prod_prop2)
done
text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Oct 17 19:03:13 2016 +0200
@@ -252,7 +252,7 @@
apply (simplesubst BnorRset.simps) \<comment>\<open>multiple redexes\<close>
apply (unfold Let_def, auto)
apply (simp add: Bnor_fin Bnor_mem_zle_swap)
- apply (subst setprod.insert)
+ apply (subst prod.insert)
apply (rule_tac [2] Bnor_prod_power_aux)
apply (unfold inj_on_def)
apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
--- a/src/HOL/Old_Number_Theory/Finite2.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Mon Oct 17 19:03:13 2016 +0200
@@ -26,9 +26,9 @@
assume "infinite S" thus ?thesis by simp
qed
-lemma setprod_same_function_zcong:
+lemma prod_same_function_zcong:
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
- shows "[setprod f S = setprod g S] (mod m)"
+ shows "[prod f S = prod g S] (mod m)"
proof cases
assume "finite S"
thus ?thesis using a by induct (simp_all add: zcong_zmult)
--- a/src/HOL/Old_Number_Theory/Gauss.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Mon Oct 17 19:03:13 2016 +0200
@@ -263,7 +263,7 @@
lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
-lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
+lemma A_prod_relprime: "zgcd (prod id A) p = 1"
by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
@@ -292,18 +292,18 @@
lemma C_card_eq_D_plus_E: "card C = card D + card E"
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
-lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
+lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
apply (insert D_E_disj finite_D finite_E C_eq)
- apply (frule setprod.union_disjoint [of D E id])
+ apply (frule prod.union_disjoint [of D E id])
apply auto
done
-lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
+lemma C_B_zcong_prod: "[prod id C = prod id B] (mod p)"
apply (auto simp add: C_def)
apply (insert finite_B SR_B_inj)
- apply (frule setprod.reindex [of "StandardRes p" B id])
+ apply (frule prod.reindex [of "StandardRes p" B id])
apply auto
- apply (rule setprod_same_function_zcong)
+ apply (rule prod_same_function_zcong)
apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
done
@@ -372,25 +372,25 @@
using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
lemma prod_D_F_eq_prod_A:
- "(setprod id D) * (setprod id F) = setprod id A"
+ "(prod id D) * (prod id F) = prod id A"
apply (insert F_D_disj finite_D finite_F)
- apply (frule setprod.union_disjoint [of F D id])
+ apply (frule prod.union_disjoint [of F D id])
apply (auto simp add: F_Un_D_eq_A)
done
lemma prod_F_zcong:
- "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
+ "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
proof -
- have "setprod id F = setprod id (op - p ` E)"
+ have "prod id F = prod id (op - p ` E)"
by (auto simp add: F_def)
- then have "setprod id F = setprod (op - p) E"
+ then have "prod id F = prod (op - p) E"
apply simp
apply (insert finite_E inj_on_pminusx_E)
- apply (frule setprod.reindex [of "minus p" E id])
+ apply (frule prod.reindex [of "minus p" E id])
apply auto
done
then have one:
- "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
+ "[prod id F = prod (StandardRes p o (op - p)) E] (mod p)"
apply simp
apply (insert p_g_0 finite_E StandardRes_prod)
by (auto)
@@ -409,20 +409,20 @@
apply (rule_tac b = "p - x" in zcong_trans, auto)
done
ultimately have c:
- "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
+ "[prod (StandardRes p o (op - p)) E = prod (uminus) E](mod p)"
apply simp
using finite_E p_g_0
- setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+ prod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
by auto
- then have two: "[setprod id F = setprod (uminus) E](mod p)"
+ then have two: "[prod id F = prod (uminus) E](mod p)"
apply (insert one c)
- apply (rule zcong_trans [of "setprod id F"
- "setprod (StandardRes p o op - p) E" p
- "setprod uminus E"], auto)
+ apply (rule zcong_trans [of "prod id F"
+ "prod (StandardRes p o op - p) E" p
+ "prod uminus E"], auto)
done
- also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
+ also have "prod uminus E = (prod id E) * (-1)^(card E)"
using finite_E by (induct set: finite) auto
- then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
+ then have "prod uminus E = (-1) ^ (card E) * (prod id E)"
by (simp add: mult.commute)
with two show ?thesis
by simp
@@ -431,52 +431,52 @@
subsection \<open>Gauss' Lemma\<close>
-lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
+lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
by (auto simp add: finite_E neg_one_special)
theorem pre_gauss_lemma:
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
- have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong)
- then have "[setprod id A = ((-1)^(card E) * setprod id E) *
- setprod id D] (mod p)"
- by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.strong_cong)
- then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
+ have "[prod id A = prod id F * prod id D](mod p)"
+ by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
+ then have "[prod id A = ((-1)^(card E) * prod id E) *
+ prod id D] (mod p)"
+ by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: prod.strong_cong)
+ then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
apply (rule zcong_trans)
apply (insert C_prod_eq_D_times_E, erule subst)
apply (subst mult.assoc)
apply auto
done
- then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
+ then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
apply (rule zcong_trans)
- apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: setprod.strong_cong)
+ apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: prod.strong_cong)
done
- then have "[setprod id A = ((-1)^(card E) *
- (setprod id ((%x. x * a) ` A)))] (mod p)"
+ then have "[prod id A = ((-1)^(card E) *
+ (prod id ((%x. x * a) ` A)))] (mod p)"
by (simp add: B_def)
- then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
+ then have "[prod id A = ((-1)^(card E) * (prod (%x. x * a) A))]
(mod p)"
- by (simp add:finite_A inj_on_xa_A setprod.reindex cong del: setprod.strong_cong)
- moreover have "setprod (%x. x * a) A =
- setprod (%x. a) A * setprod id A"
+ by (simp add:finite_A inj_on_xa_A prod.reindex cong del: prod.strong_cong)
+ moreover have "prod (%x. x * a) A =
+ prod (%x. a) A * prod id A"
using finite_A by (induct set: finite) auto
- ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
- setprod id A))] (mod p)"
+ ultimately have "[prod id A = ((-1)^(card E) * (prod (%x. a) A *
+ prod id A))] (mod p)"
by simp
- then have "[setprod id A = ((-1)^(card E) * a^(card A) *
- setprod id A)](mod p)"
- by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc)
- then have a: "[setprod id A * (-1)^(card E) =
- ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
+ then have "[prod id A = ((-1)^(card E) * a^(card A) *
+ prod id A)](mod p)"
+ by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A prod_constant mult.assoc)
+ then have a: "[prod id A * (-1)^(card E) =
+ ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
by (rule zcong_scalar)
- then have "[setprod id A * (-1)^(card E) = setprod id A *
+ then have "[prod id A * (-1)^(card E) = prod id A *
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
by (rule zcong_trans) (simp add: a mult.commute mult.left_commute)
- then have "[setprod id A * (-1)^(card E) = setprod id A *
+ then have "[prod id A * (-1)^(card E) = prod id A *
a^(card A)](mod p)"
- by (rule zcong_trans) (simp add: aux cong del: setprod.strong_cong)
- with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
+ by (rule zcong_trans) (simp add: aux cong del: prod.strong_cong)
+ with this zcong_cancel2 [of p "prod id A" "(- 1) ^ card E" "a ^ card A"]
p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (simp add: order_less_imp_le)
from this show ?thesis
--- a/src/HOL/Old_Number_Theory/Int2.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy Mon Oct 17 19:03:13 2016 +0200
@@ -170,7 +170,7 @@
done
lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |]
- ==> zgcd (setprod id A) y = 1"
+ ==> zgcd (prod id A) y = 1"
by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Mon Oct 17 19:03:13 2016 +0200
@@ -561,7 +561,7 @@
lemma nproduct_mod:
assumes fS: "finite S" and n0: "n \<noteq> 0"
- shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)"
+ shows "[prod (\<lambda>m. a(m) mod n) S = prod a S] (mod n)"
proof-
have th1:"[1 = 1] (mod n)" by (simp add: modeq_def)
from cong_mult
@@ -569,17 +569,17 @@
[x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)"
by blast
have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def)
- from setprod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS)
+ from prod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS)
qed
lemma nproduct_cmul:
assumes fS:"finite S"
- shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
-unfolding setprod.distrib setprod_constant [of c] ..
+ shows "prod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * prod a S"
+unfolding prod.distrib prod_constant [of c] ..
lemma coprime_nproduct:
assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
- shows "coprime n (setprod a S)"
+ shows "coprime n (prod a S)"
using fS by (rule finite_subset_induct)
(insert Sn, auto simp add: coprime_mul)
@@ -607,7 +607,7 @@
let ?h = "\<lambda>m. (a * m) mod n"
have eq0: "(\<Prod>i\<in>?S. ?h i) = (\<Prod>i\<in>?S. i)"
- proof (rule setprod.reindex_bij_betw)
+ proof (rule prod.reindex_bij_betw)
have "inj_on (\<lambda>i. ?h i) ?S"
proof (rule inj_onI)
fix x y assume "?h x = ?h y"
@@ -636,7 +636,7 @@
have "[(\<Prod>i\<in>?S. a * i) = (\<Prod>i\<in>?S. ?h i)] (mod n)"
by (simp add: cong_commute)
also have "[(\<Prod>i\<in>?S. ?h i) = ?P] (mod n)"
- using eq0 fS an by (simp add: setprod_def modeq_def)
+ using eq0 fS an by (simp add: prod_def modeq_def)
finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
unfolding cardfS mult.commute[of ?P "a^ (card ?S)"]
nproduct_cmul[OF fS, symmetric] mult_1_right by simp
--- a/src/HOL/Old_Number_Theory/Residues.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy Mon Oct 17 19:03:13 2016 +0200
@@ -147,7 +147,7 @@
by (auto simp add: zcong_zmod)
lemma StandardRes_prod: "[| finite X; 0 < m |]
- ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)"
+ ==> [prod f X = prod (StandardRes m o f) X] (mod m)"
apply (rule_tac F = X in finite_induct)
apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
done
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Oct 17 19:03:13 2016 +0200
@@ -229,9 +229,9 @@
apply (subgoal_tac [2] "a = 1 \<or> a = p - 1")
apply (rule_tac [3] zcong_square_zless)
apply auto
- apply (subst setprod.insert)
+ apply (subst prod.insert)
prefer 3
- apply (subst setprod.insert)
+ apply (subst prod.insert)
apply (auto simp add: fin_bijER)
apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
apply (simp add: mult.assoc)
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Oct 17 19:03:13 2016 +0200
@@ -247,8 +247,8 @@
prefer 2
apply (subst wset.simps)
apply (auto, unfold Let_def, auto)
- apply (subst setprod.insert)
- apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
+ apply (subst prod.insert)
+ apply (tactic \<open>stac @{context} @{thm prod.insert} 3\<close>)
apply (subgoal_tac [5]
"zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
prefer 5
--- a/src/HOL/Probability/Central_Limit_Theorem.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Probability/Central_Limit_Theorem.thy Mon Oct 17 19:03:13 2016 +0200
@@ -64,7 +64,7 @@
apply auto
done
also have "\<dots> = (\<psi> n t)^n"
- by (auto simp add: * setprod_constant)
+ by (auto simp add: * prod_constant)
finally have \<phi>_eq: "\<phi> n t =(\<psi> n t)^n" .
have "norm (\<psi> n t - (1 - ?t^2 * \<sigma>\<^sup>2 / 2)) \<le> ?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))"
--- a/src/HOL/Probability/Independent_Family.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Mon Oct 17 19:03:13 2016 +0200
@@ -166,7 +166,7 @@
also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
using \<open>A j = X\<close> by simp
also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
- unfolding setprod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob (A i)"]
+ unfolding prod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob (A i)"]
using \<open>j \<in> J\<close> by (simp add: insert_absorb)
finally show ?thesis .
qed
@@ -207,7 +207,7 @@
have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
using J A \<open>j \<in> K\<close> by (intro indep_setsD[OF G']) auto
then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
- using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: setprod.cong) }
+ using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: prod.cong) }
ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
by (simp add: field_simps)
also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
@@ -233,7 +233,7 @@
qed
moreover { fix k
from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
- by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: if_split_asm)
+ by (subst indep_setsD[OF F(2)]) (auto intro!: prod.cong split: if_split_asm)
also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
@@ -478,9 +478,9 @@
also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono)
also have "\<dots> = (\<Prod>j\<in>K. \<Prod>l\<in>L j. prob (E' j l))"
- using K L L_inj by (subst setprod.UNION_disjoint) auto
+ using K L L_inj by (subst prod.UNION_disjoint) auto
also have "\<dots> = (\<Prod>j\<in>K. prob (A j))"
- using K L E' by (auto simp add: A intro!: setprod.cong indep_setsD[OF indep, symmetric]) blast
+ using K L E' by (auto simp add: A intro!: prod.cong indep_setsD[OF indep, symmetric]) blast
finally show "prob (\<Inter>j\<in>K. A j) = (\<Prod>j\<in>K. prob (A j))" .
qed
next
@@ -849,8 +849,8 @@
with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
by auto
also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
- unfolding if_distrib setprod.If_cases[OF \<open>finite I\<close>]
- using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 setprod.neutral_const)
+ unfolding if_distrib prod.If_cases[OF \<open>finite I\<close>]
+ using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 prod.neutral_const)
finally show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" ..
qed
qed
@@ -1007,7 +1007,7 @@
finally show ?thesis .
qed
-lemma (in prob_space) indep_vars_setprod:
+lemma (in prob_space) indep_vars_prod:
fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
@@ -1092,7 +1092,7 @@
using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
- by (auto simp: emeasure_eq_measure setprod_ennreal measure_nonneg setprod_nonneg)
+ by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))"
using rv J by (simp add: emeasure_distr)
also have "\<dots> = emeasure ?P' E"
@@ -1133,7 +1133,7 @@
using rv J Y by (simp add: emeasure_distr)
finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" .
then show "prob (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. prob (Y' i))"
- by (auto simp: emeasure_eq_measure setprod_ennreal measure_nonneg setprod_nonneg)
+ by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
qed
qed
qed
@@ -1283,15 +1283,15 @@
by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)"
- using I(3) by (auto intro!: nn_integral_cong setprod.cong simp add: Y_def max_def)
+ using I(3) by (auto intro!: nn_integral_cong prod.cong simp add: Y_def max_def)
also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
by (subst nn_integral_distr) auto
also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. \<omega> \<partial>distr M borel (Y i)))"
- by (rule product_nn_integral_setprod) (auto intro: \<open>finite I\<close>)
+ by (rule product_nn_integral_prod) (auto intro: \<open>finite I\<close>)
also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
- by (intro setprod.cong nn_integral_cong) (auto simp: nn_integral_distr Y_def rv_X)
+ by (intro prod.cong nn_integral_cong) (auto simp: nn_integral_distr Y_def rv_X)
finally show ?thesis .
qed (simp add: emeasure_space_1)
@@ -1330,15 +1330,15 @@
also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
- by (rule product_integral_setprod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y)
+ by (rule product_integral_prod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y)
also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
- by (intro setprod.cong integral_cong)
+ by (intro prod.cong integral_cong)
(auto simp: integral_distr Y_def rv_X)
finally show ?eq .
have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))"
unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y]
- by (intro product_integrable_setprod[OF \<open>finite I\<close>])
+ by (intro product_integrable_prod[OF \<open>finite I\<close>])
(simp add: integrable_distr_eq int_Y)
then show ?int
by (simp add: integrable_distr_eq Y_def)
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Mon Oct 17 19:03:13 2016 +0200
@@ -98,7 +98,7 @@
shows "measure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. measure (M i) (X i))"
using emeasure_PiM_emb[OF assms]
unfolding emeasure_eq_measure M.emeasure_eq_measure
- by (simp add: setprod_ennreal measure_nonneg setprod_nonneg)
+ by (simp add: prod_ennreal measure_nonneg prod_nonneg)
lemma sets_Collect_single':
"i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
@@ -151,7 +151,7 @@
have "emeasure (Pi\<^sub>M I M) (prod_emb I M J (Pi\<^sub>E J A)) = emeasure (Pi\<^sub>M I ?M) (P.emb I J (Pi\<^sub>E J A))"
by (auto simp: prod_emb_def PiE_iff intro!: arg_cong2[where f=emeasure] PiM_cong)
also have "\<dots> = (\<Prod>i\<in>J. emeasure (M i) (A i))"
- using J A by (subst P.emeasure_PiM_emb[OF J]) (auto intro!: setprod.cong)
+ using J A by (subst P.emeasure_PiM_emb[OF J]) (auto intro!: prod.cong)
finally show ?thesis .
qed
@@ -173,7 +173,7 @@
have "Pi\<^sub>M (insert i' I) M ?X = (\<Prod>i\<in>J. M i (A i))"
using M J A by (intro emeasure_PiM_emb) auto
also have "\<dots> = M i' (if i' \<in> J then (A i') else space (M i')) * (\<Prod>i\<in>J-{i'}. M i (A i))"
- using setprod.insert_remove[of J "\<lambda>i. M i (A i)" i'] J M'.emeasure_space_1
+ using prod.insert_remove[of J "\<lambda>i. M i (A i)" i'] J M'.emeasure_space_1
by (cases "i' \<in> J") (auto simp: insert_absorb)
also have "(\<Prod>i\<in>J-{i'}. M i (A i)) = Pi\<^sub>M I M (prod_emb I M (J - {i'}) (Pi\<^sub>E (J - {i'}) A))"
using M J A by (intro emeasure_PiM_emb[symmetric]) auto
@@ -205,7 +205,7 @@
have "?I (prod_emb I (\<lambda>i. M (f i)) J (Pi\<^sub>E J A)) = (\<Prod>j\<in>J. M (f j) (A j))"
using f J A by (intro emeasure_PiM_emb M) auto
also have "\<dots> = (\<Prod>j\<in>f`J. M j (A (the_inv_into I f j)))"
- using f J by (subst setprod.reindex) (auto intro!: setprod.cong intro: inj_on_subset simp: the_inv_into_f_f)
+ using f J by (subst prod.reindex) (auto intro!: prod.cong intro: inj_on_subset simp: the_inv_into_f_f)
also have "\<dots> = ?K (prod_emb K M (f`J) (\<Pi>\<^sub>E j\<in>f`J. A (the_inv_into I f j)))"
using f J A by (intro emeasure_PiM_emb[symmetric] M) (auto simp: the_inv_into_f_f)
also have "prod_emb K M (f`J) (\<Pi>\<^sub>E j\<in>f`J. A (the_inv_into I f j)) = ?t -` prod_emb I (\<lambda>i. M (f i)) J (Pi\<^sub>E J A) \<inter> space ?K"
@@ -352,12 +352,12 @@
also have "emeasure S ?F = (\<Prod>j\<in>(op + i) -` J. emeasure M (E (i + j)))"
using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
also have "\<dots> = (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j))"
- by (rule setprod.reindex_cong [of "\<lambda>x. x - i"])
+ by (rule prod.reindex_cong [of "\<lambda>x. x - i"])
(auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
also have "emeasure S ?E = (\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j))"
using J by (intro emeasure_PiM_emb) simp_all
also have "(\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j)) * (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
- by (subst mult.commute) (auto simp: J setprod.subset_diff[symmetric])
+ by (subst mult.commute) (auto simp: J prod.subset_diff[symmetric])
finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
qed simp_all
@@ -383,10 +383,10 @@
also have "emeasure S ?F = (\<Prod>j\<in>Suc -` J. emeasure M (E (Suc j)))"
using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
also have "\<dots> = (\<Prod>j\<in>J - {0}. emeasure M (E j))"
- by (rule setprod.reindex_cong [of "\<lambda>x. x - 1"])
+ by (rule prod.reindex_cong [of "\<lambda>x. x - 1"])
(auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
also have "emeasure M ?E * (\<Prod>j\<in>J - {0}. emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
- by (auto simp: M.emeasure_space_1 setprod.remove J)
+ by (auto simp: M.emeasure_space_1 prod.remove J)
finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
qed simp_all
--- a/src/HOL/Probability/Probability_Measure.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Mon Oct 17 19:03:13 2016 +0200
@@ -485,7 +485,7 @@
sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^sub>M i\<in>I. M i"
proof
show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (space (\<Pi>\<^sub>M i\<in>I. M i)) = 1"
- by (simp add: measure_times M.emeasure_space_1 setprod.neutral_const space_PiM)
+ by (simp add: measure_times M.emeasure_space_1 prod.neutral_const space_PiM)
qed
lemma (in finite_product_prob_space) prob_times:
@@ -497,8 +497,8 @@
also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"
using measure_times X by simp
also have "\<dots> = ennreal (\<Prod>i\<in>I. measure (M i) (X i))"
- using X by (simp add: M.emeasure_eq_measure setprod_ennreal measure_nonneg)
- finally show ?thesis by (simp add: measure_nonneg setprod_nonneg)
+ using X by (simp add: M.emeasure_eq_measure prod_ennreal measure_nonneg)
+ finally show ?thesis by (simp add: measure_nonneg prod_nonneg)
qed
subsection \<open>Distributions\<close>
@@ -1201,8 +1201,8 @@
apply (subst emeasure_distr)
apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
apply (subst emeasure_PiM)
- apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> setprod.reindex[OF \<open>inj_on t J\<close>]
- if_distrib[where f="emeasure (M _)"] setprod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
+ apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> prod.reindex[OF \<open>inj_on t J\<close>]
+ if_distrib[where f="emeasure (M _)"] prod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
done
qed simp
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Mon Oct 17 19:03:13 2016 +0200
@@ -83,7 +83,7 @@
lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
by auto
-lemma setprod_sum_distrib_lists:
+lemma prod_sum_distrib_lists:
fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
shows "(\<Sum>ms\<in>{ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
(\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
@@ -100,7 +100,7 @@
show ?case unfolding *
using Suc[of "\<lambda>i. P (Suc i)"]
by (simp add: sum.reindex split_conv sum_cartesian_product'
- lessThan_Suc_eq_insert_0 setprod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
+ lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
qed
declare space_point_measure[simp]
@@ -169,12 +169,12 @@
case (Suc n)
then show ?case
by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
- sum.reindex setprod.reindex)
+ sum.reindex prod.reindex)
qed
then show "sum P msgs = 1"
unfolding msgs_def P_def by simp
fix x
- have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: setprod_nonneg)
+ have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: prod_nonneg)
then show "0 \<le> P x"
unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
qed auto
@@ -255,8 +255,8 @@
apply (simp add: \<mu>'_eq)
apply (simp add: * P_def)
apply (simp add: sum_cartesian_product')
- using setprod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
- by (auto simp add: sum_distrib_left[symmetric] subset_eq setprod.neutral_const)
+ using prod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
+ by (auto simp add: sum_distrib_left[symmetric] subset_eq prod.neutral_const)
qed
lemma fst_image_msgs[simp]: "fst`msgs = keys"
@@ -352,14 +352,14 @@
(\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
apply (simp add: sum_cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
- apply (subst setprod_sum_distrib_lists[OF M.finite_space]) ..
+ apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
finally have "(\<P>(OB ; fst) {(obs, k)}) / K k =
(\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
note * = this
have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k"
unfolding *[OF obs] *[OF obs']
- using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod.reindex)
+ using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: prod.reindex)
then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
using \<open>K k \<noteq> 0\<close> by auto }
note t_eq_imp = this
--- a/src/HOL/Rat.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Rat.thy Mon Oct 17 19:03:13 2016 +0200
@@ -701,7 +701,7 @@
lemma of_rat_sum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))"
by (induct rule: infinite_finite_induct) (auto simp: of_rat_add)
-lemma of_rat_setprod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"
+lemma of_rat_prod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"
by (induct rule: infinite_finite_induct) (auto simp: of_rat_mult)
lemma nonzero_of_rat_inverse: "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
--- a/src/HOL/Real_Vector_Spaces.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Oct 17 19:03:13 2016 +0200
@@ -319,7 +319,7 @@
lemma of_real_sum[simp]: "of_real (sum f s) = (\<Sum>x\<in>s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
-lemma of_real_setprod[simp]: "of_real (setprod f s) = (\<Prod>x\<in>s. of_real (f x))"
+lemma of_real_prod[simp]: "of_real (prod f s) = (\<Prod>x\<in>s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
lemma nonzero_of_real_inverse:
@@ -501,10 +501,10 @@
then show ?case by (metis Reals_0 sum.infinite)
qed simp_all
-lemma setprod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setprod f s \<in> \<real>"
+lemma prod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> prod f s \<in> \<real>"
proof (induct s rule: infinite_finite_induct)
case infinite
- then show ?case by (metis Reals_1 setprod.infinite)
+ then show ?case by (metis Reals_1 prod.infinite)
qed simp_all
lemma Reals_induct [case_names of_real, induct set: Reals]:
@@ -978,20 +978,20 @@
by simp
qed
-lemma setprod_norm: "setprod (\<lambda>x. norm (f x)) A = norm (setprod f A)"
+lemma prod_norm: "prod (\<lambda>x. norm (f x)) A = norm (prod f A)"
for f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
-lemma norm_setprod_le:
- "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))"
+lemma norm_prod_le:
+ "norm (prod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))"
proof (induct A rule: infinite_finite_induct)
case empty
then show ?case by simp
next
case (insert a A)
- then have "norm (setprod f (insert a A)) \<le> norm (f a) * norm (setprod f A)"
+ then have "norm (prod f (insert a A)) \<le> norm (f a) * norm (prod f A)"
by (simp add: norm_mult_ineq)
- also have "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
+ also have "norm (prod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
by (rule insert)
finally show ?case
by (simp add: insert mult_left_mono)
@@ -1000,7 +1000,7 @@
then show ?case by simp
qed
-lemma norm_setprod_diff:
+lemma norm_prod_diff:
fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
shows "(\<And>i. i \<in> I \<Longrightarrow> norm (z i) \<le> 1) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> norm (w i) \<le> 1) \<Longrightarrow>
norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
@@ -1020,9 +1020,9 @@
also have "norm ?t1 \<le> norm (\<Prod>i\<in>I. z i) * norm (z i - w i)"
by (rule norm_mult_ineq)
also have "\<dots> \<le> (\<Prod>i\<in>I. norm (z i)) * norm(z i - w i)"
- by (rule mult_right_mono) (auto intro: norm_setprod_le)
+ by (rule mult_right_mono) (auto intro: norm_prod_le)
also have "(\<Prod>i\<in>I. norm (z i)) \<le> (\<Prod>i\<in>I. 1)"
- by (intro setprod_mono) (auto intro!: insert)
+ by (intro prod_mono) (auto intro!: insert)
also have "norm ?t2 \<le> norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * norm (w i)"
by (rule norm_mult_ineq)
also have "norm (w i) \<le> 1"
@@ -1042,9 +1042,9 @@
shows "norm (z^m - w^m) \<le> m * norm (z - w)"
proof -
have "norm (z^m - w^m) = norm ((\<Prod> i < m. z) - (\<Prod> i < m. w))"
- by (simp add: setprod_constant)
+ by (simp add: prod_constant)
also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
- by (intro norm_setprod_diff) (auto simp add: assms)
+ by (intro norm_prod_diff) (auto simp add: assms)
also have "\<dots> = m * norm (z - w)"
by simp
finally show ?thesis .
--- a/src/HOL/Set_Interval.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Set_Interval.thy Mon Oct 17 19:03:13 2016 +0200
@@ -2018,41 +2018,41 @@
subsection \<open>Products indexed over intervals\<close>
syntax (ASCII)
- "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
- "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
syntax (latex_prod output)
- "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
- "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
- "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
- "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
syntax
- "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
- "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
translations
- "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..b}"
- "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..<b}"
- "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..n}"
- "\<Prod>i<n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..<n}"
-
-lemma setprod_int_plus_eq: "setprod int {i..i+j} = \<Prod>{int i..int (i+j)}"
+ "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}"
+ "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}"
+ "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}"
+ "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}"
+
+lemma prod_int_plus_eq: "prod int {i..i+j} = \<Prod>{int i..int (i+j)}"
by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
-lemma setprod_int_eq: "setprod int {i..j} = \<Prod>{int i..int j}"
+lemma prod_int_eq: "prod int {i..j} = \<Prod>{int i..int j}"
proof (cases "i \<le> j")
case True
then show ?thesis
- by (metis le_iff_add setprod_int_plus_eq)
+ by (metis le_iff_add prod_int_plus_eq)
next
case False
then show ?thesis
@@ -2062,37 +2062,37 @@
subsubsection \<open>Shifting bounds\<close>
-lemma setprod_shift_bounds_nat_ivl:
- "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
+lemma prod_shift_bounds_nat_ivl:
+ "prod f {m+k..<n+k} = prod (%i. f(i + k)){m..<n::nat}"
by (induct "n", auto simp:atLeastLessThanSuc)
-lemma setprod_shift_bounds_cl_nat_ivl:
- "setprod f {m+k..n+k} = setprod (%i. f(i + k)){m..n::nat}"
- by (rule setprod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
-
-corollary setprod_shift_bounds_cl_Suc_ivl:
- "setprod f {Suc m..Suc n} = setprod (%i. f(Suc i)){m..n}"
-by (simp add:setprod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
-
-corollary setprod_shift_bounds_Suc_ivl:
- "setprod f {Suc m..<Suc n} = setprod (%i. f(Suc i)){m..<n}"
-by (simp add:setprod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-
-lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
+lemma prod_shift_bounds_cl_nat_ivl:
+ "prod f {m+k..n+k} = prod (%i. f(i + k)){m..n::nat}"
+ by (rule prod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
+
+corollary prod_shift_bounds_cl_Suc_ivl:
+ "prod f {Suc m..Suc n} = prod (%i. f(Suc i)){m..n}"
+by (simp add:prod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+
+corollary prod_shift_bounds_Suc_ivl:
+ "prod f {Suc m..<Suc n} = prod (%i. f(Suc i)){m..<n}"
+by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
+
+lemma prod_lessThan_Suc: "prod f {..<Suc n} = prod f {..<n} * f n"
by (simp add: lessThan_Suc mult.commute)
-lemma setprod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
+lemma prod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
by (induction n) (simp_all add: lessThan_Suc mult_ac)
-lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
+lemma prod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> prod f {a..<Suc b} = prod f {a..<b} * f b"
by (simp add: atLeastLessThanSuc mult.commute)
-lemma setprod_nat_ivl_Suc':
+lemma prod_nat_ivl_Suc':
assumes "m \<le> Suc n"
- shows "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"
+ shows "prod f {m..Suc n} = f (Suc n) * prod f {m..n}"
proof -
from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
- also have "setprod f \<dots> = f (Suc n) * setprod f {m..n}" by simp
+ also have "prod f \<dots> = f (Suc n) * prod f {m..n}" by simp
finally show ?thesis .
qed
@@ -2133,13 +2133,13 @@
by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def)
qed
-lemma setprod_atLeastAtMost_code:
- "setprod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
+lemma prod_atLeastAtMost_code:
+ "prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
proof -
have "comp_fun_commute (\<lambda>a. op * (f a))"
by unfold_locales (auto simp: o_def mult_ac)
thus ?thesis
- by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
+ by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
qed
(* TODO: Add support for more kinds of intervals here *)
--- a/src/HOL/Transcendental.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/Transcendental.thy Mon Oct 17 19:03:13 2016 +0200
@@ -35,7 +35,7 @@
by (metis of_nat_fact of_real_of_nat_eq)
lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
- by (simp add: pochhammer_setprod)
+ by (simp add: pochhammer_prod)
lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n"
proof -
@@ -1522,7 +1522,7 @@
corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
by (simp add: exp_of_nat_mult)
-lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = setprod (\<lambda>x. exp (f x)) I"
+lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
lemma exp_divide_power_eq:
@@ -1744,9 +1744,9 @@
for x :: real
by (rule ln_unique) (simp add: exp_add)
-lemma ln_setprod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i > 0) \<Longrightarrow> ln (setprod f I) = sum (\<lambda>x. ln(f x)) I"
+lemma ln_prod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i > 0) \<Longrightarrow> ln (prod f I) = sum (\<lambda>x. ln(f x)) I"
for f :: "'a \<Rightarrow> real"
- by (induct I rule: finite_induct) (auto simp: ln_mult setprod_pos)
+ by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
for x :: real
--- a/src/HOL/ex/Birthday_Paradox.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/ex/Birthday_Paradox.thy Mon Oct 17 19:03:13 2016 +0200
@@ -64,11 +64,11 @@
by (auto intro!: finite_PiE)
have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
from assms this finite subset show ?thesis
- by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
+ by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on prod_constant)
qed
-lemma setprod_upto_nat_unfold:
- "setprod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * setprod f {m..(n - 1)}))"
+lemma prod_upto_nat_unfold:
+ "prod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * prod f {m..(n - 1)}))"
by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
section \<open>Birthday paradox\<close>
@@ -81,7 +81,7 @@
from assms show ?thesis
using card_PiE[OF \<open>finite S\<close>, of "\<lambda>i. T"] \<open>finite S\<close>
card_extensional_funcset_not_inj_on[OF \<open>finite S\<close> \<open>finite T\<close> \<open>card S <= card T\<close>]
- by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
+ by (simp add: fact_div_fact prod_upto_nat_unfold prod_constant)
qed
end
--- a/src/HOL/ex/Sum_of_Powers.thy Mon Oct 17 18:41:46 2016 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy Mon Oct 17 19:03:13 2016 +0200
@@ -23,8 +23,8 @@
next
case (Suc l)
have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
- using setprod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
- by (simp add: ac_simps setprod.atLeast0_lessThan_Suc_shift)
+ using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
+ by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift)
also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
@@ -32,7 +32,7 @@
finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
by (simp add: field_simps)
with assms show ?thesis
- by (simp add: binomial_altdef_of_nat setprod_dividef)
+ by (simp add: binomial_altdef_of_nat prod_dividef)
qed
lemma real_binomial_eq_mult_binomial_Suc: