# HG changeset patch # User wenzelm # Date 811675604 -7200 # Node ID 2a2d8c74a756bae85fd3a95e762a2e9dc61328f3 # Parent ec738ecb911c2ec25c197f600c69eb006bcea868 bicompose_aux: tuned fix_shyps; simplifier: fixed handling of shyps; diff -r ec738ecb911c -r 2a2d8c74a756 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Sep 21 11:23:30 1995 +0200 +++ b/src/Pure/thm.ML Thu Sep 21 11:26:44 1995 +0200 @@ -289,6 +289,12 @@ fun add_terms_sorts ([], Ss) = Ss | add_terms_sorts (t :: ts, Ss) = add_terms_sorts (ts, add_term_sorts (t, Ss)); +fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; + +fun add_env_sorts (env, Ss) = + add_terms_sorts (map snd (Envir.alist_of env), + add_typs_sorts (env_codT env, Ss)); + fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) = add_terms_sorts (hyps, add_term_sorts (prop, Ss)); @@ -315,8 +321,6 @@ shyps = shyps, hyps = hyps, prop = prop} end; -fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; - (* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) @@ -1103,8 +1107,8 @@ in fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) (eres_flg, orule, nsubgoal) = - let val Thm{maxidx=smax, hyps=shyps, ...} = state - and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule + let val Thm{maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state + and Thm{maxidx=rmax, shyps=rshyps, hyps=rhyps, prop=rprop,...} = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems(strip_all_body Bi, if eres_flg then ~1 else 0) @@ -1126,10 +1130,11 @@ else (*normalize the new rule fully*) (ntps, map normt (Bs @ As), normt C) end - val th = (* FIXME improve *) - fix_shyps [state, orule] (env_codT env) - (Thm{sign=sign, shyps=[], hyps=rhyps union shyps, - maxidx=maxidx, prop= Logic.rule_of normp}) + val th = (*tuned fix_shyps*) + Thm{sign=sign, + shyps=add_env_sorts (env, rshyps union sshyps), + hyps=rhyps union shyps, + maxidx=maxidx, prop= Logic.rule_of normp} in cons(th, thq) end handle Bicompose => thq val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) @@ -1251,7 +1256,7 @@ fun mk_rrule raw_thm = let - val thm = strip_shyps raw_thm; (* FIXME tmp *) + val thm = strip_shyps raw_thm; val Thm{sign,prop,maxidx,...} = thm; val prems = Logic.strip_imp_prems prop val concl = Logic.strip_imp_concl prop @@ -1262,9 +1267,7 @@ val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) andalso not(is_Var(elhs)) in - if not (null (extra_shyps thm)) then (* FIXME tmp *) - raise SIMPLIFIER ("Rewrite rule may not contain extra sort hypotheses", thm) - else if not perm andalso loops sign prems (elhs,erhs) then + if not perm andalso loops sign prems (elhs,erhs) then (prtm "Warning: ignoring looping rewrite rule" sign prop; None) else Some{thm=thm,lhs=lhs,perm=perm} end; @@ -1380,7 +1383,7 @@ fun termless tu = (termord tu = LESS); -fun check_conv(thm as Thm{hyps,prop,sign,maxidx,...}, prop0) = +fun check_conv(thm as Thm{shyps,hyps,prop,sign,maxidx,...}, prop0) = let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; trace_term "Should have proved" sign prop0; None) @@ -1389,7 +1392,7 @@ Const("==",_) $ lhs $ rhs => if (lhs = lhs0) orelse (lhs aconv Envir.norm_term (Envir.empty 0) lhs0) - then (trace_thm "SUCCEEDED" thm; Some(hyps,maxidx,rhs)) + then (trace_thm "SUCCEEDED" thm; Some(shyps,hyps,maxidx,rhs)) else err() | _ => err() end; @@ -1402,11 +1405,14 @@ | renAbs(t) = t in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; +fun add_insts_sorts ((iTs, is), Ss) = + add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); + (*Conversion to apply the meta simpset to a term*) -fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,maxidxt,t) = +fun rewritec (prover,signt) (mss as Mss{net,...}) (shypst,hypst,maxidxt,t) = let val etat = Pattern.eta_contract t; - fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = + fun rew {thm as Thm{sign,shyps,hyps,maxidx,prop,...}, lhs, perm} = let val unit = if Sign.subsig(sign,signt) then () else (trace_thm"Warning: rewrite rule from different theory" thm; @@ -1418,14 +1424,14 @@ 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 shyps' = add_insts_sorts (insts, shyps union shypst); val maxidx' = maxidx_of_term prop' - val thm' = fix_shyps [thm] [] (* FIXME ??? *) - (Thm{sign=signt, shyps=[], hyps=hyps', - prop=prop', maxidx=maxidx'}) + val thm' = Thm{sign=signt, shyps=shyps', 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',maxidx',rhs')) + then (trace_thm "Rewriting:" thm'; Some(shyps',hyps',maxidx',rhs')) else (trace_thm "Trying to rewrite:" thm'; case prover mss thm' of None => (trace_thm "FAILED" thm'; None) @@ -1438,13 +1444,13 @@ in case opt of None => rews rrules | some => some end; in case etat of - Abs(_,_,body) $ u => Some(hypst, maxidxt, subst_bounds([u], body)) + Abs(_,_,body) $ u => Some(shypst, 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,maxidxt,t) = - let val Thm{sign,hyps,maxidx,prop,...} = cong +fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxidxt,t) = + let val Thm{sign,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) @@ -1455,9 +1461,9 @@ val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH => error("Congruence rule did not match") val prop' = ren_inst(insts,rprop,rlhs,t); - val thm' = fix_shyps [cong] [] (* FIXME ??? *) - (Thm{sign=signt, shyps=[], hyps=hyps union hypst, - prop=prop', maxidx=maxidx_of_term prop'}) + val shyps' = add_insts_sorts (insts, shyps union shypst); + val thm' = Thm{sign=signt, shyps=shyps', hyps=hyps union hypst, + prop=prop', maxidx=maxidx_of_term prop'}; val unit = trace_thm "Applying congruence rule" thm'; fun err() = error("Failed congruence proof!") @@ -1486,39 +1492,39 @@ | None => trec) and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) - (trec as (hyps,maxidx,t)) = + (trec as (shyps,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,maxidx,subst_bounds([v],t)) of - Some(hyps',maxidx',t') => - Some(hyps', maxidx', Abs(a, T, abstract_over(v,t'))) + in case botc true mss' (shyps,hyps,maxidx,subst_bounds([v],t)) of + Some(shyps',hyps',maxidx',t') => + Some(shyps', hyps', maxidx', Abs(a, T, abstract_over(v,t'))) | None => None end | t$u => (case t of - Const("==>",_)$s => Some(impc(hyps,maxidx,s,u,mss)) + Const("==>",_)$s => Some(impc(shyps,hyps,maxidx,s,u,mss)) | Abs(_,_,body) => - let val trec = (hyps,maxidx,subst_bounds([u], body)) + let val trec = (shyps,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,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) + (case botc true mss (shyps,hyps,maxidx,t) of + Some(shyps1,hyps1,maxidx1,t1) => + (case botc true mss (shyps1,hyps1,maxidx,u) of + Some(shyps2,hyps2,maxidx2,u1) => + Some(shyps2,hyps2,max[maxidx1,maxidx2],t1$u1) | None => - Some(hyps1,max[maxidx1,maxidx],t1$u)) + Some(shyps1,hyps1,max[maxidx1,maxidx],t1$u)) | None => - (case botc true mss (hyps,maxidx,u) of - Some(hyps1,maxidx1,u1) => - Some(hyps1,max[maxidx,maxidx1],t$u1) + (case botc true mss (shyps,hyps,maxidx,u) of + Some(shyps1,hyps1,maxidx1,u1) => + Some(shyps1,hyps1,max[maxidx,maxidx1],t$u1) | None => None)) val (h,ts) = strip_comb t in case h of @@ -1530,18 +1536,20 @@ end) | _ => None) - 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); + and impc(shyps,hyps,maxidx,s,u,mss as Mss{mk_rews,...}) = + let val (shyps1,hyps1,_,s1) = + if simprem then try_botc mss (shyps,hyps,maxidx,s) + else (shyps,hyps,0,s); val maxidx1 = maxidx_of_term s1 val mss1 = if not useprem orelse maxidx1 <> ~1 then mss - else let val thm = fix_shyps [] [] (* FIXME ??? *) - (Thm{sign=sign,shyps=[],hyps=[s1],prop=s1,maxidx= ~1}) + else let val thm = + Thm{sign=sign,shyps=add_term_sorts(s1,[]), + hyps=[s1],prop=s1,maxidx= ~1} in add_simps(add_prems(mss,[thm]), mk_rews thm) end - val (hyps2,maxidx2,u1) = try_botc mss1 (hyps1,maxidx,u) + val (shyps2,hyps2,maxidx2,u1) = try_botc mss1 (shyps1,hyps1,maxidx,u) val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 - in (hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end + in (shyps2, hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end in try_botc end; @@ -1552,15 +1560,15 @@ mss: contains equality theorems of the form [|p1,...|] ==> t==u prover: how to solve premises in conditional rewrites and congruences *) -(* FIXME: better handling of shyps *) (*** 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,maxidxu,u) = bottomc (mode,prover,sign) mss ([],maxidx,t); + val (shyps,hyps,maxidxu,u) = + bottomc (mode,prover,sign) mss (add_term_sorts(t,[]),[],maxidx,t); val prop = Logic.mk_equals(t,u) - in fix_shyps [] [] - (Thm{sign= sign, shyps=[], hyps= hyps, maxidx= max[maxidx,maxidxu], - prop= prop}) + in + Thm{sign= sign, shyps= shyps, hyps= hyps, maxidx= max[maxidx,maxidxu], + prop= prop} end end;