# HG changeset patch # User paulson # Date 948114632 -3600 # Node ID 29e239c7b8c2be588d595cd7ea6400ddffecda8d # Parent 3a5864b465e2e1154ecfaad5334fbd7a399e492a Thm.instantiate no longer normalizes, but Drule.instantiate does diff -r 3a5864b465e2 -r 29e239c7b8c2 src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Jan 14 12:17:53 2000 +0100 +++ b/src/Pure/drule.ML Mon Jan 17 14:10:32 2000 +0100 @@ -30,6 +30,8 @@ val freeze_thaw : thm -> thm * (thm -> thm) val implies_elim_list : thm -> thm list -> thm val implies_intr_list : cterm list -> thm -> thm + val instantiate : + (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm val zero_var_indexes : thm -> thm val standard : thm -> thm val rotate_prems : int -> thm -> thm @@ -256,7 +258,7 @@ cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) end | varpairs _ = raise TERM("varpairs", []); - in instantiate (ctye, varpairs(vars,rev bs)) th end; + in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end; (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers; @@ -293,7 +295,7 @@ fun thaw th' = th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map #1 insts) - in (instantiate ([],insts) fth, thaw) end + in (Thm.instantiate ([],insts) fth, thaw) end end; @@ -359,42 +361,6 @@ [th] => th | _ => raise THM("COMP", 1, [tha,thb]); -(*Instantiate theorem th, reading instantiations under signature sg*) -fun read_instantiate_sg sg sinsts th = - let val ts = types_sorts th; - val used = add_term_tvarnames(#prop(rep_thm th),[]); - in instantiate (read_insts sg ts ts used sinsts) th end; - -(*Instantiate theorem th, reading instantiations under theory of th*) -fun read_instantiate sinsts th = - read_instantiate_sg (#sign (rep_thm th)) sinsts th; - - -(*Left-to-right replacements: tpairs = [...,(vi,ti),...]. - Instantiates distinct Vars by terms, inferring type instantiations. *) -local - fun add_types ((ct,cu), (sign,tye,maxidx)) = - let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct - and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; - val maxi = Int.max(maxidx, Int.max(maxt, maxu)); - val sign' = Sign.merge(sign, Sign.merge(signt, signu)) - val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) - handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) - in (sign', tye', maxi') end; -in -fun cterm_instantiate ctpairs0 th = - let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) - val tsig = #tsig(Sign.rep_sg sign); - fun instT(ct,cu) = let val inst = subst_TVars tye - in (cterm_fun inst ct, cterm_fun inst cu) end - fun ctyp2 (ix,T) = (ix, ctyp_of sign T) - in instantiate (map ctyp2 tye, map instT ctpairs0) th end - handle TERM _ => - raise THM("cterm_instantiate: incompatible signatures",0,[th]) - | TYPE (msg, _, _) => raise THM(msg, 0, [th]) -end; - - (** theorem equality **) (*Do the two theorems have the same signature?*) @@ -495,45 +461,6 @@ else raise THM("rewrite_goal_rule",i,[thm]); -(** Derived rules mainly for METAHYPS **) - -(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) -fun equal_abs_elim ca eqth = - let val {sign=signa, t=a, ...} = rep_cterm ca - and combth = combination eqth (reflexive ca) - val {sign,prop,...} = rep_thm eqth - val (abst,absu) = Logic.dest_equals prop - val cterm = cterm_of (Sign.merge (sign,signa)) - in transitive (symmetric (beta_conversion (cterm (abst$a)))) - (transitive combth (beta_conversion (cterm (absu$a)))) - end - handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); - -(*Calling equal_abs_elim with multiple terms*) -fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); - -local - val alpha = TVar(("'a",0), []) (* type ?'a::{} *) - fun err th = raise THM("flexpair_inst: ", 0, [th]) - fun flexpair_inst def th = - let val {prop = Const _ $ t $ u, sign,...} = rep_thm th - val cterm = cterm_of sign - fun cvar a = cterm(Var((a,0),alpha)) - val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] - def - in equal_elim def' th - end - handle THM _ => err th | Bind => err th -in -val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) -and flexpair_elim = flexpair_inst ProtoPure.flexpair_def -end; - -(*Version for flexflex pairs -- this supports lifting.*) -fun flexpair_abs_elim_list cts = - flexpair_intr o equal_abs_elim_list cts o flexpair_elim; - - (*** Some useful meta-theorems ***) (*The rule V/V, obtains assumption solving for eresolve_tac*) @@ -602,7 +529,86 @@ end; -(* GOAL (PROP A) <==> PROP A *) +(*** Instantiate theorem th, reading instantiations under signature sg ****) + +(*Version that normalizes the result: Thm.instantiate no longer does that*) +fun instantiate instpair th = Thm.instantiate instpair th COMP asm_rl; + +fun read_instantiate_sg sg sinsts th = + let val ts = types_sorts th; + val used = add_term_tvarnames(#prop(rep_thm th),[]); + in instantiate (read_insts sg ts ts used sinsts) th end; + +(*Instantiate theorem th, reading instantiations under theory of th*) +fun read_instantiate sinsts th = + read_instantiate_sg (#sign (rep_thm th)) sinsts th; + + +(*Left-to-right replacements: tpairs = [...,(vi,ti),...]. + Instantiates distinct Vars by terms, inferring type instantiations. *) +local + fun add_types ((ct,cu), (sign,tye,maxidx)) = + let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct + and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; + val maxi = Int.max(maxidx, Int.max(maxt, maxu)); + val sign' = Sign.merge(sign, Sign.merge(signt, signu)) + val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) + handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) + in (sign', tye', maxi') end; +in +fun cterm_instantiate ctpairs0 th = + let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) + val tsig = #tsig(Sign.rep_sg sign); + fun instT(ct,cu) = let val inst = subst_TVars tye + in (cterm_fun inst ct, cterm_fun inst cu) end + fun ctyp2 (ix,T) = (ix, ctyp_of sign T) + in instantiate (map ctyp2 tye, map instT ctpairs0) th end + handle TERM _ => + raise THM("cterm_instantiate: incompatible signatures",0,[th]) + | TYPE (msg, _, _) => raise THM(msg, 0, [th]) +end; + + +(** Derived rules mainly for METAHYPS **) + +(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) +fun equal_abs_elim ca eqth = + let val {sign=signa, t=a, ...} = rep_cterm ca + and combth = combination eqth (reflexive ca) + val {sign,prop,...} = rep_thm eqth + val (abst,absu) = Logic.dest_equals prop + val cterm = cterm_of (Sign.merge (sign,signa)) + in transitive (symmetric (beta_conversion (cterm (abst$a)))) + (transitive combth (beta_conversion (cterm (absu$a)))) + end + handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); + +(*Calling equal_abs_elim with multiple terms*) +fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); + +local + val alpha = TVar(("'a",0), []) (* type ?'a::{} *) + fun err th = raise THM("flexpair_inst: ", 0, [th]) + fun flexpair_inst def th = + let val {prop = Const _ $ t $ u, sign,...} = rep_thm th + val cterm = cterm_of sign + fun cvar a = cterm(Var((a,0),alpha)) + val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] + def + in equal_elim def' th + end + handle THM _ => err th | Bind => err th +in +val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) +and flexpair_elim = flexpair_inst ProtoPure.flexpair_def +end; + +(*Version for flexflex pairs -- this supports lifting.*) +fun flexpair_abs_elim_list cts = + flexpair_intr o equal_abs_elim_list cts o flexpair_elim; + + +(*** GOAL (PROP A) <==> PROP A ***) local val A = read_prop "PROP A"; diff -r 3a5864b465e2 -r 29e239c7b8c2 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Fri Jan 14 12:17:53 2000 +0100 +++ b/src/Pure/tactic.ML Mon Jan 17 14:10:32 2000 +0100 @@ -222,8 +222,8 @@ val used = add_term_tvarnames (#prop(rep_thm st) $ #prop(rep_thm rule),[]) val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts -in instantiate (map lifttvar Tinsts, map liftpair insts) - (lift_rule (st,i) rule) +in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) + (lift_rule (st,i) rule) end; (* @@ -251,8 +251,8 @@ (*lift only Var, not term, which must be lifted already*) fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) -in instantiate (map liftTpair Tinsts, map liftpair insts) - (lift_rule (st,i) rule) +in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) + (lift_rule (st,i) rule) end; (*** Resolve after lifting and instantation; may refer to parameters of the diff -r 3a5864b465e2 -r 29e239c7b8c2 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jan 14 12:17:53 2000 +0100 +++ b/src/Pure/thm.ML Mon Jan 17 14:10:32 2000 +0100 @@ -1064,15 +1064,14 @@ (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. Instantiates distinct Vars by terms of same type. - Normalizes the new theorem! *) + No longer normalizes the new theorem! *) fun instantiate ([], []) th = th - | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) = + | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) = let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[])); val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); - val newprop = - Envir.norm_term (Envir.empty 0) - (subst_atomic tpairs - (Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop)) + val newprop = subst_atomic tpairs + (Type.inst_term_tvars + (Sign.tsig_of (Sign.deref newsign_ref),vTs) prop) val newth = fix_shyps [th] (map snd vTs) (Thm{sign_ref = newsign_ref,