# HG changeset patch # User wenzelm # Date 1307653922 -7200 # Node ID 2bdec7f430d369bc1f5e5f233834f9c309e4a125 # Parent dca2c7c598f0d70347b1050a42ab20dfbacdaad1 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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 diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Import/proof_kernel.ML --- 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:" diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Import/shuffler.ML --- 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 diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Library/reflection.ML --- 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) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Multivariate_Analysis/normarith.ML --- 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 diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/Qelim/cooper.ML --- 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; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/Quickcheck/random_generators.ML --- 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) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/TFL/rules.ML --- 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)) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/lin_arith.ML --- 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 *) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/HOL/Tools/split_rule.ML --- 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; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/Provers/hypsubst.ML --- 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)), diff -r dca2c7c598f0 -r 2bdec7f430d3 src/Pure/Isar/rule_insts.ML --- 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 diff -r dca2c7c598f0 -r 2bdec7f430d3 src/Pure/conv.ML --- 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; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/Pure/drule.ML --- 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]) diff -r dca2c7c598f0 -r 2bdec7f430d3 src/Tools/induct.ML --- 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; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/ZF/Tools/cartprod.ML --- 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; diff -r dca2c7c598f0 -r 2bdec7f430d3 src/ZF/Tools/inductive_package.ML --- 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*)