author  huffman 
Sun, 24 Sep 2006 01:04:44 +0200  
changeset 20686  e3d2b881ed0f 
parent 20563  44eda2314aab 
child 20724  a1a8ba09e0ea 
permissions  rwrr 
13957  1 
(* Title : NSCA.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 2001,2002 University of Edinburgh 

4 
*) 

5 

14408  6 
header{*NonStandard Complex Analysis*} 
13957  7 

15131  8 
theory NSCA 
15140  9 
imports NSComplex 
15131  10 
begin 
13957  11 

19765  12 
definition 
13957  13 
(* standard complex numbers reagarded as an embedded subset of NS complex *) 
14 
SComplex :: "hcomplex set" 

19765  15 
"SComplex = {x. \<exists>r. x = hcomplex_of_complex r}" 
13957  16 

14408  17 
stc :: "hcomplex => hcomplex" 
18 
{* standard part map*} 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

19 
"stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)" 
14408  20 

21 

22 
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} 

23 

24 
lemma SComplex_add: "[ x \<in> SComplex; y \<in> SComplex ] ==> x + y \<in> SComplex" 

25 
apply (simp add: SComplex_def, safe) 

26 
apply (rule_tac x = "r + ra" in exI, simp) 

27 
done 

28 

29 
lemma SComplex_mult: "[ x \<in> SComplex; y \<in> SComplex ] ==> x * y \<in> SComplex" 

30 
apply (simp add: SComplex_def, safe) 

31 
apply (rule_tac x = "r * ra" in exI, simp) 

32 
done 

33 

34 
lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex" 

35 
apply (simp add: SComplex_def) 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

36 
apply (blast intro: star_of_inverse [symmetric]) 
14408  37 
done 
38 

39 
lemma SComplex_divide: "[ x \<in> SComplex; y \<in> SComplex ] ==> x/y \<in> SComplex" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14408
diff
changeset

40 
by (simp add: SComplex_mult SComplex_inverse divide_inverse) 
14408  41 

42 
lemma SComplex_minus: "x \<in> SComplex ==> x \<in> SComplex" 

43 
apply (simp add: SComplex_def) 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

44 
apply (blast intro: star_of_minus [symmetric]) 
14408  45 
done 
46 

47 
lemma SComplex_minus_iff [simp]: "(x \<in> SComplex) = (x \<in> SComplex)" 

48 
apply auto 

49 
apply (erule_tac [2] SComplex_minus) 

50 
apply (drule SComplex_minus, auto) 

51 
done 

52 

53 
lemma SComplex_diff: "[ x \<in> SComplex; y \<in> SComplex ] ==> x  y \<in> SComplex" 

54 
by (simp add: diff_minus SComplex_add) 

55 

56 
lemma SComplex_add_cancel: 

57 
"[ x + y \<in> SComplex; y \<in> SComplex ] ==> x \<in> SComplex" 

58 
by (drule SComplex_diff, assumption, simp) 

59 

60 
lemma SReal_hcmod_hcomplex_of_complex [simp]: 

61 
"hcmod (hcomplex_of_complex r) \<in> Reals" 

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

62 
by (auto simp add: hcmod SReal_def star_of_def) 
14408  63 

64 
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals" 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

65 
apply (subst star_of_number_of [symmetric]) 
14408  66 
apply (rule SReal_hcmod_hcomplex_of_complex) 
67 
done 

68 

69 
lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals" 

70 
by (auto simp add: SComplex_def) 

71 

72 
lemma SComplex_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> SComplex" 

73 
by (simp add: SComplex_def) 

74 

75 
lemma SComplex_number_of [simp]: "(number_of w ::hcomplex) \<in> SComplex" 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

76 
apply (subst star_of_number_of [symmetric]) 
14408  77 
apply (rule SComplex_hcomplex_of_complex) 
78 
done 

79 

80 
lemma SComplex_divide_number_of: 

81 
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14408
diff
changeset

82 
apply (simp only: divide_inverse) 
14408  83 
apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse) 
84 
done 

85 

86 
lemma SComplex_UNIV_complex: 

87 
"{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" 

88 
by (simp add: SComplex_def) 

89 

90 
lemma SComplex_iff: "(x \<in> SComplex) = (\<exists>y. x = hcomplex_of_complex y)" 

91 
by (simp add: SComplex_def) 

92 

93 
lemma hcomplex_of_complex_image: 

94 
"hcomplex_of_complex `(UNIV::complex set) = SComplex" 

95 
by (auto simp add: SComplex_def) 

96 

97 
lemma inv_hcomplex_of_complex_image: "inv hcomplex_of_complex `SComplex = UNIV" 

98 
apply (auto simp add: SComplex_def) 

99 
apply (rule inj_hcomplex_of_complex [THEN inv_f_f, THEN subst], blast) 

100 
done 

101 

102 
lemma SComplex_hcomplex_of_complex_image: 

103 
"[ \<exists>x. x: P; P \<le> SComplex ] ==> \<exists>Q. P = hcomplex_of_complex ` Q" 

104 
apply (simp add: SComplex_def, blast) 

105 
done 

106 

107 
lemma SComplex_SReal_dense: 

108 
"[ x \<in> SComplex; y \<in> SComplex; hcmod x < hcmod y 

109 
] ==> \<exists>r \<in> Reals. hcmod x< r & r < hcmod y" 

110 
apply (auto intro: SReal_dense simp add: SReal_hcmod_SComplex) 

111 
done 

112 

113 
lemma SComplex_hcmod_SReal: 

114 
"z \<in> SComplex ==> hcmod z \<in> Reals" 

20686  115 
by (auto simp add: SComplex_def) 
14408  116 

117 
lemma SComplex_zero [simp]: "0 \<in> SComplex" 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

118 
by (simp add: SComplex_def) 
14408  119 

120 
lemma SComplex_one [simp]: "1 \<in> SComplex" 

17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset

121 
by (simp add: SComplex_def) 
14408  122 

123 
(* 

124 
Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> SComplex" 

125 
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); 

126 
by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def, 

127 
hcomplex_of_complex_def,cmod_def])); 

128 
*) 

129 

130 

131 
subsection{*The Finite Elements form a Subring*} 

132 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

133 
lemma SComplex_subset_HFinite [simp]: "SComplex \<le> HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

134 
apply (auto simp add: SComplex_def HFinite_def) 
14408  135 
apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI) 
136 
apply (auto intro: SReal_add) 

137 
done 

138 

139 
lemma HFinite_hcmod_hcomplex_of_complex [simp]: 

140 
"hcmod (hcomplex_of_complex r) \<in> HFinite" 

141 
by (auto intro!: SReal_subset_HFinite [THEN subsetD]) 

142 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

143 
lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \<in> HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

144 
by (rule HFinite_star_of) 
14408  145 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

146 
lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

147 
by (simp add: HFinite_def) 
14408  148 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

149 
lemma HFinite_bounded_hcmod: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

150 
"[x \<in> HFinite; y \<le> hcmod x; 0 \<le> y ] ==> y: HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

151 
by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff) 
14408  152 

153 

154 
subsection{*The Complex Infinitesimals form a Subring*} 

155 

156 
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" 

157 
by auto 

158 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

159 
lemma Infinitesimal_hcmod_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

160 
"(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

161 
by (simp add: Infinitesimal_def) 
14408  162 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

163 
lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

164 
by (simp add: HInfinite_def) 
14408  165 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

166 
lemma HFinite_diff_Infinitesimal_hcmod: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

167 
"x \<in> HFinite  Infinitesimal ==> hcmod x \<in> HFinite  Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

168 
by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff) 
14408  169 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

170 
lemma hcmod_less_Infinitesimal: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

171 
"[ e \<in> Infinitesimal; hcmod x < hcmod e ] ==> x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

172 
by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) 
14408  173 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

174 
lemma hcmod_le_Infinitesimal: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

175 
"[ e \<in> Infinitesimal; hcmod x \<le> hcmod e ] ==> x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

176 
by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) 
14408  177 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

178 
lemma Infinitesimal_interval_hcmod: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

179 
"[ e \<in> Infinitesimal; 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

180 
e' \<in> Infinitesimal; 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

181 
hcmod e' < hcmod x ; hcmod x < hcmod e 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

182 
] ==> x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

183 
by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff) 
14408  184 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

185 
lemma Infinitesimal_interval2_hcmod: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

186 
"[ e \<in> Infinitesimal; 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

187 
e' \<in> Infinitesimal; 
14408  188 
hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

189 
] ==> x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

190 
by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff) 
14408  191 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

192 
lemma Infinitesimal_hcomplex_of_complex_mult: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

193 
"x \<in> Infinitesimal ==> x * hcomplex_of_complex r \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

194 
by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult) 
14408  195 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

196 
lemma Infinitesimal_hcomplex_of_complex_mult2: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

197 
"x \<in> Infinitesimal ==> hcomplex_of_complex r * x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

198 
by (auto intro!: Infinitesimal_HFinite_mult2 simp add: Infinitesimal_hcmod_iff hcmod_mult) 
14408  199 

200 

201 
subsection{*The ``Infinitely Close'' Relation*} 

202 

203 
(* 

204 
Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)" 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

205 
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); 
14408  206 
*) 
207 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

208 
lemma approx_mult_subst_SComplex: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

209 
"[ u @= x*hcomplex_of_complex v; x @= y ] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

210 
==> u @= y*hcomplex_of_complex v" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

211 
by (auto intro: approx_mult_subst2) 
14408  212 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

213 
lemma approx_hcomplex_of_complex_HFinite: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

214 
"x @= hcomplex_of_complex D ==> x \<in> HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

215 
by (rule approx_star_of_HFinite) 
14408  216 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

217 
lemma approx_mult_hcomplex_of_complex: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

218 
"[a @= hcomplex_of_complex b; c @= hcomplex_of_complex d ] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

219 
==> a*c @= hcomplex_of_complex b * hcomplex_of_complex d" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

220 
by (rule approx_mult_star_of) 
14408  221 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

222 
lemma approx_SComplex_mult_cancel_zero: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

223 
"[ a \<in> SComplex; a \<noteq> 0; a*x @= 0 ] ==> x @= 0" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

224 
apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

225 
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) 
14408  226 
done 
227 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

228 
lemma approx_mult_SComplex1: "[ a \<in> SComplex; x @= 0 ] ==> x*a @= 0" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

229 
by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1) 
14408  230 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

231 
lemma approx_mult_SComplex2: "[ a \<in> SComplex; x @= 0 ] ==> a*x @= 0" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

232 
by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult2) 
14408  233 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

234 
lemma approx_mult_SComplex_zero_cancel_iff [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

235 
"[a \<in> SComplex; a \<noteq> 0 ] ==> (a*x @= 0) = (x @= 0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

236 
by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2) 
14408  237 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

238 
lemma approx_SComplex_mult_cancel: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

239 
"[ a \<in> SComplex; a \<noteq> 0; a* w @= a*z ] ==> w @= z" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

240 
apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

241 
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) 
14408  242 
done 
243 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

244 
lemma approx_SComplex_mult_cancel_iff1 [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

245 
"[ a \<in> SComplex; a \<noteq> 0] ==> (a* w @= a*z) = (w @= z)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

246 
by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

247 
intro: approx_SComplex_mult_cancel) 
14408  248 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

249 
lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y  x) @= 0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

250 
apply (subst hcmod_diff_commute) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

251 
apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) 
14408  252 
done 
253 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

254 
lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

255 
by (simp add: approx_hcmod_approx_zero) 
14408  256 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

257 
lemma approx_minus_zero_cancel_iff [simp]: "(x @= 0) = (x @= 0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

258 
by (simp add: approx_def) 
14408  259 

260 
lemma Infinitesimal_hcmod_add_diff: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

261 
"u @= 0 ==> hcmod(x + u)  hcmod x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

262 
apply (drule approx_approx_zero_iff [THEN iffD1]) 
14408  263 
apply (rule_tac e = "hcmod u" and e' = " hcmod u" in Infinitesimal_interval2) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

264 
apply (auto simp add: mem_infmal_iff [symmetric] diff_def) 
14408  265 
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) 
266 
apply (auto simp add: diff_minus [symmetric]) 

267 
done 

268 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

269 
lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x" 
14408  270 
apply (rule approx_minus_iff [THEN iffD2]) 
271 
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) 

272 
done 

273 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

274 
lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y" 
14408  275 
by (auto intro: approx_hcmod_add_hcmod 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

276 
dest!: bex_Infinitesimal_iff2 [THEN iffD2] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

277 
simp add: mem_infmal_iff) 
13957  278 

279 

14408  280 
subsection{*Zero is the Only Infinitesimal Complex Number*} 
281 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

282 
lemma Infinitesimal_less_SComplex: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

283 
"[ x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x ] ==> hcmod y < hcmod x" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

284 
by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff) 
14408  285 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

286 
lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

287 
by (auto simp add: SComplex_def Infinitesimal_hcmod_iff) 
14408  288 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

289 
lemma SComplex_Infinitesimal_zero: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

290 
"[ x \<in> SComplex; x \<in> Infinitesimal] ==> x = 0" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

291 
by (cut_tac SComplex_Int_Infinitesimal_zero, blast) 
14408  292 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

293 
lemma SComplex_HFinite_diff_Infinitesimal: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

294 
"[ x \<in> SComplex; x \<noteq> 0 ] ==> x \<in> HFinite  Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

295 
by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD]) 
14408  296 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

297 
lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

298 
"hcomplex_of_complex x \<noteq> 0 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

299 
==> hcomplex_of_complex x \<in> HFinite  Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

300 
by (rule SComplex_HFinite_diff_Infinitesimal, auto) 
14408  301 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

302 
lemma hcomplex_of_complex_Infinitesimal_iff_0: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

303 
"(hcomplex_of_complex x \<in> Infinitesimal) = (x=0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

304 
by (rule star_of_Infinitesimal_iff_0) 
14408  305 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

306 
lemma number_of_not_Infinitesimal [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

307 
"number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

308 
by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) 
14408  309 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

310 
lemma approx_SComplex_not_zero: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

311 
"[ y \<in> SComplex; x @= y; y\<noteq> 0 ] ==> x \<noteq> 0" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

312 
by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) 
14408  313 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

314 
lemma SComplex_approx_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

315 
"[x \<in> SComplex; y \<in> SComplex] ==> (x @= y) = (x = y)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

316 
by (auto simp add: SComplex_def) 
14408  317 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

318 
lemma number_of_Infinitesimal_iff [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

319 
"((number_of w :: hcomplex) \<in> Infinitesimal) = 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

320 
(number_of w = (0::hcomplex))" 
14408  321 
apply (rule iffI) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

322 
apply (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) 
14408  323 
apply (simp (no_asm_simp)) 
324 
done 

325 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

326 
lemma hcomplex_of_complex_approx_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

327 
"(hcomplex_of_complex k @= hcomplex_of_complex m) = (k = m)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

328 
by (rule star_of_approx_iff) 
14408  329 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

330 
lemma hcomplex_of_complex_approx_number_of_iff [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

331 
"(hcomplex_of_complex k @= number_of w) = (k = number_of w)" 
14408  332 
by (subst hcomplex_of_complex_approx_iff [symmetric], auto) 
333 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

334 
lemma approx_unique_complex: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

335 
"[ r \<in> SComplex; s \<in> SComplex; r @= x; s @= x] ==> r = s" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

336 
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) 
14408  337 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

338 
lemma hcomplex_approxD1: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

339 
"star_n X @= star_n Y 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

340 
==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

341 
apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

342 
apply (drule approx_minus_iff [THEN iffD1]) 
20563  343 
apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

344 
apply (drule_tac x = m in spec) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

345 
apply (erule ultra, rule FreeUltrafilterNat_all, clarify) 
20563  346 
apply (rule_tac y="cmod (X n  Y n)" in order_le_less_trans) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

347 
apply (case_tac "X n") 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

348 
apply (case_tac "Y n") 
20563  349 
apply (auto simp add: complex_diff complex_mod 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

350 
simp del: realpow_Suc) 
14408  351 
done 
352 

353 
(* same proof *) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

354 
lemma hcomplex_approxD2: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

355 
"star_n X @= star_n Y 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

356 
==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

357 
apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

358 
apply (drule approx_minus_iff [THEN iffD1]) 
20563  359 
apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

360 
apply (drule_tac x = m in spec) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

361 
apply (erule ultra, rule FreeUltrafilterNat_all, clarify) 
20563  362 
apply (rule_tac y="cmod (X n  Y n)" in order_le_less_trans) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

363 
apply (case_tac "X n") 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

364 
apply (case_tac "Y n") 
20563  365 
apply (auto simp add: complex_diff complex_mod 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

366 
simp del: realpow_Suc) 
14408  367 
done 
368 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

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

370 
"[ star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

371 
star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

372 
] ==> star_n X @= star_n Y" 
14408  373 
apply (drule approx_minus_iff [THEN iffD1]) 
374 
apply (drule approx_minus_iff [THEN iffD1]) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

375 
apply (rule approx_minus_iff [THEN iffD2]) 
20563  376 
apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_diff Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) 
14408  377 
apply (drule_tac x = "u/2" in spec) 
378 
apply (drule_tac x = "u/2" in spec, auto, ultra) 

379 
apply (case_tac "X x") 

380 
apply (case_tac "Y x") 

20563  381 
apply (auto simp add: complex_diff complex_mod snd_conv fst_conv numeral_2_eq_2) 
14408  382 
apply (rename_tac a b c d) 
20563  383 
apply (subgoal_tac "sqrt (abs (a  c) ^ 2 + abs (b  d) ^ 2) < u") 
14408  384 
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) 
385 
apply (simp add: power2_eq_square) 

386 
done 

387 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

388 
lemma approx_approx_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

389 
"(star_n X @= star_n Y) = 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

390 
(star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)) & 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

391 
star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)))" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

392 
apply (blast intro: hcomplex_approxI hcomplex_approxD1 hcomplex_approxD2) 
14408  393 
done 
394 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

395 
lemma hcomplex_of_hypreal_approx_iff [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

396 
"(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

397 
apply (cases x, cases z) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

398 
apply (simp add: hcomplex_of_hypreal approx_approx_iff) 
14408  399 
done 
400 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

401 
lemma HFinite_HFinite_Re: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

402 
"star_n X \<in> HFinite 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

403 
==> star_n (%n. Re(X n)) \<in> HFinite" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

404 
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) 
14408  405 
apply (rule_tac x = u in exI, ultra) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

406 
apply (case_tac "X x") 
14408  407 
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) 
408 
apply (rule ccontr, drule linorder_not_less [THEN iffD1]) 

409 
apply (drule order_less_le_trans, assumption) 

410 
apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) 

411 
apply (auto simp add: numeral_2_eq_2 [symmetric]) 

412 
done 

413 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

414 
lemma HFinite_HFinite_Im: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

415 
"star_n X \<in> HFinite 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

416 
==> star_n (%n. Im(X n)) \<in> HFinite" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

417 
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) 
14408  418 
apply (rule_tac x = u in exI, ultra) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

419 
apply (case_tac "X x") 
14408  420 
apply (auto simp add: complex_mod simp del: realpow_Suc) 
421 
apply (rule ccontr, drule linorder_not_less [THEN iffD1]) 

422 
apply (drule order_less_le_trans, assumption) 

423 
apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) 

424 
done 

425 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

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

427 
"[ star_n (%n. Re(X n)) \<in> HFinite; 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

428 
star_n (%n. Im(X n)) \<in> HFinite 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

429 
] ==> star_n X \<in> HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

430 
apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

431 
apply (rename_tac u v) 
14408  432 
apply (rule_tac x = "2* (u + v) " in exI) 
433 
apply ultra 

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

434 
apply (case_tac "X x") 
14408  435 
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) 
436 
apply (subgoal_tac "0 < u") 

437 
prefer 2 apply arith 

438 
apply (subgoal_tac "0 < v") 

439 
prefer 2 apply arith 

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

440 
apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v") 
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20256
diff
changeset

441 
apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) 
14408  442 
apply (simp add: power2_eq_square) 
443 
done 

444 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

445 
lemma HFinite_HFinite_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

446 
"(star_n X \<in> HFinite) = 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

447 
(star_n (%n. Re(X n)) \<in> HFinite & 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

448 
star_n (%n. Im(X n)) \<in> HFinite)" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

449 
by (blast intro: HFinite_Re_Im_HFinite HFinite_HFinite_Im HFinite_HFinite_Re) 
14408  450 

451 
lemma SComplex_Re_SReal: 

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

452 
"star_n X \<in> SComplex 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

453 
==> star_n (%n. Re(X n)) \<in> Reals" 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

454 
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) 
14408  455 
apply (rule_tac x = "Re r" in exI, ultra) 
456 
done 

457 

458 
lemma SComplex_Im_SReal: 

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

459 
"star_n X \<in> SComplex 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

460 
==> star_n (%n. Im(X n)) \<in> Reals" 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

461 
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) 
14408  462 
apply (rule_tac x = "Im r" in exI, ultra) 
463 
done 

464 

465 
lemma Reals_Re_Im_SComplex: 

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

466 
"[ star_n (%n. Re(X n)) \<in> Reals; 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

467 
star_n (%n. Im(X n)) \<in> Reals 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

468 
] ==> star_n X \<in> SComplex" 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

469 
apply (auto simp add: SComplex_def SReal_def star_of_def star_n_eq_iff) 
14408  470 
apply (rule_tac x = "Complex r ra" in exI, ultra) 
471 
done 

472 

473 
lemma SComplex_SReal_iff: 

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

474 
"(star_n X \<in> SComplex) = 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

475 
(star_n (%n. Re(X n)) \<in> Reals & 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

476 
star_n (%n. Im(X n)) \<in> Reals)" 
14408  477 
by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) 
478 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

479 
lemma Infinitesimal_Infinitesimal_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

480 
"(star_n X \<in> Infinitesimal) = 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

481 
(star_n (%n. Re(X n)) \<in> Infinitesimal & 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

482 
star_n (%n. Im(X n)) \<in> Infinitesimal)" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

483 
by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) 
14408  484 

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

486 
"(\<exists>t. P t) = (\<exists>X. P (star_n X))" 
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17373
diff
changeset

487 
by (rule ex_star_eq) 
14408  488 

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

490 
"(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))" 
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17373
diff
changeset

491 
by (simp add: Bex_def ex_star_eq) 
14408  492 

493 
(* Here we go  easy proof now!! *) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

494 
lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

495 
apply (cases x) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

496 
apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) 
14408  497 
apply (drule st_part_Ex, safe)+ 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

498 
apply (rule_tac x = t in star_cases) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

499 
apply (rule_tac x = ta in star_cases, auto) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

500 
apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) 
14408  501 
apply auto 
502 
done 

503 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

504 
lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t" 
14408  505 
apply (drule stc_part_Ex, safe) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

506 
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

507 
apply (auto intro!: approx_unique_complex) 
14408  508 
done 
509 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

510 
lemmas hcomplex_of_complex_approx_inverse = 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

511 
hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] 
14408  512 

513 

514 
subsection{*Theorems About Monads*} 

515 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

516 
lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

517 
by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) 
14408  518 

519 

520 
subsection{*Theorems About Standard Part*} 

521 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

522 
lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x" 
14408  523 
apply (simp add: stc_def) 
524 
apply (frule stc_part_Ex, safe) 

525 
apply (rule someI2) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

526 
apply (auto intro: approx_sym) 
14408  527 
done 
528 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

529 
lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> SComplex" 
14408  530 
apply (simp add: stc_def) 
531 
apply (frule stc_part_Ex, safe) 

532 
apply (rule someI2) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

533 
apply (auto intro: approx_sym) 
14408  534 
done 
535 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

536 
lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

537 
by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]]) 
14408  538 

539 
lemma stc_SComplex_eq [simp]: "x \<in> SComplex ==> stc x = x" 

540 
apply (simp add: stc_def) 

541 
apply (rule some_equality) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

542 
apply (auto intro: SComplex_subset_HFinite [THEN subsetD]) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

543 
apply (blast dest: SComplex_approx_iff [THEN iffD1]) 
14408  544 
done 
545 

546 
lemma stc_hcomplex_of_complex: 

547 
"stc (hcomplex_of_complex x) = hcomplex_of_complex x" 

548 
by auto 

549 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

550 
lemma stc_eq_approx: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

551 
"[ x \<in> HFinite; y \<in> HFinite; stc x = stc y ] ==> x @= y" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

552 
by (auto dest!: stc_approx_self elim!: approx_trans3) 
14408  553 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

554 
lemma approx_stc_eq: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

555 
"[ x \<in> HFinite; y \<in> HFinite; x @= y ] ==> stc x = stc y" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

556 
by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

557 
dest: stc_approx_self stc_SComplex) 
13957  558 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

559 
lemma stc_eq_approx_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

560 
"[ x \<in> HFinite; y \<in> HFinite] ==> (x @= y) = (stc x = stc y)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

561 
by (blast intro: approx_stc_eq stc_eq_approx) 
14408  562 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

563 
lemma stc_Infinitesimal_add_SComplex: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

564 
"[ x \<in> SComplex; e \<in> Infinitesimal ] ==> stc(x + e) = x" 
14408  565 
apply (frule stc_SComplex_eq [THEN subst]) 
566 
prefer 2 apply assumption 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

567 
apply (frule SComplex_subset_HFinite [THEN subsetD]) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

568 
apply (frule Infinitesimal_subset_HFinite [THEN subsetD]) 
14408  569 
apply (drule stc_SComplex_eq) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

570 
apply (rule approx_stc_eq) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

571 
apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym]) 
14408  572 
done 
573 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

574 
lemma stc_Infinitesimal_add_SComplex2: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

575 
"[ x \<in> SComplex; e \<in> Infinitesimal ] ==> stc(e + x) = x" 
14408  576 
apply (rule add_commute [THEN subst]) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

577 
apply (blast intro!: stc_Infinitesimal_add_SComplex) 
14408  578 
done 
579 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

580 
lemma HFinite_stc_Infinitesimal_add: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

581 
"x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

582 
by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) 
14408  583 

584 
lemma stc_add: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

585 
"[ x \<in> HFinite; y \<in> HFinite ] ==> stc (x + y) = stc(x) + stc(y)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

586 
apply (frule HFinite_stc_Infinitesimal_add) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

587 
apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe) 
14408  588 
apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))") 
589 
apply (drule_tac [2] sym, drule_tac [2] sym) 

590 
prefer 2 apply simp 

591 
apply (simp (no_asm_simp) add: add_ac) 

592 
apply (drule stc_SComplex)+ 

593 
apply (drule SComplex_add, assumption) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

594 
apply (drule Infinitesimal_add, assumption) 
14408  595 
apply (rule add_assoc [THEN subst]) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

596 
apply (blast intro!: stc_Infinitesimal_add_SComplex2) 
14408  597 
done 
598 

599 
lemma stc_number_of [simp]: "stc (number_of w) = number_of w" 

600 
by (rule SComplex_number_of [THEN stc_SComplex_eq]) 

601 

602 
lemma stc_zero [simp]: "stc 0 = 0" 

603 
by simp 

604 

605 
lemma stc_one [simp]: "stc 1 = 1" 

606 
by simp 

607 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

608 
lemma stc_minus: "y \<in> HFinite ==> stc(y) = stc(y)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

609 
apply (frule HFinite_minus_iff [THEN iffD2]) 
14408  610 
apply (rule hcomplex_add_minus_eq_minus) 
611 
apply (drule stc_add [symmetric], assumption) 

612 
apply (simp add: add_commute) 

613 
done 

614 

615 
lemma stc_diff: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

616 
"[ x \<in> HFinite; y \<in> HFinite ] ==> stc (xy) = stc(x)  stc(y)" 
14408  617 
apply (simp add: diff_minus) 
618 
apply (frule_tac y1 = y in stc_minus [symmetric]) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

619 
apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2]) 
14408  620 
apply (auto intro: stc_add) 
621 
done 

622 

623 
lemma stc_mult: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

624 
"[ x \<in> HFinite; y \<in> HFinite ] 
14408  625 
==> stc (x * y) = stc(x) * stc(y)" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

626 
apply (frule HFinite_stc_Infinitesimal_add) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

627 
apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe) 
14408  628 
apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))") 
629 
apply (drule_tac [2] sym, drule_tac [2] sym) 

630 
prefer 2 apply simp 

631 
apply (erule_tac V = "x = stc x + e" in thin_rl) 

632 
apply (erule_tac V = "y = stc y + ea" in thin_rl) 

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

633 
apply (simp add: left_distrib right_distrib) 
14408  634 
apply (drule stc_SComplex)+ 
635 
apply (simp (no_asm_use) add: add_assoc) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

636 
apply (rule stc_Infinitesimal_add_SComplex) 
14408  637 
apply (blast intro!: SComplex_mult) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

638 
apply (drule SComplex_subset_HFinite [THEN subsetD])+ 
14408  639 
apply (rule add_assoc [THEN subst]) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

640 
apply (blast intro!: lemma_st_mult) 
14408  641 
done 
642 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

643 
lemma stc_Infinitesimal: "x \<in> Infinitesimal ==> stc x = 0" 
14408  644 
apply (rule stc_zero [THEN subst]) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

645 
apply (rule approx_stc_eq) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

646 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

647 
simp add: mem_infmal_iff [symmetric]) 
14408  648 
done 
649 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

650 
lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

651 
by (fast intro: stc_Infinitesimal) 
14408  652 

653 
lemma stc_inverse: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

654 
"[ x \<in> HFinite; stc x \<noteq> 0 ] 
14408  655 
==> stc(inverse x) = inverse (stc x)" 
656 
apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1]) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

657 
apply (auto simp add: stc_mult [symmetric] stc_not_Infinitesimal HFinite_inverse) 
14408  658 
apply (subst right_inverse, auto) 
659 
done 

660 

661 
lemma stc_divide [simp]: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

662 
"[ x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 0 ] 
14408  663 
==> stc(x/y) = (stc x) / (stc y)" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

664 
by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse) 
14408  665 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

666 
lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

667 
by (blast intro: stc_HFinite stc_approx_self approx_stc_eq) 
14408  668 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

669 
lemma HFinite_HFinite_hcomplex_of_hypreal: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

670 
"z \<in> HFinite ==> hcomplex_of_hypreal z \<in> HFinite" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

671 
apply (cases z) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

672 
apply (simp add: hcomplex_of_hypreal HFinite_HFinite_iff star_n_zero_num [symmetric]) 
14408  673 
done 
674 

675 
lemma SComplex_SReal_hcomplex_of_hypreal: 

676 
"x \<in> Reals ==> hcomplex_of_hypreal x \<in> SComplex" 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20552
diff
changeset

677 
by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20552
diff
changeset

678 
simp del: star_of_of_real) 
14408  679 

680 
lemma stc_hcomplex_of_hypreal: 

681 
"z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" 

682 
apply (simp add: st_def stc_def) 

683 
apply (frule st_part_Ex, safe) 

684 
apply (rule someI2) 

685 
apply (auto intro: approx_sym) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

686 
apply (drule HFinite_HFinite_hcomplex_of_hypreal) 
14408  687 
apply (frule stc_part_Ex, safe) 
688 
apply (rule someI2) 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

689 
apply (auto intro: approx_sym intro!: approx_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal) 
14408  690 
done 
691 

692 
(* 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

693 
Goal "x \<in> HFinite ==> hcmod(stc x) = st(hcmod x)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

694 
by (dtac stc_approx_self 1) 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

695 
by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym])); 
14408  696 

697 

698 
approx_hcmod_add_hcmod 

699 
*) 

700 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

701 
lemma Infinitesimal_hcnj_iff [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

702 
"(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

703 
by (simp add: Infinitesimal_hcmod_iff) 
14408  704 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

705 
lemma HInfinite_HInfinite_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

706 
"(star_n X \<in> HInfinite) = 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

707 
(star_n (%n. Re(X n)) \<in> HInfinite  
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

708 
star_n (%n. Im(X n)) \<in> HInfinite)" 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

709 
by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) 
14408  710 

711 
text{*These theorems should probably be deleted*} 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

712 
lemma hcomplex_split_Infinitesimal_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

713 
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> Infinitesimal) = 
14408  714 
(x \<in> Infinitesimal & y \<in> Infinitesimal)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

715 
apply (cases x, cases y) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

716 
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) 
14408  717 
done 
718 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

719 
lemma hcomplex_split_HFinite_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

720 
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HFinite) = 
14408  721 
(x \<in> HFinite & y \<in> HFinite)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

722 
apply (cases x, cases y) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

723 
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) 
14408  724 
done 
725 

726 
lemma hcomplex_split_SComplex_iff: 

727 
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) = 

728 
(x \<in> Reals & y \<in> Reals)" 

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

729 
apply (cases x, cases y) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

730 
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) 
14408  731 
done 
732 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

733 
lemma hcomplex_split_HInfinite_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

734 
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HInfinite) = 
14408  735 
(x \<in> HInfinite  y \<in> HInfinite)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

736 
apply (cases x, cases y) 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

737 
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) 
14408  738 
done 
739 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

740 
lemma hcomplex_split_approx_iff: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

741 
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= 
14408  742 
hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = 
743 
(x @= x' & y @= y')" 

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

744 
apply (cases x, cases y, cases x', cases y') 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

745 
apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) 
14408  746 
done 
747 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

748 
lemma complex_seq_to_hcomplex_Infinitesimal: 
14408  749 
"\<forall>n. cmod (X n  x) < inverse (real (Suc n)) ==> 
20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

750 
star_n X  hcomplex_of_complex x \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

751 
by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) 
14408  752 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

753 
lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

754 
"hcomplex_of_hypreal epsilon \<in> Infinitesimal" 
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

755 
by (simp add: Infinitesimal_hcmod_iff) 
14408  756 

757 
lemma hcomplex_of_complex_approx_zero_iff [simp]: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

758 
"(hcomplex_of_complex z @= 0) = (z = 0)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

759 
by (simp add: star_of_zero [symmetric] del: star_of_zero) 
14408  760 

761 
lemma hcomplex_of_complex_approx_zero_iff2 [simp]: 

20559
2116b7a371c7
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman
parents:
20557
diff
changeset

762 
"(0 @= hcomplex_of_complex z) = (z = 0)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset

763 
by (simp add: star_of_zero [symmetric] del: star_of_zero) 
14408  764 

13957  765 
end 