From: Manuel Eberl <eberlm@in.tum.de>

Somebody asked a question of StackOverflow [1] about why the "subst"

method (which should only affect the first subgoal) implicitly

discharges duplicate subgoals. I checked the code and found that it

somehow calls "distinct_subgoals_tac" somewhere, although I find the

code very difficult to read:

fun eqsubst_tac ctxt occs thms i st =

let val nprems = Thm.nprems_of st in

if nprems < i then Seq.empty else

let

val thmseq = Seq.of_list thms;

fun apply_occ occ st =

thmseq |> Seq.maps (fn r =>

eqsubst_tac' ctxt

(skip_first_occs_search occ searchf_lr_unify_valid) r

(i + (Thm.nprems_of st - nprems)) st);

val sorted_occs = Library.sort (rev_order o int_ord) occs;

in

Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ

sorted_occs) st)

end

end;

In any case, it seems to me that this violates the usual contract that a

tactic that takes a subgoal index should only affect that one subgoal.

I have no idea why it calls distinct_subgoals_tac in the first place. A

simple solution would be to just wrap the entire thing in a

"SELECT_GOAL". The performance impact should be minimal since this

tactic is typically used very sparingly for single rewrite steps; any

heavy rewriting is done with the simplifier anyway.

Any other opinions on this?

Manuel

From: Andreas Lochbihler <mail@andreas-lochbihler.de>

Hi Manuel,

when you apply a conditional rewrite rule in several places with

apply(subst (1 2 3) cond_rule)

where the assumptions of the rule end up as the same subgoal, then the

distinct_subgoals_tac ensures that the user has to discharge the assumptions only once. So

there's a point in eliminating repeated goals. But I agree with you that this should be

confined to the subgoal on which subst is operating.

Andreas

From: Makarius <makarius@sketis.net>

I have looked at the history: this odd behaviour goes back to 2005 (by Lucas

Dixon), see https://isabelle-dev.sketis.net/rISABELLE366d39e95d3c

In later years we've got sufficiently well-established means to make proof

tools behave the proper way.

It actually turned out very easy to amend that on the spot, see the following

changes for next Isabelle release:

https://isabelle-dev.sketis.net/rISABELLEe5fcbf6dc687

https://isabelle-dev.sketis.net/rAFPcb48e644eda2

(As usual, AFP serves as a sanity check to see if a hypothetical change should

become real.)

Makarius

Last updated: Dec 08 2021 at 08:24 UTC