--- a/src/HOL/Groups_Big.thy Tue May 02 18:27:51 2017 +0200
+++ b/src/HOL/Groups_Big.thy Wed May 03 14:39:04 2017 +0100
@@ -1116,6 +1116,41 @@
subsubsection \<open>Properties in more restricted classes of structures\<close>
+context linordered_nonzero_semiring
+begin
+
+lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A"
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
+next
+ case empty
+ then show ?case by simp
+next
+ case (insert x F)
+ have "1 * 1 \<le> f x * prod f F"
+ by (rule mult_mono') (use insert in auto)
+ with insert show ?case by simp
+qed
+
+lemma prod_le_1:
+ fixes f :: "'b \<Rightarrow> 'a"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1"
+ shows "prod f A \<le> 1"
+ using assms
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
+next
+ case empty
+ then show ?case by simp
+next
+ case (insert x F)
+ then show ?case by (force simp: mult.commute intro: dest: mult_le_one)
+qed
+
+end
+
context comm_semiring_1
begin
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue May 02 18:27:51 2017 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed May 03 14:39:04 2017 +0100
@@ -181,16 +181,17 @@
by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
qed
+(*These generalise their counterparts in Nat.linordered_semidom_class*)
lemma of_nat_less[simp]:
- "i < j \<Longrightarrow> of_nat i < (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0})"
+ "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
by (auto simp: less_le)
lemma of_nat_le_iff[simp]:
- "of_nat i \<le> (of_nat j::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> i \<le> j"
+ "of_nat m \<le> (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> m \<le> n"
proof (safe intro!: of_nat_mono)
- assume "of_nat i \<le> (of_nat j::'a)" then show "i \<le> j"
+ assume "of_nat m \<le> (of_nat n::'a)" then show "m \<le> n"
proof (intro leI notI)
- assume "j < i" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat i \<le> of_nat j\<close>] show False
+ assume "n < m" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat m \<le> of_nat n\<close>] show False
by blast
qed
qed