Re: [isabelle] Tips to make a simplification simpler?



The message "simp_trace_depth_limit exceeded!" merely tells you that the *trace*
depth has been exceeded. The behaviour of the simplifier is not affected, merely
its tracing is stopped until it emerges from its recursive invocations. This is
a very simpled-minded way of getting a abstract view of the trace. If you want
more tracing info, you can always increase the limit - in ProofGeneral there is
a menue item Trace Simplifier Depth for it.

We expect to provide better tracing facilities in the future.

Tobias

Am 30/07/2012 21:57, schrieb Yannick Duchêne (Hibou57):
> 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.
> 
> 





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