# HG changeset patch # User berghofe # Date 999267180 -7200 # Node ID 5f2616a1c10ae959907e265701da283dba4f4feb # Parent 6736505799d26c511554c6d6674c569b30d324f7 Replaced old derivations by proof terms. diff -r 6736505799d2 -r 5f2616a1c10a src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Aug 31 16:12:15 2001 +0200 +++ b/src/Pure/thm.ML Fri Aug 31 16:13:00 2001 +0200 @@ -36,54 +36,14 @@ string list -> bool -> (string * typ)list -> cterm list * (indexname * typ)list - (*proof terms [must DUPLICATE declaration as a specification]*) - datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv; type tag (* = string * string list *) - val keep_derivs : deriv_kind ref - datatype rule = - MinProof - | Oracle of string * Sign.sg * Object.T - | Axiom of string * tag list - | Theorem of string * tag list - | Assume of cterm - | Implies_intr of cterm - | Implies_intr_hyps - | Implies_elim - | Forall_intr of cterm - | Forall_elim of cterm - | Reflexive of cterm - | Symmetric - | Transitive - | Beta_conversion of cterm - | Eta_conversion of cterm - | Extensional - | Abstract_rule of string * cterm - | Combination - | Equal_intr - | Equal_elim - | Trivial of cterm - | Lift_rule of cterm * int - | Assumption of int * Envir.env option - | Rotate_rule of int * int - | Permute_prems of int * int - | Instantiate of (indexname * ctyp) list * (cterm * cterm) list - | Bicompose of bool * bool * int * int * Envir.env - | Flexflex_rule of Envir.env - | Class_triv of class - | VarifyT of string list - | FreezeT - | RewriteC of cterm - | CongC of cterm - | Rewrite_cterm of cterm - | Rename_params_rule of string list * int; - type deriv (* = rule mtree *) (*meta theorems*) type thm - val rep_thm : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int, + val rep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, shyps: sort list, hyps: term list, prop: term} - val crep_thm : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int, + val crep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, shyps: sort list, hyps: cterm list, prop: cterm} exception THM of string * int * thm list @@ -116,7 +76,6 @@ val transitive : thm -> thm -> thm val beta_conversion : bool -> cterm -> thm val eta_conversion : cterm -> thm - val extensional : thm -> thm val abstract_rule : string -> cterm -> thm -> thm val combination : thm -> thm -> thm val equal_intr : thm -> thm -> thm @@ -313,111 +272,17 @@ fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; - -(*** Derivations ***) - (*tags provide additional comment, apart from the axiom/theorem name*) type tag = string * string list; -(*Names of rules in derivations. Includes logically trivial rules, if - executed in ML.*) -datatype rule = - MinProof (*for building minimal proof terms*) - | Oracle of string * Sign.sg * Object.T (*oracles*) -(*Axioms/theorems*) - | Axiom of string * tag list - | Theorem of string * tag list -(*primitive inferences and compound versions of them*) - | Assume of cterm - | Implies_intr of cterm - | Implies_intr_hyps - | Implies_elim - | Forall_intr of cterm - | Forall_elim of cterm - | Reflexive of cterm - | Symmetric - | Transitive - | Beta_conversion of cterm - | Eta_conversion of cterm - | Extensional - | Abstract_rule of string * cterm - | Combination - | Equal_intr - | Equal_elim -(*derived rules for tactical proof*) - | Trivial of cterm - (*For lift_rule, the proof state is not a premise. - Use cterm instead of thm to avoid mutual recursion.*) - | Lift_rule of cterm * int - | Assumption of int * Envir.env option (*includes eq_assumption*) - | Rotate_rule of int * int - | Permute_prems of int * int - | Instantiate of (indexname * ctyp) list * (cterm * cterm) list - | Bicompose of bool * bool * int * int * Envir.env - | Flexflex_rule of Envir.env (*identifies unifier chosen*) -(*other derived rules*) - | Class_triv of class - | VarifyT of string list - | FreezeT -(*for the simplifier*) - | RewriteC of cterm - | CongC of cterm - | Rewrite_cterm of cterm -(*Logical identities, recorded since they are part of the proof process*) - | Rename_params_rule of string list * int; - - -type deriv = rule mtree; - -datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv; - -val keep_derivs = ref MinDeriv; - -local - -(*Build a minimal derivation. Keep oracles; suppress atomic inferences; - retain Theorems or their underlying links; keep anything else*) -fun squash_derivs [] = [] - | squash_derivs (der::ders) = - (case der of - Join (Oracle _, _) => der :: squash_derivs ders - | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv - then der :: squash_derivs ders - else squash_derivs (der'::ders) - | Join (Axiom _, _) => if !keep_derivs=ThmDeriv - then der :: squash_derivs ders - else squash_derivs ders - | Join (_, []) => squash_derivs ders - | _ => der :: squash_derivs ders); - -(*Ensure sharing of the most likely derivation, the empty one!*) -val min_infer = Join (MinProof, []); - -(*Make a minimal inference*) -fun make_min_infer [] = min_infer - | make_min_infer [der] = der - | make_min_infer ders = Join (MinProof, ders); - -fun is_oracle (Oracle _) = true - | is_oracle _ = false; - -in - -fun infer_derivs (rl, []: (bool * deriv) list) = (is_oracle rl, Join (rl, [])) - | infer_derivs (rl, ders) = - (is_oracle rl orelse exists #1 ders, - if !keep_derivs=FullDeriv then Join (rl, map #2 ders) - else make_min_infer (squash_derivs (map #2 ders))); - -end; - - (*** Meta theorems ***) +structure Pt = Proofterm; + datatype thm = Thm of {sign_ref: Sign.sg_ref, (*mutable reference to signature*) - der: bool * deriv, (*derivation*) + der: bool * Pt.proof, (*derivation*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort list, (*sort hypotheses*) hyps: term list, (*hypotheses*) @@ -447,9 +312,9 @@ fun eq_thm (th1, th2) = let - val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, maxidx = _, der = _} = + val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1; - val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, maxidx = _, der = _} = + val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2; in Sign.joinable (sg1, sg2) andalso @@ -601,7 +466,8 @@ Some t => Some (fix_shyps [] [] (Thm {sign_ref = Sign.self_ref sign, - der = infer_derivs (Axiom (name, []), []), + der = Pt.infer_derivs' I + (false, Pt.axm_proof name t), maxidx = maxidx_of_term t, shyps = [], hyps = [], @@ -626,23 +492,12 @@ (* name and tags -- make proof objects more readable *) -fun get_name_tags (Thm {der, ...}) = - (case #2 der of - Join (Theorem x, _) => x - | Join (Axiom x, _) => x - | _ => ("", [])); +fun get_name_tags (Thm {prop, der = (_, prf), ...}) = Pt.get_name_tags prop prf; -fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) = - let - val der' = - (case der of - Join (Theorem _, ds) => Join (Theorem x, ds) - | Join (Axiom _, ds) => Join (Axiom x, ds) - | _ => Join (Theorem x, [der])); - in - Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx, - shyps = shyps, hyps = hyps, prop = prop} - end; +fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = + Thm {sign_ref = sign_ref, + der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), + maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}; val name_of_thm = #1 o get_name_tags; val tags_of_thm = #2 o get_name_tags; @@ -691,7 +546,7 @@ raise THM("assume: assumptions may not contain scheme variables", maxidx, []) else Thm{sign_ref = sign_ref, - der = infer_derivs (Assume ct, []), + der = Pt.infer_derivs' I (false, Pt.Hyp prop), maxidx = ~1, shyps = add_term_sorts(prop,[]), hyps = [prop], @@ -711,7 +566,7 @@ raise THM("implies_intr: assumptions must have type prop", 0, [thB]) else Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), - der = infer_derivs (Implies_intr cA, [der]), + der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, maxidx = Int.max(maxidxA, maxidx), shyps = add_term_sorts (A, shyps), hyps = disch(hyps,A), @@ -735,7 +590,7 @@ if imp=implies andalso A aconv propA then Thm{sign_ref= merge_thm_sgs(thAB,thA), - der = infer_derivs (Implies_elim, [der,derA]), + der = Pt.infer_derivs (curry Pt.%) der derA, maxidx = Int.max(maxA,maxidx), shyps = union_sort (shypsA, shyps), hyps = union_term(hypsA,hyps), (*dups suppressed*) @@ -753,7 +608,7 @@ let val x = term_of cx; fun result(a,T) = fix_shyps [th] [] (Thm{sign_ref = sign_ref, - der = infer_derivs (Forall_intr cx, [der]), + der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, maxidx = maxidx, shyps = [], hyps = hyps, @@ -780,7 +635,7 @@ raise THM("forall_elim: type mismatch", 0, [th]) else let val thm = fix_shyps [th] [] (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), - der = infer_derivs (Forall_elim ct, [der]), + der = Pt.infer_derivs' (Pt.%% o rpair (Some t)) der, maxidx = Int.max(maxidx, maxt), shyps = [], hyps = hyps, @@ -801,7 +656,7 @@ fun reflexive ct = let val Cterm {sign_ref, t, T, maxidx} = ct in Thm{sign_ref= sign_ref, - der = infer_derivs (Reflexive ct, []), + der = Pt.infer_derivs' I (false, Pt.reflexive), shyps = add_term_sorts (t, []), hyps = [], maxidx = maxidx, @@ -815,10 +670,10 @@ *) fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = case prop of - (eq as Const("==",_)) $ t $ u => + (eq as Const("==", Type (_, [T, _]))) $ t $ u => (*no fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (Symmetric, [der]), + der = Pt.infer_derivs' Pt.symmetric der, maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -835,11 +690,11 @@ and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, prop=prop2,...} = th2; fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) in case (prop1,prop2) of - ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => + ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => if not (u aconv u') then err"middle term" else let val thm = Thm{sign_ref= merge_thm_sgs(th1,th2), - der = infer_derivs (Transitive, [der1, der2]), + der = Pt.infer_derivs (Pt.transitive u T) der1 der2, maxidx = Int.max(max1,max2), shyps = union_sort (shyps1, shyps2), hyps = union_term(hyps1,hyps2), @@ -858,7 +713,7 @@ let val Cterm {sign_ref, t, T, maxidx} = ct in Thm {sign_ref = sign_ref, - der = infer_derivs (Beta_conversion ct, []), + der = Pt.infer_derivs' I (false, Pt.reflexive), maxidx = maxidx, shyps = add_term_sorts (t, []), hyps = [], @@ -872,41 +727,13 @@ let val Cterm {sign_ref, t, T, maxidx} = ct in Thm {sign_ref = sign_ref, - der = infer_derivs (Eta_conversion ct, []), + der = Pt.infer_derivs' I (false, Pt.reflexive), maxidx = maxidx, shyps = add_term_sorts (t, []), hyps = [], prop = Logic.mk_equals (t, Pattern.eta_contract t)} end; -(*The extensionality rule (proviso: x not free in f, g, or hypotheses) - f(x) == g(x) - ------------ - f == g -*) -fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = - case prop of - (Const("==",_)) $ (f$x) $ (g$y) => - let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) - in (if x<>y then err"different variables" else - case y of - Free _ => - if exists (apl(y, Logic.occs)) (f::g::hyps) - then err"variable free in hyps or functions" else () - | Var _ => - if Logic.occs(y,f) orelse Logic.occs(y,g) - then err"variable free in functions" else () - | _ => err"not a variable"); - (*no fix_shyps*) - Thm{sign_ref = sign_ref, - der = infer_derivs (Extensional, [der]), - maxidx = maxidx, - shyps = shyps, - hyps = hyps, - prop = Logic.mk_equals(f,g)} - end - | _ => raise THM("extensional: premise", 0, [th]); - (*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) t == u @@ -920,7 +747,7 @@ raise THM("abstract_rule: premise not an equality", 0, [th]) fun result T = Thm{sign_ref = sign_ref, - der = infer_derivs (Abstract_rule (a,cx), [der]), + der = Pt.infer_derivs' (Pt.abstract_rule x a) der, maxidx = maxidx, shyps = add_typ_sorts (T, shyps), hyps = hyps, @@ -959,7 +786,8 @@ let val _ = chktypes fT tT val thm = (*no fix_shyps*) Thm{sign_ref = merge_thm_sgs(th1,th2), - der = infer_derivs (Combination, [der1, der2]), + der = Pt.infer_derivs + (Pt.combination f g t u fT) der1 der2, maxidx = Int.max(max1,max2), shyps = union_sort(shyps1,shyps2), hyps = union_term(hyps1,hyps2), @@ -978,7 +806,7 @@ A == B *) fun equal_intr th1 th2 = - let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, + let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2; @@ -989,7 +817,7 @@ then (*no fix_shyps*) Thm{sign_ref = merge_thm_sgs(th1,th2), - der = infer_derivs (Equal_intr, [der1, der2]), + der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, maxidx = Int.max(max1,max2), shyps = union_sort(shyps1,shyps2), hyps = union_term(hyps1,hyps2), @@ -1013,7 +841,7 @@ if not (prop2 aconv A) then err"not equal" else fix_shyps [th1, th2] [] (Thm{sign_ref= merge_thm_sgs(th1,th2), - der = infer_derivs (Equal_elim, [der1, der2]), + der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, maxidx = Int.max(max1,max2), shyps = [], hyps = union_term(hyps1,hyps2), @@ -1030,7 +858,7 @@ fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) = implies_intr_hyps (*no fix_shyps*) (Thm{sign_ref = sign_ref, - der = infer_derivs (Implies_intr_hyps, [der]), + der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, maxidx = maxidx, shyps = shyps, hyps = disch(As,A), @@ -1052,7 +880,7 @@ val newprop = Logic.list_flexpairs(distpairs, horn) in fix_shyps [th] (env_codT env) (Thm{sign_ref = sign_ref, - der = infer_derivs (Flexflex_rule env, [der]), + der = Pt.infer_derivs' (Pt.norm_proof' env) der, maxidx = maxidx_of_term newprop, shyps = [], hyps = hyps, @@ -1110,7 +938,7 @@ (Sign.tsig_of (Sign.deref newsign_ref),vTs) prop) val newth = (Thm{sign_ref = newsign_ref, - der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), + der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, maxidx = maxidx_of_term newprop, shyps = add_insts_sorts ((vTs, tpairs), shyps), hyps = hyps, @@ -1135,7 +963,7 @@ raise THM("trivial: the term must have type prop", 0, []) else fix_shyps [] [] (Thm{sign_ref = sign_ref, - der = infer_derivs (Trivial ct, []), + der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)), maxidx = maxidx, shyps = [], hyps = [], @@ -1150,7 +978,8 @@ in fix_shyps [] [] (Thm {sign_ref = sign_ref, - der = infer_derivs (Class_triv c, []), + der = Pt.infer_derivs' I + (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, Some [])), maxidx = maxidx, shyps = [], hyps = [], @@ -1163,7 +992,7 @@ let val tfrees = foldr add_term_tfree_names (hyps,fixed) in let val thm = (*no fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (VarifyT fixed, [der]), + der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, maxidx = Int.max(0,maxidx), shyps = shyps, hyps = hyps, @@ -1180,7 +1009,7 @@ let val (prop',_) = Type.freeze_thaw prop in (*no fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (FreezeT, [der]), + der = Pt.infer_derivs' (Pt.freezeT prop) der, maxidx = maxidx_of_term prop', shyps = shyps, hyps = hyps, @@ -1211,7 +1040,7 @@ val (tpairs,As,B) = Logic.strip_horn prop in (*no fix_shyps*) Thm{sign_ref = merge_thm_sgs(state,orule), - der = infer_derivs (Lift_rule(ct_Bi, i), [der]), + der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, maxidx = maxidx+smax+1, shyps=union_sort(sshyps,shyps), hyps=hyps, @@ -1224,7 +1053,8 @@ if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm {sign_ref = sign_ref, - der = der, + der = Pt.infer_derivs' (Pt.map_proof_terms + (Logic.incr_indexes ([], i)) (incr_tvar i)) der, maxidx = maxidx + i, shyps = shyps, hyps = hyps, @@ -1234,10 +1064,12 @@ fun assumption i state = let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; val (tpairs, Bs, Bi, C) = dest_state(state,i) - fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = + fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = fix_shyps [state] (env_codT env) (Thm{sign_ref = sign_ref, - der = infer_derivs (Assumption (i, Some env), [der]), + der = Pt.infer_derivs' + ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o + Pt.assumption_proof Bs Bi n) der, maxidx = maxidx, shyps = [], hyps = hyps, @@ -1246,27 +1078,28 @@ Logic.rule_of (tpairs, Bs, C) else (*normalize the new rule fully*) Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); - fun addprfs [] = Seq.empty - | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull - (Seq.mapp newth + fun addprfs [] _ = Seq.empty + | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull + (Seq.mapp (newth n) (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) - (addprfs apairs))) - in addprfs (Logic.assum_pairs Bi) end; + (addprfs apairs (n+1)))) + in addprfs (Logic.assum_pairs Bi) 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) fun eq_assumption i state = let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; val (tpairs, Bs, Bi, C) = dest_state(state,i) - in if exists (op aconv) (Logic.assum_pairs Bi) - then fix_shyps [state] [] - (Thm{sign_ref = sign_ref, - der = infer_derivs (Assumption (i,None), [der]), - maxidx = maxidx, - shyps = [], - hyps = hyps, - prop = Logic.rule_of(tpairs, Bs, C)}) - else raise THM("eq_assumption", 0, [state]) + in (case find_index (op aconv) (Logic.assum_pairs Bi) of + (~1) => raise THM("eq_assumption", 0, [state]) + | n => fix_shyps [state] [] + (Thm{sign_ref = sign_ref, + der = Pt.infer_derivs' + (Pt.assumption_proof Bs Bi (n+1)) der, + maxidx = maxidx, + shyps = [], + hyps = hyps, + prop = Logic.rule_of(tpairs, Bs, C)})) end; @@ -1289,7 +1122,8 @@ else raise THM("rotate_rule", k, [state]) in (*no fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (Rotate_rule (k,i), [der]), + der = Pt.infer_derivs' + (Pt.rotate_proof Bs Bi (if k<0 then n+k else k)) der, maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1317,7 +1151,7 @@ else raise THM("permute_prems:k", k, [rl]) in (*no fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (Permute_prems (j,k), [der]), + der = Pt.infer_derivs' (Pt.permute_prems_prf prems j k) der, maxidx = maxidx, shyps = shyps, hyps = hyps, @@ -1350,7 +1184,7 @@ state) | [] => fix_shyps [state] [] (Thm{sign_ref = sign_ref, - der = infer_derivs (Rename_params_rule(cs,i), [der]), + der = der, maxidx = maxidx, shyps = [], hyps = hyps, @@ -1471,7 +1305,7 @@ val sign_ref = merge_thm_sgs(state,orule); val sign = Sign.deref sign_ref; (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) - fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = + fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = let val normt = Envir.norm_term env; (*perform minimal copying here by examining env*) val normp = @@ -1489,22 +1323,29 @@ end val th = (*tuned fix_shyps*) Thm{sign_ref = sign_ref, - der = infer_derivs (Bicompose(match, eres_flg, - 1 + length Bs, nsubgoal, env), - [rder,sder]), + der = Pt.infer_derivs + ((if Envir.is_empty env then I + else if Envir.above (smax, env) then + (fn f => fn der => f (Pt.norm_proof' env der)) + else + curry op oo (Pt.norm_proof' env)) + (Pt.bicompose_proof Bs oldAs As A n)) rder' sder, maxidx = maxidx, shyps = add_env_sorts (env, union_sort(rshyps,sshyps)), hyps = union_term(rhyps,shyps), prop = Logic.rule_of normp} - in Seq.cons(th, thq) end handle COMPOSE => thq + in Seq.cons(th, thq) end handle COMPOSE => thq; val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); (*Modify assumptions, deleting n-th if n>0 for e-resolution*) fun newAs(As0, n, dpairs, tpairs) = - let val As1 = if !Logic.auto_rename orelse not lifted then As0 - else map (rename_bvars(dpairs,tpairs,B)) As0 - in (map (Logic.flatten_params n) As1) + let val (As1, rder') = + if !Logic.auto_rename orelse not lifted then (As0, rder) + else (map (rename_bvars(dpairs,tpairs,B)) As0, + Pt.infer_derivs' (Pt.map_proof_terms + (rename_bvars (dpairs, tpairs, Bound 0)) I) rder); + in (map (Logic.flatten_params n) As1, As1, rder', n) handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; @@ -1512,20 +1353,20 @@ val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); val dpairs = BBi :: (rtpairs@stpairs); (*elim-resolution: try each assumption in turn. Initially n=1*) - fun tryasms (_, _, []) = Seq.empty - | tryasms (As, n, (t,u)::apairs) = + fun tryasms (_, _, _, []) = Seq.empty + | tryasms (A, As, n, (t,u)::apairs) = (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of - None => tryasms (As, n+1, apairs) + None => tryasms (A, As, n+1, apairs) | cell as Some((_,tpairs),_) => - Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs))) + Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs))) (Seq.make (fn()=> cell), - Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs))))); + Seq.make (fn()=> Seq.pull (tryasms (A, As, n+1, apairs))))); fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) - | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); + | eres (A1::As) = tryasms (Some A1, As, 1, Logic.assum_pairs A1); (*ordinary resolution*) fun res(None) = Seq.empty | res(cell as Some((_,tpairs),_)) = - Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) + Seq.it_right (addth None (newAs(rev rAs, 0, [BBi], tpairs))) (Seq.make (fn()=> cell), Seq.empty) in if eres_flg then eres(rev rAs) else res(Seq.pull(Unify.unifiers(sign, env, dpairs))) @@ -1584,7 +1425,7 @@ raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else fix_shyps [] [] (Thm {sign_ref = sign_ref', - der = (true, Join (Oracle (name, sign, exn), [])), + der = (true, Pt.oracle_proof name prop), maxidx = maxidx, shyps = [], hyps = [],