author | huffman |
Thu, 19 Nov 2009 08:22:00 -0800 | |
changeset 33784 | 7e434813752f |
parent 33781 | c7d32e726bb9 |
child 33787 | 71a675065128 |
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 |
defaultsort rep |
|
12 |
||
13 |
(* |
|
14 |
||
15 |
The definitions and proofs below are for the following recursive |
|
16 |
datatypes: |
|
17 |
||
18 |
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar") |
|
19 |
and 'a bar = Bar (lazy 'a) (lazy "'a baz") |
|
20 |
and 'a baz = Baz (lazy 'a) (lazy "'a foo convex_pd") |
|
21 |
||
22 |
*) |
|
23 |
||
24 |
(********************************************************************) |
|
25 |
||
26 |
subsection {* Step 1: Define the new type combinators *} |
|
27 |
||
28 |
text {* Start with the one-step non-recursive version *} |
|
29 |
||
30 |
definition |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
31 |
foo_bar_baz_deflF :: |
33591 | 32 |
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep" |
33 |
where |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
34 |
"foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
35 |
( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2)) |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
36 |
, sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t3) |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
37 |
, sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1)))))" |
33591 | 38 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
39 |
lemma foo_bar_baz_deflF_beta: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
40 |
"foo_bar_baz_deflF\<cdot>a\<cdot>t = |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
41 |
( ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(fst (snd t)))) |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
42 |
, sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(snd (snd t))) |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
43 |
, sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t))))" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
44 |
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
|
45 |
by (simp add: split_def) |
33591 | 46 |
|
47 |
text {* Individual type combinators are projected from the fixed point. *} |
|
48 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
49 |
definition foo_defl :: "TypeRep \<rightarrow> TypeRep" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
50 |
where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))" |
33591 | 51 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
52 |
definition bar_defl :: "TypeRep \<rightarrow> TypeRep" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
53 |
where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 54 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
55 |
definition baz_defl :: "TypeRep \<rightarrow> TypeRep" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
56 |
where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))" |
33591 | 57 |
|
58 |
text {* Unfold rules for each combinator. *} |
|
59 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
60 |
lemma foo_defl_unfold: |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
61 |
"foo_defl\<cdot>a = ssum_defl\<cdot>REP(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
62 |
unfolding foo_defl_def bar_defl_def baz_defl_def |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
63 |
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 64 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
65 |
lemma bar_defl_unfold: "bar_defl\<cdot>a = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
66 |
unfolding foo_defl_def bar_defl_def baz_defl_def |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
67 |
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 68 |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
69 |
lemma baz_defl_unfold: "baz_defl\<cdot>a = sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))" |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
70 |
unfolding foo_defl_def bar_defl_def baz_defl_def |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
71 |
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta) |
33591 | 72 |
|
73 |
text "The automation for the previous steps will be quite similar to |
|
74 |
how the fixrec package works." |
|
75 |
||
76 |
(********************************************************************) |
|
77 |
||
78 |
subsection {* Step 2: Define types, prove class instances *} |
|
79 |
||
80 |
text {* Use @{text pcpodef} with the appropriate type combinator. *} |
|
81 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
82 |
pcpodef (open) 'a foo = "{x. x ::: foo_defl\<cdot>REP('a)}" |
33591 | 83 |
by (simp_all add: adm_in_deflation) |
84 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
85 |
pcpodef (open) 'a bar = "{x. x ::: bar_defl\<cdot>REP('a)}" |
33591 | 86 |
by (simp_all add: adm_in_deflation) |
87 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
88 |
pcpodef (open) 'a baz = "{x. x ::: baz_defl\<cdot>REP('a)}" |
33591 | 89 |
by (simp_all add: adm_in_deflation) |
90 |
||
91 |
text {* Prove rep instance using lemma @{text typedef_rep_class}. *} |
|
92 |
||
93 |
instantiation foo :: (rep) rep |
|
94 |
begin |
|
95 |
||
96 |
definition emb_foo :: "'a foo \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
97 |
where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)" |
33591 | 98 |
|
99 |
definition prj_foo :: "udom \<rightarrow> 'a foo" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
100 |
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>REP('a))\<cdot>y))" |
33591 | 101 |
|
102 |
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
103 |
where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_defl\<cdot>REP('a))" |
33591 | 104 |
|
105 |
instance |
|
106 |
apply (rule typedef_rep_class) |
|
107 |
apply (rule type_definition_foo) |
|
108 |
apply (rule below_foo_def) |
|
109 |
apply (rule emb_foo_def) |
|
110 |
apply (rule prj_foo_def) |
|
111 |
apply (rule approx_foo_def) |
|
112 |
done |
|
113 |
||
114 |
end |
|
115 |
||
116 |
instantiation bar :: (rep) rep |
|
117 |
begin |
|
118 |
||
119 |
definition emb_bar :: "'a bar \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
120 |
where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)" |
33591 | 121 |
|
122 |
definition prj_bar :: "udom \<rightarrow> 'a bar" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
123 |
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>REP('a))\<cdot>y))" |
33591 | 124 |
|
125 |
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
126 |
where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_defl\<cdot>REP('a))" |
33591 | 127 |
|
128 |
instance |
|
129 |
apply (rule typedef_rep_class) |
|
130 |
apply (rule type_definition_bar) |
|
131 |
apply (rule below_bar_def) |
|
132 |
apply (rule emb_bar_def) |
|
133 |
apply (rule prj_bar_def) |
|
134 |
apply (rule approx_bar_def) |
|
135 |
done |
|
136 |
||
137 |
end |
|
138 |
||
139 |
instantiation baz :: (rep) rep |
|
140 |
begin |
|
141 |
||
142 |
definition emb_baz :: "'a baz \<rightarrow> udom" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
143 |
where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)" |
33591 | 144 |
|
145 |
definition prj_baz :: "udom \<rightarrow> 'a baz" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
146 |
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>REP('a))\<cdot>y))" |
33591 | 147 |
|
148 |
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
149 |
where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_defl\<cdot>REP('a))" |
33591 | 150 |
|
151 |
instance |
|
152 |
apply (rule typedef_rep_class) |
|
153 |
apply (rule type_definition_baz) |
|
154 |
apply (rule below_baz_def) |
|
155 |
apply (rule emb_baz_def) |
|
156 |
apply (rule prj_baz_def) |
|
157 |
apply (rule approx_baz_def) |
|
158 |
done |
|
159 |
||
160 |
end |
|
161 |
||
162 |
text {* Prove REP rules using lemma @{text typedef_REP}. *} |
|
163 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
164 |
lemma REP_foo: "REP('a foo) = foo_defl\<cdot>REP('a)" |
33591 | 165 |
apply (rule typedef_REP) |
166 |
apply (rule type_definition_foo) |
|
167 |
apply (rule below_foo_def) |
|
168 |
apply (rule emb_foo_def) |
|
169 |
apply (rule prj_foo_def) |
|
170 |
done |
|
171 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
172 |
lemma REP_bar: "REP('a bar) = bar_defl\<cdot>REP('a)" |
33591 | 173 |
apply (rule typedef_REP) |
174 |
apply (rule type_definition_bar) |
|
175 |
apply (rule below_bar_def) |
|
176 |
apply (rule emb_bar_def) |
|
177 |
apply (rule prj_bar_def) |
|
178 |
done |
|
179 |
||
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
180 |
lemma REP_baz: "REP('a baz) = baz_defl\<cdot>REP('a)" |
33591 | 181 |
apply (rule typedef_REP) |
182 |
apply (rule type_definition_baz) |
|
183 |
apply (rule below_baz_def) |
|
184 |
apply (rule emb_baz_def) |
|
185 |
apply (rule prj_baz_def) |
|
186 |
done |
|
187 |
||
188 |
text {* Prove REP equations using type combinator unfold lemmas. *} |
|
189 |
||
190 |
lemma REP_foo': "REP('a foo) = REP(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
|
191 |
unfolding REP_foo REP_bar REP_baz REP_simps |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
192 |
by (rule foo_defl_unfold) |
33591 | 193 |
|
194 |
lemma REP_bar': "REP('a bar) = REP('a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>)" |
|
195 |
unfolding REP_foo REP_bar REP_baz REP_simps |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
196 |
by (rule bar_defl_unfold) |
33591 | 197 |
|
198 |
lemma REP_baz': "REP('a baz) = REP('a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>)" |
|
199 |
unfolding REP_foo REP_bar REP_baz REP_simps |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
200 |
by (rule baz_defl_unfold) |
33591 | 201 |
|
202 |
(********************************************************************) |
|
203 |
||
204 |
subsection {* Step 3: Define rep and abs functions *} |
|
205 |
||
206 |
text {* Define them all using @{text coerce}! *} |
|
207 |
||
208 |
definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)" |
|
33779 | 209 |
where "foo_rep \<equiv> coerce" |
33591 | 210 |
|
211 |
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" |
|
33779 | 212 |
where "foo_abs \<equiv> coerce" |
33591 | 213 |
|
214 |
definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>" |
|
33779 | 215 |
where "bar_rep \<equiv> coerce" |
33591 | 216 |
|
217 |
definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar" |
|
33779 | 218 |
where "bar_abs \<equiv> coerce" |
33591 | 219 |
|
220 |
definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>" |
|
33779 | 221 |
where "baz_rep \<equiv> coerce" |
33591 | 222 |
|
223 |
definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz" |
|
33779 | 224 |
where "baz_abs \<equiv> coerce" |
225 |
||
226 |
text {* Prove isomorphism rules. *} |
|
227 |
||
228 |
lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x" |
|
229 |
by (rule domain_abs_iso [OF REP_foo' foo_abs_def foo_rep_def]) |
|
230 |
||
231 |
lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x" |
|
232 |
by (rule domain_rep_iso [OF REP_foo' foo_abs_def foo_rep_def]) |
|
233 |
||
234 |
lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x" |
|
235 |
by (rule domain_abs_iso [OF REP_bar' bar_abs_def bar_rep_def]) |
|
236 |
||
237 |
lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x" |
|
238 |
by (rule domain_rep_iso [OF REP_bar' bar_abs_def bar_rep_def]) |
|
239 |
||
240 |
lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x" |
|
241 |
by (rule domain_abs_iso [OF REP_baz' baz_abs_def baz_rep_def]) |
|
242 |
||
243 |
lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x" |
|
244 |
by (rule domain_rep_iso [OF REP_baz' baz_abs_def baz_rep_def]) |
|
33591 | 245 |
|
246 |
text {* Prove isodefl rules using @{text isodefl_coerce}. *} |
|
247 |
||
248 |
lemma isodefl_foo_abs: |
|
249 |
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" |
|
33779 | 250 |
by (rule isodefl_abs_rep [OF REP_foo' foo_abs_def foo_rep_def]) |
33591 | 251 |
|
252 |
lemma isodefl_bar_abs: |
|
253 |
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" |
|
33779 | 254 |
by (rule isodefl_abs_rep [OF REP_bar' bar_abs_def bar_rep_def]) |
33591 | 255 |
|
256 |
lemma isodefl_baz_abs: |
|
257 |
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" |
|
33779 | 258 |
by (rule isodefl_abs_rep [OF REP_baz' baz_abs_def baz_rep_def]) |
33591 | 259 |
|
260 |
(********************************************************************) |
|
261 |
||
262 |
subsection {* Step 4: Define map functions, prove isodefl property *} |
|
263 |
||
264 |
text {* Start with the one-step non-recursive version. *} |
|
265 |
||
266 |
text {* Note that the type of the map function depends on which |
|
267 |
variables are used in positive and negative positions. *} |
|
268 |
||
269 |
definition |
|
270 |
foo_bar_baz_mapF :: |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
271 |
"(_ \<rightarrow> _) |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
272 |
\<rightarrow> (_ foo \<rightarrow> _ foo) \<times> (_ bar \<rightarrow> _ bar) \<times> (_ baz \<rightarrow> _ baz) |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
273 |
\<rightarrow> (_ foo \<rightarrow> _ foo) \<times> (_ bar \<rightarrow> _ bar) \<times> (_ baz \<rightarrow> _ baz)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
274 |
(* |
33591 | 275 |
"('a \<rightarrow> 'b) |
276 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz) |
|
277 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)" |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
278 |
*) |
33591 | 279 |
where |
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
280 |
"foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3). |
33591 | 281 |
( |
282 |
foo_abs oo |
|
283 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) |
|
284 |
oo foo_rep |
|
285 |
, |
|
286 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep |
|
287 |
, |
|
288 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
289 |
)))" |
33591 | 290 |
|
291 |
lemma foo_bar_baz_mapF_beta: |
|
292 |
"foo_bar_baz_mapF\<cdot>f\<cdot>d = |
|
293 |
( |
|
294 |
foo_abs oo |
|
295 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) |
|
296 |
oo foo_rep |
|
297 |
, |
|
298 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep |
|
299 |
, |
|
300 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep |
|
301 |
)" |
|
302 |
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
|
303 |
by (simp add: split_def) |
33591 | 304 |
|
305 |
text {* Individual map functions are projected from the fixed point. *} |
|
306 |
||
307 |
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" |
|
308 |
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
309 |
||
310 |
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" |
|
311 |
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
312 |
||
313 |
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)" |
|
314 |
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
315 |
||
316 |
text {* Prove isodefl rules for all map functions simultaneously. *} |
|
317 |
||
318 |
lemma isodefl_foo_bar_baz: |
|
319 |
assumes isodefl_d: "isodefl d t" |
|
320 |
shows |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
321 |
"isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and> |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
322 |
isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and> |
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
323 |
isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)" |
33591 | 324 |
apply (simp add: foo_map_def bar_map_def baz_map_def) |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
325 |
apply (simp add: foo_defl_def bar_defl_def baz_defl_def) |
33591 | 326 |
apply (rule parallel_fix_ind |
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
327 |
[where F="foo_bar_baz_deflF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"]) |
33591 | 328 |
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) |
329 |
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) |
|
330 |
apply (simp only: foo_bar_baz_mapF_beta |
|
33784
7e434813752f
change naming convention for deflation combinators
huffman
parents:
33781
diff
changeset
|
331 |
foo_bar_baz_deflF_beta |
33591 | 332 |
fst_conv snd_conv) |
333 |
apply (elim conjE) |
|
334 |
apply (intro |
|
335 |
conjI |
|
336 |
isodefl_foo_abs |
|
337 |
isodefl_bar_abs |
|
338 |
isodefl_baz_abs |
|
33779 | 339 |
isodefl_ssum isodefl_sprod isodefl_ID_REP isodefl_u isodefl_convex |
33591 | 340 |
isodefl_d |
341 |
) |
|
342 |
apply assumption+ |
|
343 |
done |
|
344 |
||
345 |
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] |
|
346 |
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] |
|
347 |
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] |
|
348 |
||
349 |
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} |
|
350 |
||
351 |
lemma foo_map_ID: "foo_map\<cdot>ID = ID" |
|
352 |
apply (rule isodefl_REP_imp_ID) |
|
353 |
apply (subst REP_foo) |
|
354 |
apply (rule isodefl_foo) |
|
355 |
apply (rule isodefl_ID_REP) |
|
356 |
done |
|
357 |
||
358 |
lemma bar_map_ID: "bar_map\<cdot>ID = ID" |
|
359 |
apply (rule isodefl_REP_imp_ID) |
|
360 |
apply (subst REP_bar) |
|
361 |
apply (rule isodefl_bar) |
|
362 |
apply (rule isodefl_ID_REP) |
|
363 |
done |
|
364 |
||
365 |
lemma baz_map_ID: "baz_map\<cdot>ID = ID" |
|
366 |
apply (rule isodefl_REP_imp_ID) |
|
367 |
apply (subst REP_baz) |
|
368 |
apply (rule isodefl_baz) |
|
369 |
apply (rule isodefl_ID_REP) |
|
370 |
done |
|
371 |
||
372 |
(********************************************************************) |
|
373 |
||
374 |
subsection {* Step 5: Define copy functions, prove reach lemmas *} |
|
375 |
||
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
376 |
text {* Define copy functions just like the old domain package does. *} |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
377 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
378 |
definition |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
379 |
foo_copy :: |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
380 |
"('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
|
381 |
'a foo \<rightarrow> 'a foo" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
382 |
where |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
383 |
"foo_copy = Abs_CFun (\<lambda>(d1, d2, d3). foo_abs oo |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
384 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d2)) |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
385 |
oo foo_rep)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
386 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
387 |
definition |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
388 |
bar_copy :: |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
389 |
"('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
|
390 |
'a bar \<rightarrow> 'a bar" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
391 |
where |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
392 |
"bar_copy = Abs_CFun (\<lambda>(d1, d2, d3). bar_abs oo |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
393 |
sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>d3) oo bar_rep)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
394 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
395 |
definition |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
396 |
baz_copy :: |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
397 |
"('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
|
398 |
'a baz \<rightarrow> 'a baz" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
399 |
where |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
400 |
"baz_copy = Abs_CFun (\<lambda>(d1, d2, d3). baz_abs oo |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
401 |
sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep)" |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
402 |
|
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
403 |
definition |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
404 |
foo_bar_baz_copy :: |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
405 |
"('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
|
406 |
('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
|
407 |
where |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
408 |
"foo_bar_baz_copy = (\<Lambda> f. (foo_copy\<cdot>f, bar_copy\<cdot>f, baz_copy\<cdot>f))" |
33591 | 409 |
|
410 |
lemma fix_foo_bar_baz_copy: |
|
411 |
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)" |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
412 |
unfolding foo_map_def bar_map_def baz_map_def |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
413 |
apply (subst beta_cfun, simp)+ |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
414 |
apply (subst pair_collapse)+ |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
415 |
apply (rule cfun_arg_cong) |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
416 |
unfolding foo_bar_baz_copy_def |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
417 |
unfolding foo_copy_def bar_copy_def baz_copy_def |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
418 |
unfolding foo_bar_baz_mapF_def |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
419 |
unfolding split_def |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
420 |
apply (subst beta_cfun, simp)+ |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
421 |
apply (rule refl) |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
422 |
done |
33591 | 423 |
|
424 |
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x" |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
425 |
unfolding fix_foo_bar_baz_copy fst_conv snd_conv |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
426 |
unfolding foo_map_ID by (rule ID1) |
33591 | 427 |
|
428 |
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
429 |
unfolding fix_foo_bar_baz_copy fst_conv snd_conv |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
430 |
unfolding bar_map_ID by (rule ID1) |
33591 | 431 |
|
432 |
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
33781
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
433 |
unfolding fix_foo_bar_baz_copy fst_conv snd_conv |
c7d32e726bb9
avoid using csplit; define copy functions exactly like the current domain package
huffman
parents:
33779
diff
changeset
|
434 |
unfolding baz_map_ID by (rule ID1) |
33591 | 435 |
|
436 |
end |