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 prove_coinduction |
199 (******************************************************************************) |
|
200 (****************************** induction rules *******************************) |
|
201 (******************************************************************************) |
|
202 |
|
203 fun prove_induction |
200 (comp_dnam, eqs : eq list) |
204 (comp_dnam, eqs : eq list) |
201 (take_lemmas : thm list) |
205 (take_lemmas : thm list) |
202 (thy : theory) : thm * theory = |
206 (axs_reach : thm list) |
|
207 (take_rews : thm list) |
|
208 (thy : theory) = |
203 let |
209 let |
204 |
|
205 val dnames = map (fst o fst) eqs; |
|
206 val comp_dname = Sign.full_bname thy comp_dnam; |
|
207 fun dc_take dn = %%:(dn^"_take"); |
|
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; |
|
213 |
|
214 (* ----- define bisimulation predicate -------------------------------------- *) |
|
215 |
|
216 local |
|
217 open HOLCF_Library |
|
218 val dtypes = map (Type o fst) eqs; |
|
219 val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes); |
|
220 val bisim_bind = Binding.name (comp_dnam ^ "_bisim"); |
|
221 val bisim_type = relprod --> boolT; |
|
222 in |
|
223 val (bisim_const, thy) = |
|
224 Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; |
|
225 end; |
|
226 |
|
227 local |
|
228 |
|
229 fun legacy_infer_term thy t = |
|
230 singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); |
|
231 fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); |
|
232 fun infer_props thy = map (apsnd (legacy_infer_prop thy)); |
|
233 fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); |
|
234 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; |
|
235 |
|
236 val comp_dname = Sign.full_bname thy comp_dnam; |
|
237 val dnames = map (fst o fst) eqs; |
210 val dnames = map (fst o fst) eqs; |
|
211 val conss = map snd eqs; |
|
212 fun dc_take dn = %%:(dn^"_take"); |
238 val x_name = idx_name dnames "x"; |
213 val x_name = idx_name dnames "x"; |
239 |
214 val P_name = idx_name dnames "P"; |
240 fun one_con (con, args) = |
|
241 let |
|
242 val nonrec_args = filter_out is_rec args; |
|
243 val rec_args = filter is_rec args; |
|
244 val recs_cnt = length rec_args; |
|
245 val allargs = nonrec_args @ rec_args |
|
246 @ map (upd_vname (fn s=> s^"'")) rec_args; |
|
247 val allvns = map vname allargs; |
|
248 fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; |
|
249 val vns1 = map (vname_arg "" ) args; |
|
250 val vns2 = map (vname_arg "'") args; |
|
251 val allargs_cnt = length nonrec_args + 2*recs_cnt; |
|
252 val rec_idxs = (recs_cnt-1) downto 0; |
|
253 val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) |
|
254 (allargs~~((allargs_cnt-1) downto 0))); |
|
255 fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ |
|
256 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
|
257 val capps = |
|
258 List.foldr |
|
259 mk_conj |
|
260 (mk_conj( |
|
261 Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), |
|
262 Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) |
|
263 (mapn rel_app 1 rec_args); |
|
264 in |
|
265 List.foldr |
|
266 mk_ex |
|
267 (Library.foldr mk_conj |
|
268 (map (defined o Bound) nonlazy_idxs,capps)) allvns |
|
269 end; |
|
270 fun one_comp n (_,cons) = |
|
271 mk_all (x_name(n+1), |
|
272 mk_all (x_name(n+1)^"'", |
|
273 mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
|
274 foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
|
275 ::map one_con cons)))); |
|
276 val bisim_eqn = |
|
277 %%:(comp_dname^"_bisim") == |
|
278 mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)); |
|
279 |
|
280 in |
|
281 val ([ax_bisim_def], thy) = |
|
282 thy |
|
283 |> Sign.add_path comp_dnam |
|
284 |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] |
|
285 ||> Sign.parent_path; |
|
286 end; (* local *) |
|
287 |
|
288 (* ----- theorem concerning coinduction ------------------------------------- *) |
|
289 |
|
290 local |
|
291 val pg = pg' thy; |
215 val pg = pg' thy; |
292 val xs = mapn (fn n => K (x_name n)) 1 dnames; |
216 |
293 fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); |
217 local |
294 val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); |
218 fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
295 val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); |
219 fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); |
296 val _ = trace " Proving coind_lemma..."; |
220 in |
297 val coind_lemma = |
221 val axs_chain_take = map (ga "chain_take") dnames; |
298 let |
222 val axs_finite_def = map (ga "finite_def") dnames; |
299 fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; |
223 val cases = map (ga "casedist" ) dnames; |
300 fun mk_eqn n dn = |
224 val con_rews = maps (gts "con_rews" ) dnames; |
301 (dc_take dn $ %:"n" ` bnd_arg n 0) === |
225 end; |
302 (dc_take dn $ %:"n" ` bnd_arg n 1); |
226 |
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^" ..."); |
|
355 |
|
356 val pg = pg' thy; |
|
357 |
|
358 (* ----- getting the composite axiom and definitions ------------------------ *) |
|
359 |
|
360 local |
|
361 fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
|
362 in |
|
363 val axs_take_def = map (ga "take_def" ) dnames; |
|
364 val axs_chain_take = map (ga "chain_take") dnames; |
|
365 val axs_lub_take = map (ga "lub_take" ) dnames; |
|
366 val axs_finite_def = map (ga "finite_def") dnames; |
|
367 end; |
|
368 |
|
369 local |
|
370 fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
|
371 fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); |
|
372 in |
|
373 val cases = map (gt "casedist" ) dnames; |
|
374 val con_rews = maps (gts "con_rews" ) dnames; |
|
375 end; |
|
376 |
|
377 fun dc_take dn = %%:(dn^"_take"); |
|
378 val x_name = idx_name dnames "x"; |
|
379 val P_name = idx_name dnames "P"; |
|
380 val n_eqs = length eqs; |
|
381 |
|
382 (* ----- theorems concerning finite approximation and finite induction ------ *) |
|
383 |
|
384 val take_rews = |
|
385 maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; |
|
386 |
|
387 local |
|
388 fun one_con p (con, args) = |
227 fun one_con p (con, args) = |
389 let |
228 let |
390 val P_names = map P_name (1 upto (length dnames)); |
229 val P_names = map P_name (1 upto (length dnames)); |
391 val vns = Name.variant_list P_names (map vname args); |
230 val vns = Name.variant_list P_names (map vname args); |
392 val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); |
231 val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); |
625 handle THM _ => |
448 handle THM _ => |
626 (warning "Induction proofs failed (THM raised)."; ([], TrueI)) |
449 (warning "Induction proofs failed (THM raised)."; ([], TrueI)) |
627 | ERROR _ => |
450 | ERROR _ => |
628 (warning "Cannot prove induction rule"; ([], TrueI)); |
451 (warning "Cannot prove induction rule"; ([], TrueI)); |
629 |
452 |
630 end; (* local *) |
|
631 |
|
632 val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy; |
|
633 |
|
634 val inducts = Project_Rule.projections (ProofContext.init thy) ind; |
453 val inducts = Project_Rule.projections (ProofContext.init thy) ind; |
635 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
454 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); |
636 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
455 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); |
|
456 |
|
457 in thy |> Sign.add_path comp_dnam |
|
458 |> snd o PureThy.add_thmss [ |
|
459 ((Binding.name "finites" , finites ), []), |
|
460 ((Binding.name "finite_ind" , [finite_ind]), []), |
|
461 ((Binding.name "ind" , [ind] ), [])] |
|
462 |> (if induct_failed then I |
|
463 else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) |
|
464 |> Sign.parent_path |
|
465 end; (* prove_induction *) |
|
466 |
|
467 (******************************************************************************) |
|
468 (************************ bisimulation and coinduction ************************) |
|
469 (******************************************************************************) |
|
470 |
|
471 fun prove_coinduction |
|
472 (comp_dnam, eqs : eq list) |
|
473 (take_lemmas : thm list) |
|
474 (thy : theory) : thm * theory = |
|
475 let |
|
476 |
|
477 val dnames = map (fst o fst) eqs; |
|
478 val comp_dname = Sign.full_bname thy comp_dnam; |
|
479 fun dc_take dn = %%:(dn^"_take"); |
|
480 val x_name = idx_name dnames "x"; |
|
481 val n_eqs = length eqs; |
|
482 |
|
483 val take_rews = |
|
484 maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; |
|
485 |
|
486 (* ----- define bisimulation predicate -------------------------------------- *) |
|
487 |
|
488 local |
|
489 open HOLCF_Library |
|
490 val dtypes = map (Type o fst) eqs; |
|
491 val relprod = mk_tupleT (map (fn tp => tp --> tp --> boolT) dtypes); |
|
492 val bisim_bind = Binding.name (comp_dnam ^ "_bisim"); |
|
493 val bisim_type = relprod --> boolT; |
|
494 in |
|
495 val (bisim_const, thy) = |
|
496 Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; |
|
497 end; |
|
498 |
|
499 local |
|
500 |
|
501 fun legacy_infer_term thy t = |
|
502 singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); |
|
503 fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); |
|
504 fun infer_props thy = map (apsnd (legacy_infer_prop thy)); |
|
505 fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); |
|
506 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; |
|
507 |
|
508 val comp_dname = Sign.full_bname thy comp_dnam; |
|
509 val dnames = map (fst o fst) eqs; |
|
510 val x_name = idx_name dnames "x"; |
|
511 |
|
512 fun one_con (con, args) = |
|
513 let |
|
514 val nonrec_args = filter_out is_rec args; |
|
515 val rec_args = filter is_rec args; |
|
516 val recs_cnt = length rec_args; |
|
517 val allargs = nonrec_args @ rec_args |
|
518 @ map (upd_vname (fn s=> s^"'")) rec_args; |
|
519 val allvns = map vname allargs; |
|
520 fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; |
|
521 val vns1 = map (vname_arg "" ) args; |
|
522 val vns2 = map (vname_arg "'") args; |
|
523 val allargs_cnt = length nonrec_args + 2*recs_cnt; |
|
524 val rec_idxs = (recs_cnt-1) downto 0; |
|
525 val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) |
|
526 (allargs~~((allargs_cnt-1) downto 0))); |
|
527 fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ |
|
528 Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); |
|
529 val capps = |
|
530 List.foldr |
|
531 mk_conj |
|
532 (mk_conj( |
|
533 Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), |
|
534 Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) |
|
535 (mapn rel_app 1 rec_args); |
|
536 in |
|
537 List.foldr |
|
538 mk_ex |
|
539 (Library.foldr mk_conj |
|
540 (map (defined o Bound) nonlazy_idxs,capps)) allvns |
|
541 end; |
|
542 fun one_comp n (_,cons) = |
|
543 mk_all (x_name(n+1), |
|
544 mk_all (x_name(n+1)^"'", |
|
545 mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
|
546 foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
|
547 ::map one_con cons)))); |
|
548 val bisim_eqn = |
|
549 %%:(comp_dname^"_bisim") == |
|
550 mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)); |
|
551 |
|
552 in |
|
553 val ([ax_bisim_def], thy) = |
|
554 thy |
|
555 |> Sign.add_path comp_dnam |
|
556 |> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] |
|
557 ||> Sign.parent_path; |
|
558 end; (* local *) |
|
559 |
|
560 (* ----- theorem concerning coinduction ------------------------------------- *) |
|
561 |
|
562 local |
|
563 val pg = pg' thy; |
|
564 val xs = mapn (fn n => K (x_name n)) 1 dnames; |
|
565 fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); |
|
566 val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); |
|
567 val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); |
|
568 val _ = trace " Proving coind_lemma..."; |
|
569 val coind_lemma = |
|
570 let |
|
571 fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; |
|
572 fun mk_eqn n dn = |
|
573 (dc_take dn $ %:"n" ` bnd_arg n 0) === |
|
574 (dc_take dn $ %:"n" ` bnd_arg n 1); |
|
575 fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); |
|
576 val goal = |
|
577 mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", |
|
578 Library.foldr mk_all2 (xs, |
|
579 Library.foldr mk_imp (mapn mk_prj 0 dnames, |
|
580 foldr1 mk_conj (mapn mk_eqn 0 dnames))))); |
|
581 fun x_tacs ctxt n x = [ |
|
582 rotate_tac (n+1) 1, |
|
583 etac all2E 1, |
|
584 eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
|
585 TRY (safe_tac HOL_cs), |
|
586 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
|
587 fun tacs ctxt = [ |
|
588 rtac impI 1, |
|
589 InductTacs.induct_tac ctxt [[SOME "n"]] 1, |
|
590 simp_tac take_ss 1, |
|
591 safe_tac HOL_cs] @ |
|
592 flat (mapn (x_tacs ctxt) 0 xs); |
|
593 in pg [ax_bisim_def] goal tacs end; |
|
594 in |
|
595 val _ = trace " Proving coind..."; |
|
596 val coind = |
|
597 let |
|
598 fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); |
|
599 fun mk_eqn x = %:x === %:(x^"'"); |
|
600 val goal = |
|
601 mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> |
|
602 Logic.list_implies (mapn mk_prj 0 xs, |
|
603 mk_trp (foldr1 mk_conj (map mk_eqn xs))); |
|
604 val tacs = |
|
605 TRY (safe_tac HOL_cs) :: |
|
606 maps (fn take_lemma => [ |
|
607 rtac take_lemma 1, |
|
608 cut_facts_tac [coind_lemma] 1, |
|
609 fast_tac HOL_cs 1]) |
|
610 take_lemmas; |
|
611 in pg [] goal (K tacs) end; |
|
612 end; (* local *) |
|
613 |
|
614 in |
|
615 (coind, thy) |
|
616 end; |
|
617 |
|
618 fun comp_theorems (comp_dnam, eqs: eq list) thy = |
|
619 let |
|
620 val map_tab = Domain_Take_Proofs.get_map_tab thy; |
|
621 |
|
622 val dnames = map (fst o fst) eqs; |
|
623 val comp_dname = Sign.full_bname thy comp_dnam; |
|
624 |
|
625 val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); |
|
626 |
|
627 (* ----- getting the composite axiom and definitions ------------------------ *) |
|
628 |
|
629 (* Test for indirect recursion *) |
|
630 local |
|
631 fun indirect_arg arg = |
|
632 rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg); |
|
633 fun indirect_con (_, args) = exists indirect_arg args; |
|
634 fun indirect_eq (_, cons) = exists indirect_con cons; |
|
635 in |
|
636 val is_indirect = exists indirect_eq eqs; |
|
637 val _ = if is_indirect |
|
638 then message "Definition uses indirect recursion." |
|
639 else (); |
|
640 end; |
|
641 |
|
642 (* theorems about take *) |
|
643 |
|
644 local |
|
645 fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); |
|
646 val axs_chain_take = map (ga "chain_take") dnames; |
|
647 val axs_lub_take = map (ga "lub_take" ) dnames; |
|
648 in |
|
649 val _ = trace " Proving take_lemmas..."; |
|
650 val take_lemmas = |
|
651 let |
|
652 fun take_lemma (ax_chain_take, ax_lub_take) = |
|
653 Drule.export_without_context |
|
654 (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]); |
|
655 in map take_lemma (axs_chain_take ~~ axs_lub_take) end; |
|
656 val axs_reach = |
|
657 let |
|
658 fun reach (ax_chain_take, ax_lub_take) = |
|
659 Drule.export_without_context |
|
660 (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]); |
|
661 in map reach (axs_chain_take ~~ axs_lub_take) end; |
|
662 end; |
|
663 |
|
664 val take_rews = |
|
665 maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; |
|
666 |
|
667 (* prove induction rules, unless definition is indirect recursive *) |
|
668 val thy = |
|
669 if is_indirect then thy else |
|
670 prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy; |
|
671 |
|
672 val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy; |
637 |
673 |
638 in thy |> Sign.add_path comp_dnam |
674 in thy |> Sign.add_path comp_dnam |
639 |> snd o PureThy.add_thmss [ |
675 |> snd o PureThy.add_thmss [ |
640 ((Binding.name "take_lemmas", take_lemmas ), []), |
676 ((Binding.name "take_lemmas", take_lemmas ), []), |
641 ((Binding.name "reach" , axs_reach ), []), |
677 ((Binding.name "reach" , axs_reach ), []), |
642 ((Binding.name "finites" , finites ), []), |
|
643 ((Binding.name "finite_ind" , [finite_ind]), []), |
|
644 ((Binding.name "ind" , [ind] ), []), |
|
645 ((Binding.name "coind" , [coind] ), [])] |
678 ((Binding.name "coind" , [coind] ), [])] |
646 |> (if induct_failed then I |
|
647 else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) |
|
648 |> Sign.parent_path |> pair take_rews |
679 |> Sign.parent_path |> pair take_rews |
649 end; (* let *) |
680 end; (* let *) |
650 end; (* struct *) |
681 end; (* struct *) |