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