Email Gateway (Aug 18 2022 at 10:12): Email Gateway (Aug 18 2022 at 10:12):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I understand from the Isabelle/Isar conversion guide that
declare zless2p zle2p [simp] ;
should add these theorems to the current simpset, just like
the ML function call
Addsimps [zless2p, zle2p] ;
However it doesn't seem to work quite so, since in the following code
lemmas zless2p = zless2 [THEN zero_less_power] ;
lemmas zle2p = zless2p [THEN order_less_imp_le] ;
declare zless2p zle2p [simp] ;
ML {*
val zless2p = thm "zless2p" ;
val zle2p = thm "zle2p" ;
Addsimps [zless2p, zle2p] ;
*}
the ML section is necessary, since, without it, subsequent proofs in my
theories don't work.
Can anyone tell me exactly what the Isar declare command does?
Thanks,
Jeremy
Email Gateway (Aug 18 2022 at 10:13):From: Stefan Berghofer <berghofe@in.tum.de>
Jeremy Dawson wrote:
No, the [simp] attribute in the above declaration is only applied to the
theorem occurring immediately before the attribute (i.e. zle2p), but not
to both zless2p and zle2p. If you want to achieve the same effect as the
above Addsimps command, you either have to write
declare zless2p [simp] zle2p [simp]
or
lemmas [simp] = zless2p zle2p
Greetings,
Stefan
Last updated: Nov 21 2024 at 12:39 UTC