Email Gateway (Aug 19 2022 at 16:49): Email Gateway (Aug 19 2022 at 16:49):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Slawomir & Isabelle users.
I'm sorry I missed this discussion going by. Thanks to Makarius for
bringing it to my attention.
The problem can be traced to the way blast_hyp_subst_tac works, and can
be triggered like this (in HOL):
theory Scratch imports main begin
lemma
"x = y ==> (!!x. True) ==> x : T ==> S <= T ==> T <= R ==> S <= R"
apply blast
This will happen when blast is called on any goal, in HOL or in ZF,
where the goal must be nontrivial, provable by blast's internal
strategy, contain a substitutable equality hypothesis, and contain some
non-atomic hypothesis (a meta-forall, meta-implication or meta-equality).
This has always been the case. What has changed is that auto no longer
removes the equality hypothesis itself before calling blast.
The problem is that blast_hyp_subst_tac just won't work if the
hypotheses aren't all atomic. The TERM exception comes from the "map
dest_Trueprop", but in any case the implementation won't work with
meta-operators either.
The trivial fix is to extend the "handle THM _ => no_tac | EQ_VAR =>
no_tac" in blast_hyp_subst_tac to also handle TERM exceptions. This will
completely solve the current problem. I recommend somebody commit this
in time for the next release, at which point [[hypsubst_thin = true]]
will no longer be needed for this auto.
This leaves the problem that there are three implementations of hypsubst
in hypsubst.ML, one which doesn't work with Vars and two which don't
work with meta-operators. I don't really know what to do about this. It
doesn't help that I don't understand what constraints blast really puts
on blast_hyp_subst_tac.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 24 2024 at 12:33 UTC