# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493818744 -3600
# Node ID a68973661472906aa2ccac37bf5a98c26698cf7a
# Parent  4a762cad298fe246be80e3abbee0a2dc3cb25639
two new theorems

diff -r 4a762cad298f -r a68973661472 src/HOL/Groups_Big.thy
--- 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
 
diff -r 4a762cad298f -r a68973661472 src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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