author  huffman 
Sun, 17 Sep 2006 16:44:51 +0200  
changeset 20562  c2f672be8522 
parent 20554  c433e78d4203 
child 20563  44eda2314aab 
permissions  rwrr 
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 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

11 
imports HyperArith "../Real/RComplete" 
15131  12 
begin 
10751  13 

19765  14 
definition 
10751  15 

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 :: "'a::norm star \<Rightarrow> real 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

17 
"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

18 

f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

19 
Infinitesimal :: "('a::real_normed_vector) star set" 
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 

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

22 
HFinite :: "('a::real_normed_vector) star set" 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

23 
"HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}" 
10751  24 

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

25 
HInfinite :: "('a::real_normed_vector) star set" 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

26 
"HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}" 
10751  27 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

28 
approx :: "['a::real_normed_vector star, 'a star] => bool" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

29 
(infixl "@=" 50) 
15229  30 
{*the `infinitely close' relation*} 
19765  31 
"(x @= y) = ((x + y) \<in> Infinitesimal)" 
14653  32 

14370  33 
st :: "hypreal => hypreal" 
15229  34 
{*the standard part of a hyperreal*} 
19765  35 
"st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)" 
10751  36 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

37 
monad :: "'a::real_normed_vector star => 'a star set" 
19765  38 
"monad x = {y. x @= y}" 
10751  39 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

40 
galaxy :: "'a::real_normed_vector star => 'a star set" 
19765  41 
"galaxy x = {y. (x + y) \<in> HFinite}" 
42 

43 
const_syntax (xsymbols) 

44 
approx (infixl "\<approx>" 50) 

45 

46 
const_syntax (HTML output) 

47 
approx (infixl "\<approx>" 50) 

14370  48 

49 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

50 
lemma hypreal_of_real_of_real_eq: "hypreal_of_real r = of_real r" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

51 
proof  
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

52 
have "hypreal_of_real r = hypreal_of_real (of_real r)" by simp 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

53 
also have "\<dots> = of_real r" by (rule star_of_of_real) 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

54 
finally show ?thesis . 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

55 
qed 
14565  56 

20554
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

57 
lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}" 
c433e78d4203
define new constant of_real for class real_algebra_1;
huffman
parents:
20552
diff
changeset

58 
by (simp add: Reals_def image_def hypreal_of_real_of_real_eq) 
14370  59 

60 

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

61 
subsection{*Nonstandard extension of the norm function*} 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

62 

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] 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

64 

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 
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

66 
"\<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

67 
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

68 

f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

69 
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

70 
"\<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

71 
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

72 

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 
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

74 
"\<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

75 
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

76 

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 
lemma hnorm_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

78 
"\<And>a (x::'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

79 
hnorm (( *f2* scaleR) a x) = \<bar>a\<bar> * 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

80 
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

81 

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 
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

83 
"\<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

84 
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

85 

f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

86 
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

87 
"\<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

88 
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

89 

f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

90 
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

91 
"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

92 
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

93 

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 
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

95 
"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

96 
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

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 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

99 
"\<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

100 
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

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_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

103 
"\<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

104 
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

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_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

107 
"\<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

108 
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

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_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

111 
"\<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

112 
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

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 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

115 
"\<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

116 
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

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 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

119 
"\<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

120 
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

121 
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

122 

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 
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

124 
"\<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

125 
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

126 
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

127 

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 
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

129 
"\<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

130 
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

131 

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 
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

133 
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

134 
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

135 
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

136 

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 
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

138 
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

139 
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

140 
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

141 
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

142 
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

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 

15229  145 
subsection{*Closure Laws for the Standard Reals*} 
14370  146 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset

147 
lemma SReal_add [simp]: 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset

148 
"[ (x::hypreal) \<in> Reals; y \<in> Reals ] ==> x + y \<in> Reals" 
14370  149 
apply (auto simp add: SReal_def) 
150 
apply (rule_tac x = "r + ra" in exI, simp) 

151 
done 

152 

153 
lemma SReal_mult: "[ (x::hypreal) \<in> Reals; y \<in> Reals ] ==> x * y \<in> Reals" 

154 
apply (simp add: SReal_def, safe) 

155 
apply (rule_tac x = "r * ra" in exI) 

15539  156 
apply (simp (no_asm)) 
14370  157 
done 
158 

159 
lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals" 

160 
apply (simp add: SReal_def) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

161 
apply (blast intro: star_of_inverse [symmetric]) 
14370  162 
done 
163 

164 
lemma SReal_divide: "[ (x::hypreal) \<in> Reals; y \<in> Reals ] ==> x/y \<in> Reals" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

165 
by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse) 
14370  166 

167 
lemma SReal_minus: "(x::hypreal) \<in> Reals ==> x \<in> Reals" 

168 
apply (simp add: SReal_def) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

169 
apply (blast intro: star_of_minus [symmetric]) 
14370  170 
done 
171 

15229  172 
lemma SReal_minus_iff [simp]: "(x \<in> Reals) = ((x::hypreal) \<in> Reals)" 
14370  173 
apply auto 
174 
apply (erule_tac [2] SReal_minus) 

175 
apply (drule SReal_minus, auto) 

176 
done 

177 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

178 
lemma SReal_add_cancel: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

179 
"[ (x::hypreal) + y \<in> Reals; y \<in> Reals ] ==> x \<in> Reals" 
14370  180 
apply (drule_tac x = y in SReal_minus) 
181 
apply (drule SReal_add, assumption, auto) 

182 
done 

183 

184 
lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

185 
apply (auto simp add: SReal_def) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

186 
apply (rule_tac x="abs r" in exI) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

187 
apply simp 
14370  188 
done 
189 

15229  190 
lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals" 
14370  191 
by (simp add: SReal_def) 
192 

15229  193 
lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

194 
apply (simp only: star_of_number_of [symmetric]) 
14370  195 
apply (rule SReal_hypreal_of_real) 
196 
done 

197 

198 
(** As always with numerals, 0 and 1 are special cases **) 

199 

15229  200 
lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

201 
apply (subst numeral_0_eq_0 [symmetric]) 
14370  202 
apply (rule SReal_number_of) 
203 
done 

204 

15229  205 
lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

206 
apply (subst numeral_1_eq_1 [symmetric]) 
14370  207 
apply (rule SReal_number_of) 
208 
done 

209 

210 
lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

211 
apply (simp only: divide_inverse) 
14370  212 
apply (blast intro!: SReal_number_of SReal_mult SReal_inverse) 
213 
done 

214 

15229  215 
text{*epsilon is not in Reals because it is an infinitesimal*} 
14370  216 
lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals" 
217 
apply (simp add: SReal_def) 

218 
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym]) 

219 
done 

220 

221 
lemma SReal_omega_not_mem: "omega \<notin> Reals" 

222 
apply (simp add: SReal_def) 

223 
apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym]) 

224 
done 

225 

226 
lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)" 

227 
by (simp add: SReal_def) 

228 

229 
lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)" 

230 
by (simp add: SReal_def) 

231 

232 
lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals" 

233 
by (auto simp add: SReal_def) 

234 

235 
lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV" 

236 
apply (auto simp add: SReal_def) 

237 
apply (rule inj_hypreal_of_real [THEN inv_f_f, THEN subst], blast) 

238 
done 

239 

240 
lemma SReal_hypreal_of_real_image: 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

241 
"[ \<exists>x. x: P; P \<subseteq> Reals ] ==> \<exists>Q. P = hypreal_of_real ` Q" 
14370  242 
apply (simp add: SReal_def, blast) 
243 
done 

244 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

245 
lemma SReal_dense: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

246 
"[ (x::hypreal) \<in> Reals; y \<in> Reals; x<y ] ==> \<exists>r \<in> Reals. x<r & r<y" 
14370  247 
apply (auto simp add: SReal_iff) 
14477  248 
apply (drule dense, safe) 
14370  249 
apply (rule_tac x = "hypreal_of_real r" in bexI, auto) 
250 
done 

251 

15229  252 
text{*Completeness of Reals, but both lemmas are unused.*} 
253 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

254 
lemma SReal_sup_lemma: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

255 
"P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) = 
14370  256 
(\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))" 
257 
by (blast dest!: SReal_iff [THEN iffD1]) 

258 

259 
lemma SReal_sup_lemma2: 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

260 
"[ P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y ] 
14370  261 
==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) & 
262 
(\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)" 

263 
apply (rule conjI) 

264 
apply (fast dest!: SReal_iff [THEN iffD1]) 

265 
apply (auto, frule subsetD, assumption) 

266 
apply (drule SReal_iff [THEN iffD1]) 

267 
apply (auto, rule_tac x = ya in exI, auto) 

268 
done 

269 

15229  270 

271 
subsection{*Lifting of the Ub and Lub Properties*} 

272 

14370  273 
lemma hypreal_of_real_isUb_iff: 
274 
"(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = 

275 
(isUb (UNIV :: real set) Q Y)" 

15229  276 
by (simp add: isUb_def setle_def) 
14370  277 

278 
lemma hypreal_of_real_isLub1: 

279 
"isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) 

280 
==> isLub (UNIV :: real set) Q Y" 

281 
apply (simp add: isLub_def leastP_def) 

282 
apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2] 

283 
simp add: hypreal_of_real_isUb_iff setge_def) 

284 
done 

285 

286 
lemma hypreal_of_real_isLub2: 

287 
"isLub (UNIV :: real set) Q Y 

288 
==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)" 

289 
apply (simp add: isLub_def leastP_def) 

290 
apply (auto simp add: hypreal_of_real_isUb_iff setge_def) 

291 
apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE]) 

292 
prefer 2 apply assumption 

293 
apply (drule_tac x = xa in spec) 

294 
apply (auto simp add: hypreal_of_real_isUb_iff) 

295 
done 

296 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

297 
lemma hypreal_of_real_isLub_iff: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

298 
"(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) = 
14370  299 
(isLub (UNIV :: real set) Q Y)" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

300 
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2) 
14370  301 

302 
lemma lemma_isUb_hypreal_of_real: 

303 
"isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)" 

304 
by (auto simp add: SReal_iff isUb_def) 

305 

306 
lemma lemma_isLub_hypreal_of_real: 

307 
"isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)" 

308 
by (auto simp add: isLub_def leastP_def isUb_def SReal_iff) 

309 

310 
lemma lemma_isLub_hypreal_of_real2: 

311 
"\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y" 

312 
by (auto simp add: isLub_def leastP_def isUb_def) 

313 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

314 
lemma SReal_complete: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

315 
"[ P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y ] 
14370  316 
==> \<exists>t::hypreal. isLub Reals P t" 
317 
apply (frule SReal_hypreal_of_real_image) 

318 
apply (auto, drule lemma_isUb_hypreal_of_real) 

15229  319 
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 
320 
simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff) 

14370  321 
done 
322 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

323 

4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

324 
subsection{* Set of Finite Elements is a Subring of the Extended Reals*} 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

325 

14370  326 
lemma HFinite_add: "[x \<in> HFinite; y \<in> HFinite] ==> (x+y) \<in> HFinite" 
327 
apply (simp add: HFinite_def) 

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

328 
apply (blast intro!: SReal_add hnorm_add_less) 
14370  329 
done 
330 

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

331 
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

332 
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

333 
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

334 
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

335 
apply (blast intro!: SReal_mult hnorm_mult_less) 
14370  336 
done 
337 

338 
lemma HFinite_minus_iff: "(x \<in> HFinite) = (x \<in> HFinite)" 

339 
by (simp add: HFinite_def) 

340 

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

341 
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

342 
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

343 
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

344 
apply (transfer, 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

345 
apply (blast intro: SReal_add SReal_hypreal_of_real Reals_1) 
14370  346 
done 
347 

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

348 
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

349 
by (auto simp add: SReal_def) 
14370  350 

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

351 
lemma HFinite_hypreal_of_real: "hypreal_of_real 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

352 
by (rule HFinite_star_of) 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

353 

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 
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t" 
14370  355 
by (simp add: HFinite_def) 
356 

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 
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

358 
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

359 

20562
c2f672be8522
add type constraint to otherwise looping iff rule
huffman
parents:
20554
diff
changeset

360 
lemma HFinite_hnorm_iff [iff]: 
c2f672be8522
add type constraint to otherwise looping iff rule
huffman
parents:
20554
diff
changeset

361 
"(hnorm (x::hypreal) \<in> HFinite) = (x \<in> HFinite)" 
14370  362 
by (simp add: HFinite_def) 
363 

15229  364 
lemma HFinite_number_of [simp]: "number_of w \<in> HFinite" 
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

365 
by (unfold star_number_def, rule HFinite_star_of) 
14370  366 

367 
(** As always with numerals, 0 and 1 are special cases **) 

368 

15229  369 
lemma HFinite_0 [simp]: "0 \<in> HFinite" 
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 
by (unfold star_zero_def, rule HFinite_star_of) 
14370  371 

15229  372 
lemma HFinite_1 [simp]: "1 \<in> HFinite" 
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

373 
by (unfold star_one_def, rule HFinite_star_of) 
14370  374 

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

375 
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

376 
"[(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

377 
apply (case_tac "x \<le> 0") 
14370  378 
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

379 
apply (drule_tac [2] order_antisym) 
14370  380 
apply (auto simp add: linorder_not_le) 
381 
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def) 

382 
done 

383 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

384 

4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

385 
subsection{* Set of Infinitesimals is a Subring of the Hyperreals*} 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

386 

20407  387 
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

388 
"(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal" 
20407  389 
by (simp add: Infinitesimal_def) 
390 

14370  391 
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

392 
"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

393 
by (simp add: Infinitesimal_def) 
14370  394 

15229  395 
lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal" 
14370  396 
by (simp add: Infinitesimal_def) 
397 

398 
lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x" 

399 
by auto 

400 

401 
lemma Infinitesimal_add: 

402 
"[ x \<in> Infinitesimal; y \<in> Infinitesimal ] ==> (x+y) \<in> Infinitesimal" 

20407  403 
apply (rule InfinitesimalI) 
14370  404 
apply (rule hypreal_sum_of_halves [THEN subst]) 
14477  405 
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

406 
apply (blast intro: hnorm_add_less SReal_divide_number_of dest: InfinitesimalD) 
14370  407 
done 
408 

15229  409 
lemma Infinitesimal_minus_iff [simp]: "(x:Infinitesimal) = (x:Infinitesimal)" 
14370  410 
by (simp add: Infinitesimal_def) 
411 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

412 
lemma Infinitesimal_diff: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

413 
"[ x \<in> Infinitesimal; y \<in> Infinitesimal ] ==> xy \<in> Infinitesimal" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

414 
by (simp add: diff_def Infinitesimal_add) 
14370  415 

416 
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

417 
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

418 
shows "[x \<in> Infinitesimal; y \<in> Infinitesimal] ==> (x * y) \<in> Infinitesimal" 
20407  419 
apply (rule InfinitesimalI) 
420 
apply (case_tac "y = 0", 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

421 
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

422 
apply (rule hnorm_mult_less) 
20407  423 
apply (simp_all add: InfinitesimalD) 
14370  424 
done 
425 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

426 
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

427 
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

428 
shows "[ x \<in> Infinitesimal; y \<in> HFinite ] ==> (x * y) \<in> Infinitesimal" 
20407  429 
apply (rule InfinitesimalI) 
430 
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

431 
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

432 
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp) 
20407  433 
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

434 
apply (rule hnorm_mult_less) 
20407  435 
apply (simp add: InfinitesimalD 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

436 
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

437 
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

438 
apply (erule order_le_less_trans [OF hnorm_ge_zero]) 
14370  439 
done 
440 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

441 
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

442 
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

443 
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

444 
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

445 
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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
apply (simp add: InfinitesimalD SReal_divide) 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

452 
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

453 
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

454 
done 
14370  455 

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

456 
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

457 
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

458 
apply (rule_tac y="r + 1" in order_less_le_trans, 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

459 
apply (simp add: SReal_add Reals_1) 
14370  460 
done 
461 

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

462 
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

463 
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

464 
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

465 
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

466 
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

467 
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

468 
apply (simp add: 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

469 
apply (simp add: HInfinite_def SReal_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

470 
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

471 
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

472 
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

473 

f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
20485
diff
changeset

474 
lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite" 
20407  475 
by (simp add: HInfinite_def) 
476 

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

477 
lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < hnorm x" 
20407  478 
by (simp add: HInfinite_def) 
479 

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

480 
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

481 
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

482 
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

483 
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

484 
apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1) 
20407  485 
apply (case_tac "x = 0", simp add: HInfinite_def) 
486 
apply (rule mult_strict_mono) 

487 
apply (simp_all add: HInfiniteD) 

14370  488 
done 
489 

15229  490 
lemma hypreal_add_zero_less_le_mono: "[r < x; (0::hypreal) \<le> y] ==> r < x+y" 
491 
by (auto dest: add_less_le_mono) 

492 

14370  493 
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

494 
"[(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x] ==> (x + y): HInfinite" 
14370  495 
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

496 
simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def) 
14370  497 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

498 
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

499 
"[(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

500 
by (auto intro!: HInfinite_add_ge_zero simp add: add_commute) 
14370  501 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

502 
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

503 
"[(x::hypreal) \<in> HInfinite; 0 < y; 0 < x] ==> (x + y): HInfinite" 
14370  504 
by (blast intro: HInfinite_add_ge_zero order_less_imp_le) 
505 

506 
lemma HInfinite_minus_iff: "(x \<in> HInfinite) = (x \<in> HInfinite)" 

507 
by (simp add: HInfinite_def) 

508 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

509 
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

510 
"[(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0] ==> (x + y): HInfinite" 
14370  511 
apply (drule HInfinite_minus_iff [THEN iffD2]) 
512 
apply (rule HInfinite_minus_iff [THEN iffD1]) 

513 
apply (auto intro: HInfinite_add_ge_zero) 

514 
done 

515 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

516 
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

517 
"[(x::hypreal) \<in> HInfinite; y < 0; x < 0] ==> (x + y): HInfinite" 
14370  518 
by (blast intro: HInfinite_add_le_zero order_less_imp_le) 
519 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

520 
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

521 
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

522 
shows "[a: HFinite; b: HFinite; c: HFinite] 
14370  523 
==> a*a + b*b + c*c \<in> HFinite" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

524 
by (auto intro: HFinite_mult HFinite_add) 
14370  525 

526 
lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0" 

527 
by auto 

528 

529 
lemma not_Infinitesimal_not_zero2: "x \<in> HFinite  Infinitesimal ==> x \<noteq> 0" 

530 
by auto 

531 

15229  532 
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

533 
"(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)" 
15003  534 
by (auto simp add: abs_if) 
14370  535 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

536 
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

537 
"(x::hypreal) \<in> HFinite  Infinitesimal ==> abs x \<in> HFinite  Infinitesimal" 
14370  538 
by blast 
539 

540 
lemma hrabs_less_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

541 
"[ e \<in> Infinitesimal; abs (x::hypreal) < e ] ==> x \<in> Infinitesimal" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

542 
by (auto simp add: Infinitesimal_def abs_less_iff) 
14370  543 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

544 
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

545 
"[ e \<in> Infinitesimal; abs (x::hypreal) \<le> e ] ==> x \<in> Infinitesimal" 
14370  546 
by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal) 
547 

548 
lemma Infinitesimal_interval: 

549 
"[ 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

550 
==> (x::hypreal) \<in> Infinitesimal" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

551 
by (auto simp add: Infinitesimal_def abs_less_iff) 
14370  552 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

553 
lemma Infinitesimal_interval2: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

554 
"[ 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

555 
e' \<le> x ; x \<le> e ] ==> (x::hypreal) \<in> Infinitesimal" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

556 
by (auto intro: Infinitesimal_interval simp add: order_le_less) 
14370  557 

558 
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

559 
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

560 
shows "[ x \<notin> Infinitesimal; y \<notin> Infinitesimal] ==> (x*y) \<notin>Infinitesimal" 
20407  561 
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

562 
apply (simp only: linorder_not_less hnorm_mult) 
20407  563 
apply (drule_tac x = "r * s" in bspec) 
564 
apply (fast intro: SReal_mult) 

565 
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

566 
apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono) 
20407  567 
apply (simp_all (no_asm_simp)) 
14370  568 
done 
569 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

570 
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

571 
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

572 
shows "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal  y \<in> Infinitesimal" 
14370  573 
apply (rule ccontr) 
574 
apply (drule de_Morgan_disj [THEN iffD1]) 

575 
apply (fast dest: not_Infinitesimal_mult) 

576 
done 

577 

578 
lemma HFinite_Infinitesimal_not_zero: "x \<in> HFiniteInfinitesimal ==> x \<noteq> 0" 

579 
by blast 

580 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

581 
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

582 
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

583 
shows "[ x \<in> HFinite  Infinitesimal; 
14370  584 
y \<in> HFinite  Infinitesimal 
585 
] ==> (x*y) \<in> HFinite  Infinitesimal" 

586 
apply clarify 

587 
apply (blast dest: HFinite_mult not_Infinitesimal_mult) 

588 
done 

589 

590 
lemma Infinitesimal_subset_HFinite: 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

591 
"Infinitesimal \<subseteq> HFinite" 
14370  592 
apply (simp add: Infinitesimal_def HFinite_def, auto) 
593 
apply (rule_tac x = 1 in bexI, auto) 

594 
done 

595 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

596 
lemma Infinitesimal_hypreal_of_real_mult: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

597 
"x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal" 
14370  598 
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult]) 
599 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

600 
lemma Infinitesimal_hypreal_of_real_mult2: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

601 
"x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal" 
14370  602 
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2]) 
603 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

604 

4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

605 
subsection{*The Infinitely Close Relation*} 
14370  606 

607 
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)" 

608 
by (simp add: Infinitesimal_def approx_def) 

609 

610 
lemma approx_minus_iff: " (x @= y) = (x + y @= 0)" 

611 
by (simp add: approx_def) 

612 

613 
lemma approx_minus_iff2: " (x @= y) = (y + x @= 0)" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

614 
by (simp add: approx_def add_commute) 
14370  615 

15229  616 
lemma approx_refl [iff]: "x @= x" 
14370  617 
by (simp add: approx_def Infinitesimal_def) 
618 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

619 
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

620 
by (simp add: add_commute) 
14477  621 

14370  622 
lemma approx_sym: "x @= y ==> y @= x" 
623 
apply (simp add: approx_def) 

624 
apply (rule hypreal_minus_distrib1 [THEN subst]) 

625 
apply (erule Infinitesimal_minus_iff [THEN iffD2]) 

626 
done 

627 

628 
lemma approx_trans: "[ x @= y; y @= z ] ==> x @= z" 

629 
apply (simp add: approx_def) 

630 
apply (drule Infinitesimal_add, assumption, auto) 

631 
done 

632 

633 
lemma approx_trans2: "[ r @= x; s @= x ] ==> r @= s" 

634 
by (blast intro: approx_sym approx_trans) 

635 

636 
lemma approx_trans3: "[ x @= r; x @= s] ==> r @= s" 

637 
by (blast intro: approx_sym approx_trans) 

638 

639 
lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)" 

640 
by (blast intro: approx_sym) 

641 

642 
lemma zero_approx_reorient: "(0 @= x) = (x @= 0)" 

643 
by (blast intro: approx_sym) 

644 

645 
lemma one_approx_reorient: "(1 @= x) = (x @= 1)" 

646 
by (blast intro: approx_sym) 

10751  647 

648 

19765  649 
ML {* 
650 
local 

14370  651 
(*** reorientation, following HOL/Integ/Bin.ML 
652 
We reorient x @=y where x is 0, 1 or a numeral, unless y is as well! 

653 
***) 

654 

655 
(*reorientation simprules using ==, for the following simproc*) 

19765  656 
val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection; 
657 
val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection; 

658 
val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection 

14370  659 

660 
(*reorientation simplification procedure: reorients (polymorphic) 

661 
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) 

662 
fun reorient_proc sg _ (_ $ t $ u) = 

663 
case u of 

15531  664 
Const("0", _) => NONE 
665 
 Const("1", _) => NONE 

666 
 Const("Numeral.number_of", _) $ _ => NONE 

667 
 _ => SOME (case t of 

14370  668 
Const("0", _) => meta_zero_approx_reorient 
669 
 Const("1", _) => meta_one_approx_reorient 

670 
 Const("Numeral.number_of", _) $ _ => 

671 
meta_number_of_approx_reorient); 

672 

19765  673 
in 
14370  674 
val approx_reorient_simproc = 
20485  675 
Int_Numeral_Base_Simprocs.prep_simproc 
14370  676 
("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc); 
19765  677 
end; 
14370  678 

679 
Addsimprocs [approx_reorient_simproc]; 

680 
*} 

681 

682 
lemma Infinitesimal_approx_minus: "(xy \<in> Infinitesimal) = (x @= y)" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

683 
by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff) 
14370  684 

685 
lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))" 

686 
apply (simp add: monad_def) 

687 
apply (auto dest: approx_sym elim!: approx_trans equalityCE) 

688 
done 

689 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

690 
lemma Infinitesimal_approx: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

691 
"[ x \<in> Infinitesimal; y \<in> Infinitesimal ] ==> x @= y" 
14370  692 
apply (simp add: mem_infmal_iff) 
693 
apply (blast intro: approx_trans approx_sym) 

694 
done 

695 

696 
lemma approx_add: "[ a @= b; c @= d ] ==> a+c @= b+d" 

697 
proof (unfold approx_def) 

698 
assume inf: "a +  b \<in> Infinitesimal" "c +  d \<in> Infinitesimal" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

699 
have "a + c +  (b + d) = (a +  b) + (c +  d)" by simp 
14370  700 
also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add) 
701 
finally show "a + c +  (b + d) \<in> Infinitesimal" . 

702 
qed 

703 

704 
lemma approx_minus: "a @= b ==> a @= b" 

705 
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym]) 

706 
apply (drule approx_minus_iff [THEN iffD1]) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

707 
apply (simp (no_asm) add: add_commute) 
14370  708 
done 
709 

710 
lemma approx_minus2: "a @= b ==> a @= b" 

711 
by (auto dest: approx_minus) 

712 

15229  713 
lemma approx_minus_cancel [simp]: "(a @= b) = (a @= b)" 
14370  714 
by (blast intro: approx_minus approx_minus2) 
715 

716 
lemma approx_add_minus: "[ a @= b; c @= d ] ==> a + c @= b + d" 

717 
by (blast intro!: approx_add approx_minus) 

718 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

719 
lemma approx_mult1: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

720 
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

721 
shows "[ a @= b; c: HFinite] ==> a*c @= b*c" 
14370  722 
by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left 
723 
left_distrib [symmetric] 

724 
del: minus_mult_left [symmetric]) 

725 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

726 
lemma approx_mult2: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

727 
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

728 
shows "[a @= b; c: HFinite] ==> c*a @= c*b" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

729 
by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

730 
right_distrib [symmetric] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

731 
del: minus_mult_right [symmetric]) 
14370  732 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

733 
lemma approx_mult_subst: 
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 @= v*x; x @= y; v \<in> HFinite] ==> u @= v*y" 
14370  736 
by (blast intro: approx_mult2 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_subst2: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

739 
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

740 
shows "[ u @= x*v; x @= y; v \<in> HFinite ] ==> u @= y*v" 
14370  741 
by (blast intro: approx_mult1 approx_trans) 
742 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

743 
lemma approx_mult_subst_star_of: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

744 
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

745 
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

746 
by (auto intro: approx_mult_subst2) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

747 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

748 
lemma approx_mult_subst_SReal: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

749 
"[ u @= x*hypreal_of_real v; x @= y ] ==> u @= y*hypreal_of_real v" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

750 
by (rule approx_mult_subst_star_of) 
14370  751 

752 
lemma approx_eq_imp: "a = b ==> a @= b" 

753 
by (simp add: approx_def) 

754 

755 
lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> x @= x" 

756 
by (blast intro: Infinitesimal_minus_iff [THEN iffD2] 

757 
mem_infmal_iff [THEN iffD1] approx_trans2) 

758 

759 
lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x + z = y) = (x @= z)" 

760 
by (simp add: approx_def) 

761 

762 
lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)" 

763 
by (force simp add: bex_Infinitesimal_iff [symmetric]) 

764 

765 
lemma Infinitesimal_add_approx: "[ y \<in> Infinitesimal; x + y = z ] ==> x @= z" 

766 
apply (rule bex_Infinitesimal_iff [THEN iffD1]) 

767 
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

768 
apply (auto simp add: add_assoc [symmetric]) 
14370  769 
done 
770 

771 
lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y" 

772 
apply (rule bex_Infinitesimal_iff [THEN iffD1]) 

773 
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

774 
apply (auto simp add: add_assoc [symmetric]) 
14370  775 
done 
776 

777 
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

778 
by (auto dest: Infinitesimal_add_approx_self simp add: add_commute) 
14370  779 

780 
lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + y" 

781 
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) 

782 

783 
lemma Infinitesimal_add_cancel: "[ y \<in> Infinitesimal; x+y @= z] ==> x @= z" 

784 
apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym]) 

785 
apply (erule approx_trans3 [THEN approx_sym], assumption) 

786 
done 

787 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

788 
lemma Infinitesimal_add_right_cancel: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

789 
"[ y \<in> Infinitesimal; x @= z + y] ==> x @= z" 
14370  790 
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym]) 
791 
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

792 
apply (simp add: add_commute) 
14370  793 
apply (erule approx_sym) 
794 
done 

795 

796 
lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" 

797 
apply (drule approx_minus_iff [THEN iffD1]) 

15539  798 
apply (simp add: approx_minus_iff [symmetric] add_ac) 
14370  799 
done 
800 

801 
lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" 

802 
apply (rule approx_add_left_cancel) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

803 
apply (simp add: add_commute) 
14370  804 
done 
805 

806 
lemma approx_add_mono1: "b @= c ==> d + b @= d + c" 

807 
apply (rule approx_minus_iff [THEN iffD2]) 

15539  808 
apply (simp add: approx_minus_iff [symmetric] add_ac) 
14370  809 
done 
810 

811 
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

812 
by (simp add: add_commute approx_add_mono1) 
14370  813 

15229  814 
lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)" 
14370  815 
by (fast elim: approx_add_left_cancel approx_add_mono1) 
816 

15229  817 
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

818 
by (simp add: add_commute) 
14370  819 

820 
lemma approx_HFinite: "[ x \<in> HFinite; x @= y ] ==> y \<in> HFinite" 

821 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) 

822 
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]]) 

823 
apply (drule HFinite_add) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

824 
apply (auto simp add: add_assoc) 
14370  825 
done 
826 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

827 
lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite" 
14370  828 
by (rule approx_sym [THEN [2] approx_HFinite], auto) 
829 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

830 
lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

831 
by (rule approx_star_of_HFinite) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

832 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

833 
lemma approx_mult_HFinite: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

834 
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

835 
shows "[a @= b; c @= d; b: HFinite; d: HFinite] ==> a*c @= b*d" 
14370  836 
apply (rule approx_trans) 
837 
apply (rule_tac [2] approx_mult2) 

838 
apply (rule approx_mult1) 

839 
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto) 

840 
done 

841 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

842 
lemma approx_mult_star_of: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

843 
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

844 
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

845 
==> 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

846 
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

847 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

848 
lemma approx_mult_hypreal_of_real: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

849 
"[a @= hypreal_of_real b; c @= hypreal_of_real d ] 
14370  850 
==> a*c @= hypreal_of_real b*hypreal_of_real d" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

851 
by (rule approx_mult_star_of) 
14370  852 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

853 
lemma approx_SReal_mult_cancel_zero: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

854 
"[ (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 ] ==> x @= 0" 
14370  855 
apply (drule SReal_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

856 
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) 
14370  857 
done 
858 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

859 
lemma approx_mult_SReal1: "[ (a::hypreal) \<in> Reals; x @= 0 ] ==> x*a @= 0" 
14370  860 
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) 
861 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

862 
lemma approx_mult_SReal2: "[ (a::hypreal) \<in> Reals; x @= 0 ] ==> a*x @= 0" 
14370  863 
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) 
864 

15229  865 
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

866 
"[(a::hypreal) \<in> Reals; a \<noteq> 0 ] ==> (a*x @= 0) = (x @= 0)" 
14370  867 
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) 
868 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

869 
lemma approx_SReal_mult_cancel: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

870 
"[ (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z ] ==> w @= z" 
14370  871 
apply (drule SReal_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

872 
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) 
14370  873 
done 
874 

15229  875 
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

876 
"[ (a::hypreal) \<in> Reals; a \<noteq> 0] ==> (a* w @= a*z) = (w @= z)" 
15229  877 
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] 
878 
intro: approx_SReal_mult_cancel) 

14370  879 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

880 
lemma approx_le_bound: "[ (z::hypreal) \<le> f; f @= g; g \<le> z ] ==> f @= z" 
14370  881 
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) 
882 
apply (rule_tac x = "g+yz" in bexI) 

883 
apply (simp (no_asm)) 

884 
apply (rule Infinitesimal_interval2) 

885 
apply (rule_tac [2] Infinitesimal_zero, auto) 

886 
done 

887 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

888 

15539  889 
subsection{* Zero is the Only Infinitesimal that is also a Real*} 
14370  890 

891 
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

892 
"[ (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x ] ==> y < x" 
14370  893 
apply (simp add: Infinitesimal_def) 
894 
apply (rule abs_ge_self [THEN order_le_less_trans], auto) 

895 
done 

896 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

897 
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

898 
"(y::hypreal) \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r > y < r" 
14370  899 
by (blast intro: Infinitesimal_less_SReal) 
900 

901 
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

902 
"[ 0 < y; (y::hypreal) \<in> Reals] ==> y \<notin> Infinitesimal" 
14370  903 
apply (simp add: Infinitesimal_def) 
15003  904 
apply (auto simp add: abs_if) 
14370  905 
done 
906 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

907 
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

908 
"[ y < 0; (y::hypreal) \<in> Reals ] ==> y \<notin> Infinitesimal" 
14370  909 
apply (subst Infinitesimal_minus_iff [symmetric]) 
910 
apply (rule SReal_not_Infinitesimal, auto) 

911 
done 

912 

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

913 
lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}" 
14370  914 
apply auto 
915 
apply (cut_tac x = x and y = 0 in linorder_less_linear) 

916 
apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) 

917 
done 

918 

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 
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

920 
"[ (x::hypreal) \<in> Reals; x \<in> Infinitesimal] ==> x = 0" 
14370  921 
by (cut_tac SReal_Int_Infinitesimal_zero, blast) 
922 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

923 
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

924 
"[ (x::hypreal) \<in> Reals; x \<noteq> 0 ] ==> x \<in> HFinite  Infinitesimal" 
14370  925 
by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD]) 
926 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

927 
lemma hypreal_of_real_HFinite_diff_Infinitesimal: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

928 
"hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite  Infinitesimal" 
14370  929 
by (rule SReal_HFinite_diff_Infinitesimal, auto) 
930 

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

931 
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

932 
"(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

933 
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

934 
apply (drule_tac x="hnorm (star_of x)" in bspec) 
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 
apply (simp add: hnorm_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

936 
apply simp 
14370  937 
done 
938 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

939 
lemma star_of_HFinite_diff_Infinitesimal: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

940 
"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

941 
by simp 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

942 

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

943 
lemma hypreal_of_real_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

944 
"(hypreal_of_real 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

945 
by (rule 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

946 

15229  947 
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

948 
"number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal" 
14370  949 
by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero]) 
950 

951 
(*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

952 
lemma one_not_Infinitesimal [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

953 
"(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> 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

954 
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

955 
apply simp 
14370  956 
done 
957 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

958 
lemma approx_SReal_not_zero: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

959 
"[ (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 ] ==> x \<noteq> 0" 
14370  960 
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp) 
961 
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal) 

962 
done 

963 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

964 
lemma HFinite_diff_Infinitesimal_approx: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

965 
"[ x @= y; y \<in> HFinite  Infinitesimal ] 
14370  966 
==> x \<in> HFinite  Infinitesimal" 
967 
apply (auto intro: approx_sym [THEN [2] approx_HFinite] 

968 
simp add: mem_infmal_iff) 

969 
apply (drule approx_trans3, assumption) 

970 
apply (blast dest: approx_sym) 

971 
done 

972 

973 
(*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the 

974 
HFinite premise.*) 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

975 
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

976 
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

977 
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

978 
==> x \<in> Infinitesimal" 
14370  979 
apply (drule Infinitesimal_HFinite_mult2, assumption) 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

980 
apply (simp add: divide_inverse mult_assoc) 
14370  981 
done 
982 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

983 
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

984 
"[ (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

985 
apply (simp add: divide_inverse) 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

986 
apply (auto intro!: Infinitesimal_HFinite_mult 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

987 
dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]]) 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

988 
done 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

989 

14370  990 
(* 
991 
Standard Part Theorem: Every finite x: R* is infinitely 

992 
close to a unique real number (i.e a member of Reals) 

993 
*) 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

994 

4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

995 
subsection{* Uniqueness: Two Infinitely Close Reals are Equal*} 
14370  996 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

997 
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

998 
apply safe 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

999 
apply (simp add: approx_def) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1000 
apply (simp only: star_of_minus [symmetric] star_of_add [symmetric]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1001 
apply (simp only: star_of_Infinitesimal_iff_0) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1002 
apply (simp only: diff_minus [symmetric] right_minus_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1003 
done 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1004 

2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1005 
lemma SReal_approx_iff: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1006 
"[(x::hypreal) \<in> Reals; y \<in> Reals] ==> (x @= y) = (x = y)" 
14370  1007 
apply auto 
1008 
apply (simp add: approx_def) 

1009 
apply (drule_tac x = y in SReal_minus) 

1010 
apply (drule SReal_add, assumption) 

1011 
apply (drule SReal_Infinitesimal_zero, assumption) 

1012 
apply (drule sym) 

1013 
apply (simp add: hypreal_eq_minus_iff [symmetric]) 

1014 
done 

1015 

15229  1016 
lemma number_of_approx_iff [simp]: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1017 
"(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

1018 
(number_of v = (number_of w :: 'a))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1019 
apply (unfold star_number_def) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1020 
apply (rule star_of_approx_iff) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1021 
done 
14370  1022 

1023 
(*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

1024 
lemma [simp]: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1025 
"(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

1026 
(number_of w = (0::'a))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1027 
"((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

1028 
(number_of w = (0::'a))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1029 
"(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

1030 
(number_of w = (1::'b))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1031 
"((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

1032 
(number_of w = (1::'b))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1033 
"~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1034 
"~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1035 
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

1036 
apply (unfold star_of_approx_iff) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1037 
by (auto intro: sym) 
14370  1038 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1039 
lemma hypreal_of_real_approx_iff: 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1040 
"(hypreal_of_real k @= hypreal_of_real m) = (k = m)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1041 
by (rule star_of_approx_iff) 
14370  1042 

15229  1043 
lemma hypreal_of_real_approx_number_of_iff [simp]: 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1044 
"(hypreal_of_real k @= number_of w) = (k = number_of w)" 
14370  1045 
by (subst hypreal_of_real_approx_iff [symmetric], auto) 
1046 

1047 
(*And also for 0 and 1.*) 

1048 
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) 

1049 
lemma [simp]: "(hypreal_of_real k @= 0) = (k = 0)" 

1050 
"(hypreal_of_real k @= 1) = (k = 1)" 

1051 
by (simp_all add: hypreal_of_real_approx_iff [symmetric]) 

1052 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1053 
lemma approx_unique_real: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1054 
"[ (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x] ==> r = s" 
14370  1055 
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) 
1056 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1057 

4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1058 
subsection{* Existence of Unique Real Infinitely Close*} 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1059 

14370  1060 
(* lemma about lubs *) 
1061 
lemma hypreal_isLub_unique: 

1062 
"[ isLub R S x; isLub R S y ] ==> x = (y::hypreal)" 

1063 
apply (frule isLub_isUb) 

1064 
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

1065 
apply (blast intro!: order_antisym dest!: isLub_le_isUb) 
14370  1066 
done 
1067 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1068 
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

1069 
"(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u" 
14370  1070 
apply (drule HFiniteD, safe) 
1071 
apply (rule exI, rule isUbI) 

1072 
apply (auto intro: setleI isUbI simp add: abs_less_iff) 

1073 
done 

1074 

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

1075 
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

1076 
"(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}" 
14370  1077 
apply (drule HFiniteD, safe) 
1078 
apply (drule SReal_minus) 

1079 
apply (rule_tac x = "t" in exI) 

1080 
apply (auto simp add: abs_less_iff) 

1081 
done 

1082 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1083 
lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals" 
14370  1084 
by auto 
1085 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1086 
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

1087 
"(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t" 
14370  1088 
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset) 
1089 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1090 
lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)" 
14370  1091 
apply safe 
1092 
apply (drule_tac c = "t" in add_left_mono) 

1093 
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

1094 
apply (auto simp add: add_assoc [symmetric]) 
14370  1095 
done 
1096 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1097 
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

1098 
"[ (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

1099 
r \<in> Reals; 0 < r ] ==> x \<le> t + r" 
14370  1100 
apply (frule isLubD1a) 
1101 
apply (rule ccontr, drule linorder_not_le [THEN iffD2]) 

1102 
apply (drule_tac x = t in SReal_add, assumption) 

1103 
apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto) 

1104 
done 

1105 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1106 
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

1107 
"[ S *<= (x::hypreal); x < y ] ==> S *<= y" 
14370  1108 
apply (simp add: setle_def) 
1109 
apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le) 

1110 
done 

1111 

1112 
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

1113 
"[ isUb R S (x::hypreal); x < y; y \<in> R ] ==> isUb R S y" 
14370  1114 
apply (simp add: isUb_def) 
1115 
apply (blast intro: hypreal_setle_less_trans) 

1116 
done 

1117 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1118 
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

1119 
"[ (x::hypreal) \<in> HFinite; x < y; y \<in> Reals ] 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1120 
==> isUb Reals {s. s \<in> Reals & s < x} y" 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1121 
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI) 
14370  1122 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1123 
lemma lemma_minus_le_zero: "t \<le> t + r ==> r \<le> (0::hypreal)" 
14370  1124 
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

1125 
apply (auto simp add: add_assoc [symmetric]) 
14370  1126 
done 
1127 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1128 
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

1129 
"[ (x::hypreal) \<in> HFinite; 
14370  1130 
isLub Reals {s. s \<in> Reals & s < x} t; 
1131 
r \<in> Reals; 0 < r ] 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1132 
==> t + r \<le> x" 
14370  1133 
apply (frule isLubD1a) 
1134 
apply (rule ccontr, drule linorder_not_le [THEN iffD1]) 

1135 
apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption) 

1136 
apply (drule lemma_st_part_gt_ub, assumption+) 

1137 
apply (drule isLub_le_isUb, assumption) 

1138 
apply (drule lemma_minus_le_zero) 

1139 
apply (auto dest: order_less_le_trans) 

1140 
done 

1141 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1142 
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

1143 
"[ (x::hypreal) \<in> HFinite; 
14370  1144 
isLub Reals {s. s \<in> Reals & s < x} t; 
1145 
r \<in> Reals; 0 < r ] 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1146 
==> x + t \<le> r" 
15229  1147 
apply (subgoal_tac "x \<le> t+r") 
1148 
apply (auto intro: lemma_st_part_le1) 

1149 
done 

14370  1150 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1151 
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

1152 
"[ (x::hypreal) \<in> HFinite; 
14370  1153 
isLub Reals {s. s \<in> Reals & s < x} t; 
1154 
r \<in> Reals; 0 < r ] 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1155 
==> (x + t) \<le> r" 
15229  1156 
apply (subgoal_tac "(t + r \<le> x)") 
1157 
apply (auto intro: lemma_st_part_le2) 

14370  1158 
done 
1159 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1160 
lemma lemma_SReal_ub: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1161 
"(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x" 
14370  1162 
by (auto intro: isUbI setleI order_less_imp_le) 
1163 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1164 
lemma lemma_SReal_lub: 
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1165 
"(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x" 
14370  1166 
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI) 
1167 
apply (frule isUbD2a) 

1168 
apply (rule_tac x = x and y = y in linorder_cases) 

1169 
apply (auto intro!: order_less_imp_le) 

1170 
apply (drule SReal_dense, assumption, assumption, safe) 

1171 
apply (drule_tac y = r in isUbD) 

1172 
apply (auto dest: order_less_le_trans) 

1173 
done 

1174 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1175 
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

1176 
"[ (x::hypreal) \<in> HFinite; 
14370  1177 
isLub Reals {s. s \<in> Reals & s < x} t; 
1178 
r \<in> Reals; 0 < r ] 

1179 
==> x + t \<noteq> r" 

1180 
apply auto 

1181 
apply (frule isLubD1a [THEN SReal_minus]) 

1182 
apply (drule SReal_add_cancel, assumption) 

1183 
apply (drule_tac x = x in lemma_SReal_lub) 

1184 
apply (drule hypreal_isLub_unique, assumption, auto) 

1185 
done 

1186 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1187 
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

1188 
"[ (x::hypreal) \<in> HFinite; 
14370  1189 
isLub Reals {s. s \<in> Reals & s < x} t; 
1190 
r \<in> Reals; 0 < r ] 

1191 
==> (x + t) \<noteq> r" 

15539  1192 
apply (auto) 
14370  1193 
apply (frule isLubD1a) 
1194 
apply (drule SReal_add_cancel, assumption) 

1195 
apply (drule_tac x = "x" in SReal_minus, simp) 

1196 
apply (drule_tac x = x in lemma_SReal_lub) 

1197 
apply (drule hypreal_isLub_unique, assumption, auto) 

1198 
done 

1199 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1200 
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

1201 
"[ (x::hypreal) \<in> HFinite; 
14370  1202 
isLub Reals {s. s \<in> Reals & s < x} t; 
1203 
r \<in> Reals; 0 < r ] 

1204 
==> abs (x + t) < r" 

1205 
apply (frule lemma_st_part1a) 

1206 
apply (frule_tac [4] lemma_st_part2a, auto) 

1207 
apply (drule order_le_imp_less_or_eq)+ 

1208 
apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff) 

1209 
done 

1210 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1211 
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

1212 
"[ (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t ] 
14370  1213 
==> \<forall>r \<in> Reals. 0 < r > abs (x + t) < r" 
14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1214 
by (blast dest!: lemma_st_part_major) 
14370  1215 

15229  1216 

1217 
text{*Existence of real and Standard Part Theorem*} 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1218 
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

1219 
"(x::hypreal) \<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

1220 
==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r > abs (x + t) < r" 
14370  1221 
apply (frule lemma_st_part_lub, safe) 
1222 
apply (frule isLubD1a) 

1223 
apply (blast dest: lemma_st_part_major2) 

1224 
done 

1225 

1226 
lemma st_part_Ex: 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20541
diff
changeset

1227 
"(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t" 
14370  1228 
apply (simp add: approx_def Infinitesimal_def) 
1229 
apply (drule lemma_st_part_Ex, auto) 

1230 
done 

1231 

15229  1232 
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

1233 
lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t" 
14370  1234 
apply (drule st_part_Ex, safe) 
1235 
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) 

1236 
apply (auto intro!: approx_unique_real) 

1237 
done 

1238 

14420
4e72cd222e0b
converted Hyperreal/HTranscendental to Isar script
paulson
parents:
14387
diff
changeset

1239 
subsection{* Finite, Infinite and Infinitesimal*} 
14370  1240 

15229  1241 
lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" 
14370  1242 
apply (simp add: HFinite_def HInfinite_def) 
1243 
apply (auto dest: order_less_trans) 

1244 
done 

1245 

1246 
lemma HFinite_not_HInfinite: 

1247 
assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite" 

1248 
proof 

1249 
assume x': "x \<in> HInfinite" 
