[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.