```
lemma Dummy: True ..
lemma X using Dummy apply simp+
```

In the above `simp+`

loops infinitely. It appears to be related to pulling the `True`

premise from wherever `using`

puts them into the regular premises of the goal beacause `apply - apply simp+`

works as expected. The problem appears to depend on how exactly the `Dummy`

lemma looks. There is no problem in the following

```
definition "A ≡ True"
lemma Dummy: A unfolding A_def ..
lemma X using Dummy apply simp+
```

I am on Isabelle 2021. Is this a known issue? Anyone have an idea how to work around this in an eisbach method? I don't want to have to type `apply -`

but `method s = -, simp`

does not fix the problem. Is this maybe fixed in Isabelle 2022?

Also, what's the proper place to look for known bugs/problems in Isabelle and report them if they are unknown? I didn't find any kind of issue tracker.

```
supply [[simp_trace]] using Dummy apply simp+
```

`+`

works by repeating a tactic until it fails

So when does simp fail? when it has nothing to do.

Except that simplifying Dummy *counts as something*

so simp is repeatedly simplifying the Dummy assumption. Then `+`

asks simp to do the same thing again.

This is why `apply -`

works: it adds Dummy to the assumption, so `simp`

can simplify only once and fails in the next iteration of `+`

So: this is exactly the expected behavior of `+`

and of `simp`

I don't know what are trying to achieve, but: `apply (simp; fail)+`

or `apply (solves simp)+`

repeats simp as long as the goal is solved, not as long as simp can do something. This is also usually more robust than `simp+`

I use simp to do some normalizations and it's used in a loop like `(simp add: norm_simps | ... | ... )+`

which forms a simple solver. Now this solver loops in the described case. I don't think I can apply your solution here because I don't expect simp to solve any goals usually.

curiously `apply (-, simp+)`

, which was my first idea for a fix, also loops

so, `simp (no_asm)`

fixes this, which would work for me, except I'm actually using

```
method_setup normalize_with_impl =
‹Attrib.thms >>
(fn thms => fn ctxt =>
SIMPLE_METHOD'
(simp_tac (
((empty_simpset ctxt) addsimps thms)
)
))›
```

because I want simp to use absolutely nothing except for my normalization rules

`simp only: norm_simps`

will use only the rule you are specifying

Leander Behr said:

curiously

`apply (-, simp+)`

, which was my first idea for a fix, also loops

you can check with `supply [[simp_trace]]`

what is looping

`apply (-, simp+)`

loops for the same reason as `simp+`

apparently. The `True`

premise is there in every invokation. `simp only: norm_simps`

still solves some trivial subgoals which I don't want

```
apply (-; simp)
```

will apply simp on all goals exactly once

Not sure if I'm missing something here, but why wouldn't you just use `simp_all`

at that point?

Last updated: Dec 07 2023 at 08:19 UTC