606 in |
607 in |
607 map4 prove premss bclausesss exhausts' main_concls |
608 map4 prove premss bclausesss exhausts' main_concls |
608 |> ProofContext.export lthy'' lthy |
609 |> ProofContext.export lthy'' lthy |
609 end |
610 end |
610 |
611 |
|
612 |
|
613 |
|
614 (** strong induction theorems **) |
|
615 |
|
616 fun add_c_prop c c_ty trm = |
|
617 let |
|
618 val (P, arg) = dest_comb trm |
|
619 val (P_name, P_ty) = dest_Free P |
|
620 val (ty_args, bool) = strip_type P_ty |
|
621 in |
|
622 Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg |
|
623 end |
|
624 |
|
625 fun add_qnt_c_prop c_name c_ty trm = |
|
626 trm |> HOLogic.dest_Trueprop |
|
627 |> incr_boundvars 1 |
|
628 |> add_c_prop (Bound 0) c_ty |
|
629 |> HOLogic.mk_Trueprop |
|
630 |> mk_all (c_name, c_ty) |
|
631 |
|
632 fun prep_prem lthy c (c_name, c_ty) bclauses (params, prems, concl) = |
|
633 let |
|
634 val tys = map snd params |
|
635 val binders = get_all_binders bclauses |
|
636 |
|
637 fun prep_binder (opt, i) = |
|
638 let |
|
639 val t = Bound (length tys - i - 1) |
|
640 in |
|
641 case opt of |
|
642 NONE => setify_ty lthy (nth tys i) t |
|
643 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
|
644 end |
|
645 |
|
646 val prems' = prems |
|
647 |> map (incr_boundvars 1) |
|
648 |> map (add_qnt_c_prop c_name c_ty) |
|
649 |
|
650 val prems'' = |
|
651 case binders of |
|
652 [] => prems' (* case: no binders *) |
|
653 | _ => binders (* case: binders *) |
|
654 |> map prep_binder |
|
655 |> fold_union_env tys |
|
656 |> incr_boundvars 1 |
|
657 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |
|
658 |> (fn t => HOLogic.mk_Trueprop t :: prems') |
|
659 |
|
660 val concl' = concl |
|
661 |> HOLogic.dest_Trueprop |
|
662 |> incr_boundvars 1 |
|
663 |> add_c_prop (Bound 0) c_ty |
|
664 |> HOLogic.mk_Trueprop |
|
665 in |
|
666 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
|
667 end |
|
668 |
|
669 fun prove_strong_induct lthy induct exhausts bclausesss = |
|
670 let |
|
671 val ((insts, [induct']), lthy') = Variable.import true [induct] lthy |
|
672 |
|
673 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
|
674 val c_ty = TFree (a, @{sort fs}) |
|
675 val c = Free (c_name, c_ty) |
|
676 |
|
677 val (prems, concl) = induct' |
|
678 |> prop_of |
|
679 |> Logic.strip_horn |
|
680 |
|
681 val concls = concl |
|
682 |> HOLogic.dest_Trueprop |
|
683 |> HOLogic.dest_conj |
|
684 |> map (add_c_prop c c_ty) |
|
685 |> map HOLogic.mk_Trueprop |
|
686 |
|
687 val prems' = prems |
|
688 |> map strip_full_horn |
|
689 |> map2 (prep_prem lthy'' c (c_name, c_ty)) (flat bclausesss) |
|
690 |> map (Syntax.check_term lthy'') |
|
691 |
|
692 val _ = tracing ("induct:\n" ^ Syntax.string_of_term lthy'' (prop_of induct')) |
|
693 val _ = tracing ("concls:\n" ^ commas (map (Syntax.string_of_term lthy'') concls)) |
|
694 val _ = tracing ("prems':\n" ^ cat_lines (map (Syntax.string_of_term lthy'') prems')) |
|
695 |
|
696 val thm = Goal.prove_multi lthy'' [] prems' concls |
|
697 (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy'')) |
|
698 in |
|
699 @{thm TrueI} |
|
700 end |
|
701 |
|
702 |
611 end (* structure *) |
703 end (* structure *) |
612 |
704 |