Email Gateway (Aug 18 2022 at 13:07): Email Gateway (Aug 18 2022 at 13:07):From: Andrei Popescu <uuomul@yahoo.com>
Say I define a function F with fun in a certain way, and then I prove some facts
which are nicer simplification rules, and would like to use the name F.simps
for these new facts. In Isabelle 2005, I used to simply overwrite the name, but
in Isabelle 2008 I am not allowed to do this any longer. It seems that now I
need to first rename the old facts instead, but I do not know how.
Thank you in advance,
Andrei Popescu
Email Gateway (Aug 18 2022 at 13:07):From: Makarius <makarius@sketis.net>
Well, you just need to come up with a fresh name, such as "F_simps". The
original "F.simps" as produced by the function package will stay for
eternity (due to strict monotonicity of the theory context). Once a
logical entity is defined it cannot be changed.
Makarius
Email Gateway (Aug 18 2022 at 13:08):From: Andrei Popescu <uuomul@yahoo.com>
Thank you for your answer.
The desire to change the name of a proposition in order to make that name available for an other proposition is, in my opinion, more than just a whim.
Coming up with a suggestive fresh name is of course not a problem.
But later in proofs,
when I may need to invoke several facts related to several concepts, I would rather not lookup theorems in the database, but count on the fact that a theorem like foo_def applies what I as a designer (and not I as an implementor) choose to be the most natural "definition". (In particular, in Isabelle 2005, I used to set up the
notations (and the simp database) in such a way that later I would not care
to remember whether I have defined a non-recursive function with "fun" or with "constdefs".)
Regards,
Andrei
Well, you just need to come up with a fresh name, such as "F_simps".
The
original "F.simps" as produced by the function package will stay for
eternity (due to strict monotonicity of the theory context). Once a
logical entity is defined it cannot be changed.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC