*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Tips to make a simplification simpler?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 31 Jul 2012 08:08:31 +0200*In-reply-to*: <op.wh9y1vs4ule2fv@douda-yannick>*References*: <op.wh9y1vs4ule2fv@douda-yannick>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:14.0) Gecko/20120713 Thunderbird/14.0

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

**Follow-Ups**:**Re: [isabelle] Tips to make a simplification simpler?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Tips to make a simplification simpler?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: [isabelle] Overloading a function: "Extra variables on rhs"
- Next by Date: Re: [isabelle] Overloading a function: "Extra variables on rhs"
- Previous by Thread: [isabelle] Tips to make a simplification simpler?
- Next by Thread: Re: [isabelle] Tips to make a simplification simpler?
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list