author | huffman |
Wed, 18 Nov 2009 16:57:58 -0800 | |
changeset 33779 | b8efeea2cebd |
parent 33679 | 331712879666 |
child 33781 | c7d32e726bb9 |
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 |
|
31 |
foo_bar_baz_typF :: |
|
32 |
"TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep \<rightarrow> TypeRep \<times> TypeRep \<times> TypeRep" |
|
33 |
where |
|
34 |
"foo_bar_baz_typF = (\<Lambda> a (t1, t2, t3). |
|
33779 | 35 |
( ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2)) |
33591 | 36 |
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t3) |
37 |
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>t1))))" |
|
38 |
||
39 |
lemma foo_bar_baz_typF_beta: |
|
40 |
"foo_bar_baz_typF\<cdot>a\<cdot>t = |
|
33779 | 41 |
( ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t)))) |
33591 | 42 |
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(snd (snd t))) |
43 |
, sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(fst t))))" |
|
44 |
unfolding foo_bar_baz_typF_def |
|
45 |
by (simp add: csplit_def cfst_def csnd_def) |
|
46 |
||
47 |
text {* Individual type combinators are projected from the fixed point. *} |
|
48 |
||
49 |
definition foo_typ :: "TypeRep \<rightarrow> TypeRep" |
|
50 |
where "foo_typ = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_typF\<cdot>a)))" |
|
51 |
||
52 |
definition bar_typ :: "TypeRep \<rightarrow> TypeRep" |
|
53 |
where "bar_typ = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))" |
|
54 |
||
55 |
definition baz_typ :: "TypeRep \<rightarrow> TypeRep" |
|
56 |
where "baz_typ = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_typF\<cdot>a))))" |
|
57 |
||
58 |
text {* Unfold rules for each combinator. *} |
|
59 |
||
60 |
lemma foo_typ_unfold: |
|
33779 | 61 |
"foo_typ\<cdot>a = ssum_typ\<cdot>REP(one)\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))" |
33591 | 62 |
unfolding foo_typ_def bar_typ_def baz_typ_def |
63 |
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) |
|
64 |
||
65 |
lemma bar_typ_unfold: "bar_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(baz_typ\<cdot>a))" |
|
66 |
unfolding foo_typ_def bar_typ_def baz_typ_def |
|
67 |
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) |
|
68 |
||
69 |
lemma baz_typ_unfold: "baz_typ\<cdot>a = sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(convex_typ\<cdot>(foo_typ\<cdot>a)))" |
|
70 |
unfolding foo_typ_def bar_typ_def baz_typ_def |
|
71 |
by (subst fix_eq, simp add: foo_bar_baz_typF_beta) |
|
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 |
||
82 |
pcpodef (open) 'a foo = "{x. x ::: foo_typ\<cdot>REP('a)}" |
|
83 |
by (simp_all add: adm_in_deflation) |
|
84 |
||
85 |
pcpodef (open) 'a bar = "{x. x ::: bar_typ\<cdot>REP('a)}" |
|
86 |
by (simp_all add: adm_in_deflation) |
|
87 |
||
88 |
pcpodef (open) 'a baz = "{x. x ::: baz_typ\<cdot>REP('a)}" |
|
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" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
100 |
where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_typ\<cdot>REP('a))\<cdot>y))" |
33591 | 101 |
|
102 |
definition approx_foo :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
103 |
where "approx_foo \<equiv> repdef_approx Rep_foo Abs_foo (foo_typ\<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" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
123 |
where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_typ\<cdot>REP('a))\<cdot>y))" |
33591 | 124 |
|
125 |
definition approx_bar :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
126 |
where "approx_bar \<equiv> repdef_approx Rep_bar Abs_bar (bar_typ\<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" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
146 |
where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_typ\<cdot>REP('a))\<cdot>y))" |
33591 | 147 |
|
148 |
definition approx_baz :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz" |
|
33679
331712879666
automate definition of representable domains from algebraic deflations
huffman
parents:
33591
diff
changeset
|
149 |
where "approx_baz \<equiv> repdef_approx Rep_baz Abs_baz (baz_typ\<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 |
||
164 |
lemma REP_foo: "REP('a foo) = foo_typ\<cdot>REP('a)" |
|
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 |
||
172 |
lemma REP_bar: "REP('a bar) = bar_typ\<cdot>REP('a)" |
|
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 |
||
180 |
lemma REP_baz: "REP('a baz) = baz_typ\<cdot>REP('a)" |
|
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 |
|
192 |
by (rule foo_typ_unfold) |
|
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 |
|
196 |
by (rule bar_typ_unfold) |
|
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 |
|
200 |
by (rule baz_typ_unfold) |
|
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 :: |
|
271 |
"('a \<rightarrow> 'b) |
|
272 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz) |
|
273 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)" |
|
274 |
where |
|
275 |
"foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3). |
|
276 |
( |
|
277 |
foo_abs oo |
|
278 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) |
|
279 |
oo foo_rep |
|
280 |
, |
|
281 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep |
|
282 |
, |
|
283 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep |
|
284 |
))" |
|
285 |
||
286 |
lemma foo_bar_baz_mapF_beta: |
|
287 |
"foo_bar_baz_mapF\<cdot>f\<cdot>d = |
|
288 |
( |
|
289 |
foo_abs oo |
|
290 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) |
|
291 |
oo foo_rep |
|
292 |
, |
|
293 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep |
|
294 |
, |
|
295 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep |
|
296 |
)" |
|
297 |
unfolding foo_bar_baz_mapF_def |
|
298 |
by (simp add: csplit_def cfst_def csnd_def) |
|
299 |
||
300 |
text {* Individual map functions are projected from the fixed point. *} |
|
301 |
||
302 |
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" |
|
303 |
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
304 |
||
305 |
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" |
|
306 |
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
307 |
||
308 |
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)" |
|
309 |
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
310 |
||
311 |
text {* Prove isodefl rules for all map functions simultaneously. *} |
|
312 |
||
313 |
lemma isodefl_foo_bar_baz: |
|
314 |
assumes isodefl_d: "isodefl d t" |
|
315 |
shows |
|
316 |
"isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and> |
|
317 |
isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and> |
|
318 |
isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)" |
|
319 |
apply (simp add: foo_map_def bar_map_def baz_map_def) |
|
320 |
apply (simp add: foo_typ_def bar_typ_def baz_typ_def) |
|
321 |
apply (rule parallel_fix_ind |
|
322 |
[where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"]) |
|
323 |
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) |
|
324 |
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) |
|
325 |
apply (simp only: foo_bar_baz_mapF_beta |
|
326 |
foo_bar_baz_typF_beta |
|
327 |
fst_conv snd_conv) |
|
328 |
apply (elim conjE) |
|
329 |
apply (intro |
|
330 |
conjI |
|
331 |
isodefl_foo_abs |
|
332 |
isodefl_bar_abs |
|
333 |
isodefl_baz_abs |
|
33779 | 334 |
isodefl_ssum isodefl_sprod isodefl_ID_REP isodefl_u isodefl_convex |
33591 | 335 |
isodefl_d |
336 |
) |
|
337 |
apply assumption+ |
|
338 |
done |
|
339 |
||
340 |
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] |
|
341 |
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] |
|
342 |
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] |
|
343 |
||
344 |
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} |
|
345 |
||
346 |
lemma foo_map_ID: "foo_map\<cdot>ID = ID" |
|
347 |
apply (rule isodefl_REP_imp_ID) |
|
348 |
apply (subst REP_foo) |
|
349 |
apply (rule isodefl_foo) |
|
350 |
apply (rule isodefl_ID_REP) |
|
351 |
done |
|
352 |
||
353 |
lemma bar_map_ID: "bar_map\<cdot>ID = ID" |
|
354 |
apply (rule isodefl_REP_imp_ID) |
|
355 |
apply (subst REP_bar) |
|
356 |
apply (rule isodefl_bar) |
|
357 |
apply (rule isodefl_ID_REP) |
|
358 |
done |
|
359 |
||
360 |
lemma baz_map_ID: "baz_map\<cdot>ID = ID" |
|
361 |
apply (rule isodefl_REP_imp_ID) |
|
362 |
apply (subst REP_baz) |
|
363 |
apply (rule isodefl_baz) |
|
364 |
apply (rule isodefl_ID_REP) |
|
365 |
done |
|
366 |
||
367 |
(********************************************************************) |
|
368 |
||
369 |
subsection {* Step 5: Define copy functions, prove reach lemmas *} |
|
370 |
||
371 |
definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID" |
|
372 |
definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))" |
|
373 |
definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))" |
|
374 |
definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))" |
|
375 |
||
376 |
lemma fix_foo_bar_baz_copy: |
|
377 |
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)" |
|
378 |
unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def |
|
379 |
by simp |
|
380 |
||
381 |
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x" |
|
382 |
unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID) |
|
383 |
||
384 |
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
385 |
unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID) |
|
386 |
||
387 |
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
388 |
unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID) |
|
389 |
||
390 |
end |