19 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>Porder.below\<close>, 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: "(\<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]) |
49 |
49 |
50 |
50 |
51 subsection \<open>Proving a subtype is chain-finite\<close> |
51 subsection \<open>Proving a subtype is chain-finite\<close> |
52 |
52 |
53 lemma ch2ch_Rep: |
53 lemma ch2ch_Rep: |
54 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
54 assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
55 shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))" |
55 shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))" |
56 unfolding chain_def below . |
56 unfolding chain_def below . |
57 |
57 |
58 theorem typedef_chfin: |
58 theorem typedef_chfin: |
59 fixes Abs :: "'a::chfin \<Rightarrow> 'b::po" |
59 fixes Abs :: "'a::chfin \<Rightarrow> 'b::po" |
60 assumes type: "type_definition Rep Abs A" |
60 assumes type: "type_definition Rep Abs A" |
61 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
61 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
62 shows "OFCLASS('b, chfin_class)" |
62 shows "OFCLASS('b, chfin_class)" |
63 apply intro_classes |
63 apply intro_classes |
64 apply (drule ch2ch_Rep [OF below]) |
64 apply (drule ch2ch_Rep [OF below]) |
65 apply (drule chfin) |
65 apply (drule chfin) |
66 apply (unfold max_in_chain_def) |
66 apply (unfold max_in_chain_def) |
77 closed if and only if membership in the set is an |
77 closed if and only if membership in the set is an |
78 admissible predicate. |
78 admissible predicate. |
79 \<close> |
79 \<close> |
80 |
80 |
81 lemma typedef_is_lubI: |
81 lemma typedef_is_lubI: |
82 assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
82 assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
83 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" |
84 by (simp add: is_lub_def is_ub_def below) |
84 by (simp add: is_lub_def is_ub_def below) |
85 |
85 |
86 lemma Abs_inverse_lub_Rep: |
86 lemma Abs_inverse_lub_Rep: |
87 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
87 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
88 assumes type: "type_definition Rep Abs A" |
88 assumes type: "type_definition Rep Abs A" |
89 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
89 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
90 and adm: "adm (\<lambda>x. x \<in> A)" |
90 and adm: "adm (\<lambda>x. x \<in> A)" |
91 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))" |
92 apply (rule type_definition.Abs_inverse [OF type]) |
92 apply (rule type_definition.Abs_inverse [OF type]) |
93 apply (erule admD [OF adm ch2ch_Rep [OF below]]) |
93 apply (erule admD [OF adm ch2ch_Rep [OF below]]) |
94 apply (rule type_definition.Rep [OF type]) |
94 apply (rule type_definition.Rep [OF type]) |
95 done |
95 done |
96 |
96 |
97 theorem typedef_is_lub: |
97 theorem typedef_is_lub: |
98 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
98 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
99 assumes type: "type_definition Rep Abs A" |
99 assumes type: "type_definition Rep Abs A" |
100 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
100 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
101 and adm: "adm (\<lambda>x. x \<in> A)" |
101 and adm: "adm (\<lambda>x. x \<in> A)" |
102 assumes S: "chain S" |
102 assumes S: "chain S" |
103 shows "range S <<| Abs (\<Squnion>i. Rep (S i))" |
103 shows "range S <<| Abs (\<Squnion>i. Rep (S i))" |
104 proof - |
104 proof - |
105 from S have "chain (\<lambda>i. Rep (S i))" |
105 from S have "chain (\<lambda>i. Rep (S i))" |
115 lemmas typedef_lub = typedef_is_lub [THEN lub_eqI] |
115 lemmas typedef_lub = typedef_is_lub [THEN lub_eqI] |
116 |
116 |
117 theorem typedef_cpo: |
117 theorem typedef_cpo: |
118 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
118 fixes Abs :: "'a::cpo \<Rightarrow> 'b::po" |
119 assumes type: "type_definition Rep Abs A" |
119 assumes type: "type_definition Rep Abs A" |
120 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
120 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
121 and adm: "adm (\<lambda>x. x \<in> A)" |
121 and adm: "adm (\<lambda>x. x \<in> A)" |
122 shows "OFCLASS('b, cpo_class)" |
122 shows "OFCLASS('b, cpo_class)" |
123 proof |
123 proof |
124 fix S :: "nat \<Rightarrow> 'b" |
124 fix S :: "nat \<Rightarrow> 'b" |
125 assume "chain S" |
125 assume "chain S" |
134 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> |
135 |
135 |
136 theorem typedef_cont_Rep: |
136 theorem typedef_cont_Rep: |
137 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
137 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
138 assumes type: "type_definition Rep Abs A" |
138 assumes type: "type_definition Rep Abs A" |
139 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
139 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
140 and adm: "adm (\<lambda>x. x \<in> A)" |
140 and adm: "adm (\<lambda>x. x \<in> A)" |
141 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))" |
142 apply (erule cont_apply [OF _ _ cont_const]) |
142 apply (erule cont_apply [OF _ _ cont_const]) |
143 apply (rule contI) |
143 apply (rule contI) |
144 apply (simp only: typedef_lub [OF type below adm]) |
144 apply (simp only: typedef_lub [OF type below adm]) |
155 |
155 |
156 theorem typedef_cont_Abs: |
156 theorem typedef_cont_Abs: |
157 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
157 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
158 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
158 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
159 assumes type: "type_definition Rep Abs A" |
159 assumes type: "type_definition Rep Abs A" |
160 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
160 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
161 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) |
161 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) |
162 and f_in_A: "\<And>x. f x \<in> A" |
162 and f_in_A: "\<And>x. f x \<in> A" |
163 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
163 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
164 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 |
165 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]) |
168 subsection \<open>Proving subtype elements are compact\<close> |
168 subsection \<open>Proving subtype elements are compact\<close> |
169 |
169 |
170 theorem typedef_compact: |
170 theorem typedef_compact: |
171 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
171 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
172 assumes type: "type_definition Rep Abs A" |
172 assumes type: "type_definition Rep Abs A" |
173 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
173 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
174 and adm: "adm (\<lambda>x. x \<in> A)" |
174 and adm: "adm (\<lambda>x. x \<in> A)" |
175 shows "compact (Rep k) \<Longrightarrow> compact k" |
175 shows "compact (Rep k) \<Longrightarrow> compact k" |
176 proof (unfold compact_def) |
176 proof (unfold compact_def) |
177 have cont_Rep: "cont Rep" |
177 have cont_Rep: "cont Rep" |
178 by (rule typedef_cont_Rep [OF type below adm cont_id]) |
178 by (rule typedef_cont_Rep [OF type below adm cont_id]) |
190 \<close> |
190 \<close> |
191 |
191 |
192 theorem typedef_pcpo_generic: |
192 theorem typedef_pcpo_generic: |
193 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
193 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
194 assumes type: "type_definition Rep Abs A" |
194 assumes type: "type_definition Rep Abs A" |
195 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
195 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
196 and z_in_A: "z \<in> A" |
196 and z_in_A: "z \<in> A" |
197 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" |
198 shows "OFCLASS('b, pcpo_class)" |
198 shows "OFCLASS('b, pcpo_class)" |
199 apply (intro_classes) |
199 apply (intro_classes) |
200 apply (rule_tac x="Abs z" in exI, rule allI) |
200 apply (rule_tac x="Abs z" in exI, rule allI) |
209 \<close> |
209 \<close> |
210 |
210 |
211 theorem typedef_pcpo: |
211 theorem typedef_pcpo: |
212 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" |
212 fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo" |
213 assumes type: "type_definition Rep Abs A" |
213 assumes type: "type_definition Rep Abs A" |
214 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
214 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
215 and bottom_in_A: "\<bottom> \<in> A" |
215 and bottom_in_A: "\<bottom> \<in> A" |
216 shows "OFCLASS('b, pcpo_class)" |
216 shows "OFCLASS('b, pcpo_class)" |
217 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 |
218 |
219 |
219 |
224 subset, @{term Rep} and @{term Abs} are both strict. |
224 subset, @{term Rep} and @{term Abs} are both strict. |
225 \<close> |
225 \<close> |
226 |
226 |
227 theorem typedef_Abs_strict: |
227 theorem typedef_Abs_strict: |
228 assumes type: "type_definition Rep Abs A" |
228 assumes type: "type_definition Rep Abs A" |
229 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
229 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
230 and bottom_in_A: "\<bottom> \<in> A" |
230 and bottom_in_A: "\<bottom> \<in> A" |
231 shows "Abs \<bottom> = \<bottom>" |
231 shows "Abs \<bottom> = \<bottom>" |
232 apply (rule bottomI, unfold below) |
232 apply (rule bottomI, unfold below) |
233 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]) |
234 done |
234 done |
235 |
235 |
236 theorem typedef_Rep_strict: |
236 theorem typedef_Rep_strict: |
237 assumes type: "type_definition Rep Abs A" |
237 assumes type: "type_definition Rep Abs A" |
238 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
238 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
239 and bottom_in_A: "\<bottom> \<in> A" |
239 and bottom_in_A: "\<bottom> \<in> A" |
240 shows "Rep \<bottom> = \<bottom>" |
240 shows "Rep \<bottom> = \<bottom>" |
241 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]) |
242 apply (rule type_definition.Abs_inverse [OF type bottom_in_A]) |
242 apply (rule type_definition.Abs_inverse [OF type bottom_in_A]) |
243 done |
243 done |
244 |
244 |
245 theorem typedef_Abs_bottom_iff: |
245 theorem typedef_Abs_bottom_iff: |
246 assumes type: "type_definition Rep Abs A" |
246 assumes type: "type_definition Rep Abs A" |
247 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
247 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
248 and bottom_in_A: "\<bottom> \<in> A" |
248 and bottom_in_A: "\<bottom> \<in> A" |
249 shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)" |
249 shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)" |
250 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]) |
251 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) |
252 done |
252 done |
253 |
253 |
254 theorem typedef_Rep_bottom_iff: |
254 theorem typedef_Rep_bottom_iff: |
255 assumes type: "type_definition Rep Abs A" |
255 assumes type: "type_definition Rep Abs A" |
256 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
256 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
257 and bottom_in_A: "\<bottom> \<in> A" |
257 and bottom_in_A: "\<bottom> \<in> A" |
258 shows "(Rep x = \<bottom>) = (x = \<bottom>)" |
258 shows "(Rep x = \<bottom>) = (x = \<bottom>)" |
259 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]) |
260 apply (simp add: type_definition.Rep_inject [OF type]) |
260 apply (simp add: type_definition.Rep_inject [OF type]) |
261 done |
261 done |
264 subsection \<open>Proving a subtype is flat\<close> |
264 subsection \<open>Proving a subtype is flat\<close> |
265 |
265 |
266 theorem typedef_flat: |
266 theorem typedef_flat: |
267 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" |
267 fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo" |
268 assumes type: "type_definition Rep Abs A" |
268 assumes type: "type_definition Rep Abs A" |
269 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
269 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
270 and bottom_in_A: "\<bottom> \<in> A" |
270 and bottom_in_A: "\<bottom> \<in> A" |
271 shows "OFCLASS('b, flat_class)" |
271 shows "OFCLASS('b, flat_class)" |
272 apply (intro_classes) |
272 apply (intro_classes) |
273 apply (unfold below) |
273 apply (unfold below) |
274 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) |
274 apply (simp add: type_definition.Rep_inject [OF type, symmetric]) |