# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1458050905 0
# Node ID dbc62f86a1a9b95b7094d00f7581bd16a6cd03f8
# Parent  7c56e4a1ad0c160e0b9c9b314790823584405274
rationalisation of theorem names esp about "real Archimedian" etc.

diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Archimedean_Field.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -31,7 +31,7 @@
   then show ?thesis ..
 qed
 
-lemma ex_less_of_nat:
+lemma reals_Archimedean2:
   fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n"
 proof -
   obtain z where "x < of_int z" using ex_less_of_int ..
@@ -40,24 +40,24 @@
   finally show ?thesis ..
 qed
 
-lemma ex_le_of_nat:
+lemma real_arch_simple:
   fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n"
 proof -
-  obtain n where "x < of_nat n" using ex_less_of_nat ..
+  obtain n where "x < of_nat n" using reals_Archimedean2 ..
   then have "x \<le> of_nat n" by simp
   then show ?thesis ..
 qed
 
 text \<open>Archimedean fields have no infinitesimal elements.\<close>
 
-lemma ex_inverse_of_nat_Suc_less:
+lemma reals_Archimedean:
   fixes x :: "'a::archimedean_field"
   assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x"
 proof -
   from \<open>0 < x\<close> have "0 < inverse x"
     by (rule positive_imp_inverse_positive)
   obtain n where "inverse x < of_nat n"
-    using ex_less_of_nat ..
+    using reals_Archimedean2 ..
   then obtain m where "inverse x < of_nat (Suc m)"
     using \<open>0 < inverse x\<close> by (cases n) (simp_all del: of_nat_Suc)
   then have "inverse (of_nat (Suc m)) < inverse (inverse x)"
@@ -70,13 +70,13 @@
 lemma ex_inverse_of_nat_less:
   fixes x :: "'a::archimedean_field"
   assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x"
-  using ex_inverse_of_nat_Suc_less [OF \<open>0 < x\<close>] by auto
+  using reals_Archimedean [OF \<open>0 < x\<close>] by auto
 
 lemma ex_less_of_nat_mult:
   fixes x :: "'a::archimedean_field"
   assumes "0 < x" shows "\<exists>n. y < of_nat n * x"
 proof -
-  obtain n where "y / x < of_nat n" using ex_less_of_nat ..
+  obtain n where "y / x < of_nat n" using reals_Archimedean2 ..
   with \<open>0 < x\<close> have "y < of_nat n * x" by (simp add: pos_divide_less_eq)
   then show ?thesis ..
 qed
@@ -105,7 +105,7 @@
   assume "0 \<le> x"
   then have "\<not> x < of_nat 0" by simp
   then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
-    using ex_less_of_nat by (rule exists_least_lemma)
+    using reals_Archimedean2 by (rule exists_least_lemma)
   then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
   then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp
   then show ?thesis ..
@@ -113,7 +113,7 @@
   assume "\<not> 0 \<le> x"
   then have "\<not> - x \<le> of_nat 0" by simp
   then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
-    using ex_le_of_nat by (rule exists_least_lemma)
+    using real_arch_simple by (rule exists_least_lemma)
   then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
   then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp
   then show ?thesis ..
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -613,7 +613,7 @@
   then obtain r where "y = ennreal r"
     by (cases y rule: ennreal_cases) auto
   then show "\<exists>i\<in>UNIV. y < of_nat i"
-    using ex_less_of_nat[of "max 1 r"] zero_less_one
+    using reals_Archimedean2[of "max 1 r"] zero_less_one
     by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
              dest!: one_less_of_natD intro: less_trans)
 qed
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -600,7 +600,7 @@
   by (metis closed_path_image valid_path_imp_path)
 
 proposition valid_path_compose:
-  assumes "valid_path g" 
+  assumes "valid_path g"
       and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
       and con: "continuous_on (path_image g) (deriv f)"
     shows "valid_path (f o g)"
@@ -609,7 +609,7 @@
     using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
   have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
     proof (rule differentiable_chain_at)
-      show "g differentiable at t" using `valid_path g` 
+      show "g differentiable at t" using `valid_path g`
         by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
@@ -625,11 +625,11 @@
       show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
         using g_diff C1_differentiable_on_eq by auto
     next
-      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))" 
-        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] 
-          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def 
+      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
+        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
+          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def
         by blast
-      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))" 
+      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
         using continuous_on_subset by blast
     next
       show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
@@ -645,11 +645,11 @@
     qed
   ultimately have "f o g C1_differentiable_on {0..1} - s"
     using C1_differentiable_on_eq by blast
-  moreover have "path (f o g)" 
+  moreover have "path (f o g)"
     proof -
-      have "isCont f x" when "x\<in>path_image g" for x 
+      have "isCont f x" when "x\<in>path_image g" for x
         proof -
-          obtain f' where "(f has_field_derivative f') (at x)" 
+          obtain f' where "(f has_field_derivative f') (at x)"
             using der[rule_format] `x\<in>path_image g` by auto
           thus ?thesis using DERIV_isCont by auto
         qed
@@ -2236,7 +2236,8 @@
     have ?thesis
       using holomorphic_point_small_triangle [OF xin contf fx, of "e/10"] e
       apply clarsimp
-      apply (rule_tac x1="K/k" in exE [OF real_arch_pow2], blast)
+      apply (rule_tac y1="K/k" in exE [OF real_arch_pow[of 2]])
+      apply force+
       done
   }
   moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
@@ -3012,7 +3013,7 @@
     unfolding uniformly_continuous_on_def dist_norm real_norm_def
     by (metis divide_pos_pos enz zero_less_numeral)
   then obtain N::nat where N: "N>0" "inverse N < d"
-    using real_arch_inv [of d]   by auto
+    using real_arch_inverse [of d]   by auto
   { fix g h
     assume g: "valid_path g" and gp: "\<forall>t\<in>{0..1}. cmod (g t - p t) < e / 3"
        and h: "valid_path h" and hp: "\<forall>t\<in>{0..1}. cmod (h t - p t) < e / 3"
@@ -5732,11 +5733,11 @@
 proof (rule valid_path_compose[OF `valid_path g`])
   fix x assume "x \<in> path_image g"
   then show "\<exists>f'. (f has_field_derivative f') (at x)"
-    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto 
+    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto
 next
   have "deriv f holomorphic_on s"
     using holomorphic_deriv holo `open s` by auto
-  then show "continuous_on (path_image g) (deriv f)" 
+  then show "continuous_on (path_image g) (deriv f)"
     using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
 qed
 
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -82,7 +82,7 @@
 
 lemma real_arch_invD:
   "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
-  by (subst(asm) real_arch_inv)
+  by (subst(asm) real_arch_inverse)
 
 
 subsection \<open>Sundries\<close>
@@ -2109,7 +2109,7 @@
     if e: "0 < e" for e
   proof -
     obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
-      using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
+      using real_arch_pow[of 2 "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
     show ?thesis
     proof (rule exI [where x=n], clarify)
       fix x y
@@ -2947,7 +2947,7 @@
   have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
   proof (rule CauchyI, goal_cases)
     case (1 e)
-    then guess N unfolding real_arch_inv[of e] .. note N=this
+    then guess N unfolding real_arch_inverse[of e] .. note N=this
     show ?case
       apply (rule_tac x=N in exI)
     proof clarify
@@ -2967,7 +2967,7 @@
     fix e :: real
     assume "e>0"
     then have *:"e/2 > 0" by auto
-    then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this
+    then guess N1 unfolding real_arch_inverse[of "e/2"] .. note N1=this
     then have N1': "N1 = N1 - 1 + 1"
       by auto
     guess N2 using y[OF *] .. note N2=this
@@ -4620,7 +4620,7 @@
       using True by (auto simp add: field_simps)
     then obtain M :: nat
          where M: "M \<noteq> 0" "0 < inverse (real_of_nat M)" "inverse (of_nat M) < e / 4 / content (cbox a b)"
-      by (subst (asm) real_arch_inv) auto
+      by (subst (asm) real_arch_inverse) auto
     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e"
     proof (rule exI [where x=M], clarify)
       fix m n
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -581,15 +581,8 @@
 
 subsection \<open>Archimedean properties and useful consequences\<close>
 
-lemma real_arch_simple: "\<exists>n::nat. x \<le> real n"
-  by (rule ex_le_of_nat)
-
-lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
-  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
-  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
-
 text\<open>Bernoulli's inequality\<close>
-lemma Bernoulli_inequality:
+proposition Bernoulli_inequality:
   fixes x :: real
   assumes "-1 \<le> x"
     shows "1 + n * x \<le> (1 + x) ^ n"
@@ -607,7 +600,7 @@
   finally show ?case .
 qed
 
-lemma Bernoulli_inequality_even:
+corollary Bernoulli_inequality_even:
   fixes x :: real
   assumes "even n"
     shows "1 + n * x \<le> (1 + x) ^ n"
@@ -629,7 +622,7 @@
   finally show ?thesis .
 qed
 
-lemma real_arch_pow:
+corollary real_arch_pow:
   fixes x :: real
   assumes x: "1 < x"
   shows "\<exists>n. y < x^n"
@@ -644,12 +637,7 @@
   then show ?thesis by metis
 qed
 
-lemma real_arch_pow2:
-  fixes x :: real
-  shows "\<exists>n. x < 2^ n"
-  using real_arch_pow[of 2 x] by simp
-
-lemma real_arch_pow_inv:
+corollary real_arch_pow_inv:
   fixes x y :: real
   assumes y: "y > 0"
     and x1: "x < 1"
@@ -673,7 +661,7 @@
 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_inv)
+  by (metis real_arch_inverse)
 
 lemma forall_pos_mono_1:
   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -5525,7 +5525,7 @@
       fix e :: real
       assume "e > 0"
       then obtain N :: nat where "N \<noteq> 0" and N: "0 < inverse (real N) \<and> inverse (real N) < e"
-        unfolding real_arch_inv[of e] by auto
+        unfolding real_arch_inverse[of e] by auto
       {
         fix n :: nat
         assume "n \<ge> N"
@@ -7492,7 +7492,7 @@
         fix e :: real
         assume "e > 0"
         then have "\<exists>N::nat. inverse (real (N + 1)) < e"
-          using real_arch_inv[of e]
+          using real_arch_inverse[of e]
           apply (auto simp add: Suc_pred')
           apply (metis Suc_pred' of_nat_Suc)
           done
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -725,7 +725,7 @@
   { fix e::real
     assume e: "0 < e"
     then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
-      by (auto simp: real_arch_inv [of e])
+      by (auto simp: real_arch_inverse [of e])
     { fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real"
       assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
       assume x: "x \<in> s"
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -270,7 +270,7 @@
     proof (rule ccontr)
       assume "\<not> 0 \<le> ?d B"
       hence "0 < - ?d B" by auto
-      from ex_inverse_of_nat_Suc_less[OF this]
+      from reals_Archimedean[OF this]
       obtain n where *: "?d B < - 1 / real (Suc n)"
         by (auto simp: field_simps)
       also have "\<dots> \<le> - 1 / real (Suc (Suc n))"
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Real.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -1135,8 +1135,9 @@
 
 subsection \<open>The Archimedean Property of the Reals\<close>
 
-lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less  (*FIXME*)
-lemmas reals_Archimedean2 = ex_less_of_nat
+lemma real_arch_inverse: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
+  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
+  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
 
 lemma reals_Archimedean3:
   assumes x_greater_zero: "0 < x"
diff -r 7c56e4a1ad0c -r dbc62f86a1a9 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 14:08:25 2016 +0000
@@ -2143,7 +2143,7 @@
     by (auto simp: lim_sequentially dist_real_def)
   { fix x :: real
     obtain n where "x \<le> real_of_nat n"
-      using ex_le_of_nat[of x] ..
+      using real_arch_simple[of x] ..
     note monoD[OF mono this]
     also have "f (real_of_nat n) \<le> y"
       by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])