Re: [isabelle] how do I rename a fact in isabelle?
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".)
--- On Sun, 3/8/09, Makarius <makarius at sketis.net> wrote:
From: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] how do I rename a fact in isabelle?
To: "Andrei Popescu" <uuomul at yahoo.com>
Cc: isabelle-users at cl.cam.ac.uk
Date: Sunday, March 8, 2009, 1:31 PM
On Sat, 7 Mar 2009, Andrei Popescu wrote:
> 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.
Well, you just need to come up with a fresh name, such as "F_simps".
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and