In our theory, we encountered some differences between using `by (cases …; auto)`

and `by (cases …) auto`

to prove a statement. In many cases, the former option is considerably slower and in one case, the first option even fails to terminate. From the specification (p. 145 and p. 148), we understood that, in this case, they should do the same; apparently, we are wrong. Can you tell us the difference and why the second option is faster? Below we created a minimal working example demonstrating this issue.

```
theory MWE
imports Main
begin
datatype ('a) t = A 'a
fun set_of_list where
"set_of_list [] = {}"
| "set_of_list (A x # xs) = insert x (set_of_list xs)"
lemma
assumes "xs = ys @ zs"
shows "set_of_list xs = set_of_list ys ∪ set_of_list zs"
using assms
proof (induction ys arbitrary: xs zs)
case Nil
then show ?case by simp
next
case (Cons y ys)
then show ?case by (cases y) auto
(* Why can the proof method not be replaced with `(cases y; auto)`? *)
qed
end
```

Weird. simp_trace_new tells you exactly why it behaves differently… but I have no idea why

Ah nothing magic here: the issue is that you are relying on the order in which the simplification happens

And the user is responsible of taking care that the rewrite system is confluent

Other examples are differences between `simp add: XXX`

and marking XXX as `[simp]`

.

Ah, okay, this explains the differences. Thank you!

(EDIT: I posted something as an answer here which was meant as a new topic)

Last updated: Dec 07 2023 at 16:21 UTC