Re: [isabelle] Add a definition to the simplifier

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

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


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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