# HG changeset patch # User paulson # Date 846858928 -3600 # Node ID 0698ddfbf6e498ecd505f0a791d47a3266e0c849 # Parent 6854b692f1fe117662ae7b4a296f4ccdd9757b1e Now uses Int.max instead of max nodup_Vars now updates maxidx diff -r 6854b692f1fe -r 0698ddfbf6e4 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Nov 01 15:32:03 1996 +0100 +++ b/src/Pure/thm.ML Fri Nov 01 15:35:28 1996 +0100 @@ -217,21 +217,23 @@ end | dest_abs _ = raise CTERM "dest_abs"; -fun adjust_maxidx (Cterm {sign, T, t, ...}) = - Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t} +(*Makes maxidx precise: it is often too big*) +fun adjust_maxidx (ct as Cterm {sign, T, t, maxidx, ...}) = + if maxidx = ~1 then ct + else Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t}; (*Form cterm out of a function and an argument*) fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) (Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) = if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty, - maxidx=max[maxidx1, maxidx2]} + maxidx=Int.max(maxidx1, maxidx2)} else raise CTERM "capply: types don't agree" | capply _ _ = raise CTERM "capply: first arg is not a function" fun cabs (Cterm {t=Free(a,ty), sign=sign1, T=T1, maxidx=maxidx1}) (Cterm {t=t2, sign=sign2, T=T2, maxidx=maxidx2}) = Cterm {t=absfree(a,ty,t2), sign=Sign.merge(sign1,sign2), - T = ty --> T2, maxidx=max[maxidx1, maxidx2]} + T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)} | cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; (** read cterms **) (*exception ERROR*) @@ -571,9 +573,18 @@ (*** Meta rules ***) -(* check that term does not contain same var with different typing/sorting *) -fun nodup_Vars(thm as Thm{prop,...}) s = - Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]); +(*Check that term does not contain same var with different typing/sorting. + If this check must be made, recalculate maxidx in hope of preventing its + recurrence.*) +fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s = + (Sign.nodup_Vars prop; + Thm {sign = sign, + der = der, + maxidx = maxidx_of_term prop, + shyps = shyps, + hyps = hyps, + prop = prop}) + handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); (** 'primitive' rules **) @@ -608,7 +619,7 @@ else fix_shyps [thB] [] (Thm{sign = Sign.merge (sign,signA), der = infer_derivs (Implies_intr cA, [der]), - maxidx = max[maxidxA, maxidx], + maxidx = Int.max(maxidxA, maxidx), shyps = [], hyps = disch(hyps,A), prop = implies$A$prop}) @@ -632,7 +643,7 @@ then fix_shyps [thAB, thA] [] (Thm{sign= merge_thm_sgs(thAB,thA), der = infer_derivs (Implies_elim, [der,derA]), - maxidx = max[maxA,maxidx], + maxidx = Int.max(maxA,maxidx), shyps = [], hyps = hypsA union hyps, (*dups suppressed*) prop = B}) @@ -671,22 +682,21 @@ fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm = let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct in case prop of - Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => - if T<>qary then - raise THM("forall_elim: type mismatch", 0, [th]) - else let val thm = fix_shyps [th] [] - (Thm{sign= Sign.merge(sign,signt), - der = infer_derivs (Forall_elim ct, [der]), - maxidx = max[maxidx, maxt], - shyps = [], - hyps = hyps, - prop = betapply(A,t)}) - in if maxt >= 0 andalso maxidx >= 0 - then nodup_Vars thm "forall_elim" - else () (*no new Vars: no expensive check!*) ; - thm - end - | _ => raise THM("forall_elim: not quantified", 0, [th]) + Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => + if T<>qary then + raise THM("forall_elim: type mismatch", 0, [th]) + else let val thm = fix_shyps [th] [] + (Thm{sign= Sign.merge(sign,signt), + der = infer_derivs (Forall_elim ct, [der]), + maxidx = Int.max(maxidx, maxt), + shyps = [], + hyps = hyps, + prop = betapply(A,t)}) + in if maxt >= 0 andalso maxidx >= 0 + then nodup_Vars thm "forall_elim" + else thm (*no new Vars: no expensive check!*) + end + | _ => raise THM("forall_elim: not quantified", 0, [th]) end handle TERM _ => raise THM("forall_elim: incompatible signatures", 0, [th]); @@ -749,14 +759,13 @@ fix_shyps [th1, th2] [] (Thm{sign= merge_thm_sgs(th1,th2), der = infer_derivs (Transitive, [der1, der2]), - maxidx = max[max1,max2], + maxidx = Int.max(max1,max2), shyps = [], hyps = hyps1 union hyps2, prop = eq$t1$t2}) in if max1 >= 0 andalso max2 >= 0 - then nodup_Vars thm "transitive" - else () (*no new Vars: no expensive check!*) ; - thm + then nodup_Vars thm "transitive" + else thm (*no new Vars: no expensive check!*) end | _ => err"premises" end; @@ -768,7 +777,7 @@ Abs(_,_,bodt) $ u => fix_shyps [] [] (Thm{sign = sign, der = infer_derivs (Beta_conversion ct, []), - maxidx = maxidx_of_term t, + maxidx = maxidx, shyps = [], hyps = [], prop = Logic.mk_equals(t, subst_bounds([u],bodt))}) @@ -855,14 +864,13 @@ val thm = (*no fix_shyps*) Thm{sign = merge_thm_sgs(th1,th2), der = infer_derivs (Combination, [der1, der2]), - maxidx = max[max1,max2], + maxidx = Int.max(max1,max2), shyps = shyps1 union shyps2, hyps = hyps1 union hyps2, prop = Logic.mk_equals(f$t, g$u)} in if max1 >= 0 andalso max2 >= 0 then nodup_Vars thm "combination" - else () (*no new Vars: no expensive check!*) ; - thm + else thm (*no new Vars: no expensive check!*) end | _ => raise THM("combination: premises", 0, [th1,th2]) end; @@ -886,7 +894,7 @@ (*no fix_shyps*) Thm{sign = merge_thm_sgs(th1,th2), der = infer_derivs (Equal_intr, [der1, der2]), - maxidx = max[max1,max2], + maxidx = Int.max(max1,max2), shyps = shyps1 union shyps2, hyps = hyps1 union hyps2, prop = Logic.mk_equals(A,B)} @@ -910,7 +918,7 @@ fix_shyps [th1, th2] [] (Thm{sign= merge_thm_sgs(th1,th2), der = infer_derivs (Equal_elim, [der1, der2]), - maxidx = max[max1,max2], + maxidx = Int.max(max1,max2), shyps = [], hyps = hyps1 union hyps2, prop = B}) @@ -1003,8 +1011,7 @@ then raise THM("instantiate: variables not distinct", 0, [th]) else if not(null(findrep(map #1 vTs))) then raise THM("instantiate: type variables not distinct", 0, [th]) - else nodup_Vars newth "instantiate"; - newth + else nodup_Vars newth "instantiate" end handle TERM _ => raise THM("instantiate: incompatible signatures",0,[th]) @@ -1048,11 +1055,11 @@ in let val thm = (*no fix_shyps*) Thm{sign = sign, der = infer_derivs (VarifyT, [der]), - maxidx = max[0,maxidx], + maxidx = Int.max(0,maxidx), shyps = shyps, hyps = hyps, prop = Type.varify(prop,tfrees)} - in nodup_Vars thm "varifyT"; thm end + in nodup_Vars thm "varifyT" end (* this nodup_Vars check can be removed if thms are guaranteed not to contain duplicate TVars with differnt sorts *) end; @@ -1278,7 +1285,7 @@ if Envir.is_empty env then (tpairs, Bs @ As, C) else let val ntps = map (pairself normt) tpairs - in if the (Envir.minidx env) > smax then + in if Envir.above (smax, env) then (*no assignments in state; normalize the rule only*) if lifted then (ntps, Bs @ map (norm_term_skip env nlift) As, C) @@ -1308,7 +1315,7 @@ handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; - val env = Envir.empty(max[rmax,smax]); + val env = Envir.empty(Int.max(rmax,smax)); 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*) @@ -1581,16 +1588,16 @@ (*Conversion to apply the meta simpset to a term*) fun rewritec (prover,signt) (mss as Mss{net,...}) - (shypst,hypst,maxidxt,t,ders) = + (shypst,hypst,maxt,t,ders) = let val etat = Pattern.eta_contract t; fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} = let val unit = if Sign.subsig(sign,signt) then () else (trace_thm_warning "rewrite rule from different theory" thm; raise Pattern.MATCH) - val rprop = if maxidxt = ~1 then prop - else Logic.incr_indexes([],maxidxt+1) prop; - val rlhs = if maxidxt = ~1 then lhs + val rprop = if maxt = ~1 then prop + else Logic.incr_indexes([],maxt+1) prop; + val rlhs = if maxt = ~1 then lhs else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat) val prop' = ren_inst(insts,rprop,rlhs,t); @@ -1634,21 +1641,21 @@ in sort rrs ([],[]) end in case etat of - Abs(_,_,body) $ u => Some(shypst, hypst, maxidxt, + Abs(_,_,body) $ u => Some(shypst, hypst, maxt, subst_bounds([u], body), ders) | _ => rews (sort_rrules (Net.match_term net etat)) end; (*Conversion to apply a congruence rule to a term*) -fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxidxt,t,ders) = +fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) = let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong val unit = if Sign.subsig(sign,signt) then () else error("Congruence rule from different theory") val tsig = #tsig(Sign.rep_sg signt) - val rprop = if maxidxt = ~1 then prop - else Logic.incr_indexes([],maxidxt+1) prop; - val rlhs = if maxidxt = ~1 then lhs + val rprop = if maxt = ~1 then prop + else Logic.incr_indexes([],maxt+1) prop; + val rlhs = if maxt = ~1 then lhs else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) val insts = Pattern.match tsig (rlhs,t) (* Pattern.match can raise Pattern.MATCH; @@ -1723,15 +1730,15 @@ Some(shyps1,hyps1,maxidx1,t1,ders1) => (case botc true mss (shyps1,hyps1,maxidx,u,ders1) of Some(shyps2,hyps2,maxidx2,u1,ders2) => - Some(shyps2, hyps2, max[maxidx1,maxidx2], + Some(shyps2, hyps2, Int.max(maxidx1,maxidx2), t1$u1, ders2) | None => - Some(shyps1, hyps1, max[maxidx1,maxidx], t1$u, + Some(shyps1, hyps1, Int.max(maxidx1,maxidx), t1$u, ders1)) | None => (case botc true mss (shyps,hyps,maxidx,u,ders) of Some(shyps1,hyps1,maxidx1,u1,ders1) => - Some(shyps1, hyps1, max[maxidx,maxidx1], + Some(shyps1, hyps1, Int.max(maxidx,maxidx1), t$u1, ders1) | None => None)) val (h,ts) = strip_comb t @@ -1758,7 +1765,7 @@ val (shyps2,hyps2,maxidx2,u1,ders2) = try_botc mss1 (shyps1,hyps1,maxidx,u,ders1) val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 - in (shyps2, hyps3, max[maxidx1,maxidx2], + in (shyps2, hyps3, Int.max(maxidx1,maxidx2), Logic.mk_implies(s1,u1), ders2) end @@ -1774,14 +1781,14 @@ (*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***) fun rewrite_cterm mode mss prover ct = let val {sign, t, T, maxidx} = rep_cterm ct; - val (shyps,hyps,maxidxu,u,ders) = + val (shyps,hyps,maxu,u,ders) = bottomc (mode,prover,sign) mss (add_term_sorts(t,[]), [], maxidx, t, []); val prop = Logic.mk_equals(t,u) in Thm{sign = sign, der = infer_derivs (Rewrite_cterm ct, ders), - maxidx = max[maxidx,maxidxu], + maxidx = Int.max (maxidx,maxu), shyps = shyps, hyps = hyps, prop = prop}