author paulson Wed, 03 May 2017 14:39:04 +0100 changeset 65687 a68973661472 parent 65686 4a762cad298f child 65711 ff8a7f20ff32
two new theorems
```--- 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```