1 (* Title: HOLCF/Pcpodef.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Subtypes of pcpos *} |
|
6 |
|
7 theory Cpodef |
|
8 imports Adm |
|
9 uses ("Tools/cpodef.ML") |
|
10 begin |
|
11 |
|
12 subsection {* Proving a subtype is a partial order *} |
|
13 |
|
14 text {* |
|
15 A subtype of a partial order is itself a partial order, |
|
16 if the ordering is defined in the standard way. |
|
17 *} |
|
18 |
|
19 setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *} |
|
20 |
|
21 theorem typedef_po: |
|
22 fixes Abs :: "'a::po \<Rightarrow> 'b::type" |
|
23 assumes type: "type_definition Rep Abs A" |
|
24 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
25 shows "OFCLASS('b, po_class)" |
|
26 apply (intro_classes, unfold below) |
|
27 apply (rule below_refl) |
|
28 apply (erule (1) below_trans) |
|
29 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
|
30 apply (erule (1) below_antisym) |
|
31 done |
|
32 |
|
33 setup {* Sign.add_const_constraint (@{const_name Porder.below}, |
|
34 SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *} |
|
35 |
|
36 subsection {* Proving a subtype is finite *} |
|
37 |
|
38 lemma typedef_finite_UNIV: |
|
39 fixes Abs :: "'a::type \<Rightarrow> 'b::type" |
|
40 assumes type: "type_definition Rep Abs A" |
|
41 shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)" |
|
42 proof - |
|
43 assume "finite A" |
|
44 hence "finite (Abs ` A)" by (rule finite_imageI) |
|
45 thus "finite (UNIV :: 'b set)" |
|
46 by (simp only: type_definition.Abs_image [OF type]) |
|
47 qed |
|
48 |
|
49 subsection {* Proving a subtype is chain-finite *} |
|
50 |
|
51 lemma ch2ch_Rep: |
|
52 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
53 shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))" |
|
54 unfolding chain_def below . |
|
55 |
|
56 theorem typedef_chfin: |
|
57 fixes Abs :: "'a::chfin \<Rightarrow> 'b::po" |
|
58 assumes type: "type_definition Rep Abs A" |
|
59 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
60 shows "OFCLASS('b, chfin_class)" |
|
61 apply intro_classes |
|
62 apply (drule ch2ch_Rep [OF below]) |
|
63 apply (drule chfin) |
|
64 apply (unfold max_in_chain_def) |
|
65 apply (simp add: type_definition.Rep_inject [OF type]) |
|
66 done |
|
67 |
|
68 subsection {* Proving a subtype is complete *} |
|
69 |
|
70 text {* |
|
71 A subtype of a cpo is itself a cpo if the ordering is |
|
72 defined in the standard way, and the defining subset |
|
73 is closed with respect to limits of chains. A set is |
|
74 closed if and only if membership in the set is an |
|
75 admissible predicate. |
|
76 *} |
|
77 |
|
78 lemma typedef_is_lubI: |
|
79 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
80 shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x" |
|
81 unfolding is_lub_def is_ub_def below by simp |
|
82 |
|
83 lemma Abs_inverse_lub_Rep: |
|
84 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
|
85 assumes type: "type_definition Rep Abs A" |
|
86 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
87 and adm: "adm (\<lambda>x. x \<in> A)" |
|
88 shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))" |
|
89 apply (rule type_definition.Abs_inverse [OF type]) |
|
90 apply (erule admD [OF adm ch2ch_Rep [OF below]]) |
|
91 apply (rule type_definition.Rep [OF type]) |
|
92 done |
|
93 |
|
94 theorem typedef_is_lub: |
|
95 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
|
96 assumes type: "type_definition Rep Abs A" |
|
97 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
98 and adm: "adm (\<lambda>x. x \<in> A)" |
|
99 shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))" |
|
100 proof - |
|
101 assume S: "chain S" |
|
102 hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below]) |
|
103 hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI) |
|
104 hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))" |
|
105 by (simp only: Abs_inverse_lub_Rep [OF type below adm S]) |
|
106 thus "range S <<| Abs (\<Squnion>i. Rep (S i))" |
|
107 by (rule typedef_is_lubI [OF below]) |
|
108 qed |
|
109 |
|
110 lemmas typedef_lub = typedef_is_lub [THEN lub_eqI, standard] |
|
111 |
|
112 theorem typedef_cpo: |
|
113 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
|
114 assumes type: "type_definition Rep Abs A" |
|
115 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
116 and adm: "adm (\<lambda>x. x \<in> A)" |
|
117 shows "OFCLASS('b, cpo_class)" |
|
118 proof |
|
119 fix S::"nat \<Rightarrow> 'b" assume "chain S" |
|
120 hence "range S <<| Abs (\<Squnion>i. Rep (S i))" |
|
121 by (rule typedef_is_lub [OF type below adm]) |
|
122 thus "\<exists>x. range S <<| x" .. |
|
123 qed |
|
124 |
|
125 subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *} |
|
126 |
|
127 text {* For any sub-cpo, the @{term Rep} function is continuous. *} |
|
128 |
|
129 theorem typedef_cont_Rep: |
|
130 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
|
131 assumes type: "type_definition Rep Abs A" |
|
132 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
133 and adm: "adm (\<lambda>x. x \<in> A)" |
|
134 shows "cont Rep" |
|
135 apply (rule contI) |
|
136 apply (simp only: typedef_lub [OF type below adm]) |
|
137 apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) |
|
138 apply (rule cpo_lubI) |
|
139 apply (erule ch2ch_Rep [OF below]) |
|
140 done |
|
141 |
|
142 text {* |
|
143 For a sub-cpo, we can make the @{term Abs} function continuous |
|
144 only if we restrict its domain to the defining subset by |
|
145 composing it with another continuous function. |
|
146 *} |
|
147 |
|
148 theorem typedef_cont_Abs: |
|
149 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
|
150 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
|
151 assumes type: "type_definition Rep Abs A" |
|
152 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
153 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) |
|
154 and f_in_A: "\<And>x. f x \<in> A" |
|
155 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
|
156 unfolding cont_def is_lub_def is_ub_def ball_simps below |
|
157 by (simp add: type_definition.Abs_inverse [OF type f_in_A]) |
|
158 |
|
159 subsection {* Proving subtype elements are compact *} |
|
160 |
|
161 theorem typedef_compact: |
|
162 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
|
163 assumes type: "type_definition Rep Abs A" |
|
164 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
165 and adm: "adm (\<lambda>x. x \<in> A)" |
|
166 shows "compact (Rep k) \<Longrightarrow> compact k" |
|
167 proof (unfold compact_def) |
|
168 have cont_Rep: "cont Rep" |
|
169 by (rule typedef_cont_Rep [OF type below adm]) |
|
170 assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)" |
|
171 with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst) |
|
172 thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below) |
|
173 qed |
|
174 |
|
175 subsection {* Proving a subtype is pointed *} |
|
176 |
|
177 text {* |
|
178 A subtype of a cpo has a least element if and only if |
|
179 the defining subset has a least element. |
|
180 *} |
|
181 |
|
182 theorem typedef_pcpo_generic: |
|
183 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
|
184 assumes type: "type_definition Rep Abs A" |
|
185 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
186 and z_in_A: "z \<in> A" |
|
187 and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x" |
|
188 shows "OFCLASS('b, pcpo_class)" |
|
189 apply (intro_classes) |
|
190 apply (rule_tac x="Abs z" in exI, rule allI) |
|
191 apply (unfold below) |
|
192 apply (subst type_definition.Abs_inverse [OF type z_in_A]) |
|
193 apply (rule z_least [OF type_definition.Rep [OF type]]) |
|
194 done |
|
195 |
|
196 text {* |
|
197 As a special case, a subtype of a pcpo has a least element |
|
198 if the defining subset contains @{term \<bottom>}. |
|
199 *} |
|
200 |
|
201 theorem typedef_pcpo: |
|
202 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" |
|
203 assumes type: "type_definition Rep Abs A" |
|
204 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
205 and UU_in_A: "\<bottom> \<in> A" |
|
206 shows "OFCLASS('b, pcpo_class)" |
|
207 by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal) |
|
208 |
|
209 subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *} |
|
210 |
|
211 text {* |
|
212 For a sub-pcpo where @{term \<bottom>} is a member of the defining |
|
213 subset, @{term Rep} and @{term Abs} are both strict. |
|
214 *} |
|
215 |
|
216 theorem typedef_Abs_strict: |
|
217 assumes type: "type_definition Rep Abs A" |
|
218 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
219 and UU_in_A: "\<bottom> \<in> A" |
|
220 shows "Abs \<bottom> = \<bottom>" |
|
221 apply (rule UU_I, unfold below) |
|
222 apply (simp add: type_definition.Abs_inverse [OF type UU_in_A]) |
|
223 done |
|
224 |
|
225 theorem typedef_Rep_strict: |
|
226 assumes type: "type_definition Rep Abs A" |
|
227 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
228 and UU_in_A: "\<bottom> \<in> A" |
|
229 shows "Rep \<bottom> = \<bottom>" |
|
230 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst]) |
|
231 apply (rule type_definition.Abs_inverse [OF type UU_in_A]) |
|
232 done |
|
233 |
|
234 theorem typedef_Abs_bottom_iff: |
|
235 assumes type: "type_definition Rep Abs A" |
|
236 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
237 and UU_in_A: "\<bottom> \<in> A" |
|
238 shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)" |
|
239 apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst]) |
|
240 apply (simp add: type_definition.Abs_inject [OF type] UU_in_A) |
|
241 done |
|
242 |
|
243 theorem typedef_Rep_bottom_iff: |
|
244 assumes type: "type_definition Rep Abs A" |
|
245 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
246 and UU_in_A: "\<bottom> \<in> A" |
|
247 shows "(Rep x = \<bottom>) = (x = \<bottom>)" |
|
248 apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst]) |
|
249 apply (simp add: type_definition.Rep_inject [OF type]) |
|
250 done |
|
251 |
|
252 theorem typedef_Abs_defined: |
|
253 assumes type: "type_definition Rep Abs A" |
|
254 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
255 and UU_in_A: "\<bottom> \<in> A" |
|
256 shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>" |
|
257 by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A]) |
|
258 |
|
259 theorem typedef_Rep_defined: |
|
260 assumes type: "type_definition Rep Abs A" |
|
261 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
262 and UU_in_A: "\<bottom> \<in> A" |
|
263 shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>" |
|
264 by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A]) |
|
265 |
|
266 subsection {* Proving a subtype is flat *} |
|
267 |
|
268 theorem typedef_flat: |
|
269 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" |
|
270 assumes type: "type_definition Rep Abs A" |
|
271 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
|
272 and UU_in_A: "\<bottom> \<in> A" |
|
273 shows "OFCLASS('b, flat_class)" |
|
274 apply (intro_classes) |
|
275 apply (unfold below) |
|
276 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) |
|
277 apply (simp add: typedef_Rep_strict [OF type below UU_in_A]) |
|
278 apply (simp add: ax_flat) |
|
279 done |
|
280 |
|
281 subsection {* HOLCF type definition package *} |
|
282 |
|
283 use "Tools/cpodef.ML" |
|
284 |
|
285 end |
|