As the topic says, It is getting annoying that the definition gets unfolded for the IH as well as the goal while performing an induction proof, and this makes the proof more complicated. Is there a way to make simp leave the IH as it is ?

Not applicable in all cases, but you might want to chain the fact in with `(simp add: IH)`

instead of Isar's `using`

/`from`

Let me reformulate the question as such:

I have a lemma in the form f x = g x

I apply induct x, the inductive case is now an implication. I only need to apply simp on the rhs of that implication, applying on the left side will just complicate the proof.

check out the rewrite tactic https://isabelle.in.tum.de/library/HOL/HOL-ex/Rewrite_Examples.html

What I have in mind is

```
proof (induct x)
case (Suc x) (* or whatever *)
note IH = this
show ?case by (simp add: IH)
qed simp
```

If I understand you correctly you want to only simplify the conclusion?

In that case `simp (no_asm_simp)`

might be what you want

@Simon Roßkopf is there an alternative with auto, so that I could work on different goals simultaneously ?

I don't think so. `auto`

does more than simplification, so I do not think it is possible to operate on just a part of the goal. If you just want to do simplification on multiple subgoals `simp_all`

has the same modifiers(Or use `all`

from Eisbach).

However, all of this is pretty much a hack imo. Similarly to what Jakub is suggesting, the correct thing would probably be to do a structured proof and only insert the information where you need it. Just throwing everything into the goal and hoping that automation works seems very brittle.

It's not really hoping that automation would work. There's just a huge amount of subgoals while the procedure for each is the same. A structured proof would be a huge repeated code.

Last updated: Sep 25 2021 at 09:17 UTC