author | huffman |
Fri, 13 Nov 2009 15:31:20 -0800 | |
changeset 33679 | 331712879666 |
parent 33591 | 51091e1041a7 |
child 33779 | b8efeea2cebd |
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). |
|
35 |
( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>t2)) |
|
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 = |
|
41 |
( ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(fst (snd t)))) |
|
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: |
|
61 |
"foo_typ\<cdot>a = ssum_typ\<cdot>one_typ\<cdot>(sprod_typ\<cdot>(u_typ\<cdot>a)\<cdot>(u_typ\<cdot>(bar_typ\<cdot>a)))" |
|
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>)" |
|
209 |
where "foo_rep = coerce" |
|
210 |
||
211 |
definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo" |
|
212 |
where "foo_abs = coerce" |
|
213 |
||
214 |
definition bar_rep :: "'a bar \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom>" |
|
215 |
where "bar_rep = coerce" |
|
216 |
||
217 |
definition bar_abs :: "'a\<^sub>\<bottom> \<otimes> ('a baz)\<^sub>\<bottom> \<rightarrow> 'a bar" |
|
218 |
where "bar_abs = coerce" |
|
219 |
||
220 |
definition baz_rep :: "'a baz \<rightarrow> 'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom>" |
|
221 |
where "baz_rep = coerce" |
|
222 |
||
223 |
definition baz_abs :: "'a\<^sub>\<bottom> \<otimes> ('a foo convex_pd)\<^sub>\<bottom> \<rightarrow> 'a baz" |
|
224 |
where "baz_abs = coerce" |
|
225 |
||
226 |
text {* Prove isodefl rules using @{text isodefl_coerce}. *} |
|
227 |
||
228 |
lemma isodefl_foo_abs: |
|
229 |
"isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t" |
|
230 |
unfolding foo_abs_def foo_rep_def |
|
231 |
by (rule isodefl_coerce [OF REP_foo']) |
|
232 |
||
233 |
lemma isodefl_bar_abs: |
|
234 |
"isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t" |
|
235 |
unfolding bar_abs_def bar_rep_def |
|
236 |
by (rule isodefl_coerce [OF REP_bar']) |
|
237 |
||
238 |
lemma isodefl_baz_abs: |
|
239 |
"isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t" |
|
240 |
unfolding baz_abs_def baz_rep_def |
|
241 |
by (rule isodefl_coerce [OF REP_baz']) |
|
242 |
||
243 |
text {* TODO: prove iso predicate for rep and abs. *} |
|
244 |
||
245 |
(********************************************************************) |
|
246 |
||
247 |
subsection {* Step 4: Define map functions, prove isodefl property *} |
|
248 |
||
249 |
text {* Start with the one-step non-recursive version. *} |
|
250 |
||
251 |
text {* Note that the type of the map function depends on which |
|
252 |
variables are used in positive and negative positions. *} |
|
253 |
||
254 |
definition |
|
255 |
foo_bar_baz_mapF :: |
|
256 |
"('a \<rightarrow> 'b) |
|
257 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz) |
|
258 |
\<rightarrow> ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('a baz \<rightarrow> 'b baz)" |
|
259 |
where |
|
260 |
"foo_bar_baz_mapF = (\<Lambda> f (d1, d2, d3). |
|
261 |
( |
|
262 |
foo_abs oo |
|
263 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2)) |
|
264 |
oo foo_rep |
|
265 |
, |
|
266 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d3) oo bar_rep |
|
267 |
, |
|
268 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>d1)) oo baz_rep |
|
269 |
))" |
|
270 |
||
271 |
lemma foo_bar_baz_mapF_beta: |
|
272 |
"foo_bar_baz_mapF\<cdot>f\<cdot>d = |
|
273 |
( |
|
274 |
foo_abs oo |
|
275 |
ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d)))) |
|
276 |
oo foo_rep |
|
277 |
, |
|
278 |
bar_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(snd (snd d))) oo bar_rep |
|
279 |
, |
|
280 |
baz_abs oo sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(convex_map\<cdot>(fst d))) oo baz_rep |
|
281 |
)" |
|
282 |
unfolding foo_bar_baz_mapF_def |
|
283 |
by (simp add: csplit_def cfst_def csnd_def) |
|
284 |
||
285 |
text {* Individual map functions are projected from the fixed point. *} |
|
286 |
||
287 |
definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)" |
|
288 |
where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))" |
|
289 |
||
290 |
definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)" |
|
291 |
where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
292 |
||
293 |
definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a baz \<rightarrow> 'b baz)" |
|
294 |
where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))" |
|
295 |
||
296 |
text {* Prove isodefl rules for all map functions simultaneously. *} |
|
297 |
||
298 |
lemma isodefl_foo_bar_baz: |
|
299 |
assumes isodefl_d: "isodefl d t" |
|
300 |
shows |
|
301 |
"isodefl (foo_map\<cdot>d) (foo_typ\<cdot>t) \<and> |
|
302 |
isodefl (bar_map\<cdot>d) (bar_typ\<cdot>t) \<and> |
|
303 |
isodefl (baz_map\<cdot>d) (baz_typ\<cdot>t)" |
|
304 |
apply (simp add: foo_map_def bar_map_def baz_map_def) |
|
305 |
apply (simp add: foo_typ_def bar_typ_def baz_typ_def) |
|
306 |
apply (rule parallel_fix_ind |
|
307 |
[where F="foo_bar_baz_typF\<cdot>t" and G="foo_bar_baz_mapF\<cdot>d"]) |
|
308 |
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id) |
|
309 |
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms) |
|
310 |
apply (simp only: foo_bar_baz_mapF_beta |
|
311 |
foo_bar_baz_typF_beta |
|
312 |
fst_conv snd_conv) |
|
313 |
apply (elim conjE) |
|
314 |
apply (intro |
|
315 |
conjI |
|
316 |
isodefl_foo_abs |
|
317 |
isodefl_bar_abs |
|
318 |
isodefl_baz_abs |
|
319 |
isodefl_ssum isodefl_sprod isodefl_one isodefl_u isodefl_convex |
|
320 |
isodefl_d |
|
321 |
) |
|
322 |
apply assumption+ |
|
323 |
done |
|
324 |
||
325 |
lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1] |
|
326 |
lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1] |
|
327 |
lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2] |
|
328 |
||
329 |
text {* Prove map ID lemmas, using isodefl_REP_imp_ID *} |
|
330 |
||
331 |
lemma foo_map_ID: "foo_map\<cdot>ID = ID" |
|
332 |
apply (rule isodefl_REP_imp_ID) |
|
333 |
apply (subst REP_foo) |
|
334 |
apply (rule isodefl_foo) |
|
335 |
apply (rule isodefl_ID_REP) |
|
336 |
done |
|
337 |
||
338 |
lemma bar_map_ID: "bar_map\<cdot>ID = ID" |
|
339 |
apply (rule isodefl_REP_imp_ID) |
|
340 |
apply (subst REP_bar) |
|
341 |
apply (rule isodefl_bar) |
|
342 |
apply (rule isodefl_ID_REP) |
|
343 |
done |
|
344 |
||
345 |
lemma baz_map_ID: "baz_map\<cdot>ID = ID" |
|
346 |
apply (rule isodefl_REP_imp_ID) |
|
347 |
apply (subst REP_baz) |
|
348 |
apply (rule isodefl_baz) |
|
349 |
apply (rule isodefl_ID_REP) |
|
350 |
done |
|
351 |
||
352 |
(********************************************************************) |
|
353 |
||
354 |
subsection {* Step 5: Define copy functions, prove reach lemmas *} |
|
355 |
||
356 |
definition "foo_bar_baz_copy = foo_bar_baz_mapF\<cdot>ID" |
|
357 |
definition "foo_copy = (\<Lambda> f. fst (foo_bar_baz_copy\<cdot>f))" |
|
358 |
definition "bar_copy = (\<Lambda> f. fst (snd (foo_bar_baz_copy\<cdot>f)))" |
|
359 |
definition "baz_copy = (\<Lambda> f. snd (snd (foo_bar_baz_copy\<cdot>f)))" |
|
360 |
||
361 |
lemma fix_foo_bar_baz_copy: |
|
362 |
"fix\<cdot>foo_bar_baz_copy = (foo_map\<cdot>ID, bar_map\<cdot>ID, baz_map\<cdot>ID)" |
|
363 |
unfolding foo_bar_baz_copy_def foo_map_def bar_map_def baz_map_def |
|
364 |
by simp |
|
365 |
||
366 |
lemma foo_reach: "fst (fix\<cdot>foo_bar_baz_copy)\<cdot>x = x" |
|
367 |
unfolding fix_foo_bar_baz_copy by (simp add: foo_map_ID) |
|
368 |
||
369 |
lemma bar_reach: "fst (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
370 |
unfolding fix_foo_bar_baz_copy by (simp add: bar_map_ID) |
|
371 |
||
372 |
lemma baz_reach: "snd (snd (fix\<cdot>foo_bar_baz_copy))\<cdot>x = x" |
|
373 |
unfolding fix_foo_bar_baz_copy by (simp add: baz_map_ID) |
|
374 |
||
375 |
end |