rationalisation of theorem names esp about "real Archimedian" etc.
authorpaulson <lp15@cam.ac.uk>
Tue Mar 15 14:08:25 2016 +0000 (2016-03-15)
changeset 62623dbc62f86a1a9
parent 62622 7c56e4a1ad0c
child 62624 59ceeb6f3079
child 62626 de25474ce728
rationalisation of theorem names esp about "real Archimedian" etc.
src/HOL/Archimedean_Field.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Weierstrass.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Tue Mar 15 08:34:04 2016 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Mar 15 14:08:25 2016 +0000
     1.3 @@ -31,7 +31,7 @@
     1.4    then show ?thesis ..
     1.5  qed
     1.6  
     1.7 -lemma ex_less_of_nat:
     1.8 +lemma reals_Archimedean2:
     1.9    fixes x :: "'a::archimedean_field" shows "\<exists>n. x < of_nat n"
    1.10  proof -
    1.11    obtain z where "x < of_int z" using ex_less_of_int ..
    1.12 @@ -40,24 +40,24 @@
    1.13    finally show ?thesis ..
    1.14  qed
    1.15  
    1.16 -lemma ex_le_of_nat:
    1.17 +lemma real_arch_simple:
    1.18    fixes x :: "'a::archimedean_field" shows "\<exists>n. x \<le> of_nat n"
    1.19  proof -
    1.20 -  obtain n where "x < of_nat n" using ex_less_of_nat ..
    1.21 +  obtain n where "x < of_nat n" using reals_Archimedean2 ..
    1.22    then have "x \<le> of_nat n" by simp
    1.23    then show ?thesis ..
    1.24  qed
    1.25  
    1.26  text \<open>Archimedean fields have no infinitesimal elements.\<close>
    1.27  
    1.28 -lemma ex_inverse_of_nat_Suc_less:
    1.29 +lemma reals_Archimedean:
    1.30    fixes x :: "'a::archimedean_field"
    1.31    assumes "0 < x" shows "\<exists>n. inverse (of_nat (Suc n)) < x"
    1.32  proof -
    1.33    from \<open>0 < x\<close> have "0 < inverse x"
    1.34      by (rule positive_imp_inverse_positive)
    1.35    obtain n where "inverse x < of_nat n"
    1.36 -    using ex_less_of_nat ..
    1.37 +    using reals_Archimedean2 ..
    1.38    then obtain m where "inverse x < of_nat (Suc m)"
    1.39      using \<open>0 < inverse x\<close> by (cases n) (simp_all del: of_nat_Suc)
    1.40    then have "inverse (of_nat (Suc m)) < inverse (inverse x)"
    1.41 @@ -70,13 +70,13 @@
    1.42  lemma ex_inverse_of_nat_less:
    1.43    fixes x :: "'a::archimedean_field"
    1.44    assumes "0 < x" shows "\<exists>n>0. inverse (of_nat n) < x"
    1.45 -  using ex_inverse_of_nat_Suc_less [OF \<open>0 < x\<close>] by auto
    1.46 +  using reals_Archimedean [OF \<open>0 < x\<close>] by auto
    1.47  
    1.48  lemma ex_less_of_nat_mult:
    1.49    fixes x :: "'a::archimedean_field"
    1.50    assumes "0 < x" shows "\<exists>n. y < of_nat n * x"
    1.51  proof -
    1.52 -  obtain n where "y / x < of_nat n" using ex_less_of_nat ..
    1.53 +  obtain n where "y / x < of_nat n" using reals_Archimedean2 ..
    1.54    with \<open>0 < x\<close> have "y < of_nat n * x" by (simp add: pos_divide_less_eq)
    1.55    then show ?thesis ..
    1.56  qed
    1.57 @@ -105,7 +105,7 @@
    1.58    assume "0 \<le> x"
    1.59    then have "\<not> x < of_nat 0" by simp
    1.60    then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
    1.61 -    using ex_less_of_nat by (rule exists_least_lemma)
    1.62 +    using reals_Archimedean2 by (rule exists_least_lemma)
    1.63    then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
    1.64    then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)" by simp
    1.65    then show ?thesis ..
    1.66 @@ -113,7 +113,7 @@
    1.67    assume "\<not> 0 \<le> x"
    1.68    then have "\<not> - x \<le> of_nat 0" by simp
    1.69    then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
    1.70 -    using ex_le_of_nat by (rule exists_least_lemma)
    1.71 +    using real_arch_simple by (rule exists_least_lemma)
    1.72    then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
    1.73    then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)" by simp
    1.74    then show ?thesis ..
     2.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Mar 15 08:34:04 2016 +0100
     2.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Mar 15 14:08:25 2016 +0000
     2.3 @@ -613,7 +613,7 @@
     2.4    then obtain r where "y = ennreal r"
     2.5      by (cases y rule: ennreal_cases) auto
     2.6    then show "\<exists>i\<in>UNIV. y < of_nat i"
     2.7 -    using ex_less_of_nat[of "max 1 r"] zero_less_one
     2.8 +    using reals_Archimedean2[of "max 1 r"] zero_less_one
     2.9      by (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_def less_ennreal.abs_eq eq_onp_def max.absorb2
    2.10               dest!: one_less_of_natD intro: less_trans)
    2.11  qed
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 08:34:04 2016 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 14:08:25 2016 +0000
     3.3 @@ -600,7 +600,7 @@
     3.4    by (metis closed_path_image valid_path_imp_path)
     3.5  
     3.6  proposition valid_path_compose:
     3.7 -  assumes "valid_path g" 
     3.8 +  assumes "valid_path g"
     3.9        and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
    3.10        and con: "continuous_on (path_image g) (deriv f)"
    3.11      shows "valid_path (f o g)"
    3.12 @@ -609,7 +609,7 @@
    3.13      using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
    3.14    have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
    3.15      proof (rule differentiable_chain_at)
    3.16 -      show "g differentiable at t" using `valid_path g` 
    3.17 +      show "g differentiable at t" using `valid_path g`
    3.18          by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
    3.19      next
    3.20        have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
    3.21 @@ -625,11 +625,11 @@
    3.22        show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
    3.23          using g_diff C1_differentiable_on_eq by auto
    3.24      next
    3.25 -      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))" 
    3.26 -        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] 
    3.27 -          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def 
    3.28 +      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
    3.29 +        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
    3.30 +          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def
    3.31          by blast
    3.32 -      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))" 
    3.33 +      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
    3.34          using continuous_on_subset by blast
    3.35      next
    3.36        show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
    3.37 @@ -645,11 +645,11 @@
    3.38      qed
    3.39    ultimately have "f o g C1_differentiable_on {0..1} - s"
    3.40      using C1_differentiable_on_eq by blast
    3.41 -  moreover have "path (f o g)" 
    3.42 +  moreover have "path (f o g)"
    3.43      proof -
    3.44 -      have "isCont f x" when "x\<in>path_image g" for x 
    3.45 +      have "isCont f x" when "x\<in>path_image g" for x
    3.46          proof -
    3.47 -          obtain f' where "(f has_field_derivative f') (at x)" 
    3.48 +          obtain f' where "(f has_field_derivative f') (at x)"
    3.49              using der[rule_format] `x\<in>path_image g` by auto
    3.50            thus ?thesis using DERIV_isCont by auto
    3.51          qed
    3.52 @@ -2236,7 +2236,8 @@
    3.53      have ?thesis
    3.54        using holomorphic_point_small_triangle [OF xin contf fx, of "e/10"] e
    3.55        apply clarsimp
    3.56 -      apply (rule_tac x1="K/k" in exE [OF real_arch_pow2], blast)
    3.57 +      apply (rule_tac y1="K/k" in exE [OF real_arch_pow[of 2]])
    3.58 +      apply force+
    3.59        done
    3.60    }
    3.61    moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
    3.62 @@ -3012,7 +3013,7 @@
    3.63      unfolding uniformly_continuous_on_def dist_norm real_norm_def
    3.64      by (metis divide_pos_pos enz zero_less_numeral)
    3.65    then obtain N::nat where N: "N>0" "inverse N < d"
    3.66 -    using real_arch_inv [of d]   by auto
    3.67 +    using real_arch_inverse [of d]   by auto
    3.68    { fix g h
    3.69      assume g: "valid_path g" and gp: "\<forall>t\<in>{0..1}. cmod (g t - p t) < e / 3"
    3.70         and h: "valid_path h" and hp: "\<forall>t\<in>{0..1}. cmod (h t - p t) < e / 3"
    3.71 @@ -5732,11 +5733,11 @@
    3.72  proof (rule valid_path_compose[OF `valid_path g`])
    3.73    fix x assume "x \<in> path_image g"
    3.74    then show "\<exists>f'. (f has_field_derivative f') (at x)"
    3.75 -    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto 
    3.76 +    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto
    3.77  next
    3.78    have "deriv f holomorphic_on s"
    3.79      using holomorphic_deriv holo `open s` by auto
    3.80 -  then show "continuous_on (path_image g) (deriv f)" 
    3.81 +  then show "continuous_on (path_image g) (deriv f)"
    3.82      using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
    3.83  qed
    3.84  
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 08:34:04 2016 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 14:08:25 2016 +0000
     4.3 @@ -82,7 +82,7 @@
     4.4  
     4.5  lemma real_arch_invD:
     4.6    "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
     4.7 -  by (subst(asm) real_arch_inv)
     4.8 +  by (subst(asm) real_arch_inverse)
     4.9  
    4.10  
    4.11  subsection \<open>Sundries\<close>
    4.12 @@ -2109,7 +2109,7 @@
    4.13      if e: "0 < e" for e
    4.14    proof -
    4.15      obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
    4.16 -      using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
    4.17 +      using real_arch_pow[of 2 "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
    4.18      show ?thesis
    4.19      proof (rule exI [where x=n], clarify)
    4.20        fix x y
    4.21 @@ -2947,7 +2947,7 @@
    4.22    have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
    4.23    proof (rule CauchyI, goal_cases)
    4.24      case (1 e)
    4.25 -    then guess N unfolding real_arch_inv[of e] .. note N=this
    4.26 +    then guess N unfolding real_arch_inverse[of e] .. note N=this
    4.27      show ?case
    4.28        apply (rule_tac x=N in exI)
    4.29      proof clarify
    4.30 @@ -2967,7 +2967,7 @@
    4.31      fix e :: real
    4.32      assume "e>0"
    4.33      then have *:"e/2 > 0" by auto
    4.34 -    then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this
    4.35 +    then guess N1 unfolding real_arch_inverse[of "e/2"] .. note N1=this
    4.36      then have N1': "N1 = N1 - 1 + 1"
    4.37        by auto
    4.38      guess N2 using y[OF *] .. note N2=this
    4.39 @@ -4620,7 +4620,7 @@
    4.40        using True by (auto simp add: field_simps)
    4.41      then obtain M :: nat
    4.42           where M: "M \<noteq> 0" "0 < inverse (real_of_nat M)" "inverse (of_nat M) < e / 4 / content (cbox a b)"
    4.43 -      by (subst (asm) real_arch_inv) auto
    4.44 +      by (subst (asm) real_arch_inverse) auto
    4.45      show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e"
    4.46      proof (rule exI [where x=M], clarify)
    4.47        fix m n
     5.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 15 08:34:04 2016 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 15 14:08:25 2016 +0000
     5.3 @@ -581,15 +581,8 @@
     5.4  
     5.5  subsection \<open>Archimedean properties and useful consequences\<close>
     5.6  
     5.7 -lemma real_arch_simple: "\<exists>n::nat. x \<le> real n"
     5.8 -  by (rule ex_le_of_nat)
     5.9 -
    5.10 -lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
    5.11 -  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
    5.12 -  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
    5.13 -
    5.14  text\<open>Bernoulli's inequality\<close>
    5.15 -lemma Bernoulli_inequality:
    5.16 +proposition Bernoulli_inequality:
    5.17    fixes x :: real
    5.18    assumes "-1 \<le> x"
    5.19      shows "1 + n * x \<le> (1 + x) ^ n"
    5.20 @@ -607,7 +600,7 @@
    5.21    finally show ?case .
    5.22  qed
    5.23  
    5.24 -lemma Bernoulli_inequality_even:
    5.25 +corollary Bernoulli_inequality_even:
    5.26    fixes x :: real
    5.27    assumes "even n"
    5.28      shows "1 + n * x \<le> (1 + x) ^ n"
    5.29 @@ -629,7 +622,7 @@
    5.30    finally show ?thesis .
    5.31  qed
    5.32  
    5.33 -lemma real_arch_pow:
    5.34 +corollary real_arch_pow:
    5.35    fixes x :: real
    5.36    assumes x: "1 < x"
    5.37    shows "\<exists>n. y < x^n"
    5.38 @@ -644,12 +637,7 @@
    5.39    then show ?thesis by metis
    5.40  qed
    5.41  
    5.42 -lemma real_arch_pow2:
    5.43 -  fixes x :: real
    5.44 -  shows "\<exists>n. x < 2^ n"
    5.45 -  using real_arch_pow[of 2 x] by simp
    5.46 -
    5.47 -lemma real_arch_pow_inv:
    5.48 +corollary real_arch_pow_inv:
    5.49    fixes x y :: real
    5.50    assumes y: "y > 0"
    5.51      and x1: "x < 1"
    5.52 @@ -673,7 +661,7 @@
    5.53  lemma forall_pos_mono:
    5.54    "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
    5.55      (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
    5.56 -  by (metis real_arch_inv)
    5.57 +  by (metis real_arch_inverse)
    5.58  
    5.59  lemma forall_pos_mono_1:
    5.60    "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 15 08:34:04 2016 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 15 14:08:25 2016 +0000
     6.3 @@ -5525,7 +5525,7 @@
     6.4        fix e :: real
     6.5        assume "e > 0"
     6.6        then obtain N :: nat where "N \<noteq> 0" and N: "0 < inverse (real N) \<and> inverse (real N) < e"
     6.7 -        unfolding real_arch_inv[of e] by auto
     6.8 +        unfolding real_arch_inverse[of e] by auto
     6.9        {
    6.10          fix n :: nat
    6.11          assume "n \<ge> N"
    6.12 @@ -7492,7 +7492,7 @@
    6.13          fix e :: real
    6.14          assume "e > 0"
    6.15          then have "\<exists>N::nat. inverse (real (N + 1)) < e"
    6.16 -          using real_arch_inv[of e]
    6.17 +          using real_arch_inverse[of e]
    6.18            apply (auto simp add: Suc_pred')
    6.19            apply (metis Suc_pred' of_nat_Suc)
    6.20            done
     7.1 --- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 08:34:04 2016 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Mar 15 14:08:25 2016 +0000
     7.3 @@ -725,7 +725,7 @@
     7.4    { fix e::real
     7.5      assume e: "0 < e"
     7.6      then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
     7.7 -      by (auto simp: real_arch_inv [of e])
     7.8 +      by (auto simp: real_arch_inverse [of e])
     7.9      { fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real"
    7.10        assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
    7.11        assume x: "x \<in> s"
     8.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 15 08:34:04 2016 +0100
     8.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 15 14:08:25 2016 +0000
     8.3 @@ -270,7 +270,7 @@
     8.4      proof (rule ccontr)
     8.5        assume "\<not> 0 \<le> ?d B"
     8.6        hence "0 < - ?d B" by auto
     8.7 -      from ex_inverse_of_nat_Suc_less[OF this]
     8.8 +      from reals_Archimedean[OF this]
     8.9        obtain n where *: "?d B < - 1 / real (Suc n)"
    8.10          by (auto simp: field_simps)
    8.11        also have "\<dots> \<le> - 1 / real (Suc (Suc n))"
     9.1 --- a/src/HOL/Real.thy	Tue Mar 15 08:34:04 2016 +0100
     9.2 +++ b/src/HOL/Real.thy	Tue Mar 15 14:08:25 2016 +0000
     9.3 @@ -1135,8 +1135,9 @@
     9.4  
     9.5  subsection \<open>The Archimedean Property of the Reals\<close>
     9.6  
     9.7 -lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less  (*FIXME*)
     9.8 -lemmas reals_Archimedean2 = ex_less_of_nat
     9.9 +lemma real_arch_inverse: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
    9.10 +  using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
    9.11 +  by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
    9.12  
    9.13  lemma reals_Archimedean3:
    9.14    assumes x_greater_zero: "0 < x"
    10.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 08:34:04 2016 +0100
    10.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 15 14:08:25 2016 +0000
    10.3 @@ -2143,7 +2143,7 @@
    10.4      by (auto simp: lim_sequentially dist_real_def)
    10.5    { fix x :: real
    10.6      obtain n where "x \<le> real_of_nat n"
    10.7 -      using ex_le_of_nat[of x] ..
    10.8 +      using real_arch_simple[of x] ..
    10.9      note monoD[OF mono this]
   10.10      also have "f (real_of_nat n) \<le> y"
   10.11        by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])