1 (* Title: HOLCF/ex/Domain_Proofs.thy
5 header {* Internal domain package proofs done manually *}
13 The definitions and proofs below are for the following recursive
16 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
17 and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
18 and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
20 TODO: add another type parameter that is strict,
21 to show the different handling of LIFTDEFL vs. DEFL.
25 (********************************************************************)
27 subsection {* Step 1: Define the new type combinators *}
29 text {* Start with the one-step non-recursive version *}
33 "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
35 "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3).
36 ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
37 , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
38 , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
40 lemma foo_bar_baz_deflF_beta:
41 "foo_bar_baz_deflF\<cdot>a\<cdot>t =
42 ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
43 , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
44 , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
45 unfolding foo_bar_baz_deflF_def
46 by (simp add: split_def)
48 text {* Individual type combinators are projected from the fixed point. *}
50 definition foo_defl :: "defl \<rightarrow> defl"
51 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
53 definition bar_defl :: "defl \<rightarrow> defl"
54 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
56 definition baz_defl :: "defl \<rightarrow> defl"
57 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
59 lemma defl_apply_thms:
60 "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
61 "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
62 "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
63 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
65 text {* Unfold rules for each combinator. *}
67 lemma foo_defl_unfold:
68 "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
71 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
74 lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
75 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
77 text "The automation for the previous steps will be quite similar to
78 how the fixrec package works."
80 (********************************************************************)
82 subsection {* Step 2: Define types, prove class instances *}
84 text {* Use @{text pcpodef} with the appropriate type combinator. *}
86 pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
87 by (rule defl_set_bottom, rule adm_defl_set)
89 pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
90 by (rule defl_set_bottom, rule adm_defl_set)
92 pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
93 by (rule defl_set_bottom, rule adm_defl_set)
95 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
97 instantiation foo :: ("domain") liftdomain
100 definition emb_foo :: "'a foo \<rightarrow> udom"
101 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
103 definition prj_foo :: "udom \<rightarrow> 'a foo"
104 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
106 definition defl_foo :: "'a foo itself \<Rightarrow> defl"
107 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
110 "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
113 "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
116 "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
119 apply (rule typedef_liftdomain_class)
120 apply (rule type_definition_foo)
121 apply (rule below_foo_def)
122 apply (rule emb_foo_def)
123 apply (rule prj_foo_def)
124 apply (rule defl_foo_def)
125 apply (rule liftemb_foo_def)
126 apply (rule liftprj_foo_def)
127 apply (rule liftdefl_foo_def)
132 instantiation bar :: ("domain") liftdomain
135 definition emb_bar :: "'a bar \<rightarrow> udom"
136 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
138 definition prj_bar :: "udom \<rightarrow> 'a bar"
139 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
141 definition defl_bar :: "'a bar itself \<Rightarrow> defl"
142 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
145 "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
148 "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
151 "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
154 apply (rule typedef_liftdomain_class)
155 apply (rule type_definition_bar)
156 apply (rule below_bar_def)
157 apply (rule emb_bar_def)
158 apply (rule prj_bar_def)
159 apply (rule defl_bar_def)
160 apply (rule liftemb_bar_def)
161 apply (rule liftprj_bar_def)
162 apply (rule liftdefl_bar_def)
167 instantiation baz :: ("domain") liftdomain
170 definition emb_baz :: "'a baz \<rightarrow> udom"
171 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
173 definition prj_baz :: "udom \<rightarrow> 'a baz"
174 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
176 definition defl_baz :: "'a baz itself \<Rightarrow> defl"
177 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
180 "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
183 "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
186 "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
189 apply (rule typedef_liftdomain_class)
190 apply (rule type_definition_baz)
191 apply (rule below_baz_def)
192 apply (rule emb_baz_def)
193 apply (rule prj_baz_def)
194 apply (rule defl_baz_def)
195 apply (rule liftemb_baz_def)
196 apply (rule liftprj_baz_def)
197 apply (rule liftdefl_baz_def)
202 text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
204 lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
205 apply (rule typedef_DEFL)
206 apply (rule defl_foo_def)
209 lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
210 apply (rule typedef_DEFL)
211 apply (rule defl_bar_def)
214 lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
215 apply (rule typedef_DEFL)
216 apply (rule defl_baz_def)
219 text {* Prove DEFL equations using type combinator unfold lemmas. *}
221 lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
222 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
223 by (rule foo_defl_unfold)
225 lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
226 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
227 by (rule bar_defl_unfold)
229 lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
230 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
231 by (rule baz_defl_unfold)
233 (********************************************************************)
235 subsection {* Step 3: Define rep and abs functions *}
237 text {* Define them all using @{text prj} and @{text emb}! *}
239 definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
240 where "foo_rep \<equiv> prj oo emb"
242 definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
243 where "foo_abs \<equiv> prj oo emb"
245 definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
246 where "bar_rep \<equiv> prj oo emb"
248 definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
249 where "bar_abs \<equiv> prj oo emb"
251 definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
252 where "baz_rep \<equiv> prj oo emb"
254 definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
255 where "baz_abs \<equiv> prj oo emb"
257 text {* Prove isomorphism rules. *}
259 lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
260 by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
262 lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
263 by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
265 lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
266 by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
268 lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
269 by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
271 lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
272 by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
274 lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
275 by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
277 text {* Prove isodefl rules using @{text isodefl_coerce}. *}
279 lemma isodefl_foo_abs:
280 "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
281 by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
283 lemma isodefl_bar_abs:
284 "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
285 by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
287 lemma isodefl_baz_abs:
288 "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
289 by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
291 (********************************************************************)
293 subsection {* Step 4: Define map functions, prove isodefl property *}
295 text {* Start with the one-step non-recursive version. *}
297 text {* Note that the type of the map function depends on which
298 variables are used in positive and negative positions. *}
302 "('a \<rightarrow> 'b) \<rightarrow>
303 ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
304 ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
306 "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
309 ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
312 bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
314 baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
317 lemma foo_bar_baz_mapF_beta:
318 "foo_bar_baz_mapF\<cdot>f\<cdot>d =
321 ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
324 bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
326 baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
328 unfolding foo_bar_baz_mapF_def
329 by (simp add: split_def)
331 text {* Individual map functions are projected from the fixed point. *}
333 definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
334 where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
336 definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
337 where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
339 definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
340 where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
342 lemma map_apply_thms:
343 "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
344 "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
345 "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
346 unfolding foo_map_def bar_map_def baz_map_def by simp_all
348 text {* Prove isodefl rules for all map functions simultaneously. *}
350 lemma isodefl_foo_bar_baz:
351 assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
353 "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
354 isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
355 isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
356 unfolding map_apply_thms defl_apply_thms
357 apply (rule parallel_fix_ind)
358 apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
359 apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
360 apply (simp only: foo_bar_baz_mapF_beta
361 foo_bar_baz_deflF_beta
370 isodefl_ID_DEFL isodefl_LIFTDEFL
376 lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
377 lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
378 lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
380 text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
382 lemma foo_map_ID: "foo_map\<cdot>ID = ID"
383 apply (rule isodefl_DEFL_imp_ID)
384 apply (subst DEFL_foo)
385 apply (rule isodefl_foo)
386 apply (rule isodefl_LIFTDEFL)
389 lemma bar_map_ID: "bar_map\<cdot>ID = ID"
390 apply (rule isodefl_DEFL_imp_ID)
391 apply (subst DEFL_bar)
392 apply (rule isodefl_bar)
393 apply (rule isodefl_LIFTDEFL)
396 lemma baz_map_ID: "baz_map\<cdot>ID = ID"
397 apply (rule isodefl_DEFL_imp_ID)
398 apply (subst DEFL_baz)
399 apply (rule isodefl_baz)
400 apply (rule isodefl_LIFTDEFL)
403 (********************************************************************)
405 subsection {* Step 5: Define take functions, prove lub-take lemmas *}
409 "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
410 ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
412 "foo_bar_baz_takeF = (\<Lambda> p.
414 ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
417 u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
419 u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
422 lemma foo_bar_baz_takeF_beta:
423 "foo_bar_baz_takeF\<cdot>p =
425 ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
428 u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
430 u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
432 unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
435 foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
437 "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
440 bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
442 "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
445 baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
447 "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
449 lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
450 unfolding foo_take_def bar_take_def baz_take_def
451 by (intro ch2ch_fst ch2ch_snd chain_iterate)+
453 lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
454 unfolding foo_take_def bar_take_def baz_take_def
455 by (simp only: iterate_0 fst_strict snd_strict)+
459 foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
461 bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
463 baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
464 unfolding foo_take_def bar_take_def baz_take_def
465 by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
467 lemma lub_take_lemma:
468 "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
469 = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
470 apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
471 apply (simp only: map_apply_thms pair_collapse)
472 apply (simp only: fix_def2)
474 apply (rule nat.induct)
475 apply (simp only: iterate_0 Pair_strict take_0_thms)
476 apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
477 foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
480 lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
481 apply (rule trans [OF _ foo_map_ID])
483 apply (elim Pair_inject)
487 lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
488 apply (rule trans [OF _ bar_map_ID])
490 apply (elim Pair_inject)
494 lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
495 apply (rule trans [OF _ baz_map_ID])
497 apply (elim Pair_inject)