--- 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";
--- 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,