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