From: Manuel Eberl <firstname.lastname@example.org>
Somebody asked a question of StackOverflow  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
val thmseq = Seq.of_list thms;
fun apply_occ occ st =
thmseq |> Seq.maps (fn r =>
(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;
Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ
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?
From: Andreas Lochbihler <email@example.com>
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.
From: Makarius <firstname.lastname@example.org>
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:
(As usual, AFP serves as a sanity check to see if a hypothetical change should
Last updated: Dec 08 2021 at 08:24 UTC