*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Using the simplifier from the ML-level*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Wed, 02 Jul 2008 11:08:52 +0200*Cc*: isabelle-users at cl.cam.ac.uk, Gudmund Grov <gg10 at macs.hw.ac.uk>*In-reply-to*: <Pine.LNX.4.64.0807021043270.13615@macbroy20.informatik.tu-muenchen.de>*References*: <4AF52F76-C4E7-4BAE-879D-41A66FCB53DD@macs.hw.ac.uk> <Pine.LNX.4.64.0807021043270.13615@macbroy20.informatik.tu-muenchen.de>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Amine. Makarius wrote:

On Tue, 1 Jul 2008, Gudmund Grov wrote:Basically, I want the same behavior as calling (simp only: ..) willgive. For example, assuming the theorem list my_ruleslemmas my_rules = ... I need a tactic "my_simp" such that apply (simp only: my_rules) = apply (tactic "my_simp @{thms my_rules}") I have tried the following ML {* fun my_simp defs = simp_tac (MetaSimplifier.addsimps (MetaSimplifier.empty_ss,defs)) 1; *} but in some cases, it fails to rewrite, while (simp only: ...) succeeds.The main problem here is empty_ss, which is insufficient to performrewrites for the object-logic. You can use HOL_basic_ss instead.The following imitates "simp only" to some degree: apply (tactic {* asm_full_simp_tac (HOL_basic_ss addsimps @{thms my_rules} *})Actually the "simp" method also wraps the tactic into the CHANGEDcombinator, making it fail if no rewrites apply.Makarius

**References**:**[isabelle] Using the simplifier from the ML-level***From:*Gudmund Grov

**Re: [isabelle] Using the simplifier from the ML-level***From:*Makarius

- Previous by Date: Re: [isabelle] Using the simplifier from the ML-level
- Next by Date: Re: [isabelle] need help
- Previous by Thread: Re: [isabelle] Using the simplifier from the ML-level
- Next by Thread: Re: [isabelle] Interpreting a locale on it's own underlying definitions
- Cl-isabelle-users July 2008 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