# HG changeset patch
# User nipkow
# Date 1572980142 -3600
# Node ID 2fab72ab919aaf12a8b938e53ae1f72d6e1a5156
# Parent  fdb6c5034c24c7d367ff718e15369c702eb5ddbd
moved duplicate lemmas up the hierarchy

diff -r fdb6c5034c24 -r 2fab72ab919a src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Nov 05 19:55:42 2019 +0100
@@ -22,95 +22,6 @@
   using openI by auto
 
 
-subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
-  fixes x :: real
-  assumes "-1 \<le> x"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
-    by (simp add: algebra_simps)
-  also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
-  also have "... \<le> (1 + x) ^ Suc n"
-    using Suc.hyps assms mult_left_mono by fastforce
-  finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
-  fixes x :: real
-  assumes "even n"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
-  case True
-  then show ?thesis
-    by (auto simp: Bernoulli_inequality)
-next
-  case False
-  then have "real n \<ge> 1"
-    by simp
-  with False have "n * x \<le> -1"
-    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
-  then have "1 + n * x \<le> 0"
-    by auto
-  also have "... \<le> (1 + x) ^ n"
-    using assms
-    using zero_le_even_power by blast
-  finally show ?thesis .
-qed
-
-corollary real_arch_pow:
-  fixes x :: real
-  assumes x: "1 < x"
-  shows "\<exists>n. y < x^n"
-proof -
-  from x have x0: "x - 1 > 0"
-    by arith
-  from reals_Archimedean3[OF x0, rule_format, of y]
-  obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> -1" by arith
-  from Bernoulli_inequality[OF x00, of n] n
-  have "y < x^n" by auto
-  then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
-  fixes x y :: real
-  assumes y: "y > 0"
-    and x1: "x < 1"
-  shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
-  case True
-  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
-  from real_arch_pow[OF ix, of "1/y"]
-  obtain n where n: "1/y < (1/x)^n" by blast
-  then show ?thesis using y \<open>x > 0\<close>
-    by (auto simp add: field_simps)
-next
-  case False
-  with y x1 show ?thesis
-    by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
-  by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
-
 subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>
 
 lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
diff -r fdb6c5034c24 -r 2fab72ab919a src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 19:55:42 2019 +0100
@@ -490,96 +490,6 @@
   by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
 
 
-subsection \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
-  fixes x :: real
-  assumes "-1 \<le> x"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
-    by (simp add: algebra_simps)
-  also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
-  also have "... \<le> (1 + x) ^ Suc n"
-    using Suc.hyps assms mult_left_mono by fastforce
-  finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
-  fixes x :: real
-  assumes "even n"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
-  case True
-  then show ?thesis
-    by (auto simp: Bernoulli_inequality)
-next
-  case False
-  then have "real n \<ge> 1"
-    by simp
-  with False have "n * x \<le> -1"
-    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
-  then have "1 + n * x \<le> 0"
-    by auto
-  also have "... \<le> (1 + x) ^ n"
-    using assms
-    using zero_le_even_power by blast
-  finally show ?thesis .
-qed
-
-corollary real_arch_pow:
-  fixes x :: real
-  assumes x: "1 < x"
-  shows "\<exists>n. y < x^n"
-proof -
-  from x have x0: "x - 1 > 0"
-    by arith
-  from reals_Archimedean3[OF x0, rule_format, of y]
-  obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> -1" by arith
-  from Bernoulli_inequality[OF x00, of n] n
-  have "y < x^n" by auto
-  then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
-  fixes x y :: real
-  assumes y: "y > 0"
-    and x1: "x < 1"
-  shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
-  case True
-  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
-  from real_arch_pow[OF ix, of "1/y"]
-  obtain n where n: "1/y < (1/x)^n" by blast
-  then show ?thesis using y \<open>x > 0\<close>
-    by (auto simp add: field_simps)
-next
-  case False
-  with y x1 show ?thesis
-    by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
-  by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
-
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Euclidean Spaces as Typeclass\<close>
 
 lemma independent_Basis: "independent Basis"
diff -r fdb6c5034c24 -r 2fab72ab919a src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 05 19:15:00 2019 +0100
+++ b/src/HOL/Real.thy	Tue Nov 05 19:55:42 2019 +0100
@@ -1313,6 +1313,96 @@
   by simp
 
 
+subsection \<open>Archimedean properties and useful consequences\<close>
+
+text\<open>Bernoulli's inequality\<close>
+proposition Bernoulli_inequality:
+  fixes x :: real
+  assumes "-1 \<le> x"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+    by (simp add: algebra_simps)
+  also have "... = (1 + x) * (1 + n*x)"
+    by (auto simp: power2_eq_square algebra_simps)
+  also have "... \<le> (1 + x) ^ Suc n"
+    using Suc.hyps assms mult_left_mono by fastforce
+  finally show ?case .
+qed
+
+corollary Bernoulli_inequality_even:
+  fixes x :: real
+  assumes "even n"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+  case True
+  then show ?thesis
+    by (auto simp: Bernoulli_inequality)
+next
+  case False
+  then have "real n \<ge> 1"
+    by simp
+  with False have "n * x \<le> -1"
+    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+  then have "1 + n * x \<le> 0"
+    by auto
+  also have "... \<le> (1 + x) ^ n"
+    using assms
+    using zero_le_even_power by blast
+  finally show ?thesis .
+qed
+
+corollary real_arch_pow:
+  fixes x :: real
+  assumes x: "1 < x"
+  shows "\<exists>n. y < x^n"
+proof -
+  from x have x0: "x - 1 > 0"
+    by arith
+  from reals_Archimedean3[OF x0, rule_format, of y]
+  obtain n :: nat where n: "y < real n * (x - 1)" by metis
+  from x0 have x00: "x- 1 \<ge> -1" by arith
+  from Bernoulli_inequality[OF x00, of n] n
+  have "y < x^n" by auto
+  then show ?thesis by metis
+qed
+
+corollary real_arch_pow_inv:
+  fixes x y :: real
+  assumes y: "y > 0"
+    and x1: "x < 1"
+  shows "\<exists>n. x^n < y"
+proof (cases "x > 0")
+  case True
+  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
+  from real_arch_pow[OF ix, of "1/y"]
+  obtain n where n: "1/y < (1/x)^n" by blast
+  then show ?thesis using y \<open>x > 0\<close>
+    by (auto simp add: field_simps)
+next
+  case False
+  with y x1 show ?thesis
+    by (metis less_le_trans not_less power_one_right)
+qed
+
+lemma forall_pos_mono:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
+  by (metis real_arch_inverse)
+
+lemma forall_pos_mono_1:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+  apply (rule forall_pos_mono)
+  apply auto
+  apply (metis Suc_pred of_nat_Suc)
+  done
+
+
 subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
 
 (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)