Re: [isabelle] Add a definition to the simplifier



Hallo,

declare continuous_def[simp]

Alternatively, you could also declare continuous an abbreviation instead
of a definition, then "continuous" would not be a separate constant, but
simply a syntactic abbreviation for whatever it is that you defined it
to mean. However, this is mainly useful for things such as "infinite A =
¬finite A", I would not use it for more complex concepts.

Personally, I find that adding def lemmas to the simpset is not a good
idea, since you often do not want proof methods to expand these things
by default; you lose some “control” and proof states get messy very quickly.

Should you still want to add continuous_def to the simpset as described
above, note that you can delete it from the simpset for individual
invocations of simp, force, auto and so on with the "del" parameter,
e.g. "apply (simp del: continuous_def)" or "apply (auto simp del:
continuous_def)".

Cheers,
Manuel

On 01/10/2014 03:55 PM, Roger H. wrote:
> Hi,
> 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".
>
>
> it would be nicer if this was not neccesary to drag by every time, meaning that somehow this proof method is added to the simplifier.
>
> how can i do this?
>
> Thank you!
>  		 	   		  





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