author | wenzelm |
Sat, 27 Feb 2021 13:20:52 +0100 | |
changeset 73310 | 6e155bb1516d |
parent 69605 | a96320074298 |
child 78793 | 2cb027b95188 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Domain_Aux.thy |
35652 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
62175 | 5 |
section \<open>Domain package support\<close> |
35652 | 6 |
|
7 |
theory Domain_Aux |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
8 |
imports Map_Functions Fixrec |
35652 | 9 |
begin |
10 |
||
62175 | 11 |
subsection \<open>Continuous isomorphisms\<close> |
35653 | 12 |
|
62175 | 13 |
text \<open>A locale for continuous isomorphisms\<close> |
35653 | 14 |
|
15 |
locale iso = |
|
16 |
fixes abs :: "'a \<rightarrow> 'b" |
|
17 |
fixes rep :: "'b \<rightarrow> 'a" |
|
18 |
assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x" |
|
19 |
assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y" |
|
20 |
begin |
|
21 |
||
22 |
lemma swap: "iso rep abs" |
|
23 |
by (rule iso.intro [OF rep_iso abs_iso]) |
|
24 |
||
25 |
lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)" |
|
26 |
proof |
|
27 |
assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" |
|
28 |
then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg) |
|
29 |
then show "x \<sqsubseteq> y" by simp |
|
30 |
next |
|
31 |
assume "x \<sqsubseteq> y" |
|
32 |
then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg) |
|
33 |
qed |
|
34 |
||
35 |
lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)" |
|
36 |
by (rule iso.abs_below [OF swap]) |
|
37 |
||
38 |
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)" |
|
39 |
by (simp add: po_eq_conv abs_below) |
|
40 |
||
41 |
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)" |
|
42 |
by (rule iso.abs_eq [OF swap]) |
|
43 |
||
44 |
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>" |
|
45 |
proof - |
|
46 |
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" .. |
|
47 |
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg) |
|
48 |
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp |
|
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset
|
49 |
then show ?thesis by (rule bottomI) |
35653 | 50 |
qed |
51 |
||
52 |
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>" |
|
53 |
by (rule iso.abs_strict [OF swap]) |
|
54 |
||
55 |
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>" |
|
56 |
proof - |
|
57 |
have "x = rep\<cdot>(abs\<cdot>x)" by simp |
|
58 |
also assume "abs\<cdot>x = \<bottom>" |
|
59 |
also note rep_strict |
|
60 |
finally show "x = \<bottom>" . |
|
61 |
qed |
|
62 |
||
63 |
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>" |
|
64 |
by (rule iso.abs_defin' [OF swap]) |
|
65 |
||
66 |
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>" |
|
67 |
by (erule contrapos_nn, erule abs_defin') |
|
68 |
||
69 |
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" |
|
70 |
by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms) |
|
71 |
||
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40216
diff
changeset
|
72 |
lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)" |
35653 | 73 |
by (auto elim: abs_defin' intro: abs_strict) |
74 |
||
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40216
diff
changeset
|
75 |
lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)" |
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40216
diff
changeset
|
76 |
by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms) |
35653 | 77 |
|
78 |
lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P" |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40216
diff
changeset
|
79 |
by (simp add: rep_bottom_iff) |
35653 | 80 |
|
81 |
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
|
82 |
proof (unfold compact_def) |
|
41182 | 83 |
assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> y)" |
40327 | 84 |
with cont_Rep_cfun2 |
41182 | 85 |
have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst) |
86 |
then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp |
|
35653 | 87 |
qed |
88 |
||
89 |
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x" |
|
90 |
by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms) |
|
91 |
||
92 |
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)" |
|
93 |
by (rule compact_rep_rev) simp |
|
94 |
||
95 |
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)" |
|
96 |
by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms) |
|
97 |
||
98 |
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)" |
|
99 |
proof |
|
100 |
assume "x = abs\<cdot>y" |
|
101 |
then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp |
|
102 |
then show "rep\<cdot>x = y" by simp |
|
103 |
next |
|
104 |
assume "rep\<cdot>x = y" |
|
105 |
then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp |
|
106 |
then show "x = abs\<cdot>y" by simp |
|
107 |
qed |
|
108 |
||
109 |
end |
|
110 |
||
62175 | 111 |
subsection \<open>Proofs about take functions\<close> |
35652 | 112 |
|
62175 | 113 |
text \<open> |
35652 | 114 |
This section contains lemmas that are used in a module that supports |
115 |
the domain isomorphism package; the module contains proofs related |
|
116 |
to take functions and the finiteness predicate. |
|
62175 | 117 |
\<close> |
35652 | 118 |
|
119 |
lemma deflation_abs_rep: |
|
120 |
fixes abs and rep and d |
|
121 |
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" |
|
122 |
assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" |
|
123 |
shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" |
|
124 |
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) |
|
125 |
||
126 |
lemma deflation_chain_min: |
|
127 |
assumes chain: "chain d" |
|
128 |
assumes defl: "\<And>n. deflation (d n)" |
|
129 |
shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" |
|
130 |
proof (rule linorder_le_cases) |
|
131 |
assume "m \<le> n" |
|
132 |
with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) |
|
133 |
then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" |
|
134 |
by (rule deflation_below_comp1 [OF defl defl]) |
|
62175 | 135 |
moreover from \<open>m \<le> n\<close> have "min m n = m" by simp |
35652 | 136 |
ultimately show ?thesis by simp |
137 |
next |
|
138 |
assume "n \<le> m" |
|
139 |
with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) |
|
140 |
then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" |
|
141 |
by (rule deflation_below_comp2 [OF defl defl]) |
|
62175 | 142 |
moreover from \<open>n \<le> m\<close> have "min m n = n" by simp |
35652 | 143 |
ultimately show ?thesis by simp |
144 |
qed |
|
145 |
||
35653 | 146 |
lemma lub_ID_take_lemma: |
147 |
assumes "chain t" and "(\<Squnion>n. t n) = ID" |
|
148 |
assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y" |
|
149 |
proof - |
|
150 |
have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)" |
|
151 |
using assms(3) by simp |
|
152 |
then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y" |
|
153 |
using assms(1) by (simp add: lub_distribs) |
|
154 |
then show "x = y" |
|
155 |
using assms(2) by simp |
|
156 |
qed |
|
157 |
||
158 |
lemma lub_ID_reach: |
|
159 |
assumes "chain t" and "(\<Squnion>n. t n) = ID" |
|
160 |
shows "(\<Squnion>n. t n\<cdot>x) = x" |
|
161 |
using assms by (simp add: lub_distribs) |
|
162 |
||
35655 | 163 |
lemma lub_ID_take_induct: |
164 |
assumes "chain t" and "(\<Squnion>n. t n) = ID" |
|
165 |
assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x" |
|
166 |
proof - |
|
62175 | 167 |
from \<open>chain t\<close> have "chain (\<lambda>n. t n\<cdot>x)" by simp |
168 |
from \<open>adm P\<close> this \<open>\<And>n. P (t n\<cdot>x)\<close> have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD) |
|
169 |
with \<open>chain t\<close> \<open>(\<Squnion>n. t n) = ID\<close> show "P x" by (simp add: lub_distribs) |
|
35655 | 170 |
qed |
171 |
||
62175 | 172 |
subsection \<open>Finiteness\<close> |
35653 | 173 |
|
62175 | 174 |
text \<open> |
35653 | 175 |
Let a ``decisive'' function be a deflation that maps every input to |
176 |
either itself or bottom. Then if a domain's take functions are all |
|
177 |
decisive, then all values in the domain are finite. |
|
62175 | 178 |
\<close> |
35653 | 179 |
|
180 |
definition |
|
181 |
decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool" |
|
182 |
where |
|
183 |
"decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)" |
|
184 |
||
185 |
lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d" |
|
186 |
unfolding decisive_def by simp |
|
187 |
||
188 |
lemma decisive_cases: |
|
189 |
assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>" |
|
190 |
using assms unfolding decisive_def by auto |
|
191 |
||
192 |
lemma decisive_bottom: "decisive \<bottom>" |
|
193 |
unfolding decisive_def by simp |
|
194 |
||
195 |
lemma decisive_ID: "decisive ID" |
|
196 |
unfolding decisive_def by simp |
|
197 |
||
198 |
lemma decisive_ssum_map: |
|
199 |
assumes f: "decisive f" |
|
200 |
assumes g: "decisive g" |
|
201 |
shows "decisive (ssum_map\<cdot>f\<cdot>g)" |
|
68383 | 202 |
apply (rule decisiveI) |
203 |
subgoal for s |
|
204 |
apply (cases s, simp_all) |
|
205 |
apply (rule_tac x=x in decisive_cases [OF f], simp_all) |
|
206 |
apply (rule_tac x=y in decisive_cases [OF g], simp_all) |
|
207 |
done |
|
208 |
done |
|
35653 | 209 |
|
210 |
lemma decisive_sprod_map: |
|
211 |
assumes f: "decisive f" |
|
212 |
assumes g: "decisive g" |
|
213 |
shows "decisive (sprod_map\<cdot>f\<cdot>g)" |
|
68383 | 214 |
apply (rule decisiveI) |
215 |
subgoal for s |
|
216 |
apply (cases s, simp) |
|
217 |
subgoal for x y |
|
218 |
apply (rule decisive_cases [OF f, where x = x], simp_all) |
|
219 |
apply (rule decisive_cases [OF g, where x = y], simp_all) |
|
220 |
done |
|
221 |
done |
|
222 |
done |
|
35653 | 223 |
|
224 |
lemma decisive_abs_rep: |
|
225 |
fixes abs rep |
|
226 |
assumes iso: "iso abs rep" |
|
227 |
assumes d: "decisive d" |
|
228 |
shows "decisive (abs oo d oo rep)" |
|
68383 | 229 |
apply (rule decisiveI) |
230 |
subgoal for s |
|
231 |
apply (rule decisive_cases [OF d, where x="rep\<cdot>s"]) |
|
232 |
apply (simp add: iso.rep_iso [OF iso]) |
|
233 |
apply (simp add: iso.abs_strict [OF iso]) |
|
234 |
done |
|
235 |
done |
|
35653 | 236 |
|
237 |
lemma lub_ID_finite: |
|
238 |
assumes chain: "chain d" |
|
239 |
assumes lub: "(\<Squnion>n. d n) = ID" |
|
240 |
assumes decisive: "\<And>n. decisive (d n)" |
|
241 |
shows "\<exists>n. d n\<cdot>x = x" |
|
242 |
proof - |
|
243 |
have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp |
|
244 |
have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach) |
|
245 |
have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>" |
|
246 |
using decisive unfolding decisive_def by simp |
|
247 |
hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}" |
|
248 |
by auto |
|
249 |
hence "finite (range (\<lambda>n. d n\<cdot>x))" |
|
250 |
by (rule finite_subset, simp) |
|
251 |
with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)" |
|
252 |
by (rule finite_range_imp_finch) |
|
253 |
then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x" |
|
254 |
unfolding finite_chain_def by (auto simp add: maxinch_is_thelub) |
|
255 |
with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym) |
|
256 |
qed |
|
257 |
||
35655 | 258 |
lemma lub_ID_finite_take_induct: |
259 |
assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)" |
|
260 |
shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x" |
|
261 |
using lub_ID_finite [OF assms] by metis |
|
262 |
||
62175 | 263 |
subsection \<open>Proofs about constructor functions\<close> |
40503 | 264 |
|
62175 | 265 |
text \<open>Lemmas for proving nchotomy rule:\<close> |
40503 | 266 |
|
267 |
lemma ex_one_bottom_iff: |
|
268 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE" |
|
269 |
by simp |
|
270 |
||
271 |
lemma ex_up_bottom_iff: |
|
272 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" |
|
273 |
by (safe, case_tac x, auto) |
|
274 |
||
275 |
lemma ex_sprod_bottom_iff: |
|
276 |
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
277 |
(\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" |
|
278 |
by (safe, case_tac y, auto) |
|
279 |
||
280 |
lemma ex_sprod_up_bottom_iff: |
|
281 |
"(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
|
282 |
(\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" |
|
283 |
by (safe, case_tac y, simp, case_tac x, auto) |
|
284 |
||
285 |
lemma ex_ssum_bottom_iff: |
|
286 |
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = |
|
287 |
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or> |
|
288 |
(\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))" |
|
289 |
by (safe, case_tac x, auto) |
|
290 |
||
291 |
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)" |
|
292 |
by auto |
|
293 |
||
294 |
lemmas ex_bottom_iffs = |
|
295 |
ex_ssum_bottom_iff |
|
296 |
ex_sprod_up_bottom_iff |
|
297 |
ex_sprod_bottom_iff |
|
298 |
ex_up_bottom_iff |
|
299 |
ex_one_bottom_iff |
|
300 |
||
62175 | 301 |
text \<open>Rules for turning nchotomy into exhaust:\<close> |
40503 | 302 |
|
303 |
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *) |
|
304 |
by auto |
|
305 |
||
306 |
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)" |
|
307 |
by rule auto |
|
308 |
||
309 |
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" |
|
310 |
by rule auto |
|
311 |
||
312 |
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)" |
|
313 |
by rule auto |
|
314 |
||
315 |
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3 |
|
316 |
||
62175 | 317 |
text \<open>Rules for proving constructor properties\<close> |
40503 | 318 |
|
319 |
lemmas con_strict_rules = |
|
320 |
sinl_strict sinr_strict spair_strict1 spair_strict2 |
|
321 |
||
322 |
lemmas con_bottom_iff_rules = |
|
323 |
sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined |
|
324 |
||
325 |
lemmas con_below_iff_rules = |
|
326 |
sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules |
|
327 |
||
328 |
lemmas con_eq_iff_rules = |
|
329 |
sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules |
|
330 |
||
331 |
lemmas sel_strict_rules = |
|
332 |
cfcomp2 sscase1 sfst_strict ssnd_strict fup1 |
|
333 |
||
334 |
lemma sel_app_extra_rules: |
|
335 |
"sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>" |
|
336 |
"sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x" |
|
337 |
"sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>" |
|
338 |
"sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x" |
|
339 |
"fup\<cdot>ID\<cdot>(up\<cdot>x) = x" |
|
340 |
by (cases "x = \<bottom>", simp, simp)+ |
|
341 |
||
342 |
lemmas sel_app_rules = |
|
343 |
sel_strict_rules sel_app_extra_rules |
|
344 |
ssnd_spair sfst_spair up_defined spair_defined |
|
345 |
||
346 |
lemmas sel_bottom_iff_rules = |
|
347 |
cfcomp2 sfst_bottom_iff ssnd_bottom_iff |
|
348 |
||
349 |
lemmas take_con_rules = |
|
350 |
ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up |
|
351 |
deflation_strict deflation_ID ID1 cfcomp2 |
|
352 |
||
62175 | 353 |
subsection \<open>ML setup\<close> |
35653 | 354 |
|
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
355 |
named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)" |
59028 | 356 |
and domain_map_ID "theorems like foo_map$ID = ID" |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
56511
diff
changeset
|
357 |
|
69605 | 358 |
ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close> |
359 |
ML_file \<open>Tools/cont_consts.ML\<close> |
|
360 |
ML_file \<open>Tools/cont_proc.ML\<close> |
|
361 |
ML_file \<open>Tools/Domain/domain_constructors.ML\<close> |
|
362 |
ML_file \<open>Tools/Domain/domain_induction.ML\<close> |
|
35652 | 363 |
|
364 |
end |