Email Gateway (Aug 19 2022 at 13:29): Email Gateway (Aug 19 2022 at 13:29):From: "Roger H." <s57076@hotmail.com>
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!
Email Gateway (Aug 19 2022 at 13:30):From: John Wickerson <johnwickerson@cantab.net>
Something like
definition continuous where [simp]: "continuous f = ..."
should work. Or make continuous a function (defined with "fun" rather than "definition") and it'll be added to the simplifier automatically.
john
Email Gateway (Aug 19 2022 at 13:30):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 19 2022 at 13:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Last updated: Apr 25 2024 at 04:18 UTC