author paulson Tue Mar 15 14:08:25 2016 +0000 (2016-03-15) changeset 62623 dbc62f86a1a9 parent 62622 7c56e4a1ad0c child 62624 59ceeb6f3079 child 62626 de25474ce728
rationalisation of theorem names esp about "real Archimedian" etc.
```     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])
```