# [isabelle] substituting in hypotheses

`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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*