1 (* Title: HOL/HOLCF/Cpodef.thy |
1 (* Title: HOL/HOLCF/Cpodef.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Subtypes of pcpos *} |
5 section \<open>Subtypes of pcpos\<close> |
6 |
6 |
7 theory Cpodef |
7 theory Cpodef |
8 imports Adm |
8 imports Adm |
9 keywords "pcpodef" "cpodef" :: thy_goal |
9 keywords "pcpodef" "cpodef" :: thy_goal |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Proving a subtype is a partial order *} |
12 subsection \<open>Proving a subtype is a partial order\<close> |
13 |
13 |
14 text {* |
14 text \<open> |
15 A subtype of a partial order is itself a partial order, |
15 A subtype of a partial order is itself a partial order, |
16 if the ordering is defined in the standard way. |
16 if the ordering is defined in the standard way. |
17 *} |
17 \<close> |
18 |
18 |
19 setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *} |
19 setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, NONE)\<close> |
20 |
20 |
21 theorem typedef_po: |
21 theorem typedef_po: |
22 fixes Abs :: "'a::po \<Rightarrow> 'b::type" |
22 fixes Abs :: "'a::po \<Rightarrow> 'b::type" |
23 assumes type: "type_definition Rep Abs A" |
23 assumes type: "type_definition Rep Abs A" |
24 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
24 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
28 apply (erule (1) below_trans) |
28 apply (erule (1) below_trans) |
29 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
29 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
30 apply (erule (1) below_antisym) |
30 apply (erule (1) below_antisym) |
31 done |
31 done |
32 |
32 |
33 setup {* Sign.add_const_constraint (@{const_name Porder.below}, |
33 setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, |
34 SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *} |
34 SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"})\<close> |
35 |
35 |
36 subsection {* Proving a subtype is finite *} |
36 subsection \<open>Proving a subtype is finite\<close> |
37 |
37 |
38 lemma typedef_finite_UNIV: |
38 lemma typedef_finite_UNIV: |
39 fixes Abs :: "'a::type \<Rightarrow> 'b::type" |
39 fixes Abs :: "'a::type \<Rightarrow> 'b::type" |
40 assumes type: "type_definition Rep Abs A" |
40 assumes type: "type_definition Rep Abs A" |
41 shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)" |
41 shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)" |
44 hence "finite (Abs ` A)" by (rule finite_imageI) |
44 hence "finite (Abs ` A)" by (rule finite_imageI) |
45 thus "finite (UNIV :: 'b set)" |
45 thus "finite (UNIV :: 'b set)" |
46 by (simp only: type_definition.Abs_image [OF type]) |
46 by (simp only: type_definition.Abs_image [OF type]) |
47 qed |
47 qed |
48 |
48 |
49 subsection {* Proving a subtype is chain-finite *} |
49 subsection \<open>Proving a subtype is chain-finite\<close> |
50 |
50 |
51 lemma ch2ch_Rep: |
51 lemma ch2ch_Rep: |
52 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
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))" |
53 shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))" |
54 unfolding chain_def below . |
54 unfolding chain_def below . |
63 apply (drule chfin) |
63 apply (drule chfin) |
64 apply (unfold max_in_chain_def) |
64 apply (unfold max_in_chain_def) |
65 apply (simp add: type_definition.Rep_inject [OF type]) |
65 apply (simp add: type_definition.Rep_inject [OF type]) |
66 done |
66 done |
67 |
67 |
68 subsection {* Proving a subtype is complete *} |
68 subsection \<open>Proving a subtype is complete\<close> |
69 |
69 |
70 text {* |
70 text \<open> |
71 A subtype of a cpo is itself a cpo if the ordering is |
71 A subtype of a cpo is itself a cpo if the ordering is |
72 defined in the standard way, and the defining subset |
72 defined in the standard way, and the defining subset |
73 is closed with respect to limits of chains. A set is |
73 is closed with respect to limits of chains. A set is |
74 closed if and only if membership in the set is an |
74 closed if and only if membership in the set is an |
75 admissible predicate. |
75 admissible predicate. |
76 *} |
76 \<close> |
77 |
77 |
78 lemma typedef_is_lubI: |
78 lemma typedef_is_lubI: |
79 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
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" |
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 |
81 unfolding is_lub_def is_ub_def below by simp |
120 hence "range S <<| Abs (\<Squnion>i. Rep (S i))" |
120 hence "range S <<| Abs (\<Squnion>i. Rep (S i))" |
121 by (rule typedef_is_lub [OF type below adm]) |
121 by (rule typedef_is_lub [OF type below adm]) |
122 thus "\<exists>x. range S <<| x" .. |
122 thus "\<exists>x. range S <<| x" .. |
123 qed |
123 qed |
124 |
124 |
125 subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *} |
125 subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close> |
126 |
126 |
127 text {* For any sub-cpo, the @{term Rep} function is continuous. *} |
127 text \<open>For any sub-cpo, the @{term Rep} function is continuous.\<close> |
128 |
128 |
129 theorem typedef_cont_Rep: |
129 theorem typedef_cont_Rep: |
130 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
130 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
131 assumes type: "type_definition Rep Abs A" |
131 assumes type: "type_definition Rep Abs A" |
132 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
132 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
138 apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) |
138 apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) |
139 apply (rule cpo_lubI) |
139 apply (rule cpo_lubI) |
140 apply (erule ch2ch_Rep [OF below]) |
140 apply (erule ch2ch_Rep [OF below]) |
141 done |
141 done |
142 |
142 |
143 text {* |
143 text \<open> |
144 For a sub-cpo, we can make the @{term Abs} function continuous |
144 For a sub-cpo, we can make the @{term Abs} function continuous |
145 only if we restrict its domain to the defining subset by |
145 only if we restrict its domain to the defining subset by |
146 composing it with another continuous function. |
146 composing it with another continuous function. |
147 *} |
147 \<close> |
148 |
148 |
149 theorem typedef_cont_Abs: |
149 theorem typedef_cont_Abs: |
150 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
150 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
151 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
151 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
152 assumes type: "type_definition Rep Abs A" |
152 assumes type: "type_definition Rep Abs A" |
155 and f_in_A: "\<And>x. f x \<in> A" |
155 and f_in_A: "\<And>x. f x \<in> A" |
156 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
156 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
157 unfolding cont_def is_lub_def is_ub_def ball_simps below |
157 unfolding cont_def is_lub_def is_ub_def ball_simps below |
158 by (simp add: type_definition.Abs_inverse [OF type f_in_A]) |
158 by (simp add: type_definition.Abs_inverse [OF type f_in_A]) |
159 |
159 |
160 subsection {* Proving subtype elements are compact *} |
160 subsection \<open>Proving subtype elements are compact\<close> |
161 |
161 |
162 theorem typedef_compact: |
162 theorem typedef_compact: |
163 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
163 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
164 assumes type: "type_definition Rep Abs A" |
164 assumes type: "type_definition Rep Abs A" |
165 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
165 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
171 assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)" |
171 assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)" |
172 with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst) |
172 with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst) |
173 thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below) |
173 thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below) |
174 qed |
174 qed |
175 |
175 |
176 subsection {* Proving a subtype is pointed *} |
176 subsection \<open>Proving a subtype is pointed\<close> |
177 |
177 |
178 text {* |
178 text \<open> |
179 A subtype of a cpo has a least element if and only if |
179 A subtype of a cpo has a least element if and only if |
180 the defining subset has a least element. |
180 the defining subset has a least element. |
181 *} |
181 \<close> |
182 |
182 |
183 theorem typedef_pcpo_generic: |
183 theorem typedef_pcpo_generic: |
184 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
184 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
185 assumes type: "type_definition Rep Abs A" |
185 assumes type: "type_definition Rep Abs A" |
186 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
186 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
192 apply (unfold below) |
192 apply (unfold below) |
193 apply (subst type_definition.Abs_inverse [OF type z_in_A]) |
193 apply (subst type_definition.Abs_inverse [OF type z_in_A]) |
194 apply (rule z_least [OF type_definition.Rep [OF type]]) |
194 apply (rule z_least [OF type_definition.Rep [OF type]]) |
195 done |
195 done |
196 |
196 |
197 text {* |
197 text \<open> |
198 As a special case, a subtype of a pcpo has a least element |
198 As a special case, a subtype of a pcpo has a least element |
199 if the defining subset contains @{term \<bottom>}. |
199 if the defining subset contains @{term \<bottom>}. |
200 *} |
200 \<close> |
201 |
201 |
202 theorem typedef_pcpo: |
202 theorem typedef_pcpo: |
203 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" |
203 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" |
204 assumes type: "type_definition Rep Abs A" |
204 assumes type: "type_definition Rep Abs A" |
205 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
205 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
206 and bottom_in_A: "\<bottom> \<in> A" |
206 and bottom_in_A: "\<bottom> \<in> A" |
207 shows "OFCLASS('b, pcpo_class)" |
207 shows "OFCLASS('b, pcpo_class)" |
208 by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal) |
208 by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal) |
209 |
209 |
210 subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *} |
210 subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close> |
211 |
211 |
212 text {* |
212 text \<open> |
213 For a sub-pcpo where @{term \<bottom>} is a member of the defining |
213 For a sub-pcpo where @{term \<bottom>} is a member of the defining |
214 subset, @{term Rep} and @{term Abs} are both strict. |
214 subset, @{term Rep} and @{term Abs} are both strict. |
215 *} |
215 \<close> |
216 |
216 |
217 theorem typedef_Abs_strict: |
217 theorem typedef_Abs_strict: |
218 assumes type: "type_definition Rep Abs A" |
218 assumes type: "type_definition Rep Abs A" |
219 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
219 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
220 and bottom_in_A: "\<bottom> \<in> A" |
220 and bottom_in_A: "\<bottom> \<in> A" |
248 shows "(Rep x = \<bottom>) = (x = \<bottom>)" |
248 shows "(Rep x = \<bottom>) = (x = \<bottom>)" |
249 apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst]) |
249 apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst]) |
250 apply (simp add: type_definition.Rep_inject [OF type]) |
250 apply (simp add: type_definition.Rep_inject [OF type]) |
251 done |
251 done |
252 |
252 |
253 subsection {* Proving a subtype is flat *} |
253 subsection \<open>Proving a subtype is flat\<close> |
254 |
254 |
255 theorem typedef_flat: |
255 theorem typedef_flat: |
256 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" |
256 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" |
257 assumes type: "type_definition Rep Abs A" |
257 assumes type: "type_definition Rep Abs A" |
258 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
258 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
263 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) |
263 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) |
264 apply (simp add: typedef_Rep_strict [OF type below bottom_in_A]) |
264 apply (simp add: typedef_Rep_strict [OF type below bottom_in_A]) |
265 apply (simp add: ax_flat) |
265 apply (simp add: ax_flat) |
266 done |
266 done |
267 |
267 |
268 subsection {* HOLCF type definition package *} |
268 subsection \<open>HOLCF type definition package\<close> |
269 |
269 |
270 ML_file "Tools/cpodef.ML" |
270 ML_file "Tools/cpodef.ML" |
271 |
271 |
272 end |
272 end |