|
1 (* Title: HOLCF/dnat.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for dnat.thy |
|
7 *) |
|
8 |
|
9 open Dnat; |
|
10 |
|
11 (* ------------------------------------------------------------------------*) |
|
12 (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict *) |
|
13 (* ------------------------------------------------------------------------*) |
|
14 |
|
15 val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS |
|
16 (allI RSN (2,allI RS iso_strict))); |
|
17 |
|
18 val dnat_rews = [dnat_iso_strict RS conjunct1, |
|
19 dnat_iso_strict RS conjunct2]; |
|
20 |
|
21 (* ------------------------------------------------------------------------*) |
|
22 (* Properties of dnat_copy *) |
|
23 (* ------------------------------------------------------------------------*) |
|
24 |
|
25 fun prover defs thm = prove_goalw Dnat.thy defs thm |
|
26 (fn prems => |
|
27 [ |
|
28 (cut_facts_tac prems 1), |
|
29 (asm_simp_tac (HOLCF_ss addsimps |
|
30 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
|
31 ]); |
|
32 |
|
33 val dnat_copy = |
|
34 [ |
|
35 prover [dnat_copy_def] "dnat_copy[f][UU]=UU", |
|
36 prover [dnat_copy_def,dzero_def] "dnat_copy[f][dzero]= dzero", |
|
37 prover [dnat_copy_def,dsucc_def] |
|
38 "n~=UU ==> dnat_copy[f][dsucc[n]] = dsucc[f[n]]" |
|
39 ]; |
|
40 |
|
41 val dnat_rews = dnat_copy @ dnat_rews; |
|
42 |
|
43 (* ------------------------------------------------------------------------*) |
|
44 (* Exhaustion and elimination for dnat *) |
|
45 (* ------------------------------------------------------------------------*) |
|
46 |
|
47 val Exh_dnat = prove_goalw Dnat.thy [dsucc_def,dzero_def] |
|
48 "n = UU | n = dzero | (? x . x~=UU & n = dsucc[x])" |
|
49 (fn prems => |
|
50 [ |
|
51 (simp_tac HOLCF_ss 1), |
|
52 (rtac (dnat_rep_iso RS subst) 1), |
|
53 (res_inst_tac [("p","dnat_rep[n]")] ssumE 1), |
|
54 (rtac disjI1 1), |
|
55 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
56 (rtac (disjI1 RS disjI2) 1), |
|
57 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
58 (res_inst_tac [("p","x")] oneE 1), |
|
59 (contr_tac 1), |
|
60 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
61 (rtac (disjI2 RS disjI2) 1), |
|
62 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
63 (fast_tac HOL_cs 1) |
|
64 ]); |
|
65 |
|
66 val dnatE = prove_goal Dnat.thy |
|
67 "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc[x];x~=UU|]==>Q|]==>Q" |
|
68 (fn prems => |
|
69 [ |
|
70 (rtac (Exh_dnat RS disjE) 1), |
|
71 (eresolve_tac prems 1), |
|
72 (etac disjE 1), |
|
73 (eresolve_tac prems 1), |
|
74 (REPEAT (etac exE 1)), |
|
75 (resolve_tac prems 1), |
|
76 (fast_tac HOL_cs 1), |
|
77 (fast_tac HOL_cs 1) |
|
78 ]); |
|
79 |
|
80 (* ------------------------------------------------------------------------*) |
|
81 (* Properties of dnat_when *) |
|
82 (* ------------------------------------------------------------------------*) |
|
83 |
|
84 fun prover defs thm = prove_goalw Dnat.thy defs thm |
|
85 (fn prems => |
|
86 [ |
|
87 (cut_facts_tac prems 1), |
|
88 (asm_simp_tac (HOLCF_ss addsimps |
|
89 (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1) |
|
90 ]); |
|
91 |
|
92 |
|
93 val dnat_when = [ |
|
94 prover [dnat_when_def] "dnat_when[c][f][UU]=UU", |
|
95 prover [dnat_when_def,dzero_def] "dnat_when[c][f][dzero]=c", |
|
96 prover [dnat_when_def,dsucc_def] |
|
97 "n~=UU ==> dnat_when[c][f][dsucc[n]]=f[n]" |
|
98 ]; |
|
99 |
|
100 val dnat_rews = dnat_when @ dnat_rews; |
|
101 |
|
102 (* ------------------------------------------------------------------------*) |
|
103 (* Rewrites for discriminators and selectors *) |
|
104 (* ------------------------------------------------------------------------*) |
|
105 |
|
106 fun prover defs thm = prove_goalw Dnat.thy defs thm |
|
107 (fn prems => |
|
108 [ |
|
109 (simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
110 ]); |
|
111 |
|
112 val dnat_discsel = [ |
|
113 prover [is_dzero_def] "is_dzero[UU]=UU", |
|
114 prover [is_dsucc_def] "is_dsucc[UU]=UU", |
|
115 prover [dpred_def] "dpred[UU]=UU" |
|
116 ]; |
|
117 |
|
118 |
|
119 fun prover defs thm = prove_goalw Dnat.thy defs thm |
|
120 (fn prems => |
|
121 [ |
|
122 (cut_facts_tac prems 1), |
|
123 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
124 ]); |
|
125 |
|
126 val dnat_discsel = [ |
|
127 prover [is_dzero_def] "is_dzero[dzero]=TT", |
|
128 prover [is_dzero_def] "n~=UU ==>is_dzero[dsucc[n]]=FF", |
|
129 prover [is_dsucc_def] "is_dsucc[dzero]=FF", |
|
130 prover [is_dsucc_def] "n~=UU ==> is_dsucc[dsucc[n]]=TT", |
|
131 prover [dpred_def] "dpred[dzero]=UU", |
|
132 prover [dpred_def] "n~=UU ==> dpred[dsucc[n]]=n" |
|
133 ] @ dnat_discsel; |
|
134 |
|
135 val dnat_rews = dnat_discsel @ dnat_rews; |
|
136 |
|
137 (* ------------------------------------------------------------------------*) |
|
138 (* Definedness and strictness *) |
|
139 (* ------------------------------------------------------------------------*) |
|
140 |
|
141 fun prover contr thm = prove_goal Dnat.thy thm |
|
142 (fn prems => |
|
143 [ |
|
144 (res_inst_tac [("P1",contr)] classical3 1), |
|
145 (simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
146 (dtac sym 1), |
|
147 (asm_simp_tac HOLCF_ss 1), |
|
148 (simp_tac (HOLCF_ss addsimps (prems @ dnat_rews)) 1) |
|
149 ]); |
|
150 |
|
151 val dnat_constrdef = [ |
|
152 prover "is_dzero[UU] ~= UU" "dzero~=UU", |
|
153 prover "is_dsucc[UU] ~= UU" "n~=UU ==> dsucc[n]~=UU" |
|
154 ]; |
|
155 |
|
156 |
|
157 fun prover defs thm = prove_goalw Dnat.thy defs thm |
|
158 (fn prems => |
|
159 [ |
|
160 (simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
161 ]); |
|
162 |
|
163 val dnat_constrdef = [ |
|
164 prover [dsucc_def] "dsucc[UU]=UU" |
|
165 ] @ dnat_constrdef; |
|
166 |
|
167 val dnat_rews = dnat_constrdef @ dnat_rews; |
|
168 |
|
169 |
|
170 (* ------------------------------------------------------------------------*) |
|
171 (* Distinctness wrt. << and = *) |
|
172 (* ------------------------------------------------------------------------*) |
|
173 |
|
174 fun prover contrfun thm = prove_goal Dnat.thy thm |
|
175 (fn prems => |
|
176 [ |
|
177 (cut_facts_tac prems 1), |
|
178 (res_inst_tac [("P1","TT << FF")] classical3 1), |
|
179 (resolve_tac dist_less_tr 1), |
|
180 (dres_inst_tac [("fo5",contrfun)] monofun_cfun_arg 1), |
|
181 (etac box_less 1), |
|
182 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
183 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
184 ]); |
|
185 |
|
186 val dnat_dist_less = |
|
187 [ |
|
188 prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]", |
|
189 prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero" |
|
190 ]; |
|
191 |
|
192 fun prover contrfun thm = prove_goal Dnat.thy thm |
|
193 (fn prems => |
|
194 [ |
|
195 (cut_facts_tac prems 1), |
|
196 (res_inst_tac [("P1","TT = FF")] classical3 1), |
|
197 (resolve_tac dist_eq_tr 1), |
|
198 (dres_inst_tac [("f",contrfun)] cfun_arg_cong 1), |
|
199 (etac box_equals 1), |
|
200 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
201 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
202 ]); |
|
203 |
|
204 val dnat_dist_eq = |
|
205 [ |
|
206 prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]", |
|
207 prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero" |
|
208 ]; |
|
209 |
|
210 val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews; |
|
211 |
|
212 (* ------------------------------------------------------------------------*) |
|
213 (* Invertibility *) |
|
214 (* ------------------------------------------------------------------------*) |
|
215 |
|
216 val dnat_invert = |
|
217 [ |
|
218 prove_goal Dnat.thy |
|
219 "[|x1~=UU; y1~=UU; dsucc[x1] << dsucc[y1] |] ==> x1<< y1" |
|
220 (fn prems => |
|
221 [ |
|
222 (cut_facts_tac prems 1), |
|
223 (dres_inst_tac [("fo5","dnat_when[c][LAM x.x]")] monofun_cfun_arg 1), |
|
224 (etac box_less 1), |
|
225 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
226 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
227 ]) |
|
228 ]; |
|
229 |
|
230 (* ------------------------------------------------------------------------*) |
|
231 (* Injectivity *) |
|
232 (* ------------------------------------------------------------------------*) |
|
233 |
|
234 val dnat_inject = |
|
235 [ |
|
236 prove_goal Dnat.thy |
|
237 "[|x1~=UU; y1~=UU; dsucc[x1] = dsucc[y1] |] ==> x1= y1" |
|
238 (fn prems => |
|
239 [ |
|
240 (cut_facts_tac prems 1), |
|
241 (dres_inst_tac [("f","dnat_when[c][LAM x.x]")] cfun_arg_cong 1), |
|
242 (etac box_equals 1), |
|
243 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
244 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
245 ]) |
|
246 ]; |
|
247 |
|
248 (* ------------------------------------------------------------------------*) |
|
249 (* definedness for discriminators and selectors *) |
|
250 (* ------------------------------------------------------------------------*) |
|
251 |
|
252 |
|
253 fun prover thm = prove_goal Dnat.thy thm |
|
254 (fn prems => |
|
255 [ |
|
256 (cut_facts_tac prems 1), |
|
257 (rtac dnatE 1), |
|
258 (contr_tac 1), |
|
259 (REPEAT (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)) |
|
260 ]); |
|
261 |
|
262 val dnat_discsel_def = |
|
263 [ |
|
264 prover "n~=UU ==> is_dzero[n]~=UU", |
|
265 prover "n~=UU ==> is_dsucc[n]~=UU" |
|
266 ]; |
|
267 |
|
268 val dnat_rews = dnat_discsel_def @ dnat_rews; |
|
269 |
|
270 |
|
271 (* ------------------------------------------------------------------------*) |
|
272 (* Properties dnat_take *) |
|
273 (* ------------------------------------------------------------------------*) |
|
274 |
|
275 val dnat_take = |
|
276 [ |
|
277 prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU" |
|
278 (fn prems => |
|
279 [ |
|
280 (res_inst_tac [("n","n")] natE 1), |
|
281 (asm_simp_tac iterate_ss 1), |
|
282 (asm_simp_tac iterate_ss 1), |
|
283 (simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
284 ]), |
|
285 prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU" |
|
286 (fn prems => |
|
287 [ |
|
288 (asm_simp_tac iterate_ss 1) |
|
289 ])]; |
|
290 |
|
291 fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm |
|
292 (fn prems => |
|
293 [ |
|
294 (cut_facts_tac prems 1), |
|
295 (simp_tac iterate_ss 1), |
|
296 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1) |
|
297 ]); |
|
298 |
|
299 val dnat_take = [ |
|
300 prover "dnat_take(Suc(n))[dzero]=dzero", |
|
301 prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]" |
|
302 ] @ dnat_take; |
|
303 |
|
304 |
|
305 val dnat_rews = dnat_take @ dnat_rews; |
|
306 |
|
307 (* ------------------------------------------------------------------------*) |
|
308 (* take lemma for dnats *) |
|
309 (* ------------------------------------------------------------------------*) |
|
310 |
|
311 fun prover reach defs thm = prove_goalw Dnat.thy defs thm |
|
312 (fn prems => |
|
313 [ |
|
314 (res_inst_tac [("t","s1")] (reach RS subst) 1), |
|
315 (res_inst_tac [("t","s2")] (reach RS subst) 1), |
|
316 (rtac (fix_def2 RS ssubst) 1), |
|
317 (rtac (contlub_cfun_fun RS ssubst) 1), |
|
318 (rtac is_chain_iterate 1), |
|
319 (rtac (contlub_cfun_fun RS ssubst) 1), |
|
320 (rtac is_chain_iterate 1), |
|
321 (rtac lub_equal 1), |
|
322 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
|
323 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
|
324 (rtac allI 1), |
|
325 (resolve_tac prems 1) |
|
326 ]); |
|
327 |
|
328 val dnat_take_lemma = prover dnat_reach [dnat_take_def] |
|
329 "(!!n.dnat_take(n)[s1]=dnat_take(n)[s2]) ==> s1=s2"; |
|
330 |
|
331 |
|
332 (* ------------------------------------------------------------------------*) |
|
333 (* Co -induction for dnats *) |
|
334 (* ------------------------------------------------------------------------*) |
|
335 |
|
336 val dnat_coind_lemma = prove_goalw Dnat.thy [dnat_bisim_def] |
|
337 "dnat_bisim(R) ==> ! p q.R(p,q) --> dnat_take(n)[p]=dnat_take(n)[q]" |
|
338 (fn prems => |
|
339 [ |
|
340 (cut_facts_tac prems 1), |
|
341 (nat_ind_tac "n" 1), |
|
342 (simp_tac (HOLCF_ss addsimps dnat_take) 1), |
|
343 (strip_tac 1), |
|
344 ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)), |
|
345 (atac 1), |
|
346 (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1), |
|
347 (etac disjE 1), |
|
348 (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1), |
|
349 (etac exE 1), |
|
350 (etac exE 1), |
|
351 (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1), |
|
352 (REPEAT (etac conjE 1)), |
|
353 (rtac cfun_arg_cong 1), |
|
354 (fast_tac HOL_cs 1) |
|
355 ]); |
|
356 |
|
357 val dnat_coind = prove_goal Dnat.thy "[|dnat_bisim(R);R(p,q)|] ==> p = q" |
|
358 (fn prems => |
|
359 [ |
|
360 (rtac dnat_take_lemma 1), |
|
361 (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1), |
|
362 (resolve_tac prems 1), |
|
363 (resolve_tac prems 1) |
|
364 ]); |
|
365 |
|
366 |
|
367 (* ------------------------------------------------------------------------*) |
|
368 (* structural induction for admissible predicates *) |
|
369 (* ------------------------------------------------------------------------*) |
|
370 |
|
371 val dnat_ind = prove_goal Dnat.thy |
|
372 "[| adm(P);\ |
|
373 \ P(UU);\ |
|
374 \ P(dzero);\ |
|
375 \ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)" |
|
376 (fn prems => |
|
377 [ |
|
378 (rtac (dnat_reach RS subst) 1), |
|
379 (res_inst_tac [("x","s")] spec 1), |
|
380 (rtac fix_ind 1), |
|
381 (rtac adm_all2 1), |
|
382 (rtac adm_subst 1), |
|
383 (contX_tacR 1), |
|
384 (resolve_tac prems 1), |
|
385 (simp_tac HOLCF_ss 1), |
|
386 (resolve_tac prems 1), |
|
387 (strip_tac 1), |
|
388 (res_inst_tac [("n","xa")] dnatE 1), |
|
389 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
390 (resolve_tac prems 1), |
|
391 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
392 (resolve_tac prems 1), |
|
393 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
394 (res_inst_tac [("Q","x[xb]=UU")] classical2 1), |
|
395 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
396 (resolve_tac prems 1), |
|
397 (eresolve_tac prems 1), |
|
398 (etac spec 1) |
|
399 ]); |
|
400 |
|
401 |
|
402 val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)" |
|
403 (fn prems => |
|
404 [ |
|
405 (rtac allI 1), |
|
406 (res_inst_tac [("s","x")] dnat_ind 1), |
|
407 (REPEAT (resolve_tac adm_thms 1)), |
|
408 (contX_tacR 1), |
|
409 (REPEAT (resolve_tac adm_thms 1)), |
|
410 (contX_tacR 1), |
|
411 (REPEAT (resolve_tac adm_thms 1)), |
|
412 (contX_tacR 1), |
|
413 (fast_tac HOL_cs 1), |
|
414 (rtac allI 1), |
|
415 (res_inst_tac [("n","y")] dnatE 1), |
|
416 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
|
417 (asm_simp_tac HOLCF_ss 1), |
|
418 (asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1), |
|
419 (rtac allI 1), |
|
420 (res_inst_tac [("n","y")] dnatE 1), |
|
421 (fast_tac (HOL_cs addSIs [UU_I]) 1), |
|
422 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
423 (hyp_subst_tac 1), |
|
424 (strip_tac 1), |
|
425 (rtac disjI2 1), |
|
426 (forward_tac dnat_invert 1), |
|
427 (atac 2), |
|
428 (atac 1), |
|
429 (etac allE 1), |
|
430 (dtac mp 1), |
|
431 (atac 1), |
|
432 (etac disjE 1), |
|
433 (contr_tac 1), |
|
434 (asm_simp_tac HOLCF_ss 1) |
|
435 ]); |
|
436 |
|
437 val dnat_ind = prove_goal Dnat.thy |
|
438 "[| adm(P);\ |
|
439 \ P(UU);\ |
|
440 \ P(dzero);\ |
|
441 \ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)" |
|
442 (fn prems => |
|
443 [ |
|
444 (rtac (dnat_reach RS subst) 1), |
|
445 (res_inst_tac [("x","s")] spec 1), |
|
446 (rtac fix_ind 1), |
|
447 (rtac adm_all2 1), |
|
448 (rtac adm_subst 1), |
|
449 (contX_tacR 1), |
|
450 (resolve_tac prems 1), |
|
451 (simp_tac HOLCF_ss 1), |
|
452 (resolve_tac prems 1), |
|
453 (strip_tac 1), |
|
454 (res_inst_tac [("n","xa")] dnatE 1), |
|
455 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
456 (resolve_tac prems 1), |
|
457 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
458 (resolve_tac prems 1), |
|
459 (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1), |
|
460 (res_inst_tac [("Q","x[xb]=UU")] classical2 1), |
|
461 (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1), |
|
462 (resolve_tac prems 1), |
|
463 (eresolve_tac prems 1), |
|
464 (etac spec 1) |
|
465 ]); |
|
466 |
|
467 val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind; |
|
468 (* "[| ?P(UU); ?P(dzero); |
|
469 !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm |
|
470 *) |
|
471 |