# [isabelle] Tips to make a simplification simpler?

```Hi all again,

I have a question from part of “prog-prove.pdf”

On page 34, “prog-prove.pdf”, propose a inductive definition:

inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)"
for r
where
refl: "((star r) x x)"
| step: "(r x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"

```
Then it suggest that “star r” is transitive and invite the reader to prove it. As the transitivity looked not obvious to me, I was afraid the proof may be not that simple, but it was.
```
The e‑book suggest to prove it this way:

lemma star_trans: "((star r) x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"
apply (induction rule: star.induct)
apply (assumption)
apply (metis step)
done

But I did it this way:

lemma star_trans: "((star r) x y) ⟹ ((star r) y z) ⟹ ((star r) x z)"
apply (induction x y rule: star.induct)
apply (assumption)
apply (simp)
done

```
The two first steps are obvious, and the e‑books used the same. After the first two steps, remains a single goal:
```
1. ⋀x y za.
r x y ⟹
star r y za ⟹
(star r za z ⟹ star r y z) ⟹ star r za z ⟹ star r x z

```
My first “simp” is because “star r za z” appears as a supposedly True hypothesis, so that “(star r za z ⟹ star r y z)” can be simplified to “star r y z” and the goal then become:
```
1. ⋀x y za.
r x y ⟹
star r y za ⟹
star r y z ⟹ star r za z ⟹ star r x z

```
Then, I noticed “r x y” and “star r y z” and “star r x z”, present in the hypothesis covers all of “star.step”, so that “star.step” is a more general case of the goal to prove.
```
```
As the simplifier is able to prove something like “(A⟹B⟹Z)⟹(A⟹B⟹C⟹Z)”, I supposed it should be able to prove the less general goal by the more general “star.step”.
```
```
Looked quite straightforward, but the simplifier trace tells me *five times*:
```
simp_trace_depth_limit exceeded!

Amazingly, it was still able to prove the goal by simplification.

```
My question is: how to make similar simplification more simple? By the way, should I really see it as an issue?
```
Thanks for any pointers and feeling on the topic.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

```

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