# [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)
apply (simp add: step)
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.*