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
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
Description: OpenPGP digital signature



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