# HG changeset patch # User nipkow # Date 798026384 -7200 # Node ID 8425cb5acb7778a2317d41433ca952e445dcedfd # Parent 5d6fb2c938e0254e63f3cf5196c51896df31701b Fixed old bug in the simplifier. Term to be simplified now carries around its maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1 in most cases (ie no Vars), hence reasonable overhead. diff -r 5d6fb2c938e0 -r 8425cb5acb77 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Apr 16 11:56:11 1995 +0200 +++ b/src/Pure/thm.ML Sun Apr 16 11:59:44 1995 +0200 @@ -1203,7 +1203,7 @@ fun termless tu = (termord tu = LESS); -fun check_conv(thm as Thm{hyps,prop,sign,...}, prop0) = +fun check_conv(thm as Thm{hyps,prop,sign,maxidx,...}, prop0) = let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; trace_term "Should have proved" sign prop0; None) @@ -1212,7 +1212,7 @@ Const("==",_) $ lhs $ rhs => if (lhs = lhs0) orelse (lhs aconv Envir.norm_term (Envir.empty 0) lhs0) - then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) + then (trace_thm "SUCCEEDED" thm; Some(hyps,maxidx,rhs)) else err() | _ => err() end; @@ -1227,22 +1227,26 @@ (*Conversion to apply the meta simpset to a term*) -fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = +fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,maxidxt,t) = let val etat = Pattern.eta_contract t; fun rew {thm as Thm{sign,hyps,maxidx,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 insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,etat) - val prop' = ren_inst(insts,prop,lhs,t); + val rprop = if maxidxt = ~1 then prop + else Logic.incr_indexes([],maxidxt+1) prop; + val rlhs = if maxidxt = ~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); val hyps' = hyps union hypst; - val thm' = Thm{sign=signt, hyps=hyps', prop=prop', - maxidx=maxidx_of_term prop'} + val maxidx' = maxidx_of_term prop' + val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx'} val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') in if perm andalso not(termless(rhs',lhs')) then None else if Logic.count_prems(prop',0) = 0 - then (trace_thm "Rewriting:" thm'; Some(hyps',rhs')) + then (trace_thm "Rewriting:" thm'; Some(hyps',maxidx',rhs')) else (trace_thm "Trying to rewrite:" thm'; case prover mss thm' of None => (trace_thm "FAILED" thm'; None) @@ -1255,19 +1259,23 @@ in case opt of None => rews rrules | some => some end; in case etat of - Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body)) + Abs(_,_,body) $ u => Some(hypst, maxidxt, subst_bounds([u], body)) | _ => rews(Net.match_term net etat) end; (*Conversion to apply a congruence rule to a term*) -fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) = +fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,maxidxt,t) = let val Thm{sign,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 insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => + val rprop = if maxidxt = ~1 then prop + else Logic.incr_indexes([],maxidxt+1) prop; + val rlhs = if maxidxt = ~1 then lhs + else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) + val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH => error("Congruence rule did not match") - val prop' = ren_inst(insts,prop,lhs,t); + val prop' = ren_inst(insts,rprop,rlhs,t); val thm' = Thm{sign=signt, hyps=hyps union hypst, prop=prop', maxidx=maxidx_of_term prop'} val unit = trace_thm "Applying congruence rule" thm'; @@ -1298,36 +1306,39 @@ | None => trec) and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) - (trec as (hyps,t)) = + (trec as (hyps,maxidx,t)) = (case t of Abs(a,T,t) => let val b = variant bounds a val v = Free("." ^ b,T) val mss' = Mss{net=net, congs=congs, bounds=b::bounds, prems=prems,mk_rews=mk_rews} - in case botc true mss' (hyps,subst_bounds([v],t)) of - Some(hyps',t') => - Some(hyps', Abs(a, T, abstract_over(v,t'))) + in case botc true mss' (hyps,maxidx,subst_bounds([v],t)) of + Some(hyps',maxidx',t') => + Some(hyps', maxidx', Abs(a, T, abstract_over(v,t'))) | None => None end | t$u => (case t of - Const("==>",_)$s => Some(impc(hyps,s,u,mss)) + Const("==>",_)$s => Some(impc(hyps,maxidx,s,u,mss)) | Abs(_,_,body) => - let val trec = (hyps,subst_bounds([u], body)) + let val trec = (hyps,maxidx,subst_bounds([u], body)) in case subc mss trec of None => Some(trec) | trec => trec end | _ => let fun appc() = - (case botc true mss (hyps,t) of - Some(hyps1,t1) => - (case botc true mss (hyps1,u) of - Some(hyps2,u1) => Some(hyps2,t1$u1) - | None => Some(hyps1,t1$u)) + (case botc true mss (hyps,maxidx,t) of + Some(hyps1,maxidx1,t1) => + (case botc true mss (hyps1,maxidx,u) of + Some(hyps2,maxidx2,u1) => + Some(hyps2,max[maxidx1,maxidx2],t1$u1) + | None => + Some(hyps1,max[maxidx1,maxidx],t1$u)) | None => - (case botc true mss (hyps,u) of - Some(hyps1,u1) => Some(hyps1,t$u1) + (case botc true mss (hyps,maxidx,u) of + Some(hyps1,maxidx1,u1) => + Some(hyps1,max[maxidx,maxidx1],t$u1) | None => None)) val (h,ts) = strip_comb t in case h of @@ -1339,16 +1350,17 @@ end) | _ => None) - and impc(hyps,s,u,mss as Mss{mk_rews,...}) = - let val (hyps1,s1) = if simprem then try_botc mss (hyps,s) - else (hyps,s) + and impc(hyps,maxidx,s,u,mss as Mss{mk_rews,...}) = + let val (hyps1,_,s1) = if simprem then try_botc mss (hyps,maxidx,s) + else (hyps,0,s); + val maxidx1 = maxidx_of_term s1 val mss1 = - if not useprem orelse maxidx_of_term s1 <> ~1 then mss + if not useprem orelse maxidx1 <> ~1 then mss else let val thm = Thm{sign=sign,hyps=[s1],prop=s1,maxidx= ~1} in add_simps(add_prems(mss,[thm]), mk_rews thm) end - val (hyps2,u1) = try_botc mss1 (hyps1,u) + val (hyps2,maxidx2,u1) = try_botc mss1 (hyps1,maxidx,u) val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 - in (hyps3, Logic.mk_implies(s1,u1)) end + in (hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end in try_botc end; @@ -1363,9 +1375,9 @@ (*** 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 (hyps,u) = bottomc (mode,prover,sign) mss ([],t); + val (hyps,maxidxu,u) = bottomc (mode,prover,sign) mss ([],maxidx,t); val prop = Logic.mk_equals(t,u) - in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} + in Thm{sign= sign, hyps= hyps, maxidx= max[maxidx,maxidxu], prop= prop} end end;