author | huffman |
Tue, 08 May 2007 03:03:23 +0200 | |
changeset 22856 | eb0e0582092a |
parent 22630 | 2a9b64b26612 |
child 22881 | c23ded11158f |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : NSA.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
4 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
5 |
Converted to Isar and polished by lcp |
14370 | 6 |
*) |
10751 | 7 |
|
14370 | 8 |
header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
9 |
||
15131 | 10 |
theory NSA |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
11 |
imports HyperDef "../Real/RComplete" |
15131 | 12 |
begin |
10751 | 13 |
|
19765 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
15 |
hnorm :: "'a::norm star \<Rightarrow> real star" where |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
16 |
"hnorm = *f* norm" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
17 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
18 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
19 |
Infinitesimal :: "('a::real_normed_vector) star set" where |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
20 |
"Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}" |
10751 | 21 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
22 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
23 |
HFinite :: "('a::real_normed_vector) star set" where |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
24 |
"HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}" |
10751 | 25 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
26 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
27 |
HInfinite :: "('a::real_normed_vector) star set" where |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
28 |
"HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}" |
10751 | 29 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
30 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
31 |
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where |
15229 | 32 |
--{*the `infinitely close' relation*} |
20563 | 33 |
"(x @= y) = ((x - y) \<in> Infinitesimal)" |
14653 | 34 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
35 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
36 |
st :: "hypreal => hypreal" where |
15229 | 37 |
--{*the standard part of a hyperreal*} |
19765 | 38 |
"st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)" |
10751 | 39 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
40 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
41 |
monad :: "'a::real_normed_vector star => 'a star set" where |
19765 | 42 |
"monad x = {y. x @= y}" |
10751 | 43 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
44 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
45 |
galaxy :: "'a::real_normed_vector star => 'a star set" where |
19765 | 46 |
"galaxy x = {y. (x + -y) \<in> HFinite}" |
47 |
||
21210 | 48 |
notation (xsymbols) |
19765 | 49 |
approx (infixl "\<approx>" 50) |
50 |
||
21210 | 51 |
notation (HTML output) |
19765 | 52 |
approx (infixl "\<approx>" 50) |
14370 | 53 |
|
20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset
|
54 |
lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}" |
20729 | 55 |
by (simp add: Reals_def image_def) |
14370 | 56 |
|
20721 | 57 |
subsection {* Nonstandard Extension of the Norm Function *} |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
58 |
|
20794 | 59 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
60 |
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where |
20794 | 61 |
"scaleHR = starfun2 scaleR" |
62 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
63 |
declare hnorm_def [transfer_unfold] |
20794 | 64 |
declare scaleHR_def [transfer_unfold] |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
65 |
|
20728 | 66 |
lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard" |
67 |
by (simp add: hnorm_def) |
|
68 |
||
69 |
lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)" |
|
70 |
by transfer (rule refl) |
|
71 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
72 |
lemma hnorm_ge_zero [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
73 |
"\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
74 |
by transfer (rule norm_ge_zero) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
75 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
76 |
lemma hnorm_eq_zero [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
77 |
"\<And>x::'a::real_normed_vector star. (hnorm x = 0) = (x = 0)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
78 |
by transfer (rule norm_eq_zero) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
79 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
80 |
lemma hnorm_triangle_ineq: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
81 |
"\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
82 |
by transfer (rule norm_triangle_ineq) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
83 |
|
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
84 |
lemma hnorm_triangle_ineq3: |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
85 |
"\<And>x y::'a::real_normed_vector star. \<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
86 |
by transfer (rule norm_triangle_ineq3) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
87 |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
88 |
lemma hnorm_scaleR: |
20794 | 89 |
"\<And>x::'a::real_normed_vector star. |
90 |
hnorm (a *# x) = \<bar>star_of a\<bar> * hnorm x" |
|
91 |
by transfer (rule norm_scaleR) |
|
92 |
||
93 |
lemma hnorm_scaleHR: |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
94 |
"\<And>a (x::'a::real_normed_vector star). |
20794 | 95 |
hnorm (scaleHR a x) = \<bar>a\<bar> * hnorm x" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
96 |
by transfer (rule norm_scaleR) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
97 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
98 |
lemma hnorm_mult_ineq: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
99 |
"\<And>x y::'a::real_normed_algebra star. hnorm (x * y) \<le> hnorm x * hnorm y" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
100 |
by transfer (rule norm_mult_ineq) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
101 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
102 |
lemma hnorm_mult: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
103 |
"\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
104 |
by transfer (rule norm_mult) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
105 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
106 |
lemma hnorm_one [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
107 |
"hnorm (1\<Colon>'a::real_normed_div_algebra star) = 1" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
108 |
by transfer (rule norm_one) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
109 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
110 |
lemma hnorm_zero [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
111 |
"hnorm (0\<Colon>'a::real_normed_vector star) = 0" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
112 |
by transfer (rule norm_zero) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
113 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
114 |
lemma zero_less_hnorm_iff [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
115 |
"\<And>x::'a::real_normed_vector star. (0 < hnorm x) = (x \<noteq> 0)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
116 |
by transfer (rule zero_less_norm_iff) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
117 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
118 |
lemma hnorm_minus_cancel [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
119 |
"\<And>x::'a::real_normed_vector star. hnorm (- x) = hnorm x" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
120 |
by transfer (rule norm_minus_cancel) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
121 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
122 |
lemma hnorm_minus_commute: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
123 |
"\<And>a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
124 |
by transfer (rule norm_minus_commute) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
125 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
126 |
lemma hnorm_triangle_ineq2: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
127 |
"\<And>a b::'a::real_normed_vector star. hnorm a - hnorm b \<le> hnorm (a - b)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
128 |
by transfer (rule norm_triangle_ineq2) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
129 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
130 |
lemma hnorm_triangle_ineq4: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
131 |
"\<And>a b::'a::real_normed_vector star. hnorm (a - b) \<le> hnorm a + hnorm b" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
132 |
by transfer (rule norm_triangle_ineq4) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
133 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
134 |
lemma nonzero_hnorm_inverse: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
135 |
"\<And>a::'a::real_normed_div_algebra star. |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
136 |
a \<noteq> 0 \<Longrightarrow> hnorm (inverse a) = inverse (hnorm a)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
137 |
by transfer (rule nonzero_norm_inverse) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
138 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
139 |
lemma hnorm_inverse: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
140 |
"\<And>a::'a::{real_normed_div_algebra,division_by_zero} star. |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
141 |
hnorm (inverse a) = inverse (hnorm a)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
142 |
by transfer (rule norm_inverse) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
143 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
144 |
lemma hypreal_hnorm_def [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
145 |
"\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
146 |
by transfer (rule real_norm_def) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
147 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
148 |
lemma hnorm_add_less: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
149 |
fixes x y :: "'a::real_normed_vector star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
150 |
shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x + y) < r + s" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
151 |
by (rule order_le_less_trans [OF hnorm_triangle_ineq add_strict_mono]) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
152 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
153 |
lemma hnorm_mult_less: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
154 |
fixes x y :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
155 |
shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x * y) < r * s" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
156 |
apply (rule order_le_less_trans [OF hnorm_mult_ineq]) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
157 |
apply (simp add: mult_strict_mono') |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
158 |
done |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
159 |
|
20794 | 160 |
lemma hnorm_scaleHR_less: |
161 |
"\<lbrakk>\<bar>x\<bar> < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (scaleHR x y) < r * s" |
|
162 |
apply (simp only: hnorm_scaleHR) |
|
163 |
apply (simp add: mult_strict_mono') |
|
164 |
done |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
165 |
|
15229 | 166 |
subsection{*Closure Laws for the Standard Reals*} |
14370 | 167 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
168 |
lemma Reals_minus_iff [simp]: "(-x \<in> Reals) = (x \<in> Reals)" |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
169 |
apply auto |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
170 |
apply (drule Reals_minus, auto) |
14370 | 171 |
done |
172 |
||
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
173 |
lemma Reals_add_cancel: "\<lbrakk>x + y \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals" |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
174 |
by (drule (1) Reals_diff, simp) |
14370 | 175 |
|
176 |
lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals" |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
177 |
by (simp add: Reals_eq_Standard) |
14370 | 178 |
|
15229 | 179 |
lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals" |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
180 |
by (simp add: Reals_eq_Standard) |
14370 | 181 |
|
182 |
lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals" |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
183 |
by simp |
14370 | 184 |
|
15229 | 185 |
text{*epsilon is not in Reals because it is an infinitesimal*} |
14370 | 186 |
lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals" |
187 |
apply (simp add: SReal_def) |
|
188 |
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym]) |
|
189 |
done |
|
190 |
||
191 |
lemma SReal_omega_not_mem: "omega \<notin> Reals" |
|
192 |
apply (simp add: SReal_def) |
|
193 |
apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym]) |
|
194 |
done |
|
195 |
||
196 |
lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)" |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
197 |
by simp |
14370 | 198 |
|
199 |
lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)" |
|
200 |
by (simp add: SReal_def) |
|
201 |
||
202 |
lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals" |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
203 |
by (simp add: Reals_eq_Standard Standard_def) |
14370 | 204 |
|
205 |
lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV" |
|
206 |
apply (auto simp add: SReal_def) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
207 |
apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast) |
14370 | 208 |
done |
209 |
||
210 |
lemma SReal_hypreal_of_real_image: |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
211 |
"[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q" |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
212 |
by (simp add: SReal_def image_def, blast) |
14370 | 213 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
214 |
lemma SReal_dense: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
215 |
"[| (x::hypreal) \<in> Reals; y \<in> Reals; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y" |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
216 |
apply (auto simp add: SReal_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
217 |
apply (drule dense, auto) |
14370 | 218 |
done |
219 |
||
15229 | 220 |
text{*Completeness of Reals, but both lemmas are unused.*} |
221 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
222 |
lemma SReal_sup_lemma: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
223 |
"P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) = |
14370 | 224 |
(\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))" |
225 |
by (blast dest!: SReal_iff [THEN iffD1]) |
|
226 |
||
227 |
lemma SReal_sup_lemma2: |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
228 |
"[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |] |
14370 | 229 |
==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) & |
230 |
(\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)" |
|
231 |
apply (rule conjI) |
|
232 |
apply (fast dest!: SReal_iff [THEN iffD1]) |
|
233 |
apply (auto, frule subsetD, assumption) |
|
234 |
apply (drule SReal_iff [THEN iffD1]) |
|
235 |
apply (auto, rule_tac x = ya in exI, auto) |
|
236 |
done |
|
237 |
||
15229 | 238 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
239 |
subsection{* Set of Finite Elements is a Subring of the Extended Reals*} |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
240 |
|
14370 | 241 |
lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite" |
242 |
apply (simp add: HFinite_def) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
243 |
apply (blast intro!: Reals_add hnorm_add_less) |
14370 | 244 |
done |
245 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
246 |
lemma HFinite_mult: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
247 |
fixes x y :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
248 |
shows "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
249 |
apply (simp add: HFinite_def) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
250 |
apply (blast intro!: Reals_mult hnorm_mult_less) |
14370 | 251 |
done |
252 |
||
20794 | 253 |
lemma HFinite_scaleHR: |
254 |
"[|x \<in> HFinite; y \<in> HFinite|] ==> scaleHR x y \<in> HFinite" |
|
255 |
apply (simp add: HFinite_def) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
256 |
apply (blast intro!: Reals_mult hnorm_scaleHR_less) |
20794 | 257 |
done |
258 |
||
14370 | 259 |
lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)" |
260 |
by (simp add: HFinite_def) |
|
261 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
262 |
lemma HFinite_star_of [simp]: "star_of x \<in> HFinite" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
263 |
apply (simp add: HFinite_def) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
264 |
apply (rule_tac x="star_of (norm x) + 1" in bexI) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
265 |
apply (transfer, simp) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
266 |
apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1) |
14370 | 267 |
done |
268 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
269 |
lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
270 |
by (auto simp add: SReal_def) |
14370 | 271 |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
272 |
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t" |
14370 | 273 |
by (simp add: HFinite_def) |
274 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
275 |
lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
276 |
by (simp add: HFinite_def) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
277 |
|
20562
c2f672be8522
add type constraint to otherwise looping iff rule
huffman
parents:
20554
diff
changeset
|
278 |
lemma HFinite_hnorm_iff [iff]: |
c2f672be8522
add type constraint to otherwise looping iff rule
huffman
parents:
20554
diff
changeset
|
279 |
"(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" |
14370 | 280 |
by (simp add: HFinite_def) |
281 |
||
15229 | 282 |
lemma HFinite_number_of [simp]: "number_of w \<in> HFinite" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
283 |
unfolding star_number_def by (rule HFinite_star_of) |
14370 | 284 |
|
285 |
(** As always with numerals, 0 and 1 are special cases **) |
|
286 |
||
15229 | 287 |
lemma HFinite_0 [simp]: "0 \<in> HFinite" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
288 |
unfolding star_zero_def by (rule HFinite_star_of) |
14370 | 289 |
|
15229 | 290 |
lemma HFinite_1 [simp]: "1 \<in> HFinite" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
291 |
unfolding star_one_def by (rule HFinite_star_of) |
14370 | 292 |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
293 |
lemma hrealpow_HFinite: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
294 |
fixes x :: "'a::{real_normed_algebra,recpower} star" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
295 |
shows "x \<in> HFinite ==> x ^ n \<in> HFinite" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
296 |
apply (induct_tac "n") |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
297 |
apply (auto simp add: power_Suc intro: HFinite_mult) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
298 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
299 |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
300 |
lemma HFinite_bounded: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
301 |
"[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
302 |
apply (case_tac "x \<le> 0") |
14370 | 303 |
apply (drule_tac y = x in order_trans) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
304 |
apply (drule_tac [2] order_antisym) |
14370 | 305 |
apply (auto simp add: linorder_not_le) |
306 |
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def) |
|
307 |
done |
|
308 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
309 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
310 |
subsection{* Set of Infinitesimals is a Subring of the Hyperreals*} |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
311 |
|
20407 | 312 |
lemma InfinitesimalI: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
313 |
"(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal" |
20407 | 314 |
by (simp add: Infinitesimal_def) |
315 |
||
14370 | 316 |
lemma InfinitesimalD: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
317 |
"x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> hnorm x < r" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
318 |
by (simp add: Infinitesimal_def) |
14370 | 319 |
|
20749 | 320 |
lemma InfinitesimalI2: |
321 |
"(\<And>r. 0 < r \<Longrightarrow> hnorm x < star_of r) \<Longrightarrow> x \<in> Infinitesimal" |
|
322 |
by (auto simp add: Infinitesimal_def SReal_def) |
|
323 |
||
324 |
lemma InfinitesimalD2: |
|
325 |
"\<lbrakk>x \<in> Infinitesimal; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < star_of r" |
|
326 |
by (auto simp add: Infinitesimal_def SReal_def) |
|
327 |
||
15229 | 328 |
lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal" |
14370 | 329 |
by (simp add: Infinitesimal_def) |
330 |
||
331 |
lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x" |
|
332 |
by auto |
|
333 |
||
334 |
lemma Infinitesimal_add: |
|
335 |
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal" |
|
20407 | 336 |
apply (rule InfinitesimalI) |
14370 | 337 |
apply (rule hypreal_sum_of_halves [THEN subst]) |
14477 | 338 |
apply (drule half_gt_zero) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
339 |
apply (blast intro: hnorm_add_less SReal_divide_number_of dest: InfinitesimalD) |
14370 | 340 |
done |
341 |
||
15229 | 342 |
lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)" |
14370 | 343 |
by (simp add: Infinitesimal_def) |
344 |
||
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
345 |
lemma Infinitesimal_hnorm_iff: |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
346 |
"(hnorm x \<in> Infinitesimal) = (x \<in> Infinitesimal)" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
347 |
by (simp add: Infinitesimal_def) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
348 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
349 |
lemma Infinitesimal_diff: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
350 |
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
351 |
by (simp add: diff_def Infinitesimal_add) |
14370 | 352 |
|
353 |
lemma Infinitesimal_mult: |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
354 |
fixes x y :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
355 |
shows "[|x \<in> Infinitesimal; y \<in> Infinitesimal|] ==> (x * y) \<in> Infinitesimal" |
20407 | 356 |
apply (rule InfinitesimalI) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
357 |
apply (subgoal_tac "hnorm (x * y) < 1 * r", simp only: mult_1) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
358 |
apply (rule hnorm_mult_less) |
20407 | 359 |
apply (simp_all add: InfinitesimalD) |
14370 | 360 |
done |
361 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
362 |
lemma Infinitesimal_HFinite_mult: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
363 |
fixes x y :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
364 |
shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal" |
20407 | 365 |
apply (rule InfinitesimalI) |
366 |
apply (drule HFiniteD, clarify) |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
367 |
apply (subgoal_tac "0 < t") |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
368 |
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp) |
20407 | 369 |
apply (subgoal_tac "0 < r / t") |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
370 |
apply (rule hnorm_mult_less) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
371 |
apply (simp add: InfinitesimalD Reals_divide) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
372 |
apply assumption |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
373 |
apply (simp only: divide_pos_pos) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
374 |
apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
14370 | 375 |
done |
376 |
||
20794 | 377 |
lemma Infinitesimal_HFinite_scaleHR: |
378 |
"[| x \<in> Infinitesimal; y \<in> HFinite |] ==> scaleHR x y \<in> Infinitesimal" |
|
379 |
apply (rule InfinitesimalI) |
|
380 |
apply (drule HFiniteD, clarify) |
|
381 |
apply (drule InfinitesimalD) |
|
382 |
apply (simp add: hnorm_scaleHR) |
|
383 |
apply (subgoal_tac "0 < t") |
|
384 |
apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp) |
|
385 |
apply (subgoal_tac "0 < r / t") |
|
386 |
apply (rule mult_strict_mono', simp_all) |
|
387 |
apply (simp only: divide_pos_pos) |
|
388 |
apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
|
389 |
done |
|
390 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
391 |
lemma Infinitesimal_HFinite_mult2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
392 |
fixes x y :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
393 |
shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
394 |
apply (rule InfinitesimalI) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
395 |
apply (drule HFiniteD, clarify) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
396 |
apply (subgoal_tac "0 < t") |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
397 |
apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
398 |
apply (subgoal_tac "0 < r / t") |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
399 |
apply (rule hnorm_mult_less) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
400 |
apply assumption |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
401 |
apply (simp add: InfinitesimalD Reals_divide) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
402 |
apply (simp only: divide_pos_pos) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
403 |
apply (erule order_le_less_trans [OF hnorm_ge_zero]) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
404 |
done |
14370 | 405 |
|
20794 | 406 |
lemma Infinitesimal_scaleR2: |
407 |
"x \<in> Infinitesimal ==> a *# x \<in> Infinitesimal" |
|
408 |
apply (case_tac "a = 0", simp) |
|
409 |
apply (rule InfinitesimalI) |
|
410 |
apply (drule InfinitesimalD) |
|
411 |
apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec) |
|
412 |
apply (simp add: Reals_eq_Standard) |
|
413 |
apply (simp add: divide_pos_pos) |
|
414 |
apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute) |
|
415 |
done |
|
416 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
417 |
lemma Compl_HFinite: "- HFinite = HInfinite" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
418 |
apply (auto simp add: HInfinite_def HFinite_def linorder_not_less) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
419 |
apply (rule_tac y="r + 1" in order_less_le_trans, simp) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
420 |
apply simp |
14370 | 421 |
done |
422 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
423 |
lemma HInfinite_inverse_Infinitesimal: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
424 |
fixes x :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
425 |
shows "x \<in> HInfinite ==> inverse x \<in> Infinitesimal" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
426 |
apply (rule InfinitesimalI) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
427 |
apply (subgoal_tac "x \<noteq> 0") |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
428 |
apply (rule inverse_less_imp_less) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
429 |
apply (simp add: nonzero_hnorm_inverse) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
430 |
apply (simp add: HInfinite_def Reals_inverse) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
431 |
apply assumption |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
432 |
apply (clarify, simp add: Compl_HFinite [symmetric]) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
433 |
done |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
434 |
|
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
435 |
lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite" |
20407 | 436 |
by (simp add: HInfinite_def) |
437 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
438 |
lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < hnorm x" |
20407 | 439 |
by (simp add: HInfinite_def) |
440 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
441 |
lemma HInfinite_mult: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
442 |
fixes x y :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
443 |
shows "[|x \<in> HInfinite; y \<in> HInfinite|] ==> (x*y) \<in> HInfinite" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
444 |
apply (rule HInfiniteI, simp only: hnorm_mult) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
445 |
apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1) |
20407 | 446 |
apply (case_tac "x = 0", simp add: HInfinite_def) |
447 |
apply (rule mult_strict_mono) |
|
448 |
apply (simp_all add: HInfiniteD) |
|
14370 | 449 |
done |
450 |
||
15229 | 451 |
lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y" |
452 |
by (auto dest: add_less_le_mono) |
|
453 |
||
14370 | 454 |
lemma HInfinite_add_ge_zero: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
455 |
"[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite" |
14370 | 456 |
by (auto intro!: hypreal_add_zero_less_le_mono |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
457 |
simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def) |
14370 | 458 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
459 |
lemma HInfinite_add_ge_zero2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
460 |
"[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
461 |
by (auto intro!: HInfinite_add_ge_zero simp add: add_commute) |
14370 | 462 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
463 |
lemma HInfinite_add_gt_zero: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
464 |
"[|(x::hypreal) \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite" |
14370 | 465 |
by (blast intro: HInfinite_add_ge_zero order_less_imp_le) |
466 |
||
467 |
lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)" |
|
468 |
by (simp add: HInfinite_def) |
|
469 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
470 |
lemma HInfinite_add_le_zero: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
471 |
"[|(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite" |
14370 | 472 |
apply (drule HInfinite_minus_iff [THEN iffD2]) |
473 |
apply (rule HInfinite_minus_iff [THEN iffD1]) |
|
474 |
apply (auto intro: HInfinite_add_ge_zero) |
|
475 |
done |
|
476 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
477 |
lemma HInfinite_add_lt_zero: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
478 |
"[|(x::hypreal) \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite" |
14370 | 479 |
by (blast intro: HInfinite_add_le_zero order_less_imp_le) |
480 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
481 |
lemma HFinite_sum_squares: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
482 |
fixes a b c :: "'a::real_normed_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
483 |
shows "[|a: HFinite; b: HFinite; c: HFinite|] |
14370 | 484 |
==> a*a + b*b + c*c \<in> HFinite" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
485 |
by (auto intro: HFinite_mult HFinite_add) |
14370 | 486 |
|
487 |
lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0" |
|
488 |
by auto |
|
489 |
||
490 |
lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0" |
|
491 |
by auto |
|
492 |
||
15229 | 493 |
lemma Infinitesimal_hrabs_iff [iff]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
494 |
"(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)" |
15003 | 495 |
by (auto simp add: abs_if) |
14370 | 496 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
497 |
lemma HFinite_diff_Infinitesimal_hrabs: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
498 |
"(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal" |
14370 | 499 |
by blast |
500 |
||
20743 | 501 |
lemma hnorm_le_Infinitesimal: |
502 |
"\<lbrakk>e \<in> Infinitesimal; hnorm x \<le> e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal" |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
503 |
by (auto simp add: Infinitesimal_def abs_less_iff) |
14370 | 504 |
|
20743 | 505 |
lemma hnorm_less_Infinitesimal: |
506 |
"\<lbrakk>e \<in> Infinitesimal; hnorm x < e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal" |
|
507 |
by (erule hnorm_le_Infinitesimal, erule order_less_imp_le) |
|
508 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
509 |
lemma hrabs_le_Infinitesimal: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
510 |
"[| e \<in> Infinitesimal; abs (x::hypreal) \<le> e |] ==> x \<in> Infinitesimal" |
20743 | 511 |
by (erule hnorm_le_Infinitesimal, simp) |
512 |
||
513 |
lemma hrabs_less_Infinitesimal: |
|
514 |
"[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal" |
|
515 |
by (erule hnorm_less_Infinitesimal, simp) |
|
14370 | 516 |
|
517 |
lemma Infinitesimal_interval: |
|
518 |
"[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |] |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
519 |
==> (x::hypreal) \<in> Infinitesimal" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
520 |
by (auto simp add: Infinitesimal_def abs_less_iff) |
14370 | 521 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
522 |
lemma Infinitesimal_interval2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
523 |
"[| e \<in> Infinitesimal; e' \<in> Infinitesimal; |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
524 |
e' \<le> x ; x \<le> e |] ==> (x::hypreal) \<in> Infinitesimal" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
525 |
by (auto intro: Infinitesimal_interval simp add: order_le_less) |
14370 | 526 |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
527 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
528 |
lemma lemma_Infinitesimal_hyperpow: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
529 |
"[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
530 |
apply (unfold Infinitesimal_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
531 |
apply (auto intro!: hyperpow_Suc_le_self2 |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
532 |
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
533 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
534 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
535 |
lemma Infinitesimal_hyperpow: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
536 |
"[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
537 |
apply (rule hrabs_le_Infinitesimal) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
538 |
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
539 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
540 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
541 |
lemma hrealpow_hyperpow_Infinitesimal_iff: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
542 |
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
543 |
by (simp only: hyperpow_hypnat_of_nat) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
544 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
545 |
lemma Infinitesimal_hrealpow: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
546 |
"[| (x::hypreal) \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
547 |
by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
548 |
|
14370 | 549 |
lemma not_Infinitesimal_mult: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
550 |
fixes x y :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
551 |
shows "[| x \<notin> Infinitesimal; y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal" |
20407 | 552 |
apply (unfold Infinitesimal_def, clarify, rename_tac r s) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
553 |
apply (simp only: linorder_not_less hnorm_mult) |
20407 | 554 |
apply (drule_tac x = "r * s" in bspec) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
555 |
apply (fast intro: Reals_mult) |
20407 | 556 |
apply (drule mp, blast intro: mult_pos_pos) |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
557 |
apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono) |
20407 | 558 |
apply (simp_all (no_asm_simp)) |
14370 | 559 |
done |
560 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
561 |
lemma Infinitesimal_mult_disj: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
562 |
fixes x y :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
563 |
shows "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal" |
14370 | 564 |
apply (rule ccontr) |
565 |
apply (drule de_Morgan_disj [THEN iffD1]) |
|
566 |
apply (fast dest: not_Infinitesimal_mult) |
|
567 |
done |
|
568 |
||
569 |
lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0" |
|
570 |
by blast |
|
571 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
572 |
lemma HFinite_Infinitesimal_diff_mult: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
573 |
fixes x y :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
574 |
shows "[| x \<in> HFinite - Infinitesimal; |
14370 | 575 |
y \<in> HFinite - Infinitesimal |
576 |
|] ==> (x*y) \<in> HFinite - Infinitesimal" |
|
577 |
apply clarify |
|
578 |
apply (blast dest: HFinite_mult not_Infinitesimal_mult) |
|
579 |
done |
|
580 |
||
581 |
lemma Infinitesimal_subset_HFinite: |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
582 |
"Infinitesimal \<subseteq> HFinite" |
14370 | 583 |
apply (simp add: Infinitesimal_def HFinite_def, auto) |
584 |
apply (rule_tac x = 1 in bexI, auto) |
|
585 |
done |
|
586 |
||
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
587 |
lemma Infinitesimal_star_of_mult: |
21783 | 588 |
fixes x :: "'a::real_normed_algebra star" |
589 |
shows "x \<in> Infinitesimal ==> x * star_of r \<in> Infinitesimal" |
|
590 |
by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult]) |
|
14370 | 591 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
592 |
lemma Infinitesimal_star_of_mult2: |
21783 | 593 |
fixes x :: "'a::real_normed_algebra star" |
594 |
shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal" |
|
595 |
by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2]) |
|
14370 | 596 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
597 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
598 |
subsection{*The Infinitely Close Relation*} |
14370 | 599 |
|
600 |
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)" |
|
601 |
by (simp add: Infinitesimal_def approx_def) |
|
602 |
||
20563 | 603 |
lemma approx_minus_iff: " (x @= y) = (x - y @= 0)" |
14370 | 604 |
by (simp add: approx_def) |
605 |
||
606 |
lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)" |
|
20563 | 607 |
by (simp add: approx_def diff_minus add_commute) |
14370 | 608 |
|
15229 | 609 |
lemma approx_refl [iff]: "x @= x" |
14370 | 610 |
by (simp add: approx_def Infinitesimal_def) |
611 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
612 |
lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
613 |
by (simp add: add_commute) |
14477 | 614 |
|
14370 | 615 |
lemma approx_sym: "x @= y ==> y @= x" |
616 |
apply (simp add: approx_def) |
|
20563 | 617 |
apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
618 |
apply simp |
|
14370 | 619 |
done |
620 |
||
621 |
lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z" |
|
622 |
apply (simp add: approx_def) |
|
20563 | 623 |
apply (drule (1) Infinitesimal_add) |
624 |
apply (simp add: diff_def) |
|
14370 | 625 |
done |
626 |
||
627 |
lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s" |
|
628 |
by (blast intro: approx_sym approx_trans) |
|
629 |
||
630 |
lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s" |
|
631 |
by (blast intro: approx_sym approx_trans) |
|
632 |
||
633 |
lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)" |
|
634 |
by (blast intro: approx_sym) |
|
635 |
||
636 |
lemma zero_approx_reorient: "(0 @= x) = (x @= 0)" |
|
637 |
by (blast intro: approx_sym) |
|
638 |
||
639 |
lemma one_approx_reorient: "(1 @= x) = (x @= 1)" |
|
640 |
by (blast intro: approx_sym) |
|
10751 | 641 |
|
642 |
||
19765 | 643 |
ML {* |
644 |
local |
|
14370 | 645 |
(*** re-orientation, following HOL/Integ/Bin.ML |
646 |
We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well! |
|
647 |
***) |
|
648 |
||
649 |
(*reorientation simprules using ==, for the following simproc*) |
|
19765 | 650 |
val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection; |
651 |
val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection; |
|
652 |
val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection |
|
14370 | 653 |
|
654 |
(*reorientation simplification procedure: reorients (polymorphic) |
|
655 |
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
|
656 |
fun reorient_proc sg _ (_ $ t $ u) = |
|
657 |
case u of |
|
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20652
diff
changeset
|
658 |
Const("HOL.zero", _) => NONE |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20652
diff
changeset
|
659 |
| Const("HOL.one", _) => NONE |
15531 | 660 |
| Const("Numeral.number_of", _) $ _ => NONE |
661 |
| _ => SOME (case t of |
|
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20652
diff
changeset
|
662 |
Const("HOL.zero", _) => meta_zero_approx_reorient |
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20652
diff
changeset
|
663 |
| Const("HOL.one", _) => meta_one_approx_reorient |
14370 | 664 |
| Const("Numeral.number_of", _) $ _ => |
665 |
meta_number_of_approx_reorient); |
|
666 |
||
19765 | 667 |
in |
14370 | 668 |
val approx_reorient_simproc = |
20485 | 669 |
Int_Numeral_Base_Simprocs.prep_simproc |
14370 | 670 |
("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc); |
19765 | 671 |
end; |
14370 | 672 |
|
673 |
Addsimprocs [approx_reorient_simproc]; |
|
674 |
*} |
|
675 |
||
676 |
lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)" |
|
20563 | 677 |
by (simp add: approx_minus_iff [symmetric] mem_infmal_iff) |
14370 | 678 |
|
679 |
lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" |
|
680 |
apply (simp add: monad_def) |
|
681 |
apply (auto dest: approx_sym elim!: approx_trans equalityCE) |
|
682 |
done |
|
683 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
684 |
lemma Infinitesimal_approx: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
685 |
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y" |
14370 | 686 |
apply (simp add: mem_infmal_iff) |
687 |
apply (blast intro: approx_trans approx_sym) |
|
688 |
done |
|
689 |
||
690 |
lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d" |
|
691 |
proof (unfold approx_def) |
|
20563 | 692 |
assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal" |
693 |
have "a + c - (b + d) = (a - b) + (c - d)" by simp |
|
14370 | 694 |
also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add) |
20563 | 695 |
finally show "a + c - (b + d) \<in> Infinitesimal" . |
14370 | 696 |
qed |
697 |
||
698 |
lemma approx_minus: "a @= b ==> -a @= -b" |
|
699 |
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) |
|
700 |
apply (drule approx_minus_iff [THEN iffD1]) |
|
20563 | 701 |
apply (simp add: add_commute diff_def) |
14370 | 702 |
done |
703 |
||
704 |
lemma approx_minus2: "-a @= -b ==> a @= b" |
|
705 |
by (auto dest: approx_minus) |
|
706 |
||
15229 | 707 |
lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)" |
14370 | 708 |
by (blast intro: approx_minus approx_minus2) |
709 |
||
710 |
lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d" |
|
711 |
by (blast intro!: approx_add approx_minus) |
|
712 |
||
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
713 |
lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
714 |
by (simp only: diff_minus approx_add approx_minus) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
715 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
716 |
lemma approx_mult1: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
717 |
fixes a b c :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
718 |
shows "[| a @= b; c: HFinite|] ==> a*c @= b*c" |
20563 | 719 |
by (simp add: approx_def Infinitesimal_HFinite_mult |
720 |
left_diff_distrib [symmetric]) |
|
14370 | 721 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
722 |
lemma approx_mult2: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
723 |
fixes a b c :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
724 |
shows "[|a @= b; c: HFinite|] ==> c*a @= c*b" |
20563 | 725 |
by (simp add: approx_def Infinitesimal_HFinite_mult2 |
726 |
right_diff_distrib [symmetric]) |
|
14370 | 727 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
728 |
lemma approx_mult_subst: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
729 |
fixes u v x y :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
730 |
shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y" |
14370 | 731 |
by (blast intro: approx_mult2 approx_trans) |
732 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
733 |
lemma approx_mult_subst2: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
734 |
fixes u v x y :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
735 |
shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v" |
14370 | 736 |
by (blast intro: approx_mult1 approx_trans) |
737 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
738 |
lemma approx_mult_subst_star_of: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
739 |
fixes u x y :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
740 |
shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
741 |
by (auto intro: approx_mult_subst2) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
742 |
|
14370 | 743 |
lemma approx_eq_imp: "a = b ==> a @= b" |
744 |
by (simp add: approx_def) |
|
745 |
||
746 |
lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x" |
|
747 |
by (blast intro: Infinitesimal_minus_iff [THEN iffD2] |
|
748 |
mem_infmal_iff [THEN iffD1] approx_trans2) |
|
749 |
||
20563 | 750 |
lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)" |
14370 | 751 |
by (simp add: approx_def) |
752 |
||
753 |
lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)" |
|
754 |
by (force simp add: bex_Infinitesimal_iff [symmetric]) |
|
755 |
||
756 |
lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z" |
|
757 |
apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
|
758 |
apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
759 |
apply (auto simp add: add_assoc [symmetric]) |
14370 | 760 |
done |
761 |
||
762 |
lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y" |
|
763 |
apply (rule bex_Infinitesimal_iff [THEN iffD1]) |
|
764 |
apply (drule Infinitesimal_minus_iff [THEN iffD2]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
765 |
apply (auto simp add: add_assoc [symmetric]) |
14370 | 766 |
done |
767 |
||
768 |
lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
769 |
by (auto dest: Infinitesimal_add_approx_self simp add: add_commute) |
14370 | 770 |
|
771 |
lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y" |
|
772 |
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) |
|
773 |
||
774 |
lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z" |
|
775 |
apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) |
|
776 |
apply (erule approx_trans3 [THEN approx_sym], assumption) |
|
777 |
done |
|
778 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
779 |
lemma Infinitesimal_add_right_cancel: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
780 |
"[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z" |
14370 | 781 |
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) |
782 |
apply (erule approx_trans3 [THEN approx_sym]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
783 |
apply (simp add: add_commute) |
14370 | 784 |
apply (erule approx_sym) |
785 |
done |
|
786 |
||
787 |
lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" |
|
788 |
apply (drule approx_minus_iff [THEN iffD1]) |
|
15539 | 789 |
apply (simp add: approx_minus_iff [symmetric] add_ac) |
14370 | 790 |
done |
791 |
||
792 |
lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" |
|
793 |
apply (rule approx_add_left_cancel) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
794 |
apply (simp add: add_commute) |
14370 | 795 |
done |
796 |
||
797 |
lemma approx_add_mono1: "b @= c ==> d + b @= d + c" |
|
798 |
apply (rule approx_minus_iff [THEN iffD2]) |
|
15539 | 799 |
apply (simp add: approx_minus_iff [symmetric] add_ac) |
14370 | 800 |
done |
801 |
||
802 |
lemma approx_add_mono2: "b @= c ==> b + a @= c + a" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
803 |
by (simp add: add_commute approx_add_mono1) |
14370 | 804 |
|
15229 | 805 |
lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)" |
14370 | 806 |
by (fast elim: approx_add_left_cancel approx_add_mono1) |
807 |
||
15229 | 808 |
lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
809 |
by (simp add: add_commute) |
14370 | 810 |
|
811 |
lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite" |
|
812 |
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) |
|
813 |
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) |
|
814 |
apply (drule HFinite_add) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
815 |
apply (auto simp add: add_assoc) |
14370 | 816 |
done |
817 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
818 |
lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite" |
14370 | 819 |
by (rule approx_sym [THEN [2] approx_HFinite], auto) |
820 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
821 |
lemma approx_mult_HFinite: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
822 |
fixes a b c d :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
823 |
shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d" |
14370 | 824 |
apply (rule approx_trans) |
825 |
apply (rule_tac [2] approx_mult2) |
|
826 |
apply (rule approx_mult1) |
|
827 |
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
|
828 |
done |
|
829 |
||
20794 | 830 |
lemma scaleHR_left_diff_distrib: |
831 |
"\<And>a b x. scaleHR (a - b) x = scaleHR a x - scaleHR b x" |
|
832 |
by transfer (rule scaleR_left_diff_distrib) |
|
833 |
||
834 |
lemma approx_scaleR1: |
|
835 |
"[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *# c" |
|
836 |
apply (unfold approx_def) |
|
837 |
apply (drule (1) Infinitesimal_HFinite_scaleHR) |
|
838 |
apply (simp only: scaleHR_left_diff_distrib) |
|
839 |
apply (simp add: scaleHR_def star_scaleR_def [symmetric]) |
|
840 |
done |
|
841 |
||
842 |
lemma approx_scaleR2: |
|
843 |
"a @= b ==> c *# a @= c *# b" |
|
844 |
by (simp add: approx_def Infinitesimal_scaleR2 |
|
845 |
scaleR_right_diff_distrib [symmetric]) |
|
846 |
||
847 |
lemma approx_scaleR_HFinite: |
|
848 |
"[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *# d" |
|
849 |
apply (rule approx_trans) |
|
850 |
apply (rule_tac [2] approx_scaleR2) |
|
851 |
apply (rule approx_scaleR1) |
|
852 |
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) |
|
853 |
done |
|
854 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
855 |
lemma approx_mult_star_of: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
856 |
fixes a c :: "'a::real_normed_algebra star" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
857 |
shows "[|a @= star_of b; c @= star_of d |] |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
858 |
==> a*c @= star_of b*star_of d" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
859 |
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
860 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
861 |
lemma approx_SReal_mult_cancel_zero: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
862 |
"[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
863 |
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
864 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14370 | 865 |
done |
866 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
867 |
lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0" |
14370 | 868 |
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) |
869 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
870 |
lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0" |
14370 | 871 |
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) |
872 |
||
15229 | 873 |
lemma approx_mult_SReal_zero_cancel_iff [simp]: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
874 |
"[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)" |
14370 | 875 |
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) |
876 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
877 |
lemma approx_SReal_mult_cancel: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
878 |
"[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
879 |
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
880 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14370 | 881 |
done |
882 |
||
15229 | 883 |
lemma approx_SReal_mult_cancel_iff1 [simp]: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
884 |
"[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)" |
15229 | 885 |
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] |
886 |
intro: approx_SReal_mult_cancel) |
|
14370 | 887 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
888 |
lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z" |
14370 | 889 |
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) |
890 |
apply (rule_tac x = "g+y-z" in bexI) |
|
891 |
apply (simp (no_asm)) |
|
892 |
apply (rule Infinitesimal_interval2) |
|
893 |
apply (rule_tac [2] Infinitesimal_zero, auto) |
|
894 |
done |
|
895 |
||
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
896 |
lemma approx_hnorm: |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
897 |
fixes x y :: "'a::real_normed_vector star" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
898 |
shows "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
899 |
proof (unfold approx_def) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
900 |
assume "x - y \<in> Infinitesimal" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
901 |
hence 1: "hnorm (x - y) \<in> Infinitesimal" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
902 |
by (simp only: Infinitesimal_hnorm_iff) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
903 |
moreover have 2: "(0::real star) \<in> Infinitesimal" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
904 |
by (rule Infinitesimal_zero) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
905 |
moreover have 3: "0 \<le> \<bar>hnorm x - hnorm y\<bar>" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
906 |
by (rule abs_ge_zero) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
907 |
moreover have 4: "\<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
908 |
by (rule hnorm_triangle_ineq3) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
909 |
ultimately have "\<bar>hnorm x - hnorm y\<bar> \<in> Infinitesimal" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
910 |
by (rule Infinitesimal_interval2) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
911 |
thus "hnorm x - hnorm y \<in> Infinitesimal" |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
912 |
by (simp only: Infinitesimal_hrabs_iff) |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
913 |
qed |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
914 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
915 |
|
15539 | 916 |
subsection{* Zero is the Only Infinitesimal that is also a Real*} |
14370 | 917 |
|
918 |
lemma Infinitesimal_less_SReal: |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
919 |
"[| (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x" |
14370 | 920 |
apply (simp add: Infinitesimal_def) |
921 |
apply (rule abs_ge_self [THEN order_le_less_trans], auto) |
|
922 |
done |
|
923 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
924 |
lemma Infinitesimal_less_SReal2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
925 |
"(y::hypreal) \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r" |
14370 | 926 |
by (blast intro: Infinitesimal_less_SReal) |
927 |
||
928 |
lemma SReal_not_Infinitesimal: |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
929 |
"[| 0 < y; (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal" |
14370 | 930 |
apply (simp add: Infinitesimal_def) |
15003 | 931 |
apply (auto simp add: abs_if) |
14370 | 932 |
done |
933 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
934 |
lemma SReal_minus_not_Infinitesimal: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
935 |
"[| y < 0; (y::hypreal) \<in> Reals |] ==> y \<notin> Infinitesimal" |
14370 | 936 |
apply (subst Infinitesimal_minus_iff [symmetric]) |
937 |
apply (rule SReal_not_Infinitesimal, auto) |
|
938 |
done |
|
939 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
940 |
lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}" |
14370 | 941 |
apply auto |
942 |
apply (cut_tac x = x and y = 0 in linorder_less_linear) |
|
943 |
apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) |
|
944 |
done |
|
945 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
946 |
lemma SReal_Infinitesimal_zero: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
947 |
"[| (x::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0" |
14370 | 948 |
by (cut_tac SReal_Int_Infinitesimal_zero, blast) |
949 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
950 |
lemma SReal_HFinite_diff_Infinitesimal: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
951 |
"[| (x::hypreal) \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal" |
14370 | 952 |
by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD]) |
953 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
954 |
lemma hypreal_of_real_HFinite_diff_Infinitesimal: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
955 |
"hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal" |
14370 | 956 |
by (rule SReal_HFinite_diff_Infinitesimal, auto) |
957 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
958 |
lemma star_of_Infinitesimal_iff_0 [iff]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
959 |
"(star_of x \<in> Infinitesimal) = (x = 0)" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
960 |
apply (auto simp add: Infinitesimal_def) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
961 |
apply (drule_tac x="hnorm (star_of x)" in bspec) |
20728 | 962 |
apply (simp add: SReal_def) |
963 |
apply (rule_tac x="norm x" in exI, simp) |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
964 |
apply simp |
14370 | 965 |
done |
966 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
967 |
lemma star_of_HFinite_diff_Infinitesimal: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
968 |
"x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
969 |
by simp |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
970 |
|
15229 | 971 |
lemma number_of_not_Infinitesimal [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
972 |
"number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
973 |
by (fast dest: Reals_number_of [THEN SReal_Infinitesimal_zero]) |
14370 | 974 |
|
975 |
(*again: 1 is a special case, but not 0 this time*) |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
976 |
lemma one_not_Infinitesimal [simp]: |
20633 | 977 |
"(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
978 |
apply (simp only: star_one_def star_of_Infinitesimal_iff_0) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
979 |
apply simp |
14370 | 980 |
done |
981 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
982 |
lemma approx_SReal_not_zero: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
983 |
"[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
14370 | 984 |
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp) |
985 |
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) |
|
986 |
done |
|
987 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
988 |
lemma HFinite_diff_Infinitesimal_approx: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
989 |
"[| x @= y; y \<in> HFinite - Infinitesimal |] |
14370 | 990 |
==> x \<in> HFinite - Infinitesimal" |
991 |
apply (auto intro: approx_sym [THEN [2] approx_HFinite] |
|
992 |
simp add: mem_infmal_iff) |
|
993 |
apply (drule approx_trans3, assumption) |
|
994 |
apply (blast dest: approx_sym) |
|
995 |
done |
|
996 |
||
997 |
(*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the |
|
998 |
HFinite premise.*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
999 |
lemma Infinitesimal_ratio: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1000 |
fixes x y :: "'a::{real_normed_div_algebra,field} star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1001 |
shows "[| y \<noteq> 0; y \<in> Infinitesimal; x/y \<in> HFinite |] |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1002 |
==> x \<in> Infinitesimal" |
14370 | 1003 |
apply (drule Infinitesimal_HFinite_mult2, assumption) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1004 |
apply (simp add: divide_inverse mult_assoc) |
14370 | 1005 |
done |
1006 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1007 |
lemma Infinitesimal_SReal_divide: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1008 |
"[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal" |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14420
diff
changeset
|
1009 |
apply (simp add: divide_inverse) |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1010 |
apply (auto intro!: Infinitesimal_HFinite_mult |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1011 |
dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1012 |
done |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1013 |
|
14370 | 1014 |
(*------------------------------------------------------------------ |
1015 |
Standard Part Theorem: Every finite x: R* is infinitely |
|
1016 |
close to a unique real number (i.e a member of Reals) |
|
1017 |
------------------------------------------------------------------*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1018 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1019 |
subsection{* Uniqueness: Two Infinitely Close Reals are Equal*} |
14370 | 1020 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1021 |
lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1022 |
apply safe |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1023 |
apply (simp add: approx_def) |
20563 | 1024 |
apply (simp only: star_of_diff [symmetric]) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1025 |
apply (simp only: star_of_Infinitesimal_iff_0) |
20563 | 1026 |
apply simp |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1027 |
done |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1028 |
|
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1029 |
lemma SReal_approx_iff: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1030 |
"[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)" |
14370 | 1031 |
apply auto |
1032 |
apply (simp add: approx_def) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1033 |
apply (drule (1) Reals_diff) |
20563 | 1034 |
apply (drule (1) SReal_Infinitesimal_zero) |
1035 |
apply simp |
|
14370 | 1036 |
done |
1037 |
||
15229 | 1038 |
lemma number_of_approx_iff [simp]: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1039 |
"(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1040 |
(number_of v = (number_of w :: 'a))" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1041 |
apply (unfold star_number_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1042 |
apply (rule star_of_approx_iff) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1043 |
done |
14370 | 1044 |
|
1045 |
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1046 |
lemma [simp]: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1047 |
"(number_of w @= (0::'a::{number,real_normed_vector} star)) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1048 |
(number_of w = (0::'a))" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1049 |
"((0::'a::{number,real_normed_vector} star) @= number_of w) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1050 |
(number_of w = (0::'a))" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1051 |
"(number_of w @= (1::'b::{number,one,real_normed_vector} star)) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1052 |
(number_of w = (1::'b))" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1053 |
"((1::'b::{number,one,real_normed_vector} star) @= number_of w) = |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1054 |
(number_of w = (1::'b))" |
20633 | 1055 |
"~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))" |
1056 |
"~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))" |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1057 |
apply (unfold star_number_def star_zero_def star_one_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1058 |
apply (unfold star_of_approx_iff) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1059 |
by (auto intro: sym) |
14370 | 1060 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1061 |
lemma star_of_approx_number_of_iff [simp]: |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1062 |
"(star_of k @= number_of w) = (k = number_of w)" |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1063 |
by (subst star_of_approx_iff [symmetric], auto) |
14370 | 1064 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1065 |
lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)" |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1066 |
by (simp_all add: star_of_approx_iff [symmetric]) |
14370 | 1067 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1068 |
lemma star_of_approx_one_iff [simp]: "(star_of k @= 1) = (k = 1)" |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1069 |
by (simp_all add: star_of_approx_iff [symmetric]) |
14370 | 1070 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1071 |
lemma approx_unique_real: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1072 |
"[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s" |
14370 | 1073 |
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) |
1074 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1075 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1076 |
subsection{* Existence of Unique Real Infinitely Close*} |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1077 |
|
20721 | 1078 |
subsubsection{*Lifting of the Ub and Lub Properties*} |
1079 |
||
1080 |
lemma hypreal_of_real_isUb_iff: |
|
1081 |
"(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = |
|
1082 |
(isUb (UNIV :: real set) Q Y)" |
|
1083 |
by (simp add: isUb_def setle_def) |
|
1084 |
||
1085 |
lemma hypreal_of_real_isLub1: |
|
1086 |
"isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) |
|
1087 |
==> isLub (UNIV :: real set) Q Y" |
|
1088 |
apply (simp add: isLub_def leastP_def) |
|
1089 |
apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2] |
|
1090 |
simp add: hypreal_of_real_isUb_iff setge_def) |
|
1091 |
done |
|
1092 |
||
1093 |
lemma hypreal_of_real_isLub2: |
|
1094 |
"isLub (UNIV :: real set) Q Y |
|
1095 |
==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)" |
|
1096 |
apply (simp add: isLub_def leastP_def) |
|
1097 |
apply (auto simp add: hypreal_of_real_isUb_iff setge_def) |
|
1098 |
apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE]) |
|
1099 |
prefer 2 apply assumption |
|
1100 |
apply (drule_tac x = xa in spec) |
|
1101 |
apply (auto simp add: hypreal_of_real_isUb_iff) |
|
1102 |
done |
|
1103 |
||
1104 |
lemma hypreal_of_real_isLub_iff: |
|
1105 |
"(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) = |
|
1106 |
(isLub (UNIV :: real set) Q Y)" |
|
1107 |
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2) |
|
1108 |
||
1109 |
lemma lemma_isUb_hypreal_of_real: |
|
1110 |
"isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)" |
|
1111 |
by (auto simp add: SReal_iff isUb_def) |
|
1112 |
||
1113 |
lemma lemma_isLub_hypreal_of_real: |
|
1114 |
"isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)" |
|
1115 |
by (auto simp add: isLub_def leastP_def isUb_def SReal_iff) |
|
1116 |
||
1117 |
lemma lemma_isLub_hypreal_of_real2: |
|
1118 |
"\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y" |
|
1119 |
by (auto simp add: isLub_def leastP_def isUb_def) |
|
1120 |
||
1121 |
lemma SReal_complete: |
|
1122 |
"[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y |] |
|
1123 |
==> \<exists>t::hypreal. isLub Reals P t" |
|
1124 |
apply (frule SReal_hypreal_of_real_image) |
|
1125 |
apply (auto, drule lemma_isUb_hypreal_of_real) |
|
1126 |
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 |
|
1127 |
simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff) |
|
1128 |
done |
|
1129 |
||
14370 | 1130 |
(* lemma about lubs *) |
1131 |
lemma hypreal_isLub_unique: |
|
1132 |
"[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)" |
|
1133 |
apply (frule isLub_isUb) |
|
1134 |
apply (frule_tac x = y in isLub_isUb) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1135 |
apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
14370 | 1136 |
done |
1137 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1138 |
lemma lemma_st_part_ub: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1139 |
"(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u" |
14370 | 1140 |
apply (drule HFiniteD, safe) |
1141 |
apply (rule exI, rule isUbI) |
|
1142 |
apply (auto intro: setleI isUbI simp add: abs_less_iff) |
|
1143 |
done |
|
1144 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1145 |
lemma lemma_st_part_nonempty: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1146 |
"(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}" |
14370 | 1147 |
apply (drule HFiniteD, safe) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1148 |
apply (drule Reals_minus) |
14370 | 1149 |
apply (rule_tac x = "-t" in exI) |
1150 |
apply (auto simp add: abs_less_iff) |
|
1151 |
done |
|
1152 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1153 |
lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals" |
14370 | 1154 |
by auto |
1155 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1156 |
lemma lemma_st_part_lub: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1157 |
"(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t" |
14370 | 1158 |
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset) |
1159 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1160 |
lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)" |
14370 | 1161 |
apply safe |
1162 |
apply (drule_tac c = "-t" in add_left_mono) |
|
1163 |
apply (drule_tac [2] c = t in add_left_mono) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1164 |
apply (auto simp add: add_assoc [symmetric]) |
14370 | 1165 |
done |
1166 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1167 |
lemma lemma_st_part_le1: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1168 |
"[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t; |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1169 |
r \<in> Reals; 0 < r |] ==> x \<le> t + r" |
14370 | 1170 |
apply (frule isLubD1a) |
1171 |
apply (rule ccontr, drule linorder_not_le [THEN iffD2]) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1172 |
apply (drule (1) Reals_add) |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1173 |
apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto) |
14370 | 1174 |
done |
1175 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1176 |
lemma hypreal_setle_less_trans: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1177 |
"[| S *<= (x::hypreal); x < y |] ==> S *<= y" |
14370 | 1178 |
apply (simp add: setle_def) |
1179 |
apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le) |
|
1180 |
done |
|
1181 |
||
1182 |
lemma hypreal_gt_isUb: |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1183 |
"[| isUb R S (x::hypreal); x < y; y \<in> R |] ==> isUb R S y" |
14370 | 1184 |
apply (simp add: isUb_def) |
1185 |
apply (blast intro: hypreal_setle_less_trans) |
|
1186 |
done |
|
1187 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1188 |
lemma lemma_st_part_gt_ub: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1189 |
"[| (x::hypreal) \<in> HFinite; x < y; y \<in> Reals |] |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1190 |
==> isUb Reals {s. s \<in> Reals & s < x} y" |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1191 |
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) |
14370 | 1192 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1193 |
lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)" |
14370 | 1194 |
apply (drule_tac c = "-t" in add_left_mono) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1195 |
apply (auto simp add: add_assoc [symmetric]) |
14370 | 1196 |
done |
1197 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1198 |
lemma lemma_st_part_le2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1199 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1200 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1201 |
r \<in> Reals; 0 < r |] |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1202 |
==> t + -r \<le> x" |
14370 | 1203 |
apply (frule isLubD1a) |
1204 |
apply (rule ccontr, drule linorder_not_le [THEN iffD1]) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1205 |
apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption) |
14370 | 1206 |
apply (drule lemma_st_part_gt_ub, assumption+) |
1207 |
apply (drule isLub_le_isUb, assumption) |
|
1208 |
apply (drule lemma_minus_le_zero) |
|
1209 |
apply (auto dest: order_less_le_trans) |
|
1210 |
done |
|
1211 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1212 |
lemma lemma_st_part1a: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1213 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1214 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1215 |
r \<in> Reals; 0 < r |] |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1216 |
==> x + -t \<le> r" |
15229 | 1217 |
apply (subgoal_tac "x \<le> t+r") |
1218 |
apply (auto intro: lemma_st_part_le1) |
|
1219 |
done |
|
14370 | 1220 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1221 |
lemma lemma_st_part2a: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1222 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1223 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1224 |
r \<in> Reals; 0 < r |] |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1225 |
==> -(x + -t) \<le> r" |
15229 | 1226 |
apply (subgoal_tac "(t + -r \<le> x)") |
1227 |
apply (auto intro: lemma_st_part_le2) |
|
14370 | 1228 |
done |
1229 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1230 |
lemma lemma_SReal_ub: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1231 |
"(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x" |
14370 | 1232 |
by (auto intro: isUbI setleI order_less_imp_le) |
1233 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1234 |
lemma lemma_SReal_lub: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1235 |
"(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x" |
14370 | 1236 |
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI) |
1237 |
apply (frule isUbD2a) |
|
1238 |
apply (rule_tac x = x and y = y in linorder_cases) |
|
1239 |
apply (auto intro!: order_less_imp_le) |
|
1240 |
apply (drule SReal_dense, assumption, assumption, safe) |
|
1241 |
apply (drule_tac y = r in isUbD) |
|
1242 |
apply (auto dest: order_less_le_trans) |
|
1243 |
done |
|
1244 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1245 |
lemma lemma_st_part_not_eq1: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1246 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1247 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1248 |
r \<in> Reals; 0 < r |] |
|
1249 |
==> x + -t \<noteq> r" |
|
1250 |
apply auto |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1251 |
apply (frule isLubD1a [THEN Reals_minus]) |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1252 |
apply (drule Reals_add_cancel, assumption) |
14370 | 1253 |
apply (drule_tac x = x in lemma_SReal_lub) |
1254 |
apply (drule hypreal_isLub_unique, assumption, auto) |
|
1255 |
done |
|
1256 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1257 |
lemma lemma_st_part_not_eq2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1258 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1259 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1260 |
r \<in> Reals; 0 < r |] |
|
1261 |
==> -(x + -t) \<noteq> r" |
|
15539 | 1262 |
apply (auto) |
14370 | 1263 |
apply (frule isLubD1a) |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1264 |
apply (drule Reals_add_cancel, assumption) |
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1265 |
apply (drule_tac a = "-x" in Reals_minus, simp) |
14370 | 1266 |
apply (drule_tac x = x in lemma_SReal_lub) |
1267 |
apply (drule hypreal_isLub_unique, assumption, auto) |
|
1268 |
done |
|
1269 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1270 |
lemma lemma_st_part_major: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1271 |
"[| (x::hypreal) \<in> HFinite; |
14370 | 1272 |
isLub Reals {s. s \<in> Reals & s < x} t; |
1273 |
r \<in> Reals; 0 < r |] |
|
20563 | 1274 |
==> abs (x - t) < r" |
14370 | 1275 |
apply (frule lemma_st_part1a) |
1276 |
apply (frule_tac [4] lemma_st_part2a, auto) |
|
1277 |
apply (drule order_le_imp_less_or_eq)+ |
|
1278 |
apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff) |
|
1279 |
done |
|
1280 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1281 |
lemma lemma_st_part_major2: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1282 |
"[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |] |
20563 | 1283 |
==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1284 |
by (blast dest!: lemma_st_part_major) |
14370 | 1285 |
|
15229 | 1286 |
|
1287 |
text{*Existence of real and Standard Part Theorem*} |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1288 |
lemma lemma_st_part_Ex: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1289 |
"(x::hypreal) \<in> HFinite |
20563 | 1290 |
==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r" |
14370 | 1291 |
apply (frule lemma_st_part_lub, safe) |
1292 |
apply (frule isLubD1a) |
|
1293 |
apply (blast dest: lemma_st_part_major2) |
|
1294 |
done |
|
1295 |
||
1296 |
lemma st_part_Ex: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1297 |
"(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t" |
14370 | 1298 |
apply (simp add: approx_def Infinitesimal_def) |
1299 |
apply (drule lemma_st_part_Ex, auto) |
|
1300 |
done |
|
1301 |
||
15229 | 1302 |
text{*There is a unique real infinitely close*} |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1303 |
lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t" |
14370 | 1304 |
apply (drule st_part_Ex, safe) |
1305 |
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) |
|
1306 |
apply (auto intro!: approx_unique_real) |
|
1307 |
done |
|
1308 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1309 |
subsection{* Finite, Infinite and Infinitesimal*} |
14370 | 1310 |
|
15229 | 1311 |
lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" |
14370 | 1312 |
apply (simp add: HFinite_def HInfinite_def) |
1313 |
apply (auto dest: order_less_trans) |
|
1314 |
done |
|
1315 |
||
1316 |
lemma HFinite_not_HInfinite: |
|
1317 |
assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite" |
|
1318 |
proof |
|
1319 |
assume x': "x \<in> HInfinite" |
|
1320 |
with x have "x \<in> HFinite \<inter> HInfinite" by blast |
|
1321 |
thus False by auto |
|
1322 |
qed |
|
1323 |
||
1324 |
lemma not_HFinite_HInfinite: "x\<notin> HFinite ==> x \<in> HInfinite" |
|
1325 |
apply (simp add: HInfinite_def HFinite_def, auto) |
|
1326 |
apply (drule_tac x = "r + 1" in bspec) |
|
15539 | 1327 |
apply (auto) |
14370 | 1328 |
done |
1329 |
||
1330 |
lemma HInfinite_HFinite_disj: "x \<in> HInfinite | x \<in> HFinite" |
|
1331 |
by (blast intro: not_HFinite_HInfinite) |
|
1332 |
||
1333 |
lemma HInfinite_HFinite_iff: "(x \<in> HInfinite) = (x \<notin> HFinite)" |
|
1334 |
by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite) |
|
1335 |
||
1336 |
lemma HFinite_HInfinite_iff: "(x \<in> HFinite) = (x \<notin> HInfinite)" |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1337 |
by (simp add: HInfinite_HFinite_iff) |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1338 |
|
14370 | 1339 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1340 |
lemma HInfinite_diff_HFinite_Infinitesimal_disj: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1341 |
"x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal" |
14370 | 1342 |
by (fast intro: not_HFinite_HInfinite) |
1343 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1344 |
lemma HFinite_inverse: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1345 |
fixes x :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1346 |
shows "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite" |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1347 |
apply (subgoal_tac "x \<noteq> 0") |
14370 | 1348 |
apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj) |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1349 |
apply (auto dest!: HInfinite_inverse_Infinitesimal |
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1350 |
simp add: nonzero_inverse_inverse_eq) |
14370 | 1351 |
done |
1352 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1353 |
lemma HFinite_inverse2: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1354 |
fixes x :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1355 |
shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite" |
14370 | 1356 |
by (blast intro: HFinite_inverse) |
1357 |
||
1358 |
(* stronger statement possible in fact *) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1359 |
lemma Infinitesimal_inverse_HFinite: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1360 |
fixes x :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1361 |
shows "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite" |
14370 | 1362 |
apply (drule HInfinite_diff_HFinite_Infinitesimal_disj) |
1363 |
apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD]) |
|
1364 |
done |
|
1365 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1366 |
lemma HFinite_not_Infinitesimal_inverse: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1367 |
fixes x :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1368 |
shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal" |
14370 | 1369 |
apply (auto intro: Infinitesimal_inverse_HFinite) |
1370 |
apply (drule Infinitesimal_HFinite_mult2, assumption) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1371 |
apply (simp add: not_Infinitesimal_not_zero right_inverse) |
14370 | 1372 |
done |
1373 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1374 |
lemma approx_inverse: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1375 |
fixes x y :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1376 |
shows |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1377 |
"[| x @= y; y \<in> HFinite - Infinitesimal |] |
14370 | 1378 |
==> inverse x @= inverse y" |
1379 |
apply (frule HFinite_diff_Infinitesimal_approx, assumption) |
|
1380 |
apply (frule not_Infinitesimal_not_zero2) |
|
1381 |
apply (frule_tac x = x in not_Infinitesimal_not_zero2) |
|
1382 |
apply (drule HFinite_inverse2)+ |
|
1383 |
apply (drule approx_mult2, assumption, auto) |
|
1384 |
apply (drule_tac c = "inverse x" in approx_mult1, assumption) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1385 |
apply (auto intro: approx_sym simp add: mult_assoc) |
14370 | 1386 |
done |
1387 |
||
1388 |
(*Used for NSLIM_inverse, NSLIMSEQ_inverse*) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1389 |
lemmas star_of_approx_inverse = star_of_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
14370 | 1390 |
lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] |
1391 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1392 |
lemma inverse_add_Infinitesimal_approx: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1393 |
fixes x h :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1394 |
shows |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1395 |
"[| x \<in> HFinite - Infinitesimal; |
14370 | 1396 |
h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x" |
1397 |
apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self) |
|
1398 |
done |
|
1399 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1400 |
lemma inverse_add_Infinitesimal_approx2: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1401 |
fixes x h :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1402 |
shows |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1403 |
"[| x \<in> HFinite - Infinitesimal; |
14370 | 1404 |
h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1405 |
apply (rule add_commute [THEN subst]) |
14370 | 1406 |
apply (blast intro: inverse_add_Infinitesimal_approx) |
1407 |
done |
|
1408 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1409 |
lemma inverse_add_Infinitesimal_approx_Infinitesimal: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1410 |
fixes x h :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1411 |
shows |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1412 |
"[| x \<in> HFinite - Infinitesimal; |
20563 | 1413 |
h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h" |
14370 | 1414 |
apply (rule approx_trans2) |
15229 | 1415 |
apply (auto intro: inverse_add_Infinitesimal_approx |
1416 |
simp add: mem_infmal_iff approx_minus_iff [symmetric]) |
|
14370 | 1417 |
done |
1418 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1419 |
lemma Infinitesimal_square_iff: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1420 |
fixes x :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1421 |
shows "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)" |
14370 | 1422 |
apply (auto intro: Infinitesimal_mult) |
1423 |
apply (rule ccontr, frule Infinitesimal_inverse_HFinite) |
|
1424 |
apply (frule not_Infinitesimal_not_zero) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1425 |
apply (auto dest: Infinitesimal_HFinite_mult simp add: mult_assoc) |
14370 | 1426 |
done |
1427 |
declare Infinitesimal_square_iff [symmetric, simp] |
|
1428 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1429 |
lemma HFinite_square_iff [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1430 |
fixes x :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1431 |
shows "(x*x \<in> HFinite) = (x \<in> HFinite)" |
14370 | 1432 |
apply (auto intro: HFinite_mult) |
1433 |
apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff) |
|
1434 |
done |
|
1435 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1436 |
lemma HInfinite_square_iff [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1437 |
fixes x :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1438 |
shows "(x*x \<in> HInfinite) = (x \<in> HInfinite)" |
14370 | 1439 |
by (auto simp add: HInfinite_HFinite_iff) |
1440 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1441 |
lemma approx_HFinite_mult_cancel: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1442 |
fixes a w z :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1443 |
shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z" |
14370 | 1444 |
apply safe |
1445 |
apply (frule HFinite_inverse, assumption) |
|
1446 |
apply (drule not_Infinitesimal_not_zero) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1447 |
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) |
14370 | 1448 |
done |
1449 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1450 |
lemma approx_HFinite_mult_cancel_iff1: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1451 |
fixes a w z :: "'a::real_normed_div_algebra star" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1452 |
shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)" |
14370 | 1453 |
by (auto intro: approx_mult2 approx_HFinite_mult_cancel) |
1454 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1455 |
lemma HInfinite_HFinite_add_cancel: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1456 |
"[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite" |
14370 | 1457 |
apply (rule ccontr) |
1458 |
apply (drule HFinite_HInfinite_iff [THEN iffD2]) |
|
1459 |
apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff) |
|
1460 |
done |
|
1461 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1462 |
lemma HInfinite_HFinite_add: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1463 |
"[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite" |
14370 | 1464 |
apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1465 |
apply (auto simp add: add_assoc HFinite_minus_iff) |
14370 | 1466 |
done |
1467 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1468 |
lemma HInfinite_ge_HInfinite: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1469 |
"[| (x::hypreal) \<in> HInfinite; x \<le> y; 0 \<le> x |] ==> y \<in> HInfinite" |
14370 | 1470 |
by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff) |
1471 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1472 |
lemma Infinitesimal_inverse_HInfinite: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1473 |
fixes x :: "'a::real_normed_div_algebra star" |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1474 |
shows "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite" |
14370 | 1475 |
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
1476 |
apply (auto dest: Infinitesimal_HFinite_mult2) |
|
1477 |
done |
|
1478 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1479 |
lemma HInfinite_HFinite_not_Infinitesimal_mult: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1480 |
fixes x y :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1481 |
shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |] |
14370 | 1482 |
==> x * y \<in> HInfinite" |
1483 |
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
|
1484 |
apply (frule HFinite_Infinitesimal_not_zero) |
|
1485 |
apply (drule HFinite_not_Infinitesimal_inverse) |
|
1486 |
apply (safe, drule HFinite_mult) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1487 |
apply (auto simp add: mult_assoc HFinite_HInfinite_iff) |
14370 | 1488 |
done |
1489 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1490 |
lemma HInfinite_HFinite_not_Infinitesimal_mult2: |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1491 |
fixes x y :: "'a::real_normed_div_algebra star" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1492 |
shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |] |
14370 | 1493 |
==> y * x \<in> HInfinite" |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1494 |
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1495 |
apply (frule HFinite_Infinitesimal_not_zero) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1496 |
apply (drule HFinite_not_Infinitesimal_inverse) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1497 |
apply (safe, drule_tac x="inverse y" in HFinite_mult) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1498 |
apply assumption |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1499 |
apply (auto simp add: mult_assoc [symmetric] HFinite_HInfinite_iff) |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1500 |
done |
14370 | 1501 |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1502 |
lemma HInfinite_gt_SReal: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1503 |
"[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x" |
15003 | 1504 |
by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le) |
14370 | 1505 |
|
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1506 |
lemma HInfinite_gt_zero_gt_one: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1507 |
"[| (x::hypreal) \<in> HInfinite; 0 < x |] ==> 1 < x" |
14370 | 1508 |
by (auto intro: HInfinite_gt_SReal) |
1509 |
||
1510 |
||
15229 | 1511 |
lemma not_HInfinite_one [simp]: "1 \<notin> HInfinite" |
14370 | 1512 |
apply (simp (no_asm) add: HInfinite_HFinite_iff) |
1513 |
done |
|
1514 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1515 |
lemma approx_hrabs_disj: "abs (x::hypreal) @= x | abs x @= -x" |
14370 | 1516 |
by (cut_tac x = x in hrabs_disj, auto) |
1517 |
||
1518 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1519 |
subsection{*Theorems about Monads*} |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1520 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1521 |
lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x::hypreal) Un monad(-x)" |
14370 | 1522 |
by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto) |
1523 |
||
1524 |
lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x" |
|
1525 |
by (fast intro!: Infinitesimal_add_approx_self [THEN approx_sym] approx_monad_iff [THEN iffD1]) |
|
1526 |
||
1527 |
lemma mem_monad_iff: "(u \<in> monad x) = (-u \<in> monad (-x))" |
|
1528 |
by (simp add: monad_def) |
|
1529 |
||
1530 |
lemma Infinitesimal_monad_zero_iff: "(x \<in> Infinitesimal) = (x \<in> monad 0)" |
|
1531 |
by (auto intro: approx_sym simp add: monad_def mem_infmal_iff) |
|
1532 |
||
1533 |
lemma monad_zero_minus_iff: "(x \<in> monad 0) = (-x \<in> monad 0)" |
|
1534 |
apply (simp (no_asm) add: Infinitesimal_monad_zero_iff [symmetric]) |
|
1535 |
done |
|
1536 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1537 |
lemma monad_zero_hrabs_iff: "((x::hypreal) \<in> monad 0) = (abs x \<in> monad 0)" |
14370 | 1538 |
apply (rule_tac x1 = x in hrabs_disj [THEN disjE]) |
1539 |
apply (auto simp add: monad_zero_minus_iff [symmetric]) |
|
1540 |
done |
|
1541 |
||
15229 | 1542 |
lemma mem_monad_self [simp]: "x \<in> monad x" |
14370 | 1543 |
by (simp add: monad_def) |
15229 | 1544 |
|
14370 | 1545 |
|
15229 | 1546 |
subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*} |
1547 |
||
1548 |
lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x" |
|
14370 | 1549 |
apply (simp (no_asm)) |
1550 |
apply (simp add: approx_monad_iff) |
|
1551 |
done |
|
1552 |
||
15229 | 1553 |
lemma approx_subset_monad2: "x @= y ==> {x,y} \<le> monad y" |
14370 | 1554 |
apply (drule approx_sym) |
1555 |
apply (fast dest: approx_subset_monad) |
|
1556 |
done |
|
1557 |
||
1558 |
lemma mem_monad_approx: "u \<in> monad x ==> x @= u" |
|
1559 |
by (simp add: monad_def) |
|
1560 |
||
1561 |
lemma approx_mem_monad: "x @= u ==> u \<in> monad x" |
|
1562 |
by (simp add: monad_def) |
|
1563 |
||
1564 |
lemma approx_mem_monad2: "x @= u ==> x \<in> monad u" |
|
1565 |
apply (simp add: monad_def) |
|
1566 |
apply (blast intro!: approx_sym) |
|
1567 |
done |
|
1568 |
||
1569 |
lemma approx_mem_monad_zero: "[| x @= y;x \<in> monad 0 |] ==> y \<in> monad 0" |
|
1570 |
apply (drule mem_monad_approx) |
|
1571 |
apply (fast intro: approx_mem_monad approx_trans) |
|
1572 |
done |
|
1573 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1574 |
lemma Infinitesimal_approx_hrabs: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1575 |
"[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> abs x @= abs y" |
14370 | 1576 |
apply (drule Infinitesimal_monad_zero_iff [THEN iffD1]) |
1577 |
apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3) |
|
1578 |
done |
|
1579 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1580 |
lemma less_Infinitesimal_less: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1581 |
"[| 0 < x; (x::hypreal) \<notin>Infinitesimal; e :Infinitesimal |] ==> e < x" |
14370 | 1582 |
apply (rule ccontr) |
1583 |
apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval] |
|
1584 |
dest!: order_le_imp_less_or_eq simp add: linorder_not_less) |
|
1585 |
done |
|
1586 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1587 |
lemma Ball_mem_monad_gt_zero: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1588 |
"[| 0 < (x::hypreal); x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u" |
14370 | 1589 |
apply (drule mem_monad_approx [THEN approx_sym]) |
1590 |
apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE]) |
|
1591 |
apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto) |
|
1592 |
done |
|
1593 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1594 |
lemma Ball_mem_monad_less_zero: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1595 |
"[| (x::hypreal) < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0" |
14370 | 1596 |
apply (drule mem_monad_approx [THEN approx_sym]) |
1597 |
apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE]) |
|
1598 |
apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto) |
|
1599 |
done |
|
1600 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1601 |
lemma lemma_approx_gt_zero: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1602 |
"[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y" |
14370 | 1603 |
by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad) |
1604 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1605 |
lemma lemma_approx_less_zero: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1606 |
"[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0" |
14370 | 1607 |
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) |
1608 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1609 |
theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y" |
20652
6e9b7617c89a
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
huffman
parents:
20633
diff
changeset
|
1610 |
by (drule approx_hnorm, simp) |
14370 | 1611 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1612 |
lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0" |
14370 | 1613 |
apply (cut_tac x = x in hrabs_disj) |
1614 |
apply (auto dest: approx_minus) |
|
1615 |
done |
|
1616 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1617 |
lemma approx_hrabs_add_Infinitesimal: |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1618 |
"(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x+e)" |
14370 | 1619 |
by (fast intro: approx_hrabs Infinitesimal_add_approx_self) |
1620 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1621 |
lemma approx_hrabs_add_minus_Infinitesimal: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1622 |
"(e::hypreal) \<in> Infinitesimal ==> abs x @= abs(x + -e)" |
14370 | 1623 |
by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self) |
1624 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1625 |
lemma hrabs_add_Infinitesimal_cancel: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1626 |
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
14370 | 1627 |
abs(x+e) = abs(y+e')|] ==> abs x @= abs y" |
1628 |
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal) |
|
1629 |
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal) |
|
1630 |
apply (auto intro: approx_trans2) |
|
1631 |
done |
|
1632 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1633 |
lemma hrabs_add_minus_Infinitesimal_cancel: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1634 |
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal; |
14370 | 1635 |
abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y" |
1636 |
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal) |
|
1637 |
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal) |
|
1638 |
apply (auto intro: approx_trans2) |
|
1639 |
done |
|
1640 |
||
20721 | 1641 |
subsection {* More @{term HFinite} and @{term Infinitesimal} Theorems *} |
1642 |
||
14370 | 1643 |
(* interesting slightly counterintuitive theorem: necessary |
1644 |
for proving that an open interval is an NS open set |
|
1645 |
*) |
|
1646 |
lemma Infinitesimal_add_hypreal_of_real_less: |
|
1647 |
"[| x < y; u \<in> Infinitesimal |] |
|
1648 |
==> hypreal_of_real x + u < hypreal_of_real y" |
|
1649 |
apply (simp add: Infinitesimal_def) |
|
17431 | 1650 |
apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp) |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
1651 |
apply (simp add: abs_less_iff) |
14370 | 1652 |
done |
1653 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
1654 |
lemma Infinitesimal_add_hrabs_hypreal_of_real_less: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
1655 |
"[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] |
14370 | 1656 |
==> abs (hypreal_of_real r + x) < hypreal_of_real y" |
1657 |
apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal) |
|
1658 |
apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]]) |
|
15229 | 1659 |
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1660 |
simp del: star_of_abs |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1661 |
simp add: star_of_abs [symmetric]) |
14370 | 1662 |
done |
1663 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1664 |
lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1665 |
"[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] |
14370 | 1666 |
==> abs (x + hypreal_of_real r) < hypreal_of_real y" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1667 |
apply (rule add_commute [THEN subst]) |
14370 | 1668 |
apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption) |
1669 |
done |
|
1670 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1671 |
lemma hypreal_of_real_le_add_Infininitesimal_cancel: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1672 |
"[| u \<in> Infinitesimal; v \<in> Infinitesimal; |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1673 |
hypreal_of_real x + u \<le> hypreal_of_real y + v |] |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1674 |
==> hypreal_of_real x \<le> hypreal_of_real y" |
14370 | 1675 |
apply (simp add: linorder_not_less [symmetric], auto) |
1676 |
apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less) |
|
1677 |
apply (auto simp add: Infinitesimal_diff) |
|
1678 |
done |
|
1679 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1680 |
lemma hypreal_of_real_le_add_Infininitesimal_cancel2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1681 |
"[| u \<in> Infinitesimal; v \<in> Infinitesimal; |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1682 |
hypreal_of_real x + u \<le> hypreal_of_real y + v |] |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1683 |
==> x \<le> y" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1684 |
by (blast intro: star_of_le [THEN iffD1] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1685 |
intro!: hypreal_of_real_le_add_Infininitesimal_cancel) |
14370 | 1686 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1687 |
lemma hypreal_of_real_less_Infinitesimal_le_zero: |
15229 | 1688 |
"[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0" |
14370 | 1689 |
apply (rule linorder_not_less [THEN iffD1], safe) |
1690 |
apply (drule Infinitesimal_interval) |
|
1691 |
apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto) |
|
1692 |
done |
|
1693 |
||
1694 |
(*used once, in Lim/NSDERIV_inverse*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1695 |
lemma Infinitesimal_add_not_zero: |
21783 | 1696 |
"[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> star_of x + h \<noteq> 0" |
14370 | 1697 |
apply auto |
21783 | 1698 |
apply (subgoal_tac "h = - star_of x", auto intro: equals_zero_I [symmetric]) |
14370 | 1699 |
done |
1700 |
||
15229 | 1701 |
lemma Infinitesimal_square_cancel [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1702 |
"(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
14370 | 1703 |
apply (rule Infinitesimal_interval2) |
1704 |
apply (rule_tac [3] zero_le_square, assumption) |
|
1705 |
apply (auto simp add: zero_le_square) |
|
1706 |
done |
|
1707 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1708 |
lemma HFinite_square_cancel [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1709 |
"(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite" |
14370 | 1710 |
apply (rule HFinite_bounded, assumption) |
1711 |
apply (auto simp add: zero_le_square) |
|
1712 |
done |
|
1713 |
||
15229 | 1714 |
lemma Infinitesimal_square_cancel2 [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1715 |
"(x::hypreal)*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal" |
14370 | 1716 |
apply (rule Infinitesimal_square_cancel) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1717 |
apply (rule add_commute [THEN subst]) |
14370 | 1718 |
apply (simp (no_asm)) |
1719 |
done |
|
1720 |
||
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1721 |
lemma HFinite_square_cancel2 [simp]: |
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1722 |
"(x::hypreal)*x + y*y \<in> HFinite ==> y*y \<in> HFinite" |
14370 | 1723 |
apply (rule HFinite_square_cancel) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1724 |
apply (rule add_commute [THEN subst]) |
14370 | 1725 |
apply (simp (no_asm)) |
1726 |
done |
|
1727 |
||
15229 | 1728 |
lemma Infinitesimal_sum_square_cancel [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1729 |
"(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
14370 | 1730 |
apply (rule Infinitesimal_interval2, assumption) |
1731 |
apply (rule_tac [2] zero_le_square, simp) |
|
1732 |
apply (insert zero_le_square [of y]) |
|
1733 |
apply (insert zero_le_square [of z], simp) |
|
1734 |
done |
|
1735 |
||
15229 | 1736 |
lemma HFinite_sum_square_cancel [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1737 |
"(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite" |
14370 | 1738 |
apply (rule HFinite_bounded, assumption) |
1739 |
apply (rule_tac [2] zero_le_square) |
|
1740 |
apply (insert zero_le_square [of y]) |
|
1741 |
apply (insert zero_le_square [of z], simp) |
|
1742 |
done |
|
1743 |
||
15229 | 1744 |
lemma Infinitesimal_sum_square_cancel2 [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1745 |
"(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
14370 | 1746 |
apply (rule Infinitesimal_sum_square_cancel) |
1747 |
apply (simp add: add_ac) |
|
1748 |
done |
|
1749 |
||
15229 | 1750 |
lemma HFinite_sum_square_cancel2 [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1751 |
"(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite" |
14370 | 1752 |
apply (rule HFinite_sum_square_cancel) |
1753 |
apply (simp add: add_ac) |
|
1754 |
done |
|
1755 |
||
15229 | 1756 |
lemma Infinitesimal_sum_square_cancel3 [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1757 |
"(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
14370 | 1758 |
apply (rule Infinitesimal_sum_square_cancel) |
1759 |
apply (simp add: add_ac) |
|
1760 |
done |
|
1761 |
||
15229 | 1762 |
lemma HFinite_sum_square_cancel3 [simp]: |
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset
|
1763 |
"(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite" |
14370 | 1764 |
apply (rule HFinite_sum_square_cancel) |
1765 |
apply (simp add: add_ac) |
|
1766 |
done |
|
1767 |
||
15229 | 1768 |
lemma monad_hrabs_less: |
1769 |
"[| y \<in> monad x; 0 < hypreal_of_real e |] |
|
20563 | 1770 |
==> abs (y - x) < hypreal_of_real e" |
14370 | 1771 |
apply (drule mem_monad_approx [THEN approx_sym]) |
1772 |
apply (drule bex_Infinitesimal_iff [THEN iffD2]) |
|
1773 |
apply (auto dest!: InfinitesimalD) |
|
1774 |
done |
|
1775 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1776 |
lemma mem_monad_SReal_HFinite: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1777 |
"x \<in> monad (hypreal_of_real a) ==> x \<in> HFinite" |
14370 | 1778 |
apply (drule mem_monad_approx [THEN approx_sym]) |
1779 |
apply (drule bex_Infinitesimal_iff2 [THEN iffD2]) |
|
1780 |
apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD]) |
|
1781 |
apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add]) |
|
1782 |
done |
|
1783 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1784 |
|
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1785 |
subsection{* Theorems about Standard Part*} |
14370 | 1786 |
|
1787 |
lemma st_approx_self: "x \<in> HFinite ==> st x @= x" |
|
1788 |
apply (simp add: st_def) |
|
1789 |
apply (frule st_part_Ex, safe) |
|
1790 |
apply (rule someI2) |
|
1791 |
apply (auto intro: approx_sym) |
|
1792 |
done |
|
1793 |
||
1794 |
lemma st_SReal: "x \<in> HFinite ==> st x \<in> Reals" |
|
1795 |
apply (simp add: st_def) |
|
1796 |
apply (frule st_part_Ex, safe) |
|
1797 |
apply (rule someI2) |
|
1798 |
apply (auto intro: approx_sym) |
|
1799 |
done |
|
1800 |
||
1801 |
lemma st_HFinite: "x \<in> HFinite ==> st x \<in> HFinite" |
|
1802 |
by (erule st_SReal [THEN SReal_subset_HFinite [THEN subsetD]]) |
|
1803 |
||
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1804 |
lemma st_unique: "\<lbrakk>r \<in> \<real>; r \<approx> x\<rbrakk> \<Longrightarrow> st x = r" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1805 |
apply (frule SReal_subset_HFinite [THEN subsetD]) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1806 |
apply (drule (1) approx_HFinite) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1807 |
apply (unfold st_def) |
14370 | 1808 |
apply (rule some_equality) |
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1809 |
apply (auto intro: approx_unique_real) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1810 |
done |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1811 |
|
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1812 |
lemma st_SReal_eq: "x \<in> Reals ==> st x = x" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1813 |
apply (erule st_unique) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1814 |
apply (rule approx_refl) |
14370 | 1815 |
done |
1816 |
||
15229 | 1817 |
lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x" |
14370 | 1818 |
by (rule SReal_hypreal_of_real [THEN st_SReal_eq]) |
1819 |
||
1820 |
lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y" |
|
1821 |
by (auto dest!: st_approx_self elim!: approx_trans3) |
|
1822 |
||
1823 |
lemma approx_st_eq: |
|
1824 |
assumes "x \<in> HFinite" and "y \<in> HFinite" and "x @= y" |
|
1825 |
shows "st x = st y" |
|
1826 |
proof - |
|
1827 |
have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals" |
|
1828 |
by (simp_all add: st_approx_self st_SReal prems) |
|
1829 |
with prems show ?thesis |
|
1830 |
by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1]) |
|
1831 |
qed |
|
1832 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1833 |
lemma st_eq_approx_iff: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1834 |
"[| x \<in> HFinite; y \<in> HFinite|] |
14370 | 1835 |
==> (x @= y) = (st x = st y)" |
1836 |
by (blast intro: approx_st_eq st_eq_approx) |
|
1837 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1838 |
lemma st_Infinitesimal_add_SReal: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1839 |
"[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x" |
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1840 |
apply (erule st_unique) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1841 |
apply (erule Infinitesimal_add_approx_self) |
14370 | 1842 |
done |
1843 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1844 |
lemma st_Infinitesimal_add_SReal2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1845 |
"[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x" |
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1846 |
apply (erule st_unique) |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1847 |
apply (erule Infinitesimal_add_approx_self2) |
14370 | 1848 |
done |
1849 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1850 |
lemma HFinite_st_Infinitesimal_add: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1851 |
"x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = st(x) + e" |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1852 |
by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) |
14370 | 1853 |
|
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1854 |
lemma st_add: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x + y) = st x + st y" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1855 |
by (simp add: st_unique st_SReal st_approx_self approx_add) |
14370 | 1856 |
|
15229 | 1857 |
lemma st_number_of [simp]: "st (number_of w) = number_of w" |
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
1858 |
by (rule Reals_number_of [THEN st_SReal_eq]) |
14370 | 1859 |
|
1860 |
(*the theorem above for the special cases of zero and one*) |
|
1861 |
lemma [simp]: "st 0 = 0" "st 1 = 1" |
|
1862 |
by (simp_all add: st_SReal_eq) |
|
1863 |
||
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1864 |
lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1865 |
by (simp add: st_unique st_SReal st_approx_self approx_minus) |
14370 | 1866 |
|
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1867 |
lemma st_diff: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x - y) = st x - st y" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1868 |
by (simp add: st_unique st_SReal st_approx_self approx_diff) |
14370 | 1869 |
|
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1870 |
lemma st_mult: "\<lbrakk>x \<in> HFinite; y \<in> HFinite\<rbrakk> \<Longrightarrow> st (x * y) = st x * st y" |
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1871 |
by (simp add: st_unique st_SReal st_approx_self approx_mult_HFinite) |
14370 | 1872 |
|
1873 |
lemma st_Infinitesimal: "x \<in> Infinitesimal ==> st x = 0" |
|
20723
3758db26a3fd
add lemmas approx_diff and st_unique, shorten st proofs
huffman
parents:
20721
diff
changeset
|
1874 |
by (simp add: st_unique mem_infmal_iff) |
14370 | 1875 |
|
1876 |
lemma st_not_Infinitesimal: "st(x) \<noteq> 0 ==> x \<notin> Infinitesimal" |
|
1877 |
by (fast intro: st_Infinitesimal) |
|
1878 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1879 |
lemma st_inverse: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1880 |
"[| x \<in> HFinite; st x \<noteq> 0 |] |
14370 | 1881 |
==> st(inverse x) = inverse (st x)" |
1882 |
apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1]) |
|
1883 |
apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1884 |
apply (subst right_inverse, auto) |
14370 | 1885 |
done |
1886 |
||
15229 | 1887 |
lemma st_divide [simp]: |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1888 |
"[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |] |
14370 | 1889 |
==> st(x/y) = (st x) / (st y)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1890 |
by (simp add: divide_inverse st_mult st_not_Infinitesimal HFinite_inverse st_inverse) |
14370 | 1891 |
|
15229 | 1892 |
lemma st_idempotent [simp]: "x \<in> HFinite ==> st(st(x)) = st(x)" |
14370 | 1893 |
by (blast intro: st_HFinite st_approx_self approx_st_eq) |
1894 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1895 |
lemma Infinitesimal_add_st_less: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1896 |
"[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |] |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1897 |
==> st x + u < st y" |
14370 | 1898 |
apply (drule st_SReal)+ |
1899 |
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff) |
|
1900 |
done |
|
1901 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1902 |
lemma Infinitesimal_add_st_le_cancel: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1903 |
"[| x \<in> HFinite; y \<in> HFinite; |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1904 |
u \<in> Infinitesimal; st x \<le> st y + u |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1905 |
|] ==> st x \<le> st y" |
14370 | 1906 |
apply (simp add: linorder_not_less [symmetric]) |
1907 |
apply (auto dest: Infinitesimal_add_st_less) |
|
1908 |
done |
|
1909 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1910 |
lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x \<le> y |] ==> st(x) \<le> st(y)" |
14370 | 1911 |
apply (frule HFinite_st_Infinitesimal_add) |
1912 |
apply (rotate_tac 1) |
|
1913 |
apply (frule HFinite_st_Infinitesimal_add, safe) |
|
1914 |
apply (rule Infinitesimal_add_st_le_cancel) |
|
1915 |
apply (rule_tac [3] x = ea and y = e in Infinitesimal_diff) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1916 |
apply (auto simp add: add_assoc [symmetric]) |
14370 | 1917 |
done |
1918 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1919 |
lemma st_zero_le: "[| 0 \<le> x; x \<in> HFinite |] ==> 0 \<le> st x" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
1920 |
apply (subst numeral_0_eq_0 [symmetric]) |
14370 | 1921 |
apply (rule st_number_of [THEN subst]) |
1922 |
apply (rule st_le, auto) |
|
1923 |
done |
|
1924 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1925 |
lemma st_zero_ge: "[| x \<le> 0; x \<in> HFinite |] ==> st x \<le> 0" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
1926 |
apply (subst numeral_0_eq_0 [symmetric]) |
14370 | 1927 |
apply (rule st_number_of [THEN subst]) |
1928 |
apply (rule st_le, auto) |
|
1929 |
done |
|
1930 |
||
1931 |
lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)" |
|
1932 |
apply (simp add: linorder_not_le st_zero_le abs_if st_minus |
|
1933 |
linorder_not_less) |
|
1934 |
apply (auto dest!: st_zero_ge [OF order_less_imp_le]) |
|
1935 |
done |
|
1936 |
||
1937 |
||
1938 |
||
20721 | 1939 |
subsection {* Alternative Definitions using Free Ultrafilter *} |
1940 |
||
1941 |
subsubsection {* @{term HFinite} *} |
|
14370 | 1942 |
|
1943 |
lemma HFinite_FreeUltrafilterNat: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1944 |
"star_n X \<in> HFinite |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1945 |
==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1946 |
apply (auto simp add: HFinite_def SReal_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1947 |
apply (rule_tac x=r in exI) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1948 |
apply (simp add: hnorm_def star_of_def starfun_star_n) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1949 |
apply (simp add: star_less_def starP2_star_n) |
14370 | 1950 |
done |
1951 |
||
1952 |
lemma FreeUltrafilterNat_HFinite: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1953 |
"\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1954 |
==> star_n X \<in> HFinite" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1955 |
apply (auto simp add: HFinite_def mem_Rep_star_iff) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1956 |
apply (rule_tac x="star_of u" in bexI) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1957 |
apply (simp add: hnorm_def starfun_star_n star_of_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1958 |
apply (simp add: star_less_def starP2_star_n) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1959 |
apply (simp add: SReal_def) |
14370 | 1960 |
done |
1961 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1962 |
lemma HFinite_FreeUltrafilterNat_iff: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1963 |
"(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1964 |
by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite) |
14370 | 1965 |
|
20721 | 1966 |
subsubsection {* @{term HInfinite} *} |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1967 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1968 |
lemma lemma_Compl_eq: "- {n. u < norm (xa n)} = {n. norm (xa n) \<le> u}" |
14370 | 1969 |
by auto |
1970 |
||
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1971 |
lemma lemma_Compl_eq2: "- {n. norm (xa n) < u} = {n. u \<le> norm (xa n)}" |
14370 | 1972 |
by auto |
1973 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1974 |
lemma lemma_Int_eq1: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1975 |
"{n. norm (xa n) \<le> u} Int {n. u \<le> norm (xa n)} |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1976 |
= {n. norm(xa n) = u}" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
1977 |
by auto |
14370 | 1978 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1979 |
lemma lemma_FreeUltrafilterNat_one: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1980 |
"{n. norm (xa n) = u} \<le> {n. norm (xa n) < u + (1::real)}" |
14370 | 1981 |
by auto |
1982 |
||
1983 |
(*------------------------------------- |
|
1984 |
Exclude this type of sets from free |
|
1985 |
ultrafilter for Infinite numbers! |
|
1986 |
-------------------------------------*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
1987 |
lemma FreeUltrafilterNat_const_Finite: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1988 |
"{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite" |
14370 | 1989 |
apply (rule FreeUltrafilterNat_HFinite) |
1990 |
apply (rule_tac x = "u + 1" in exI) |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1991 |
apply (erule ultra, simp) |
14370 | 1992 |
done |
1993 |
||
1994 |
lemma HInfinite_FreeUltrafilterNat: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1995 |
"star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1996 |
apply (drule HInfinite_HFinite_iff [THEN iffD1]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1997 |
apply (simp add: HFinite_FreeUltrafilterNat_iff) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
1998 |
apply (rule allI, drule_tac x="u + 1" in spec) |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
1999 |
apply (drule FreeUltrafilterNat.not_memD) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2000 |
apply (simp add: Collect_neg_eq [symmetric] linorder_not_less) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2001 |
apply (erule ultra, simp) |
14370 | 2002 |
done |
2003 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2004 |
lemma lemma_Int_HI: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2005 |
"{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2006 |
by auto |
14370 | 2007 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2008 |
lemma lemma_Int_HIa: "{n. u < norm (X n)} Int {n. norm (X n) < u} = {}" |
14370 | 2009 |
by (auto intro: order_less_asym) |
2010 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2011 |
lemma FreeUltrafilterNat_HInfinite: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2012 |
"\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite" |
14370 | 2013 |
apply (rule HInfinite_HFinite_iff [THEN iffD2]) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2014 |
apply (safe, drule HFinite_FreeUltrafilterNat, safe) |
14370 | 2015 |
apply (drule_tac x = u in spec) |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2016 |
apply (drule (1) FreeUltrafilterNat.Int) |
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2017 |
apply (simp add: Collect_conj_eq [symmetric]) |
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2018 |
apply (subgoal_tac "\<forall>n. \<not> (norm (X n) < u \<and> u < norm (X n))", auto) |
14370 | 2019 |
done |
2020 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2021 |
lemma HInfinite_FreeUltrafilterNat_iff: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2022 |
"(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)" |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2023 |
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite) |
14370 | 2024 |
|
20721 | 2025 |
subsubsection {* @{term Infinitesimal} *} |
10751 | 2026 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2027 |
lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2028 |
by (unfold SReal_def, auto) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2029 |
|
14370 | 2030 |
lemma Infinitesimal_FreeUltrafilterNat: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2031 |
"star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2032 |
apply (simp add: Infinitesimal_def ball_SReal_eq) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2033 |
apply (simp add: hnorm_def starfun_star_n star_of_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2034 |
apply (simp add: star_less_def starP2_star_n) |
14370 | 2035 |
done |
2036 |
||
2037 |
lemma FreeUltrafilterNat_Infinitesimal: |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2038 |
"\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2039 |
apply (simp add: Infinitesimal_def ball_SReal_eq) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2040 |
apply (simp add: hnorm_def starfun_star_n star_of_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2041 |
apply (simp add: star_less_def starP2_star_n) |
14370 | 2042 |
done |
2043 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2044 |
lemma Infinitesimal_FreeUltrafilterNat_iff: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2045 |
"(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
2046 |
by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal) |
14370 | 2047 |
|
2048 |
(*------------------------------------------------------------------------ |
|
2049 |
Infinitesimals as smaller than 1/n for all n::nat (> 0) |
|
2050 |
------------------------------------------------------------------------*) |
|
2051 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2052 |
lemma lemma_Infinitesimal: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2053 |
"(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))" |
14370 | 2054 |
apply (auto simp add: real_of_nat_Suc_gt_zero) |
2055 |
apply (blast dest!: reals_Archimedean intro: order_less_trans) |
|
2056 |
done |
|
2057 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2058 |
lemma lemma_Infinitesimal2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2059 |
"(\<forall>r \<in> Reals. 0 < r --> x < r) = |
14370 | 2060 |
(\<forall>n. x < inverse(hypreal_of_nat (Suc n)))" |
2061 |
apply safe |
|
2062 |
apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec) |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21783
diff
changeset
|
2063 |
apply (simp (no_asm_use)) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
2064 |
apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE]) |
14370 | 2065 |
prefer 2 apply assumption |
20730 | 2066 |
apply (simp add: real_of_nat_def) |
14370 | 2067 |
apply (auto dest!: reals_Archimedean simp add: SReal_iff) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset
|
2068 |
apply (drule star_of_less [THEN iffD2]) |
20730 | 2069 |
apply (simp add: real_of_nat_def) |
14370 | 2070 |
apply (blast intro: order_less_trans) |
2071 |
done |
|
2072 |
||
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
2073 |
|
14370 | 2074 |
lemma Infinitesimal_hypreal_of_nat_iff: |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2075 |
"Infinitesimal = {x. \<forall>n. hnorm x < inverse (hypreal_of_nat (Suc n))}" |
14370 | 2076 |
apply (simp add: Infinitesimal_def) |
2077 |
apply (auto simp add: lemma_Infinitesimal2) |
|
2078 |
done |
|
2079 |
||
2080 |
||
15229 | 2081 |
subsection{*Proof that @{term omega} is an infinite number*} |
2082 |
||
2083 |
text{*It will follow that epsilon is an infinitesimal number.*} |
|
2084 |
||
14370 | 2085 |
lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}" |
2086 |
by (auto simp add: less_Suc_eq) |
|
2087 |
||
2088 |
(*------------------------------------------- |
|
2089 |
Prove that any segment is finite and |
|
2090 |
hence cannot belong to FreeUltrafilterNat |
|
2091 |
-------------------------------------------*) |
|
2092 |
lemma finite_nat_segment: "finite {n::nat. n < m}" |
|
15251 | 2093 |
apply (induct "m") |
14370 | 2094 |
apply (auto simp add: Suc_Un_eq) |
2095 |
done |
|
2096 |
||
2097 |
lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}" |
|
2098 |
by (auto intro: finite_nat_segment) |
|
2099 |
||
2100 |
lemma finite_real_of_nat_less_real: "finite {n::nat. real n < u}" |
|
2101 |
apply (cut_tac x = u in reals_Archimedean2, safe) |
|
2102 |
apply (rule finite_real_of_nat_segment [THEN [2] finite_subset]) |
|
2103 |
apply (auto dest: order_less_trans) |
|
2104 |
done |
|
2105 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2106 |
lemma lemma_real_le_Un_eq: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2107 |
"{n. f n \<le> u} = {n. f n < u} Un {n. u = (f n :: real)}" |
14370 | 2108 |
by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le) |
2109 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2110 |
lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}" |
14370 | 2111 |
by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real) |
2112 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2113 |
lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}" |
14370 | 2114 |
apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real) |
2115 |
done |
|
2116 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2117 |
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2118 |
"{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat" |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2119 |
by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real) |
14370 | 2120 |
|
2121 |
lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat" |
|
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2122 |
apply (rule ccontr, drule FreeUltrafilterNat.not_memD) |
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2123 |
apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}") |
14370 | 2124 |
prefer 2 apply force |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2125 |
apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite]) |
14370 | 2126 |
done |
2127 |
||
2128 |
(*-------------------------------------------------------------- |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2129 |
The complement of {n. abs(real n) \<le> u} = |
14370 | 2130 |
{n. u < abs (real n)} is in FreeUltrafilterNat |
2131 |
by property of (free) ultrafilters |
|
2132 |
--------------------------------------------------------------*) |
|
2133 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2134 |
lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}" |
14370 | 2135 |
by (auto dest!: order_le_less_trans simp add: linorder_not_le) |
2136 |
||
15229 | 2137 |
text{*@{term omega} is a member of @{term HInfinite}*} |
14370 | 2138 |
|
2139 |
lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat" |
|
2140 |
apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat) |
|
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2141 |
apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq) |
14370 | 2142 |
done |
2143 |
||
15229 | 2144 |
theorem HInfinite_omega [simp]: "omega \<in> HInfinite" |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2145 |
apply (simp add: omega_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2146 |
apply (rule FreeUltrafilterNat_HInfinite) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2147 |
apply (simp (no_asm) add: real_norm_def real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega) |
14370 | 2148 |
done |
2149 |
||
2150 |
(*----------------------------------------------- |
|
2151 |
Epsilon is a member of Infinitesimal |
|
2152 |
-----------------------------------------------*) |
|
2153 |
||
15229 | 2154 |
lemma Infinitesimal_epsilon [simp]: "epsilon \<in> Infinitesimal" |
14370 | 2155 |
by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega) |
2156 |
||
15229 | 2157 |
lemma HFinite_epsilon [simp]: "epsilon \<in> HFinite" |
14370 | 2158 |
by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) |
2159 |
||
15229 | 2160 |
lemma epsilon_approx_zero [simp]: "epsilon @= 0" |
14370 | 2161 |
apply (simp (no_asm) add: mem_infmal_iff [symmetric]) |
2162 |
done |
|
2163 |
||
2164 |
(*------------------------------------------------------------------------ |
|
2165 |
Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given |
|
2166 |
that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM. |
|
2167 |
-----------------------------------------------------------------------*) |
|
2168 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2169 |
lemma real_of_nat_less_inverse_iff: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2170 |
"0 < u ==> (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)" |
14370 | 2171 |
apply (simp add: inverse_eq_divide) |
2172 |
apply (subst pos_less_divide_eq, assumption) |
|
2173 |
apply (subst pos_less_divide_eq) |
|
2174 |
apply (simp add: real_of_nat_Suc_gt_zero) |
|
2175 |
apply (simp add: real_mult_commute) |
|
2176 |
done |
|
2177 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2178 |
lemma finite_inverse_real_of_posnat_gt_real: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2179 |
"0 < u ==> finite {n. u < inverse(real(Suc n))}" |
14370 | 2180 |
apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff) |
2181 |
apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric]) |
|
2182 |
apply (rule finite_real_of_nat_less_real) |
|
2183 |
done |
|
2184 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2185 |
lemma lemma_real_le_Un_eq2: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2186 |
"{n. u \<le> inverse(real(Suc n))} = |
14370 | 2187 |
{n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}" |
2188 |
apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le) |
|
2189 |
done |
|
2190 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2191 |
lemma real_of_nat_inverse_eq_iff: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2192 |
"(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)" |
15539 | 2193 |
by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym]) |
14370 | 2194 |
|
2195 |
lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}" |
|
2196 |
apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff) |
|
2197 |
apply (cut_tac x = "inverse u - 1" in lemma_finite_omega_set) |
|
2198 |
apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute) |
|
2199 |
done |
|
2200 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2201 |
lemma finite_inverse_real_of_posnat_ge_real: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2202 |
"0 < u ==> finite {n. u \<le> inverse(real(Suc n))}" |
14370 | 2203 |
by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_omega_set2 finite_inverse_real_of_posnat_gt_real) |
2204 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2205 |
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2206 |
"0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat" |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2207 |
by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real) |
14370 | 2208 |
|
2209 |
(*-------------------------------------------------------------- |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2210 |
The complement of {n. u \<le> inverse(real(Suc n))} = |
14370 | 2211 |
{n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat |
2212 |
by property of (free) ultrafilters |
|
2213 |
--------------------------------------------------------------*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2214 |
lemma Compl_le_inverse_eq: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2215 |
"- {n. u \<le> inverse(real(Suc n))} = |
14370 | 2216 |
{n. inverse(real(Suc n)) < u}" |
2217 |
apply (auto dest!: order_le_less_trans simp add: linorder_not_le) |
|
2218 |
done |
|
2219 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2220 |
lemma FreeUltrafilterNat_inverse_real_of_posnat: |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2221 |
"0 < u ==> |
14370 | 2222 |
{n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat" |
2223 |
apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat) |
|
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2224 |
apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq) |
14370 | 2225 |
done |
2226 |
||
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2227 |
text{* Example of an hypersequence (i.e. an extended standard sequence) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2228 |
whose term with an hypernatural suffix is an infinitesimal i.e. |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2229 |
the whn'nth term of the hypersequence is a member of Infinitesimal*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2230 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2231 |
lemma SEQ_Infinitesimal: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2232 |
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2233 |
apply (simp add: hypnat_omega_def starfun_star_n star_n_inverse) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2234 |
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2235 |
apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2236 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21855
diff
changeset
|
2237 |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2238 |
text{* Example where we get a hyperreal from a real sequence |
14370 | 2239 |
for which a particular property holds. The theorem is |
2240 |
used in proofs about equivalence of nonstandard and |
|
2241 |
standard neighbourhoods. Also used for equivalence of |
|
2242 |
nonstandard ans standard definitions of pointwise |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2243 |
limit.*} |
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2244 |
|
14370 | 2245 |
(*----------------------------------------------------- |
2246 |
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal |
|
2247 |
-----------------------------------------------------*) |
|
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2248 |
lemma real_seq_to_hypreal_Infinitesimal: |
20563 | 2249 |
"\<forall>n. norm(X n - x) < inverse(real(Suc n)) |
2250 |
==> star_n X - star_of x \<in> Infinitesimal" |
|
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2251 |
apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int intro: order_less_trans FreeUltrafilterNat.subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse) |
14370 | 2252 |
done |
2253 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2254 |
lemma real_seq_to_hypreal_approx: |
20563 | 2255 |
"\<forall>n. norm(X n - x) < inverse(real(Suc n)) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2256 |
==> star_n X @= star_of x" |
14370 | 2257 |
apply (subst approx_minus_iff) |
2258 |
apply (rule mem_infmal_iff [THEN subst]) |
|
2259 |
apply (erule real_seq_to_hypreal_Infinitesimal) |
|
2260 |
done |
|
2261 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2262 |
lemma real_seq_to_hypreal_approx2: |
20563 | 2263 |
"\<forall>n. norm(x - X n) < inverse(real(Suc n)) |
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2264 |
==> star_n X @= star_of x" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2265 |
apply (rule real_seq_to_hypreal_approx) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2266 |
apply (subst norm_minus_cancel [symmetric]) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset
|
2267 |
apply (simp del: norm_minus_cancel) |
14370 | 2268 |
done |
2269 |
||
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset
|
2270 |
lemma real_seq_to_hypreal_Infinitesimal2: |
20563 | 2271 |
"\<forall>n. norm(X n - Y n) < inverse(real(Suc n)) |
2272 |
==> star_n X - star_n Y \<in> Infinitesimal" |
|
14370 | 2273 |
by (auto intro!: bexI |
2274 |
dest: FreeUltrafilterNat_inverse_real_of_posnat |
|
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2275 |
FreeUltrafilterNat.Int |
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
2276 |
intro: order_less_trans FreeUltrafilterNat.subset |
20563 | 2277 |
simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff |
2278 |
star_n_inverse) |
|
14370 | 2279 |
|
10751 | 2280 |
end |