*To*: cl-isabelle-users at lists.cam.ac.uk, "Roger H." <s57076 at hotmail.com>*Subject*: Re: [isabelle] Add a definition to the simplifier*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 10 Jan 2014 19:37:44 +0100*In-reply-to*: <DUB124-W464ABCFC12E1C831CBACBD8FB30@phx.gbl>*Organization*: TU Munich*References*: <DUB124-W464ABCFC12E1C831CBACBD8FB30@phx.gbl>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hi Roger, On 10.01.2014 15:55, Roger H. wrote: > can i add a definition to the simplifier? > > means, lets say i define a predicate "continuous" > > ------- > definition continuous :: ... > ... > ----------- > > All my lemmas need this, and everytime i need to prove lemmas , i have to add as proof method "continuous_def". you can (as others have already pointed out). But if you want to do this, maybe your definition does not make sense. The idea of a definition is that you establish a concept (the left hand side) in terms of more primitive ones (the right hand side), then prove properties about that concept (inadvertently unfolding its definition), but then use those properties (which may be simp-rules, or intro-rules, or…) to reason about that concept exclusively without doing unfolding any longer. If you always unfold something, it does not add any »abstraction height« to your theory! E.g. have a look at the following examples from HOL/Nat.thy in Isabelle2013-2: > definition of_nat :: "nat \<Rightarrow> 'a" where > "of_nat n = (plus 1 ^^ n) 0" > > lemma of_nat_simps [simp]: > shows of_nat_0: "of_nat 0 = 0" > and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" > by (simp_all add: of_nat_def) You do not want the definition of of_nat to be unfolded, but rather the recursive rules in the lemma statement! For purely notational constants, you can use »abbreviation«s. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Add a definition to the simplifier***From:*Roger H .

- Previous by Date: Re: [isabelle] Build HOL
- Next by Date: [isabelle] AFP: first entry for 2014
- Previous by Thread: Re: [isabelle] Add a definition to the simplifier
- Next by Thread: [isabelle] Isabelle 2013 / Print goals on failed proof method
- Cl-isabelle-users January 2014 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