## Stream: Isabelle/ML

### Topic: Structural composition vs. terminal proof

#### Yannick Stade (Jul 13 2023 at 06:19):

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
``````

#### Mathias Fleury (Jul 13 2023 at 06:24):

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

#### Mathias Fleury (Jul 13 2023 at 06:27):

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

#### Mathias Fleury (Jul 13 2023 at 06:28):

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

#### Mathias Fleury (Jul 13 2023 at 06:29):

Other examples are differences between `simp add: XXX` and marking XXX as `[simp]`.

#### Yannick Stade (Jul 13 2023 at 06:31):

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

#### Hanno Becker (Aug 08 2023 at 06:02):

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

Last updated: Dec 07 2023 at 16:21 UTC