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".)  

Regards, 
   Andrei 

--- 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". 
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







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