Added "ALL x > y" and relatives.
--- a/src/HOL/HOL.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/HOL.thy Thu Dec 02 11:42:01 2004 +0100
@@ -1109,12 +1109,22 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)
+
syntax (xsymbols)
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
syntax (HOL)
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
@@ -1127,11 +1137,20 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+ "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
+ "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
+ "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+ "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+
translations
"ALL x<y. P" => "ALL x. x < y --> P"
"EX x<y. P" => "EX x. x < y & P"
"ALL x<=y. P" => "ALL x. x <= y --> P"
"EX x<=y. P" => "EX x. x <= y & P"
+ "ALL x>y. P" => "ALL x. x > y --> P"
+ "EX x>y. P" => "EX x. x > y & P"
+ "ALL x>=y. P" => "ALL x. x >= y --> P"
+ "EX x>=y. P" => "EX x. x >= y & P"
print_translation {*
let
--- a/src/HOL/Hyperreal/HyperPow.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Thu Dec 02 11:42:01 2004 +0100
@@ -7,7 +7,7 @@
header{*Exponentials on the Hyperreals*}
theory HyperPow
-imports HyperArith HyperNat "../Real/RealPow"
+imports HyperArith HyperNat
begin
instance hypreal :: power ..
--- a/src/HOL/Hyperreal/Integration.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Integration.thy Thu Dec 02 11:42:01 2004 +0100
@@ -17,13 +17,13 @@
--{*Partitions and tagged partitions etc.*}
partition :: "[(real*real),nat => real] => bool"
- "partition == %(a,b) D. ((D 0 = a) &
- (\<exists>N. ((\<forall>n. n < N --> D(n) < D(Suc n)) &
- (\<forall>n. N \<le> n --> (D(n) = b)))))"
+ "partition == %(a,b) D. D 0 = a &
+ (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
+ (\<forall>n \<ge> N. D(n) = b))"
psize :: "(nat => real) => nat"
- "psize D == @N. (\<forall>n. n < N --> D(n) < D(Suc n)) &
- (\<forall>n. N \<le> n --> (D(n) = D(N)))"
+ "psize D == SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+ (\<forall>n \<ge> N. D(n) = D(N))"
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
"tpart == %(a,b) (D,p). partition(a,b) D &
@@ -45,7 +45,7 @@
--{*Gauge integrability (definite)*}
Integral :: "[(real*real),real=>real,real] => bool"
- "Integral == %(a,b) f k. \<forall>e. 0 < e -->
+ "Integral == %(a,b) f k. \<forall>e > 0.
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
\<bar>rsum(D,p) f - k\<bar> < e))"
@@ -70,8 +70,8 @@
lemma partition:
"(partition(a,b) D) =
((D 0 = a) &
- (\<forall>n. n < (psize D) --> D n < D(Suc n)) &
- (\<forall>n. (psize D) \<le> n --> (D n = b)))"
+ (\<forall>n < psize D. D n < D(Suc n)) &
+ (\<forall>n \<ge> psize D. D n = b))"
apply (simp add: partition_def, auto)
apply (subgoal_tac [!] "psize D = N", auto)
apply (simp_all (no_asm) add: psize_def)
@@ -181,13 +181,11 @@
lemma lemma_partition_append1:
"[| partition (a, b) D1; partition (b, c) D2 |]
- ==> (\<forall>n.
- n < psize D1 + psize D2 -->
+ ==> (\<forall>n < psize D1 + psize D2.
(if n < psize D1 then D1 n else D2 (n - psize D1))
< (if Suc n < psize D1 then D1 (Suc n)
else D2 (Suc n - psize D1))) &
- (\<forall>n.
- psize D1 + psize D2 \<le> n -->
+ (\<forall>n \<ge> psize D1 + psize D2.
(if n < psize D1 then D1 n else D2 (n - psize D1)) =
(if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
else D2 (psize D1 + psize D2 - psize D1)))"
@@ -412,9 +410,8 @@
--> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
apply (simp add: gauge_def)
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b -->
- (\<exists>d. 0 < d &
- (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
- \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u)))")
+ (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
+ \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u))")
apply (drule choiceP, auto)
apply (drule spec, auto)
apply (auto simp add: DERIV_iff2 LIM_def)
@@ -445,7 +442,7 @@
apply (drule order_le_imp_less_or_eq, auto)
apply (auto simp add: Integral_def)
apply (rule ccontr)
-apply (subgoal_tac "\<forall>e. 0 < e --> (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e))")
+apply (subgoal_tac "\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e)")
apply (rotate_tac 3)
apply (drule_tac x = "e/2" in spec, auto)
apply (drule spec, auto)
@@ -796,7 +793,7 @@
lemma lemma_Integral_le:
"[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
tpart(a,b) (D,p)
- |] ==> \<forall>n. n \<le> psize D --> f (p n) \<le> g (p n)"
+ |] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)"
apply (simp add: tpart_def)
apply (auto, frule partition [THEN iffD1], auto)
apply (drule_tac x = "p n" in spec, auto)
@@ -842,12 +839,11 @@
lemma Integral_imp_Cauchy:
"(\<exists>k. Integral(a,b) f k) ==>
- (\<forall>e. 0 < e -->
- (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
+ (\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
(\<forall>D1 D2 p1 p2.
tpart(a,b) (D1, p1) & fine g (D1,p1) &
tpart(a,b) (D2, p2) & fine g (D2,p2) -->
- \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e)))"
+ \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e))"
apply (simp add: Integral_def, auto)
apply (drule_tac x = "e/2" in spec, auto)
apply (rule exI, auto)
@@ -862,13 +858,12 @@
lemma Cauchy_iff2:
"Cauchy X =
- (\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n -->
- \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
+ (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
apply (simp add: Cauchy_def, auto)
apply (drule reals_Archimedean, safe)
apply (drule_tac x = n in spec, auto)
apply (rule_tac x = M in exI, auto)
-apply (drule_tac x = m in spec)
+apply (drule_tac x = m in spec, simp)
apply (drule_tac x = na in spec, auto)
done
--- a/src/HOL/Hyperreal/Lim.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.thy Thu Dec 02 11:42:01 2004 +0100
@@ -8,7 +8,7 @@
header{*Limits, Continuity and Differentiation*}
theory Lim
-imports SEQ RealDef
+imports SEQ
begin
text{*Standard and Nonstandard Definitions*}
@@ -17,9 +17,8 @@
LIM :: "[real=>real,real,real] => bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
"f -- a --> L ==
- \<forall>r. 0 < r -->
- (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (\<bar>x + -a\<bar> < s)
- --> \<bar>f x + -L\<bar> < r)))"
+ \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
+ --> \<bar>f x + -L\<bar> < r"
NSLIM :: "[real=>real,real,real] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
@@ -58,9 +57,7 @@
inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
isUCont :: "(real=>real) => bool"
- "isUCont f == (\<forall>r. 0 < r -->
- (\<exists>s. 0 < s & (\<forall>x y. \<bar>x + -y\<bar> < s
- --> \<bar>f x + -f y\<bar> < r)))"
+ "isUCont f == \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
isNSUCont :: "(real=>real) => bool"
"isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
@@ -84,12 +81,12 @@
lemma LIM_eq:
"f -- a --> L =
- (\<forall>r. 0<r --> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))"
+ (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
by (simp add: LIM_def diff_minus)
lemma LIM_D:
"[| f -- a --> L; 0<r |]
- ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
+ ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r"
by (simp add: LIM_eq)
lemma LIM_const [simp]: "(%x. k) -- x --> k"
@@ -111,8 +108,7 @@
where gs: "0 < gs"
and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
by blast
- show "\<exists>s. 0 < s \<and>
- (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r)"
+ show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r"
proof (intro exI conjI strip)
show "0 < min fs gs" by (simp add: fs gs)
fix x :: real
@@ -143,8 +139,7 @@
lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
assume k: "k < L"
- show "\<exists>r. 0 < r \<and>
- (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+ show "\<exists>r>0. \<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
proof (intro exI conjI strip)
show "0 < L-k" by (simp add: k compare_rls)
fix s :: real
@@ -157,8 +152,7 @@
qed
next
assume k: "L < k"
- show "\<exists>r. 0 < r \<and>
- (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
+ show "\<exists>r>0.\<forall>s>0. (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r"
proof (intro exI conjI strip)
show "0 < k-L" by (simp add: k compare_rls)
fix s :: real
@@ -245,8 +239,8 @@
subsubsection{*Limit: The NS definition implies the standard definition.*}
-lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
- \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>)
+lemma lemma_LIM: "\<forall>s>0.\<exists>xa. xa \<noteq> x &
+ \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>
==> \<forall>n::nat. \<exists>xa. xa \<noteq> x &
\<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
apply clarify
@@ -254,8 +248,7 @@
done
lemma lemma_skolemize_LIM2:
- "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
- \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>)
+ "\<forall>s>0.\<exists>xa. xa \<noteq> x & \<bar>xa + - x\<bar> < s & r \<le> \<bar>f xa + -L\<bar>
==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
\<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
apply (drule lemma_LIM)
@@ -598,17 +591,15 @@
apply (drule FreeUltrafilterNat_all, ultra)
done
-lemma lemma_LIMu: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
- ==> \<forall>n::nat. \<exists>z y.
- \<bar>z + -y\<bar> < inverse(real(Suc n)) &
- r \<le> \<bar>f z + -f y\<bar>"
+lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
+ ==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
apply clarify
apply (cut_tac n1 = n
in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
done
lemma lemma_skolemize_LIM2u:
- "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
+ "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
==> \<exists>X Y. \<forall>n::nat.
abs(X n + -(Y n)) < inverse(real(Suc n)) &
r \<le> abs(f (X n) + -f (Y n))"
@@ -687,7 +678,7 @@
subsubsection{*Alternative definition for differentiability*}
lemma LIM_I:
- "(!!r. 0<r ==> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))
+ "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)
==> f -- a --> L"
by (simp add: LIM_eq)
@@ -1438,7 +1429,7 @@
apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
apply (drule_tac x = x in spec)+
apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
+apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
apply safe
apply simp
apply (drule_tac x = s in spec, clarify)
@@ -1594,11 +1585,10 @@
lemma DERIV_left_inc:
assumes der: "DERIV f x :> l"
and l: "0 < l"
- shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
+ shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
proof -
from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
- have "\<exists>s. 0 < s \<and>
- (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
+ have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
by (simp add: diff_minus)
then obtain s
where s: "0 < s"
@@ -1608,7 +1598,7 @@
proof (intro exI conjI strip)
show "0<s" .
fix h::real
- assume "0 < h \<and> h < s"
+ assume "0 < h" "h < s"
with all [of h] show "f x < f (x+h)"
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
split add: split_if_asm)
@@ -1624,11 +1614,10 @@
lemma DERIV_left_dec:
assumes der: "DERIV f x :> l"
and l: "l < 0"
- shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x-h))"
+ shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
proof -
from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
- have "\<exists>s. 0 < s \<and>
- (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
+ have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
by (simp add: diff_minus)
then obtain s
where s: "0 < s"
@@ -1638,7 +1627,7 @@
proof (intro exI conjI strip)
show "0<s" .
fix h::real
- assume "0 < h \<and> h < s"
+ assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
split add: split_if_asm)
@@ -1662,7 +1651,7 @@
case less
from DERIV_left_dec [OF der less]
obtain d' where d': "0 < d'"
- and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
+ and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
from real_lbound_gt_zero [OF d d']
obtain e where "0 < e \<and> e < d \<and> e < d'" ..
with lt le [THEN spec [where x="x-e"]]
@@ -1671,7 +1660,7 @@
case greater
from DERIV_left_inc [OF der greater]
obtain d' where d': "0 < d'"
- and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x + h)" by blast
+ and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
from real_lbound_gt_zero [OF d d']
obtain e where "0 < e \<and> e < d \<and> e < d'" ..
with lt le [THEN spec [where x="x+e"]]
@@ -1857,7 +1846,7 @@
lemma DERIV_isconst_end: "[| a < b;
\<forall>x. a \<le> x & x \<le> b --> isCont f x;
\<forall>x. a < x & x < b --> DERIV f x :> 0 |]
- ==> (f b = f a)"
+ ==> f b = f a"
apply (drule MVT, assumption)
apply (blast intro: differentiableI)
apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
@@ -1992,7 +1981,7 @@
assumes d: "0 < d"
and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
- shows "\<exists>e. 0<e & (\<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y))"
+ shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
proof -
have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
by (auto simp add: abs_le_interval_iff)
@@ -2045,7 +2034,7 @@
shows "isCont g (f x)"
proof (simp add: isCont_iff LIM_eq)
show "\<forall>r. 0 < r \<longrightarrow>
- (\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r))"
+ (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
proof (intro strip)
fix r::real
assume r: "0<r"
@@ -2058,7 +2047,7 @@
obtain e' where e': "0 < e'"
and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
by blast
- show "\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
+ show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
proof (intro exI conjI)
show "0<e'" .
show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
@@ -2269,4 +2258,3 @@
end
-
--- a/src/HOL/Hyperreal/NatStar.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy Thu Dec 02 11:42:01 2004 +0100
@@ -8,7 +8,7 @@
header{*Star-transforms for the Hypernaturals*}
theory NatStar
-imports "../Real/RealPow" HyperPow
+imports HyperPow
begin
text{*Extends sets of nats, and functions from the nats to nats or reals*}
@@ -638,5 +638,3 @@
end
-
-
--- a/src/HOL/Hyperreal/SEQ.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Thu Dec 02 11:42:01 2004 +0100
@@ -37,7 +37,7 @@
Bseq :: "(nat => real) => bool"
--{*Standard definition for bounded sequence*}
- "Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))"
+ "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K"
NSBseq :: "(nat=>real) => bool"
--{*Nonstandard definition for bounded sequence*}
@@ -45,18 +45,15 @@
monoseq :: "(nat=>real)=>bool"
--{*Definition for monotonicity*}
- "monoseq X == ((\<forall>(m::nat) n. m \<le> n --> X m \<le> X n) |
- (\<forall>m n. m \<le> n --> X n \<le> X m))"
+ "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
subseq :: "(nat => nat) => bool"
--{*Definition of subsequence*}
- "subseq f == (\<forall>m n. m < n --> (f m) < (f n))"
+ "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)"
Cauchy :: "(nat => real) => bool"
--{*Standard definition of the Cauchy condition*}
- "Cauchy X == (\<forall>e. (0 < e -->
- (\<exists>M. (\<forall>m n. M \<le> m & M \<le> n
- --> abs((X m) + -(X n)) < e))))"
+ "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e"
NSCauchy :: "(nat => real) => bool"
--{*Nonstandard definition*}
@@ -80,8 +77,7 @@
subsection{*LIMSEQ and NSLIMSEQ*}
lemma LIMSEQ_iff:
- "(X ----> L) =
- (\<forall>r. 0 <r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+ "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
by (simp add: LIMSEQ_def)
lemma NSLIMSEQ_iff:
@@ -363,10 +359,10 @@
apply (auto intro: order_trans)
done
-lemma monoI1: "\<forall>m n. m \<le> n --> X m \<le> X n ==> monoseq X"
+lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
by (simp add: monoseq_def)
-lemma monoI2: "\<forall>m n. m \<le> n --> X n \<le> X m ==> monoseq X"
+lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
by (simp add: monoseq_def)
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
@@ -385,7 +381,7 @@
by (auto simp add: Bseq_def)
lemma lemma_NBseq_def:
- "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
+ "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
(\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
apply auto
prefer 2 apply force
@@ -402,8 +398,7 @@
done
lemma lemma_NBseq_def2:
- "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
- (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+ "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
apply (subst lemma_NBseq_def, auto)
apply (rule_tac x = "Suc N" in exI)
apply (rule_tac [2] x = N in exI)
@@ -449,13 +444,13 @@
which woulid be useless.*}
lemma lemmaNSBseq:
- "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+ "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
apply safe
apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
done
-lemma lemmaNSBseq2: "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
apply (drule lemmaNSBseq)
apply (drule choice, blast)
@@ -558,9 +553,9 @@
subsection{*A Bounded and Monotonic Sequence Converges*}
lemma lemma_converg1:
- "!!(X::nat=>real). [| \<forall>m n. m \<le> n --> X m \<le> X n;
+ "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
- |] ==> \<forall>n. ma \<le> n --> X n = X ma"
+ |] ==> \<forall>n \<ge> ma. X n = X ma"
apply safe
apply (drule_tac y = "X n" in isLubD2)
apply (blast dest: order_antisym)+
@@ -578,7 +573,7 @@
done
text{*Now, the same theorem in terms of NS limit *}
-lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----NS> L)"
+lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
lemma lemma_converg2:
@@ -610,7 +605,7 @@
text{*A standard proof of the theorem for monotone increasing sequence*}
lemma Bseq_mono_convergent:
- "[| Bseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> convergent X"
+ "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
apply (simp add: convergent_def)
apply (frule Bseq_isLub, safe)
apply (case_tac "\<exists>m. X m = U", auto)
@@ -629,7 +624,7 @@
text{*Nonstandard version of the theorem*}
lemma NSBseq_mono_NSconvergent:
- "[| NSBseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> NSconvergent X"
+ "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
by (auto intro: Bseq_mono_convergent
simp add: convergent_NSconvergent_iff [symmetric]
Bseq_NSBseq_iff [symmetric])
@@ -655,16 +650,16 @@
subsection{*A Few More Equivalence Theorems for Boundedness*}
text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + -x\<bar> \<le> k))"
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
apply (unfold Bseq_def, safe)
apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
-apply (rule_tac x = K in exI)
+apply (rule_tac x = K in exI, simp)
apply (rule exI [where x = 0], auto)
apply (drule_tac x=n in spec, arith)+
done
text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + -X(N)) \<le> k))"
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
apply safe
apply (simp add: Bseq_def, safe)
apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
@@ -746,8 +741,8 @@
text{*A Cauchy sequence is bounded -- this is the standard
proof mechanization rather than the nonstandard proof*}
-lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
- ==> \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
+lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
+ ==> \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
apply safe
apply (drule spec, auto, arith)
done
@@ -757,7 +752,7 @@
text{* FIXME: Long. Maximal element in subsequence *}
lemma SUP_rabs_subseq:
- "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
+ "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
apply (induct M)
apply (rule_tac x = 0 in exI, simp, safe)
apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
@@ -772,28 +767,28 @@
lemma lemma_Nat_covered:
"[| \<forall>m::nat. m \<le> M --> P M m;
- \<forall>m. M \<le> m --> P M m |]
+ \<forall>m \<ge> M. P M m |]
==> \<forall>m. P M m"
by (auto elim: less_asym simp add: le_def)
lemma lemma_trans1:
- "[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a; a < b |]
- ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+ "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a; a < b |]
+ ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
by (blast intro: order_le_less_trans [THEN order_less_imp_le])
lemma lemma_trans2:
- "[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
- ==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
+ "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
+ ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
by (blast intro: order_less_trans [THEN order_less_imp_le])
lemma lemma_trans3:
- "[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
- ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+ "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
+ ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
by auto
-lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
- ==> \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
+lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
+ ==> \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
by (blast intro: order_less_imp_le)
@@ -857,8 +852,8 @@
lemma NSLIMSEQ_le:
"[| f ----NS> l; g ----NS> m;
- \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
- |] ==> l \<le> m"
+ \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
+ |] ==> l \<le> m"
apply (simp add: NSLIMSEQ_def, safe)
apply (drule starfun_le_mono)
apply (drule HNatInfinite_whn [THEN [2] bspec])+
@@ -870,7 +865,7 @@
(* standard version *)
lemma LIMSEQ_le:
- "[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
+ "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
==> l \<le> m"
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
@@ -952,7 +947,7 @@
text{* standard proof seems easier *}
lemma LIMSEQ_inverse_zero:
- "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
+ "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
apply (simp add: LIMSEQ_def, safe)
apply (drule_tac x = "inverse r" in spec, safe)
apply (rule_tac x = N in exI, safe)
@@ -967,7 +962,7 @@
done
lemma NSLIMSEQ_inverse_zero:
- "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
+ "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
==> (%n. inverse(f n)) ----NS> 0"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
@@ -1240,4 +1235,3 @@
end
-
--- a/src/HOL/Hyperreal/Series.thy Thu Dec 02 11:09:19 2004 +0100
+++ b/src/HOL/Hyperreal/Series.thy Thu Dec 02 11:42:01 2004 +0100
@@ -84,7 +84,7 @@
done
lemma sumr_interval_const2:
- "[|\<forall>n. m \<le> n --> f n = r; m \<le> k|]
+ "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
==> sumr m k f = (real (k - m) * r)"
apply (induct "k", auto)
apply (drule_tac x = k in spec)
@@ -94,7 +94,7 @@
lemma sumr_le:
- "[|\<forall>n. m \<le> n --> 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
+ "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
apply (induct "k")
apply (auto simp add: less_Suc_eq_le)
apply (drule_tac x = k in spec, safe)
@@ -109,7 +109,7 @@
apply (auto intro: add_mono simp add: le_def)
done
-lemma sumr_ge_zero: "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumr m n f"
+lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
apply (induct "n", auto)
apply (drule_tac x = n in spec, arith)
done
@@ -119,11 +119,11 @@
by (induct "n", simp_all add: add_increasing)
lemma sumr_zero [rule_format]:
- "\<forall>n. N \<le> n --> f n = 0 ==> N \<le> m --> sumr m n f = 0"
+ "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
by (induct "n", auto)
lemma Suc_le_imp_diff_ge2:
- "[|\<forall>n. N \<le> n --> f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
+ "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
apply (rule sumr_zero)
apply (case_tac "n", auto)
done
@@ -289,7 +289,7 @@
great as any partial sum.*}
lemma series_pos_le:
- "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
+ "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
apply (drule summable_sums)
apply (simp add: sums_def)
apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
@@ -300,7 +300,7 @@
done
lemma series_pos_less:
- "[| summable f; \<forall>m. n \<le> m --> 0 < f(m) |] ==> sumr 0 n f < suminf f"
+ "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f"
apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
apply (rule_tac [2] series_pos_le, auto)
apply (drule_tac x = m in spec, auto)
@@ -332,14 +332,14 @@
lemma summable_Cauchy:
"summable f =
- (\<forall>e. 0 < e --> (\<exists>N. \<forall>m n. N \<le> m --> abs(sumr m n f) < e))"
+ (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def)
apply (drule_tac [!] spec, auto)
apply (rule_tac x = M in exI)
apply (rule_tac [2] x = N in exI, auto)
apply (cut_tac [!] m = m and n = n in less_linear, auto)
apply (frule le_less_trans [THEN less_imp_le], assumption)
-apply (drule_tac x = n in spec)
+apply (drule_tac x = n in spec, simp)
apply (drule_tac x = m in spec)
apply (auto intro: abs_minus_add_cancel [THEN subst]
simp add: sumr_split_add_minus abs_minus_add_cancel)
@@ -348,7 +348,7 @@
text{*Comparison test*}
lemma summable_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
+ "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
apply (auto simp add: summable_Cauchy)
apply (drule spec, auto)
apply (rule_tac x = "N + Na" in exI, auto)
@@ -362,7 +362,7 @@
done
lemma summable_rabs_comparison_test:
- "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |]
+ "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |]
==> summable (%k. abs (f k))"
apply (rule summable_comparison_test)
apply (auto simp add: abs_idempotent)
@@ -419,7 +419,7 @@
(*All this trouble just to get 0<c *)
lemma ratio_test_lemma2:
- "[| \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]
+ "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]
==> 0 < c | summable f"
apply (simp (no_asm) add: linorder_not_le [symmetric])
apply (simp add: summable_Cauchy)
@@ -430,7 +430,7 @@
done
lemma ratio_test:
- "[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]
+ "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]
==> summable f"
apply (frule ratio_test_lemma2, auto)
apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n"