# Re: [isabelle] substituting in hypotheses

```John Matthews wrote:
```
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

```
```John,

```
I've written routines inspired by the conversions and conversionals of HOL. Not necessarily more concise in your example, but here's how it would look:
```
Goal "(x::nat)+1 = x+1+0";
auto();
qed "L1";

Goal "[| P(x+1::nat); R(%(x::nat). x+1) |] ==> R(%x. x+1+0)" ;

```
open Conv ; (* get this from http://users.rsise.anu.edu.au/~jeremy/isabelle/gen/*conv.ML *)
```val conv = eqc [mk_eq L1] ;
val tac = CONV_TAC (TDSTOP_CONV conv) ;
(* this changes all three spots *)

val abs_tac = CONV_TAC (TDSTOP_CONV (ABS_CONV conv)) ;
(* this changes only immediately under an abstraction *)
val ntac = CONV_TAC (TDSTOP_CONV (NTH_CONV  conv)) ;
(* this changes only the second occurrence *)

or indeed

val ptac = CONV_GOAL_TAC (PREM_CONV 2 (TDSTOP_CONV conv)) 1 ;
(* this works in premise 2 of goal 1 *)
val ptac' = CONV_GOALS_TAC (PREM_CONV 2 (TDSTOP_CONV conv)) ;
(* this works in premise 2 of any goal *)
val ptac'' = CONV_TAC (TDSTOP_CONV (PREM_CONV 2 (TDSTOP_CONV conv))) ;
(* this works anywhere in any second premise anywhere in the term *)

(* and so on, as complicated as you like! *)

Regards,

Jeremy

```

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