819 (*** Instantiate theorem th, reading instantiations in theory thy ****) |
819 (*** Instantiate theorem th, reading instantiations in theory thy ****) |
820 |
820 |
821 fun instantiate_normalize instpair th = |
821 fun instantiate_normalize instpair th = |
822 Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); |
822 Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); |
823 |
823 |
824 (*Left-to-right replacements: tpairs = [...,(vi,ti),...]. |
824 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. |
825 Instantiates distinct Vars by terms, inferring type instantiations. *) |
825 Instantiates distinct Vars by terms, inferring type instantiations.*) |
826 local |
826 local |
827 fun add_types ((ct,cu), (thy,tye,maxidx)) = |
827 fun add_types (ct, cu) (thy, tye, maxidx) = |
828 let |
828 let |
829 val thyt = Thm.theory_of_cterm ct; |
829 val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; |
830 val thyu = Thm.theory_of_cterm cu; |
830 val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; |
831 val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct; |
831 val maxi = Int.max (maxidx, Int.max (maxt, maxu)); |
832 val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu; |
832 val thy' = Theory.merge (thy, Theory.merge (Thm.theory_of_cterm ct, Thm.theory_of_cterm cu)); |
833 val maxi = Int.max(maxidx, Int.max(maxt, maxu)); |
833 val (tye', maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) |
834 val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) |
834 handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^ |
835 val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) |
835 Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ |
836 handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^ |
836 "\nof variable " ^ |
837 Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^ |
837 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ |
838 "\nof variable " ^ |
838 "\ncannot be unified with type\n" ^ |
839 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^ |
839 Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ |
840 "\ncannot be unified with type\n" ^ |
840 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), |
841 Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^ |
841 [T, U], [t, u]) |
842 Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u), |
842 in (thy', tye', maxi') end; |
843 [T, U], [t, u]) |
|
844 in (thy', tye', maxi') end; |
|
845 in |
843 in |
|
844 |
846 fun cterm_instantiate [] th = th |
845 fun cterm_instantiate [] th = th |
847 | cterm_instantiate ctpairs0 th = |
846 | cterm_instantiate ctpairs0 th = |
848 let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 |
847 let |
849 fun instT(ct,cu) = |
848 val (thy, tye, _) = fold_rev add_types ctpairs0 (Thm.theory_of_thm th, Vartab.empty, 0); |
850 let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of |
849 val certT = ctyp_of thy; |
851 in (inst ct, inst cu) end |
850 fun instT (ct, cu) = |
852 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T)) |
851 let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of |
853 in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end |
852 in (inst ct, inst cu) end; |
854 handle TERM _ => |
853 fun ctyp2 (ixn, (S, T)) = (certT (TVar (ixn, S)), certT (Envir.norm_type tye T)); |
855 raise THM("cterm_instantiate: incompatible theories",0,[th]) |
854 in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end |
856 | TYPE (msg, _, _) => raise THM(msg, 0, [th]) |
855 handle TERM _ => raise THM ("cterm_instantiate: incompatible theories", 0, [th]) |
|
856 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
857 end; |
857 end; |
858 |
858 |
859 |
859 |
860 |
860 |
861 (** variations on instantiate **) |
861 (** variations on instantiate **) |