renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Jun 09 23:12:02 2011 +0200
@@ -67,8 +67,8 @@
fun fw mi th th' th'' =
let
val th0 = if mi then
- instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
- else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
+ Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
+ else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
@@ -114,11 +114,11 @@
val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
- nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
+ nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
- npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
+ npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
- ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
+ ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
fun decomp_mpinf fm =
case term_of fm of
--- a/src/HOL/Import/proof_kernel.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Jun 09 23:12:02 2011 +0200
@@ -1419,7 +1419,7 @@
| NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
))
(zip tys_before tys_after)
- val res = Drule.instantiate (tyinst,[]) th1
+ val res = Drule.instantiate_normalize (tyinst,[]) th1
val hth = HOLThm([],res)
val res = norm_hthm thy hth
val _ = message "RESULT:"
--- a/src/HOL/Import/shuffler.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Jun 09 23:12:02 2011 +0200
@@ -249,7 +249,7 @@
val mid =
case rens of
[] => thm'
- | [((_, S), idx)] => instantiate
+ | [((_, S), idx)] => Drule.instantiate_normalize
([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
| _ => error "Shuffler.inst_tfrees internal error"
in
--- a/src/HOL/Library/reflection.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Library/reflection.ML Thu Jun 09 23:12:02 2011 +0200
@@ -157,7 +157,7 @@
map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
in ((fts ~~ (replicate (length fts) ctxt),
- Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
+ Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
end;
@@ -230,7 +230,7 @@
val substt =
let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end
- val th = (instantiate (subst_ty, substt) eq) RS sym
+ val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym
in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
handle Pattern.MATCH => tryeqs eqs bds)
in tryeqs (filter isat eqs) bds end), bds);
@@ -277,7 +277,7 @@
val cert = cterm_of (Proof_Context.theory_of ctxt)
val cvs = map (fn (v as Var(n,t)) => (cert v,
the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
- val th' = instantiate ([], cvs) th
+ val th' = Drule.instantiate_normalize ([], cvs) th
val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
(fn _ => simp_tac (simpset_of ctxt) 1)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Thu Jun 09 23:12:02 2011 +0200
@@ -306,7 +306,7 @@
(fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
in fst (RealArith.real_linear_prover translator
- (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
+ (map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
@@ -343,7 +343,7 @@
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
val cps = map (swap o Thm.dest_equals) (cprems_of th11)
- val th12 = instantiate ([], cps) th11
+ val th12 = Drule.instantiate_normalize ([], cps) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Jun 09 23:12:02 2011 +0200
@@ -206,7 +206,7 @@
|> map (fn (x, (S, T)) =>
pairself (ctyp_of thy) (TVar (x, S), T)) of
[] => raise TERM z
- | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
+ | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
end
fun s_not (@{const Not} $ t) = t
@@ -562,7 +562,7 @@
tyenv []
val t_inst =
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
- in th |> instantiate (ty_inst, t_inst) end
+ in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
| _ => raise Fail "expected a single non-zapped, non-Metis Var"
in
(DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jun 09 23:12:02 2011 +0200
@@ -156,10 +156,10 @@
[(th_1,th_2,th_3), (th_1',th_2',th_3')] =
let
val (mp', mq') = (get_pmi th_1, get_pmi th_1')
- val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
+ val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
[th_1, th_1']
- val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
- val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
+ val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
+ val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
in (mi_th, set_th, infD_th)
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 23:12:02 2011 +0200
@@ -100,7 +100,7 @@
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
- |> Drule.instantiate ([(aT, icT)],
+ |> Drule.instantiate_normalize ([(aT, icT)],
[(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
val tac = ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac rew_ss)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 09 23:12:02 2011 +0200
@@ -108,7 +108,7 @@
| SOME thm' =>
(case try (get_match_inst thy (get_lhs thm')) redex of
NONE => NONE
- | SOME inst2 => try (Drule.instantiate inst2) thm'))
+ | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
end
fun ball_bex_range_simproc ss redex =
@@ -490,7 +490,7 @@
if ty_c = ty_d
then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
- val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
+ val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
--- a/src/HOL/Tools/TFL/rules.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jun 09 23:12:02 2011 +0200
@@ -270,7 +270,7 @@
val gspec = Thm.forall_intr (cterm_of thy x) spec
in
fun SPEC tm thm =
- let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
+ let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
@@ -298,7 +298,7 @@
val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
- val allI2 = instantiate (certify thy theta) allI
+ val allI2 = Drule.instantiate_normalize (certify thy theta) allI
val thm = Thm.implies_elim allI2 gth
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
val prop' = tp $ (A $ Abs(x,ty,M))
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 09 23:12:02 2011 +0200
@@ -63,9 +63,9 @@
let
val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
and ct = cterm_of thy t
- in instantiate ([], [(cn, ct)]) @{thm le0} end;
+ in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
-end; (* LA_Logic *)
+end;
(* arith context data *)
--- a/src/HOL/Tools/split_rule.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/split_rule.ML Thu Jun 09 23:12:02 2011 +0200
@@ -73,7 +73,7 @@
val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+ (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
end
| complete_split_rule_var _ x = x;
--- a/src/Provers/hypsubst.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Provers/hypsubst.ML Thu Jun 09 23:12:02 2011 +0200
@@ -163,7 +163,7 @@
| t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
val thy = Thm.theory_of_thm rl';
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
- in compose_tac (true, Drule.instantiate (instT,
+ in compose_tac (true, Drule.instantiate_normalize (instT,
map (pairself (cterm_of thy))
[(Var (ixn, Ts ---> U --> body_type T), u),
(Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
--- a/src/Pure/Isar/rule_insts.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Thu Jun 09 23:12:02 2011 +0200
@@ -173,7 +173,7 @@
else
Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
- Drule.instantiate insts thm |> Rule_Cases.save thm
+ Drule.instantiate_normalize insts thm |> Rule_Cases.save thm
end;
fun read_instantiate_mixed' ctxt (args, concl_args) thm =
@@ -323,7 +323,7 @@
fun liftpair (cv,ct) =
(cterm_fun liftvar cv, cterm_fun liftterm ct)
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
- val rule = Drule.instantiate
+ val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule (Thm.cprem_of st i) thm)
in
@@ -347,7 +347,7 @@
val maxidx = Thm.maxidx_of rl;
fun cvar xi = cert (Var (xi, propT));
val revcut_rl' =
- instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
+ Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
in
(case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
--- a/src/Pure/conv.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Pure/conv.ML Thu Jun 09 23:12:02 2011 +0200
@@ -162,7 +162,7 @@
val lhs = Thm.lhs_of rule1;
val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
in
- Drule.instantiate (Thm.match (lhs, ct)) rule2
+ Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
end;
--- a/src/Pure/drule.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Pure/drule.ML Thu Jun 09 23:12:02 2011 +0200
@@ -24,7 +24,7 @@
val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
- val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+ val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
val implies_intr_hyps: thm -> thm
@@ -821,8 +821,7 @@
(*** Instantiate theorem th, reading instantiations in theory thy ****)
-(*Version that normalizes the result: Thm.instantiate no longer does that*)
-fun instantiate instpair th =
+fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
@@ -854,7 +853,7 @@
let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
in (inst ct, inst cu) end
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T))
- in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
+ in instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
handle TERM _ =>
raise THM("cterm_instantiate: incompatible theories",0,[th])
| TYPE (msg, _, _) => raise THM(msg, 0, [th])
--- a/src/Tools/induct.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Tools/induct.ML Thu Jun 09 23:12:02 2011 +0200
@@ -588,9 +588,10 @@
val concl = Logic.strip_assums_concl goal;
in
Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
- |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
+ |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
end
- end handle General.Subscript => Seq.empty;
+ end
+ handle General.Subscript => Seq.empty;
end;
--- a/src/ZF/Tools/cartprod.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/ZF/Tools/cartprod.ML Thu Jun 09 23:12:02 2011 +0200
@@ -108,7 +108,7 @@
val newt = ap_split T1 T2 (Var(v,T'))
val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
in
- remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
+ remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
cterm newt)]) rl)
end
| split_rule_var (t,T,rl) = rl;
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jun 09 23:12:02 2011 +0200
@@ -493,7 +493,7 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
+ | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
cterm_of thy1 elem_tuple)]);
(*strip quantifier and the implication*)