194 |> Sign.parent_path |
194 |> Sign.parent_path |
195 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
195 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
196 pat_rews @ dist_les @ dist_eqs) |
196 pat_rews @ dist_les @ dist_eqs) |
197 end; (* let *) |
197 end; (* let *) |
198 |
198 |
199 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
199 fun prove_coinduction |
|
200 (comp_dnam, eqs : eq list) |
|
201 (take_lemmas : thm list) |
|
202 (thy : theory) : thm * theory = |
200 let |
203 let |
201 val map_tab = Domain_Take_Proofs.get_map_tab thy; |
|
202 |
204 |
203 val dnames = map (fst o fst) eqs; |
205 val dnames = map (fst o fst) eqs; |
204 val conss = map snd eqs; |
|
205 val comp_dname = Sign.full_bname thy comp_dnam; |
206 val comp_dname = Sign.full_bname thy comp_dnam; |
206 |
207 fun dc_take dn = %%:(dn^"_take"); |
207 val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); |
208 val x_name = idx_name dnames "x"; |
|
209 val n_eqs = length eqs; |
|
210 |
|
211 val take_rews = |
|
212 maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; |
208 |
213 |
209 (* ----- define bisimulation predicate -------------------------------------- *) |
214 (* ----- define bisimulation predicate -------------------------------------- *) |
210 |
215 |
211 local |
216 local |
212 open HOLCF_Library |
217 open HOLCF_Library |
277 thy |
282 thy |
278 |> Sign.add_path comp_dnam |
283 |> Sign.add_path comp_dnam |
279 |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] |
284 |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] |
280 ||> Sign.parent_path; |
285 ||> Sign.parent_path; |
281 end; (* local *) |
286 end; (* local *) |
|
287 |
|
288 (* ----- theorem concerning coinduction ------------------------------------- *) |
|
289 |
|
290 local |
|
291 val pg = pg' thy; |
|
292 val xs = mapn (fn n => K (x_name n)) 1 dnames; |
|
293 fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); |
|
294 val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); |
|
295 val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); |
|
296 val _ = trace " Proving coind_lemma..."; |
|
297 val coind_lemma = |
|
298 let |
|
299 fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; |
|
300 fun mk_eqn n dn = |
|
301 (dc_take dn $ %:"n" ` bnd_arg n 0) === |
|
302 (dc_take dn $ %:"n" ` bnd_arg n 1); |
|
303 fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); |
|
304 val goal = |
|
305 mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", |
|
306 Library.foldr mk_all2 (xs, |
|
307 Library.foldr mk_imp (mapn mk_prj 0 dnames, |
|
308 foldr1 mk_conj (mapn mk_eqn 0 dnames))))); |
|
309 fun x_tacs ctxt n x = [ |
|
310 rotate_tac (n+1) 1, |
|
311 etac all2E 1, |
|
312 eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
|
313 TRY (safe_tac HOL_cs), |
|
314 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
|
315 fun tacs ctxt = [ |
|
316 rtac impI 1, |
|
317 InductTacs.induct_tac ctxt [[SOME "n"]] 1, |
|
318 simp_tac take_ss 1, |
|
319 safe_tac HOL_cs] @ |
|
320 flat (mapn (x_tacs ctxt) 0 xs); |
|
321 in pg [ax_bisim_def] goal tacs end; |
|
322 in |
|
323 val _ = trace " Proving coind..."; |
|
324 val coind = |
|
325 let |
|
326 fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); |
|
327 fun mk_eqn x = %:x === %:(x^"'"); |
|
328 val goal = |
|
329 mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> |
|
330 Logic.list_implies (mapn mk_prj 0 xs, |
|
331 mk_trp (foldr1 mk_conj (map mk_eqn xs))); |
|
332 val tacs = |
|
333 TRY (safe_tac HOL_cs) :: |
|
334 maps (fn take_lemma => [ |
|
335 rtac take_lemma 1, |
|
336 cut_facts_tac [coind_lemma] 1, |
|
337 fast_tac HOL_cs 1]) |
|
338 take_lemmas; |
|
339 in pg [] goal (K tacs) end; |
|
340 end; (* local *) |
|
341 |
|
342 in |
|
343 (coind, thy) |
|
344 end; |
|
345 |
|
346 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
|
347 let |
|
348 val map_tab = Domain_Take_Proofs.get_map_tab thy; |
|
349 |
|
350 val dnames = map (fst o fst) eqs; |
|
351 val conss = map snd eqs; |
|
352 val comp_dname = Sign.full_bname thy comp_dnam; |
|
353 |
|
354 val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); |
282 |
355 |
283 val pg = pg' thy; |
356 val pg = pg' thy; |
284 |
357 |
285 (* ----- getting the composite axiom and definitions ------------------------ *) |
358 (* ----- getting the composite axiom and definitions ------------------------ *) |
286 |
359 |
554 | ERROR _ => |
627 | ERROR _ => |
555 (warning "Cannot prove induction rule"; ([], TrueI)); |
628 (warning "Cannot prove induction rule"; ([], TrueI)); |
556 |
629 |
557 end; (* local *) |
630 end; (* local *) |
558 |
631 |
559 (* ----- theorem concerning coinduction ------------------------------------- *) |
632 val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy; |
560 |
|
561 local |
|
562 val xs = mapn (fn n => K (x_name n)) 1 dnames; |
|
563 fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); |
|
564 val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); |
|
565 val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); |
|
566 val _ = trace " Proving coind_lemma..."; |
|
567 val coind_lemma = |
|
568 let |
|
569 fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; |
|
570 fun mk_eqn n dn = |
|
571 (dc_take dn $ %:"n" ` bnd_arg n 0) === |
|
572 (dc_take dn $ %:"n" ` bnd_arg n 1); |
|
573 fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); |
|
574 val goal = |
|
575 mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", |
|
576 Library.foldr mk_all2 (xs, |
|
577 Library.foldr mk_imp (mapn mk_prj 0 dnames, |
|
578 foldr1 mk_conj (mapn mk_eqn 0 dnames))))); |
|
579 fun x_tacs ctxt n x = [ |
|
580 rotate_tac (n+1) 1, |
|
581 etac all2E 1, |
|
582 eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
|
583 TRY (safe_tac HOL_cs), |
|
584 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
|
585 fun tacs ctxt = [ |
|
586 rtac impI 1, |
|
587 InductTacs.induct_tac ctxt [[SOME "n"]] 1, |
|
588 simp_tac take_ss 1, |
|
589 safe_tac HOL_cs] @ |
|
590 flat (mapn (x_tacs ctxt) 0 xs); |
|
591 in pg [ax_bisim_def] goal tacs end; |
|
592 in |
|
593 val _ = trace " Proving coind..."; |
|
594 val coind = |
|
595 let |
|
596 fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); |
|
597 fun mk_eqn x = %:x === %:(x^"'"); |
|
598 val goal = |
|
599 mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> |
|
600 Logic.list_implies (mapn mk_prj 0 xs, |
|
601 mk_trp (foldr1 mk_conj (map mk_eqn xs))); |
|
602 val tacs = |
|
603 TRY (safe_tac HOL_cs) :: |
|
604 maps (fn take_lemma => [ |
|
605 rtac take_lemma 1, |
|
606 cut_facts_tac [coind_lemma] 1, |
|
607 fast_tac HOL_cs 1]) |
|
608 take_lemmas; |
|
609 in pg [] goal (K tacs) end; |
|
610 end; (* local *) |
|
611 |
633 |
612 val inducts = Project_Rule.projections (ProofContext.init thy) ind; |
634 val inducts = Project_Rule.projections (ProofContext.init thy) ind; |
613 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
635 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
614 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
636 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
615 |
637 |