Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: John Matthews <matthews@galois.com>
Hi Larry and Jeremy (and Lucas),
The "subst (asm)" method worked well in my current Isabelle theory.
Jeremy, your extensive conversions library also looks very useful for
fine-grained control over rewriting, as does your file for manipulating
Isar contexts within ML.
Thanks for the tips,
-john
Email Gateway (Aug 17 2022 at 13:26):From: John Matthews <matthews@galois.com>
Is there anything analogous to Isar's "subst" method that allows me to
perform a one-off substitution in a selected subgoal's hypothesis? Here
is a contrived example that could be proved trivially by auto, but
demonstrates what I'm trying to do in general:
lemma L1: "(x::nat)+1 = x+1+0"
by auto
lemma silly: "[| P(x+1::nat); R(%(x::nat). x+1) |] ==> R(%x. x+1+0)"
When proving "silly" I'd like to use lemma L1 to substitute "x+1+0" for
"x+1" in the second hypotheses. Note that
apply (simp only: L1)
will cause Isabelle to loop, and
apply (unfold L1)
fails. Even if unfold didn't fail here, it would likely also loop or
unfold the occurrence of x+1 in the other hypothesis and conclusion of
"silly", which I don't want.
Currently, the easiest way I know of to perform the substitution in the
hypothesis is through these cumbersome series of methods:
apply (erule_tac Q="R(%x. x+1)" in contrapos_pp)
apply (subst L1)
apply (erule_tac Q="R (%x. x+1+0)" in contrapos_nn)
Is there a more concise way to do this?
Thanks,
-john
Email Gateway (Aug 17 2022 at 13:26):From: Lawrence Paulson <lp15@cam.ac.uk>
In the developer's version of Isabelle (and in the next release) you
can do this:
apply (subst (asm) L1)
The new version of subst also lets you specify which instance of the
LHS to substitute for, and many other things. All thanks to Lucas Dixon.
Larry
Last updated: May 03 2024 at 08:18 UTC