*To*: Jared Davis <jared at cs.utexas.edu>*Subject*: Re: [isabelle] Simplifier questions*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 20 Sep 2006 16:51:06 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4510D3C9.70205@cs.utexas.edu>*References*: <450EE44B.8010009@cs.utexas.edu> <450FAF70.5090508@in.tum.de> <4510D3C9.70205@cs.utexas.edu>*User-agent*: Thunderbird 1.5.0.2 (Macintosh/20060308)

Thanks for the help yesterday. Now I have some more questions, mostlyabout how to control the rewriter more effectively. I have used ACL2before, and when I give it a rule of the form,[| hyp1 ; ... ; hypN |] ==> lhs = rhs, its simplifier will basically: 1. Try to match lhs against subterms in the goal, inside-out,2. Upon finding a match, sigma, instantiate the hyps with sigma andtry to rewrite them to True using other rewrite rules,3. If all hyps rewrite to True, replace the matched subterm withrhs/sigma.Does Isabelle's simplifier use a similar strategy?

Yes.

If so, how does ithandle free variables in hypotheses?

They can be instantiated by matching with assumptions.

Also, is there any way to tell thesimplifier to only backwards chain a few times when trying to relievecertain hyps that might be expensive or trigger looping?

Eg: ML"simp_depth_limit := 5"

Is there a wayto write syntactic conditions as hypotheses, e.g., apply unless somevariable has literally matched "0", etc.?

No. Tobias

**Follow-Ups**:**[isabelle] Theory loader: cannot update finished theory "Main"***From:*Jeremy Dawson

**References**:**[isabelle] questions***From:*Jared Davis

**Re: [isabelle] questions***From:*Tobias Nipkow

**[isabelle] Simplifier questions***From:*Jared Davis

- Previous by Date: Re: [isabelle] Sequence case
- Next by Date: [isabelle] Applying elimination rules
- Previous by Thread: [isabelle] Simplifier questions
- Next by Thread: [isabelle] Theory loader: cannot update finished theory "Main"
- Cl-isabelle-users September 2006 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