author | huffman |
Fri, 09 Sep 2005 19:34:22 +0200 | |
changeset 17318 | bc1c75855f3d |
parent 17294 | d7acf9f05eb2 |
child 17332 | 4910cf8c0cd2 |
permissions | -rw-r--r-- |
17294 | 1 |
(* Title : HOL/Hyperreal/StarType.thy |
2 |
ID : $Id$ |
|
3 |
Author : Jacques D. Fleuriot and Brian Huffman |
|
4 |
*) |
|
5 |
||
6 |
header {* Construction of Star Types Using Ultrafilters *} |
|
7 |
||
8 |
theory StarType |
|
9 |
imports Filter |
|
10 |
begin |
|
11 |
||
12 |
subsection {* A Free Ultrafilter over the Naturals *} |
|
13 |
||
14 |
constdefs |
|
15 |
FreeUltrafilterNat :: "nat set set" ("\<U>") |
|
16 |
"\<U> \<equiv> SOME U. freeultrafilter U" |
|
17 |
||
18 |
lemma freeultrafilter_FUFNat: "freeultrafilter \<U>" |
|
19 |
apply (unfold FreeUltrafilterNat_def) |
|
20 |
apply (rule someI_ex) |
|
21 |
apply (rule freeultrafilter_Ex) |
|
22 |
apply (rule nat_infinite) |
|
23 |
done |
|
24 |
||
25 |
lemmas ultrafilter_FUFNat = |
|
26 |
freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter] |
|
27 |
||
28 |
lemmas filter_FUFNat = |
|
29 |
freeultrafilter_FUFNat [THEN freeultrafilter.filter] |
|
30 |
||
31 |
lemmas FUFNat_empty [iff] = |
|
32 |
filter_FUFNat [THEN filter.empty] |
|
33 |
||
34 |
lemmas FUFNat_UNIV [iff] = |
|
35 |
filter_FUFNat [THEN filter.UNIV] |
|
36 |
||
37 |
text {* This rule takes the place of the old ultra tactic *} |
|
38 |
||
39 |
lemma ultra: |
|
40 |
"\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>" |
|
41 |
by (simp add: Collect_imp_eq |
|
42 |
ultrafilter_FUFNat [THEN ultrafilter.Un_iff] |
|
43 |
ultrafilter_FUFNat [THEN ultrafilter.Compl_iff]) |
|
44 |
||
45 |
||
46 |
subsection {* Definition of @{text star} type constructor *} |
|
47 |
||
48 |
constdefs |
|
49 |
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" |
|
50 |
"starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}" |
|
51 |
||
52 |
typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel" |
|
53 |
by (auto intro: quotientI) |
|
54 |
||
55 |
text {* Proving that @{term starrel} is an equivalence relation *} |
|
56 |
||
57 |
lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)" |
|
58 |
by (simp add: starrel_def) |
|
59 |
||
60 |
lemma equiv_starrel: "equiv UNIV starrel" |
|
61 |
proof (rule equiv.intro) |
|
62 |
show "reflexive starrel" by (simp add: refl_def) |
|
63 |
show "sym starrel" by (simp add: sym_def eq_commute) |
|
64 |
show "trans starrel" by (auto intro: transI elim!: ultra) |
|
65 |
qed |
|
66 |
||
67 |
lemmas equiv_starrel_iff = |
|
68 |
eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I] |
|
69 |
-- {* @{term "(starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel)"} *} |
|
70 |
||
71 |
lemma starrel_in_star: "starrel``{x} \<in> star" |
|
72 |
by (simp add: star_def starrel_def quotient_def, fast) |
|
73 |
||
74 |
lemma eq_Abs_star: |
|
75 |
"(\<And>x. z = Abs_star (starrel``{x}) \<Longrightarrow> P) \<Longrightarrow> P" |
|
76 |
apply (rule_tac x=z in Abs_star_cases) |
|
77 |
apply (unfold star_def) |
|
78 |
apply (erule quotientE) |
|
79 |
apply simp |
|
80 |
done |
|
81 |
||
82 |
||
83 |
subsection {* Constructors for type @{typ "'a star"} *} |
|
84 |
||
85 |
constdefs |
|
86 |
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" |
|
87 |
"star_n X \<equiv> Abs_star (starrel `` {X})" |
|
88 |
||
89 |
star_of :: "'a \<Rightarrow> 'a star" |
|
90 |
"star_of x \<equiv> star_n (\<lambda>n. x)" |
|
91 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
92 |
theorem star_cases [case_names star_n, cases type: star]: |
17294 | 93 |
"(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P" |
94 |
by (unfold star_n_def, rule eq_Abs_star[of x], blast) |
|
95 |
||
96 |
lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))" |
|
97 |
by (auto, rule_tac x=x in star_cases, simp) |
|
98 |
||
99 |
lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))" |
|
100 |
by (auto, rule_tac x=x in star_cases, auto) |
|
101 |
||
102 |
lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)" |
|
103 |
apply (unfold star_n_def) |
|
104 |
apply (simp add: Abs_star_inject starrel_in_star equiv_starrel_iff) |
|
105 |
done |
|
106 |
||
107 |
lemma star_of_inject: "(star_of x = star_of y) = (x = y)" |
|
108 |
by (simp add: star_of_def star_n_eq_iff) |
|
109 |
||
110 |
||
111 |
subsection {* Internal functions *} |
|
112 |
||
113 |
constdefs |
|
114 |
Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) |
|
115 |
"Ifun f \<equiv> \<lambda>x. Abs_star |
|
116 |
(\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})" |
|
117 |
||
118 |
lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))" |
|
119 |
apply (unfold Ifun_def star_n_def) |
|
120 |
apply (simp add: Abs_star_inverse starrel_in_star) |
|
121 |
apply (rule_tac f=Abs_star in arg_cong) |
|
122 |
apply safe |
|
123 |
apply (erule ultra)+ |
|
124 |
apply simp |
|
125 |
apply force |
|
126 |
done |
|
127 |
||
128 |
lemma Ifun [simp]: "star_of f \<star> star_of x = star_of (f x)" |
|
129 |
by (simp only: star_of_def Ifun_star_n) |
|
130 |
||
131 |
||
132 |
subsection {* Testing lifted booleans *} |
|
133 |
||
134 |
constdefs |
|
135 |
unstar :: "bool star \<Rightarrow> bool" |
|
136 |
"unstar b \<equiv> b = star_of True" |
|
137 |
||
138 |
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)" |
|
139 |
by (simp add: unstar_def star_of_def star_n_eq_iff) |
|
140 |
||
141 |
lemma unstar [simp]: "unstar (star_of p) = p" |
|
142 |
by (simp add: unstar_def star_of_inject) |
|
143 |
||
144 |
||
145 |
subsection {* Internal functions and predicates *} |
|
146 |
||
147 |
constdefs |
|
148 |
Ifun_of :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)" |
|
149 |
"Ifun_of f \<equiv> Ifun (star_of f)" |
|
150 |
||
151 |
Ifun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)" |
|
152 |
"Ifun2 f \<equiv> \<lambda>x y. f \<star> x \<star> y" |
|
153 |
||
154 |
Ifun2_of :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)" |
|
155 |
"Ifun2_of f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y" |
|
156 |
||
157 |
Ipred :: "('a \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> bool)" |
|
158 |
"Ipred P \<equiv> \<lambda>x. unstar (P \<star> x)" |
|
159 |
||
160 |
Ipred_of :: "('a \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> bool)" |
|
161 |
"Ipred_of P \<equiv> \<lambda>x. unstar (star_of P \<star> x)" |
|
162 |
||
163 |
Ipred2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)" |
|
164 |
"Ipred2 P \<equiv> \<lambda>x y. unstar (P \<star> x \<star> y)" |
|
165 |
||
166 |
Ipred2_of :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)" |
|
167 |
"Ipred2_of P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)" |
|
168 |
||
169 |
lemma Ifun_of [simp]: |
|
170 |
"Ifun_of f (star_of x) = star_of (f x)" |
|
171 |
by (simp only: Ifun_of_def Ifun) |
|
172 |
||
173 |
lemma Ifun2_of [simp]: |
|
174 |
"Ifun2_of f (star_of x) (star_of y) = star_of (f x y)" |
|
175 |
by (simp only: Ifun2_of_def Ifun) |
|
176 |
||
177 |
lemma Ipred_of [simp]: |
|
178 |
"Ipred_of P (star_of x) = P x" |
|
179 |
by (simp only: Ipred_of_def Ifun unstar) |
|
180 |
||
181 |
lemma Ipred2_of [simp]: |
|
182 |
"Ipred2_of P (star_of x) (star_of y) = P x y" |
|
183 |
by (simp only: Ipred2_of_def Ifun unstar) |
|
184 |
||
185 |
lemmas Ifun_defs = |
|
186 |
star_of_def Ifun_of_def Ifun2_def Ifun2_of_def |
|
187 |
Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def |
|
188 |
||
189 |
||
190 |
subsection {* Internal sets *} |
|
191 |
||
192 |
constdefs |
|
193 |
Iset :: "'a set star \<Rightarrow> 'a star set" |
|
194 |
"Iset A \<equiv> {x. Ipred2_of (op \<in>) x A}" |
|
195 |
||
196 |
Iset_of :: "'a set \<Rightarrow> 'a star set" |
|
197 |
"Iset_of A \<equiv> Iset (star_of A)" |
|
198 |
||
199 |
lemma Iset_star_n: |
|
200 |
"(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)" |
|
201 |
by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
|
202 |
||
203 |
||
204 |
subsection {* Class constants *} |
|
205 |
||
206 |
instance star :: (ord) ord .. |
|
207 |
instance star :: (zero) zero .. |
|
208 |
instance star :: (one) one .. |
|
209 |
instance star :: (plus) plus .. |
|
210 |
instance star :: (times) times .. |
|
211 |
instance star :: (minus) minus .. |
|
212 |
instance star :: (inverse) inverse .. |
|
213 |
instance star :: (number) number .. |
|
214 |
instance star :: ("Divides.div") "Divides.div" .. |
|
215 |
instance star :: (power) power .. |
|
216 |
||
217 |
defs (overloaded) |
|
218 |
star_zero_def: "0 \<equiv> star_of 0" |
|
219 |
star_one_def: "1 \<equiv> star_of 1" |
|
220 |
star_number_def: "number_of b \<equiv> star_of (number_of b)" |
|
221 |
star_add_def: "(op +) \<equiv> Ifun2_of (op +)" |
|
222 |
star_diff_def: "(op -) \<equiv> Ifun2_of (op -)" |
|
223 |
star_minus_def: "uminus \<equiv> Ifun_of uminus" |
|
224 |
star_mult_def: "(op *) \<equiv> Ifun2_of (op *)" |
|
225 |
star_divide_def: "(op /) \<equiv> Ifun2_of (op /)" |
|
226 |
star_inverse_def: "inverse \<equiv> Ifun_of inverse" |
|
227 |
star_le_def: "(op \<le>) \<equiv> Ipred2_of (op \<le>)" |
|
228 |
star_less_def: "(op <) \<equiv> Ipred2_of (op <)" |
|
229 |
star_abs_def: "abs \<equiv> Ifun_of abs" |
|
230 |
star_div_def: "(op div) \<equiv> Ifun2_of (op div)" |
|
231 |
star_mod_def: "(op mod) \<equiv> Ifun2_of (op mod)" |
|
232 |
star_power_def: "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x" |
|
233 |
||
234 |
lemmas star_class_defs = |
|
235 |
star_zero_def star_one_def star_number_def |
|
236 |
star_add_def star_diff_def star_minus_def |
|
237 |
star_mult_def star_divide_def star_inverse_def |
|
238 |
star_le_def star_less_def star_abs_def |
|
239 |
star_div_def star_mod_def star_power_def |
|
240 |
||
241 |
text {* @{term star_of} preserves class operations *} |
|
242 |
||
243 |
lemma star_of_add: "star_of (x + y) = star_of x + star_of y" |
|
244 |
by (simp add: star_add_def) |
|
245 |
||
246 |
lemma star_of_diff: "star_of (x - y) = star_of x - star_of y" |
|
247 |
by (simp add: star_diff_def) |
|
248 |
||
249 |
lemma star_of_minus: "star_of (-x) = - star_of x" |
|
250 |
by (simp add: star_minus_def) |
|
251 |
||
252 |
lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" |
|
253 |
by (simp add: star_mult_def) |
|
254 |
||
255 |
lemma star_of_divide: "star_of (x / y) = star_of x / star_of y" |
|
256 |
by (simp add: star_divide_def) |
|
257 |
||
258 |
lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)" |
|
259 |
by (simp add: star_inverse_def) |
|
260 |
||
261 |
lemma star_of_div: "star_of (x div y) = star_of x div star_of y" |
|
262 |
by (simp add: star_div_def) |
|
263 |
||
264 |
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y" |
|
265 |
by (simp add: star_mod_def) |
|
266 |
||
267 |
lemma star_of_power: "star_of (x ^ n) = star_of x ^ n" |
|
268 |
by (simp add: star_power_def) |
|
269 |
||
270 |
lemma star_of_abs: "star_of (abs x) = abs (star_of x)" |
|
271 |
by (simp add: star_abs_def) |
|
272 |
||
273 |
text {* @{term star_of} preserves numerals *} |
|
274 |
||
275 |
lemma star_of_zero: "star_of 0 = 0" |
|
276 |
by (simp add: star_zero_def) |
|
277 |
||
278 |
lemma star_of_one: "star_of 1 = 1" |
|
279 |
by (simp add: star_one_def) |
|
280 |
||
281 |
lemma star_of_number_of: "star_of (number_of x) = number_of x" |
|
282 |
by (simp add: star_number_def) |
|
283 |
||
284 |
text {* @{term star_of} preserves orderings *} |
|
285 |
||
286 |
lemma star_of_less: "(star_of x < star_of y) = (x < y)" |
|
287 |
by (simp add: star_less_def) |
|
288 |
||
289 |
lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)" |
|
290 |
by (simp add: star_le_def) |
|
291 |
||
292 |
lemma star_of_eq: "(star_of x = star_of y) = (x = y)" |
|
293 |
by (rule star_of_inject) |
|
294 |
||
295 |
text{*As above, for 0*} |
|
296 |
||
297 |
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero] |
|
298 |
lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero] |
|
299 |
lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero] |
|
300 |
||
301 |
lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero] |
|
302 |
lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero] |
|
303 |
lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero] |
|
304 |
||
305 |
text{*As above, for 1*} |
|
306 |
||
307 |
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one] |
|
308 |
lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one] |
|
309 |
lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one] |
|
310 |
||
311 |
lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one] |
|
312 |
lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one] |
|
313 |
lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] |
|
314 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
315 |
text{*As above, for numerals*} |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
316 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
317 |
lemmas star_of_number_less = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
318 |
star_of_less [of "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
319 |
lemmas star_of_number_le = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
320 |
star_of_le [of "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
321 |
lemmas star_of_number_eq = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
322 |
star_of_eq [of "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
323 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
324 |
lemmas star_of_less_number = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
325 |
star_of_less [of _ "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
326 |
lemmas star_of_le_number = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
327 |
star_of_le [of _ "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
328 |
lemmas star_of_eq_number = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
329 |
star_of_eq [of _ "number_of b", simplified star_of_number_of, standard] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
330 |
|
17294 | 331 |
lemmas star_of_simps = |
332 |
star_of_add star_of_diff star_of_minus |
|
333 |
star_of_mult star_of_divide star_of_inverse |
|
334 |
star_of_div star_of_mod |
|
335 |
star_of_power star_of_abs |
|
336 |
star_of_zero star_of_one star_of_number_of |
|
337 |
star_of_less star_of_le star_of_eq |
|
338 |
star_of_0_less star_of_0_le star_of_0_eq |
|
339 |
star_of_less_0 star_of_le_0 star_of_eq_0 |
|
340 |
star_of_1_less star_of_1_le star_of_1_eq |
|
341 |
star_of_less_1 star_of_le_1 star_of_eq_1 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
342 |
star_of_number_less star_of_number_le star_of_number_eq |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17294
diff
changeset
|
343 |
star_of_less_number star_of_le_number star_of_eq_number |
17294 | 344 |
|
345 |
declare star_of_simps [simp] |
|
346 |
||
347 |
end |