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 |
|
92 theorem star_cases [case_names star_n, cases type: star]: |
|
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 lemmas Ifun_defs = |
|
170 Ifun_of_def Ifun2_def Ifun2_of_def |
|
171 Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def |
|
172 |
|
173 lemma Ifun_of [simp]: |
|
174 "Ifun_of f (star_of x) = star_of (f x)" |
|
175 by (simp only: Ifun_of_def Ifun) |
|
176 |
|
177 lemma Ifun2_of [simp]: |
|
178 "Ifun2_of f (star_of x) (star_of y) = star_of (f x y)" |
|
179 by (simp only: Ifun2_of_def Ifun) |
|
180 |
|
181 lemma Ipred_of [simp]: |
|
182 "Ipred_of P (star_of x) = P x" |
|
183 by (simp only: Ipred_of_def Ifun unstar) |
|
184 |
|
185 lemma Ipred2_of [simp]: |
|
186 "Ipred2_of P (star_of x) (star_of y) = P x y" |
|
187 by (simp only: Ipred2_of_def Ifun unstar) |
|
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 |
|
205 end |
|