author | huffman |
Wed, 17 Nov 2010 08:47:58 -0800 | |
changeset 40592 | f432973ce0f6 |
parent 40575 | b9a86f15e763 |
child 40771 | 1c6f7d4b110e |
permissions | -rw-r--r-- |
33591 | 1 |
(* Title: HOLCF/ex/Domain_Proofs.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Internal domain package proofs done manually *} |
|
6 |
||
7 |
theory Domain_Proofs |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
11 |
(* |
|
12 |
||
13 |
The definitions and proofs below are for the following recursive |
|
14 |
datatypes: |
|
15 |
||
16 |
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar") |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
17 |
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr") |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
18 |
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr") |
33591 | 19 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
20 |
TODO: add another type parameter that is strict, |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
21 |
to show the different handling of LIFTDEFL vs. DEFL. |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
22 |
|
33591 | 23 |
*) |
24 |
||
25 |
(********************************************************************) |
|
26 |
||
27 |
subsection {* Step 1: Define the new type combinators *} |
|
28 |
||
29 |
text {* Start with the one-step non-recursive version *} |
|
30 |
||
31 |
definition |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
32 |
foo_bar_baz_deflF :: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
33 |
"defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl" |
33591 | 34 |
where |
40327 | 35 |
"foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
36 |
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2)) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
37 |
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr)) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
38 |
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))" |
33591 | 39 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
40 |
lemma foo_bar_baz_deflF_beta: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
41 |
"foo_bar_baz_deflF\<cdot>a\<cdot>t = |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
42 |
( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t)))) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
43 |
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr)) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
44 |
, u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
45 |
unfolding foo_bar_baz_deflF_def |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
46 |
by (simp add: split_def) |
33591 | 47 |
|
48 |
text {* Individual type combinators are projected from the fixed point. *} |
|
49 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
50 |
definition foo_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
51 |
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
33591 | 52 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
53 |
definition bar_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
54 |
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 55 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
56 |
definition baz_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
57 |
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 58 |
|
36132 | 59 |
lemma defl_apply_thms: |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
60 |
"foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
61 |
"bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
62 |
"baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
63 |
unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all |
36132 | 64 |
|
33591 | 65 |
text {* Unfold rules for each combinator. *} |
66 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
67 |
lemma foo_defl_unfold: |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
68 |
"foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
69 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 70 |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
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))" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
72 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 73 |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40575
diff
changeset
|
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))" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
75 |
unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 76 |
|
77 |
text "The automation for the previous steps will be quite similar to |
|
78 |
how the fixrec package works." |
|
79 |
||
80 |
(********************************************************************) |
|
81 |
||
82 |
subsection {* Step 2: Define types, prove class instances *} |
|
83 |
||
84 |
text {* Use @{text pcpodef} with the appropriate type combinator. *} |
|
85 |
||
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
86 |
pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))" |
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset
|
87 |
by (rule defl_set_bottom, rule adm_defl_set) |
33591 | 88 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
89 |
pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))" |
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset
|
90 |
by (rule defl_set_bottom, rule adm_defl_set) |
33591 | 91 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
92 |
pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))" |
40038
9d061b3d8f46
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
huffman
parents:
40037
diff
changeset
|
93 |
by (rule defl_set_bottom, rule adm_defl_set) |
33591 | 94 |
|
95 |
text {* Prove rep instance using lemma @{text typedef_rep_class}. *} |
|
96 |
||
40497 | 97 |
instantiation foo :: ("domain") liftdomain |
33591 | 98 |
begin |
99 |
||
100 |
definition emb_foo :: "'a foo \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
101 |
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" |
33591 | 102 |
|
103 |
definition prj_foo :: "udom \<rightarrow> 'a foo" |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
104 |
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))" |
33591 | 105 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
106 |
definition defl_foo :: "'a foo itself \<Rightarrow> defl" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
107 |
where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
108 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
109 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
110 |
"(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
111 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
112 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
113 |
"(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
114 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
115 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
116 |
"liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)" |
33591 | 117 |
|
118 |
instance |
|
40575 | 119 |
apply (rule typedef_liftdomain_class) |
33591 | 120 |
apply (rule type_definition_foo) |
121 |
apply (rule below_foo_def) |
|
122 |
apply (rule emb_foo_def) |
|
123 |
apply (rule prj_foo_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
124 |
apply (rule defl_foo_def) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
125 |
apply (rule liftemb_foo_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
126 |
apply (rule liftprj_foo_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
127 |
apply (rule liftdefl_foo_def) |
33591 | 128 |
done |
129 |
||
130 |
end |
|
131 |
||
40497 | 132 |
instantiation bar :: ("domain") liftdomain |
33591 | 133 |
begin |
134 |
||
135 |
definition emb_bar :: "'a bar \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
136 |
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" |
33591 | 137 |
|
138 |
definition prj_bar :: "udom \<rightarrow> 'a bar" |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
139 |
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))" |
33591 | 140 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
141 |
definition defl_bar :: "'a bar itself \<Rightarrow> defl" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
142 |
where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
143 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
144 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
145 |
"(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
146 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
147 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
148 |
"(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
149 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
150 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
151 |
"liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)" |
33591 | 152 |
|
153 |
instance |
|
40575 | 154 |
apply (rule typedef_liftdomain_class) |
33591 | 155 |
apply (rule type_definition_bar) |
156 |
apply (rule below_bar_def) |
|
157 |
apply (rule emb_bar_def) |
|
158 |
apply (rule prj_bar_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
159 |
apply (rule defl_bar_def) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
160 |
apply (rule liftemb_bar_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
161 |
apply (rule liftprj_bar_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
162 |
apply (rule liftdefl_bar_def) |
33591 | 163 |
done |
164 |
||
165 |
end |
|
166 |
||
40497 | 167 |
instantiation baz :: ("domain") liftdomain |
33591 | 168 |
begin |
169 |
||
170 |
definition emb_baz :: "'a baz \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
171 |
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" |
33591 | 172 |
|
173 |
definition prj_baz :: "udom \<rightarrow> 'a baz" |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
174 |
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))" |
33591 | 175 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
176 |
definition defl_baz :: "'a baz itself \<Rightarrow> defl" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
177 |
where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
178 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
179 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
180 |
"(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
181 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
182 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
183 |
"(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx" |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
184 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
185 |
definition |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
186 |
"liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)" |
33591 | 187 |
|
188 |
instance |
|
40575 | 189 |
apply (rule typedef_liftdomain_class) |
33591 | 190 |
apply (rule type_definition_baz) |
191 |
apply (rule below_baz_def) |
|
192 |
apply (rule emb_baz_def) |
|
193 |
apply (rule prj_baz_def) |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
194 |
apply (rule defl_baz_def) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
195 |
apply (rule liftemb_baz_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
196 |
apply (rule liftprj_baz_def) |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
197 |
apply (rule liftdefl_baz_def) |
33591 | 198 |
done |
199 |
||
200 |
end |
|
201 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
202 |
text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *} |
33591 | 203 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
204 |
lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
205 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
206 |
apply (rule defl_foo_def) |
33591 | 207 |
done |
208 |
||
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
209 |
lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
210 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
211 |
apply (rule defl_bar_def) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset
|
212 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset
|
213 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
214 |
lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
215 |
apply (rule typedef_DEFL) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
216 |
apply (rule defl_baz_def) |
33591 | 217 |
done |
218 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
219 |
text {* Prove DEFL equations using type combinator unfold lemmas. *} |
33591 | 220 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
221 |
lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
222 |
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
223 |
by (rule foo_defl_unfold) |
33591 | 224 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
225 |
lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
226 |
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
227 |
by (rule bar_defl_unfold) |
33591 | 228 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
229 |
lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
230 |
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
231 |
by (rule baz_defl_unfold) |
33591 | 232 |
|
233 |
(********************************************************************) |
|
234 |
||
235 |
subsection {* Step 3: Define rep and abs functions *} |
|
236 |
||
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
237 |
text {* Define them all using @{text prj} and @{text emb}! *} |
33591 | 238 |
|
239 |
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
|
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
240 |
where "foo_rep \<equiv> prj oo emb" |
33591 | 241 |
|
242 |
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" |
|
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
243 |
where "foo_abs \<equiv> prj oo emb" |
33591 | 244 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
245 |
definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>" |
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
246 |
where "bar_rep \<equiv> prj oo emb" |
33591 | 247 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
248 |
definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar" |
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
249 |
where "bar_abs \<equiv> prj oo emb" |
33591 | 250 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
251 |
definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>" |
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
252 |
where "baz_rep \<equiv> prj oo emb" |
33591 | 253 |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
254 |
definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz" |
40037
81e6b89d8f58
eliminate constant 'coerce'; use 'prj oo emb' instead
huffman
parents:
39989
diff
changeset
|
255 |
where "baz_abs \<equiv> prj oo emb" |
33779 | 256 |
|
257 |
text {* Prove isomorphism rules. *} |
|
258 |
||
259 |
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
260 |
by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33779 | 261 |
|
262 |
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
263 |
by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33779 | 264 |
|
265 |
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
266 |
by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33779 | 267 |
|
268 |
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
269 |
by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33779 | 270 |
|
271 |
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
272 |
by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33779 | 273 |
|
274 |
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
275 |
by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33591 | 276 |
|
277 |
text {* Prove isodefl rules using @{text isodefl_coerce}. *} |
|
278 |
||
279 |
lemma isodefl_foo_abs: |
|
280 |
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
281 |
by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def]) |
33591 | 282 |
|
283 |
lemma isodefl_bar_abs: |
|
284 |
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
285 |
by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def]) |
33591 | 286 |
|
287 |
lemma isodefl_baz_abs: |
|
288 |
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
289 |
by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def]) |
33591 | 290 |
|
291 |
(********************************************************************) |
|
292 |
||
293 |
subsection {* Step 4: Define map functions, prove isodefl property *} |
|
294 |
||
295 |
text {* Start with the one-step non-recursive version. *} |
|
296 |
||
297 |
text {* Note that the type of the map function depends on which |
|
298 |
variables are used in positive and negative positions. *} |
|
299 |
||
300 |
definition |
|
301 |
foo_bar_baz_mapF :: |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
302 |
"('a \<rightarrow> 'b) \<rightarrow> |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
303 |
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow> |
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
304 |
('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)" |
33591 | 305 |
where |
40327 | 306 |
"foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3). |
33591 | 307 |
( |
308 |
foo_abs oo |
|
309 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) |
|
310 |
oo foo_rep |
|
311 |
, |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
312 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep |
33591 | 313 |
, |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
314 |
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
315 |
)))" |
33591 | 316 |
|
317 |
lemma foo_bar_baz_mapF_beta: |
|
318 |
"foo_bar_baz_mapF\<cdot>f\<cdot>d = |
|
319 |
( |
|
320 |
foo_abs oo |
|
321 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) |
|
322 |
oo foo_rep |
|
323 |
, |
|
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
324 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep |
33591 | 325 |
, |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
326 |
baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep |
33591 | 327 |
)" |
328 |
unfolding foo_bar_baz_mapF_def |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
329 |
by (simp add: split_def) |
33591 | 330 |
|
331 |
text {* Individual map functions are projected from the fixed point. *} |
|
332 |
||
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)))" |
|
335 |
||
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))))" |
|
338 |
||
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
339 |
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)" |
33591 | 340 |
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
341 |
||
36132 | 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 |
|
347 |
||
33591 | 348 |
text {* Prove isodefl rules for all map functions simultaneously. *} |
349 |
||
350 |
lemma isodefl_foo_bar_baz: |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
351 |
assumes isodefl_d: "isodefl (u_map\<cdot>d) t" |
33591 | 352 |
shows |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
353 |
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and> |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
354 |
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and> |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
355 |
isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)" |
36132 | 356 |
unfolding map_apply_thms defl_apply_thms |
33787
71a675065128
change example to use recursion with continuous function space
huffman
parents:
33784
diff
changeset
|
357 |
apply (rule parallel_fix_ind) |
33591 | 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 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
361 |
foo_bar_baz_deflF_beta |
33591 | 362 |
fst_conv snd_conv) |
363 |
apply (elim conjE) |
|
364 |
apply (intro |
|
365 |
conjI |
|
366 |
isodefl_foo_abs |
|
367 |
isodefl_bar_abs |
|
368 |
isodefl_baz_abs |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
369 |
domain_isodefl |
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
370 |
isodefl_ID_DEFL isodefl_LIFTDEFL |
33591 | 371 |
isodefl_d |
372 |
) |
|
373 |
apply assumption+ |
|
374 |
done |
|
375 |
||
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] |
|
379 |
||
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
380 |
text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *} |
33591 | 381 |
|
382 |
lemma foo_map_ID: "foo_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
383 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
384 |
apply (subst DEFL_foo) |
33591 | 385 |
apply (rule isodefl_foo) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
386 |
apply (rule isodefl_LIFTDEFL) |
33591 | 387 |
done |
388 |
||
389 |
lemma bar_map_ID: "bar_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
390 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
391 |
apply (subst DEFL_bar) |
33591 | 392 |
apply (rule isodefl_bar) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
393 |
apply (rule isodefl_LIFTDEFL) |
33591 | 394 |
done |
395 |
||
396 |
lemma baz_map_ID: "baz_map\<cdot>ID = ID" |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
397 |
apply (rule isodefl_DEFL_imp_ID) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39986
diff
changeset
|
398 |
apply (subst DEFL_baz) |
33591 | 399 |
apply (rule isodefl_baz) |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40327
diff
changeset
|
400 |
apply (rule isodefl_LIFTDEFL) |
33591 | 401 |
done |
402 |
||
403 |
(********************************************************************) |
|
404 |
||
36132 | 405 |
subsection {* Step 5: Define take functions, prove lub-take lemmas *} |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
406 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
407 |
definition |
36132 | 408 |
foo_bar_baz_takeF :: |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
409 |
"('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow> |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
410 |
('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
411 |
where |
36132 | 412 |
"foo_bar_baz_takeF = (\<Lambda> p. |
413 |
( foo_abs oo |
|
414 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) |
|
415 |
oo foo_rep |
|
416 |
, bar_abs oo |
|
417 |
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep |
|
418 |
, baz_abs oo |
|
419 |
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep |
|
420 |
))" |
|
421 |
||
422 |
lemma foo_bar_baz_takeF_beta: |
|
423 |
"foo_bar_baz_takeF\<cdot>p = |
|
424 |
( foo_abs oo |
|
425 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p)))) |
|
426 |
oo foo_rep |
|
427 |
, bar_abs oo |
|
428 |
u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep |
|
429 |
, baz_abs oo |
|
430 |
u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep |
|
431 |
)" |
|
432 |
unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp) |
|
433 |
||
434 |
definition |
|
435 |
foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" |
|
436 |
where |
|
437 |
"foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))" |
|
438 |
||
439 |
definition |
|
440 |
bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" |
|
441 |
where |
|
442 |
"bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" |
|
33591 | 443 |
|
36132 | 444 |
definition |
445 |
baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" |
|
446 |
where |
|
447 |
"baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))" |
|
448 |
||
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)+ |
|
452 |
||
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)+ |
|
456 |
||
457 |
lemma take_Suc_thms: |
|
458 |
"foo_take (Suc n) = |
|
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" |
|
460 |
"bar_take (Suc n) = |
|
461 |
bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep" |
|
462 |
"baz_take (Suc n) = |
|
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)+ |
|
466 |
||
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: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms) |
|
471 |
apply (simp only: map_apply_thms pair_collapse) |
|
472 |
apply (simp only: fix_def2) |
|
473 |
apply (rule lub_eq) |
|
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) |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
478 |
done |
33591 | 479 |
|
36132 | 480 |
lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID" |
481 |
apply (rule trans [OF _ foo_map_ID]) |
|
482 |
using lub_take_lemma |
|
483 |
apply (elim Pair_inject) |
|
484 |
apply assumption |
|
485 |
done |
|
33591 | 486 |
|
36132 | 487 |
lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID" |
488 |
apply (rule trans [OF _ bar_map_ID]) |
|
489 |
using lub_take_lemma |
|
490 |
apply (elim Pair_inject) |
|
491 |
apply assumption |
|
492 |
done |
|
33591 | 493 |
|
36132 | 494 |
lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID" |
495 |
apply (rule trans [OF _ baz_map_ID]) |
|
496 |
using lub_take_lemma |
|
497 |
apply (elim Pair_inject) |
|
498 |
apply assumption |
|
499 |
done |
|
33591 | 500 |
|
501 |
end |