20 val lift_all: Proof.context -> cterm -> thm -> thm |
20 val lift_all: Proof.context -> cterm -> thm -> thm |
21 val implies_elim_list: thm -> thm list -> thm |
21 val implies_elim_list: thm -> thm list -> thm |
22 val implies_intr_list: cterm list -> thm -> thm |
22 val implies_intr_list: cterm list -> thm -> thm |
23 val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
23 val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> |
24 thm -> thm |
24 thm -> thm |
|
25 val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm |
25 val zero_var_indexes_list: thm list -> thm list |
26 val zero_var_indexes_list: thm list -> thm list |
26 val zero_var_indexes: thm -> thm |
27 val zero_var_indexes: thm -> thm |
27 val implies_intr_hyps: thm -> thm |
28 val implies_intr_hyps: thm -> thm |
28 val rotate_prems: int -> thm -> thm |
29 val rotate_prems: int -> thm -> thm |
29 val rearrange_prems: int list -> thm -> thm |
30 val rearrange_prems: int list -> thm -> thm |
737 (** variations on Thm.instantiate **) |
738 (** variations on Thm.instantiate **) |
738 |
739 |
739 fun instantiate_normalize instpair th = |
740 fun instantiate_normalize instpair th = |
740 Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); |
741 Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); |
741 |
742 |
|
743 (*instantiation with type-inference for variables*) |
|
744 fun infer_instantiate _ [] th = th |
|
745 | infer_instantiate ctxt args th = |
|
746 let |
|
747 val thy = Proof_Context.theory_of ctxt; |
|
748 |
|
749 val vars = Term.add_vars (Thm.full_prop_of th) []; |
|
750 val dups = duplicates (eq_fst op =) vars; |
|
751 val _ = null dups orelse |
|
752 raise THM ("infer_instantiate: inconsistent types for variables " ^ |
|
753 commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), |
|
754 0, [th]); |
|
755 fun var_type xi = |
|
756 (case AList.lookup (op =) vars xi of |
|
757 SOME T => T |
|
758 | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th])); |
|
759 |
|
760 fun infer (xi, cu) (tyenv, maxidx) = |
|
761 let |
|
762 val T = var_type xi; |
|
763 val U = Thm.typ_of_cterm cu; |
|
764 val (tyenv', maxidx') = |
|
765 Sign.typ_unify thy (T, U) |
|
766 (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu)) |
|
767 handle Type.TUNIFY => |
|
768 let |
|
769 val t = Var (xi, T); |
|
770 val u = Thm.term_of cu; |
|
771 in |
|
772 raise TYPE ("Ill-typed instantiation:\nType\n" ^ |
|
773 Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ |
|
774 "\nof variable " ^ |
|
775 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ |
|
776 "\ncannot be unified with type\n" ^ |
|
777 Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^ |
|
778 Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), |
|
779 [T, U], [t, u]) |
|
780 end; |
|
781 in (((xi, T), cu), (tyenv', maxidx')) end; |
|
782 |
|
783 val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0); |
|
784 val instT = |
|
785 Vartab.fold (fn (xi, (S, T)) => |
|
786 cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; |
|
787 val inst = args' |> map (fn ((xi, T), cu) => |
|
788 ((xi, Envir.norm_type tyenv T), |
|
789 Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); |
|
790 in instantiate_normalize (instT, inst) th end; |
|
791 |
742 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. |
792 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. |
743 Instantiates distinct Vars by terms, inferring type instantiations.*) |
793 Instantiates distinct Vars by terms, inferring type instantiations.*) |
744 local |
794 local |
745 fun add_types (ct, cu) (thy, tye, maxidx) = |
795 fun add_types (ct, cu) (thy, tye, maxidx) = |
746 let |
796 let |