# HG changeset patch # User wenzelm # Date 1702292778 -3600 # Node ID 1f59664dab5170bb5bdaca815faf2b446d2e6664 # Parent 42b2177a9d19c8ca098c3c6eff3ed847bba26479 tuned whitespace; diff -r 42b2177a9d19 -r 1f59664dab51 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Dec 11 11:50:50 2023 +0100 +++ b/src/Pure/thm.ML Mon Dec 11 12:06:18 2023 +0100 @@ -2311,112 +2311,115 @@ nsubgoal is the number of new subgoals (written m above). Curried so that resolution calls dest_state only once. *) -local exception COMPOSE -in +local exception COMPOSE in + fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted) - (eres_flg, orule, nsubgoal) = - let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state - and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1, - tpairs=rtpairs, 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) - val (context, cert) = - make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule)); - (*Add new theorem with prop = "\Bs; As\ \ C" to thq*) - fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = - let val normt = Envir.norm_term env; - (*perform minimal copying here by examining env*) - val (ntpairs, normp) = - if Envir.is_empty env then (tpairs, (Bs @ As, C)) - else - let val ntps = map (apply2 normt) tpairs - in if Envir.above env smax then - (*no assignments in state; normalize the rule only*) - if lifted - then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) - else (ntps, (Bs @ map normt As, C)) - else if match then raise COMPOSE - else (*normalize the new rule fully*) - (ntps, (map normt (Bs @ As), normt C)) - end - val thy' = Context.certificate_theory cert handle ERROR msg => - raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt); - val constraints' = - union_constraints constraints1 constraints2 - |> insert_constraints_env thy' env; - fun zproof p q = ZTerm.todo_proof p; - fun bicompose_proof p q = - Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) p q; - val proof = - if Envir.is_empty env then bicompose_proof - else if Envir.above env smax - then bicompose_proof o Proofterm.norm_proof_remove_types env - else Proofterm.norm_proof_remove_types env oo bicompose_proof; - val th = - Thm (deriv_rule2 zproof proof rder' sder, - {tags = [], - maxidx = Envir.maxidx_of env, - constraints = constraints', - shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), - hyps = union_hyps hyps1 hyps2, - tpairs = ntpairs, - prop = Logic.list_implies normp, - cert = cert}) - in Seq.cons th thq end handle COMPOSE => thq; - val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) - 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, rder') = - if not lifted then (As0, rder) - else - let - val rename = rename_bvars dpairs tpairs B As0; - fun proof p = Proofterm.map_proof_terms (rename K) I p; - fun zproof p = ZTerm.todo_proof p; - in (map (rename strip_apply) As0, deriv_rule1 zproof proof rder) end; - in (if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n) - handle TERM _ => - raise THM("bicompose: 1st premise", 0, [orule]) - end; - val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); - val dpairs = BBi :: (rtpairs@stpairs); + (eres_flg, orule, nsubgoal) = + let + val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state + and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1, + tpairs = rtpairs, 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); + val (context, cert) = + make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule)); + (*Add new theorem with prop = "\Bs; As\ \ C" to thq*) + fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = + let + val normt = Envir.norm_term env; + (*perform minimal copying here by examining env*) + val (ntpairs, normp) = + if Envir.is_empty env then (tpairs, (Bs @ As, C)) + else + let val ntps = map (apply2 normt) tpairs in + if Envir.above env smax then + (*no assignments in state; normalize the rule only*) + if lifted + then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) + else (ntps, (Bs @ map normt As, C)) + else if match then raise COMPOSE + else (*normalize the new rule fully*) + (ntps, (map normt (Bs @ As), normt C)) + end; + val thy' = Context.certificate_theory cert handle ERROR msg => + raise CONTEXT (msg, [], [], [state, orule], Option.map Context.Proof opt_ctxt); + val constraints' = + union_constraints constraints1 constraints2 + |> insert_constraints_env thy' env; + fun zproof p q = ZTerm.todo_proof p; + fun bicompose_proof p q = + Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) p q; + val proof = + if Envir.is_empty env then bicompose_proof + else if Envir.above env smax + then bicompose_proof o Proofterm.norm_proof_remove_types env + else Proofterm.norm_proof_remove_types env oo bicompose_proof; + val th = + Thm (deriv_rule2 zproof proof rder' sder, + {tags = [], + maxidx = Envir.maxidx_of env, + constraints = constraints', + shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), + hyps = union_hyps hyps1 hyps2, + tpairs = ntpairs, + prop = Logic.list_implies normp, + cert = cert}) + in Seq.cons th thq end handle COMPOSE => thq; + val (rAs, B) = Logic.strip_prems (nsubgoal, [], rprop) + 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, rder') = + if not lifted then (As0, rder) + else + let + val rename = rename_bvars dpairs tpairs B As0; + fun proof p = Proofterm.map_proof_terms (rename K) I p; + fun zproof p = ZTerm.todo_proof p; + in (map (rename strip_apply) As0, deriv_rule1 zproof proof rder) end; + in + (if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n) + handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) + end; + val BBi = if lifted then strip_assums2 (B, Bi) else (B, Bi); + val dpairs = BBi :: (rtpairs @ stpairs); - (*elim-resolution: try each assumption in turn*) - fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) - | eres env (A1 :: As) = - let - val A = SOME A1; - val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); - val concl' = close concl; - fun tryasms [] _ = Seq.empty - | tryasms (asm :: rest) n = - if Term.could_unify (asm, concl) then - let val asm' = close asm in - (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of - NONE => tryasms rest (n + 1) - | cell as SOME ((_, tpairs), _) => - Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) - (Seq.make (fn () => cell), - Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) - end - else tryasms rest (n + 1); - in tryasms asms 1 end; + (*elim-resolution: try each assumption in turn*) + fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) + | eres env (A1 :: As) = + let + val A = SOME A1; + val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); + val concl' = close concl; + fun tryasms [] _ = Seq.empty + | tryasms (asm :: rest) n = + if Term.could_unify (asm, concl) then + let val asm' = close asm in + (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of + NONE => tryasms rest (n + 1) + | cell as SOME ((_, tpairs), _) => + Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) + (Seq.make (fn () => cell), + Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) + end + else tryasms rest (n + 1); + in tryasms asms 1 end; (*ordinary resolution*) - fun res env = - (case Seq.pull (Unify.unifiers (context, env, dpairs)) of - NONE => Seq.empty - | cell as SOME ((_, tpairs), _) => - Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) - (Seq.make (fn () => cell), Seq.empty)); + fun res env = + (case Seq.pull (Unify.unifiers (context, env, dpairs)) of + NONE => Seq.empty + | cell as SOME ((_, tpairs), _) => + Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) + (Seq.make (fn () => cell), Seq.empty)); - val env0 = Envir.empty (Int.max (rmax, smax)); - in - (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of - NONE => Seq.empty - | SOME env => if eres_flg then eres env (rev rAs) else res env) - end; + val env0 = Envir.empty (Int.max (rmax, smax)); + in + (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of + NONE => Seq.empty + | SOME env => if eres_flg then eres env (rev rAs) else res env) + end; + end; fun bicompose opt_ctxt flags arg i state =