Re: [isabelle] naming facts



You are not alone, John.  Tom Hales uses a script to generate a random
sequence of 7 letters for the names of the lemmas in his Flyspeck project.
Although this is for HOL Light.

Mark.

on 22/5/12 11:51 AM, John Wickerson <jpw48 at cam.ac.uk> wrote:

> Thanks Larry. Yes, I am aware of the chaining features (though not all of
> the features Johannes helpfully pointed out), and do try not to use my
> "random-name" trick *too* often. Regarding your suggestion of conflating
> variable-names and fact-names, I'm rather uneasy about this practice:
> doesn't it make the proof rather confusing if, for instance, "[OF k]" and
> "[of k]" are actually referring to different k's?
>
> John
>
> On 22 May 2012, at 11:33, Lawrence Paulson wrote:
>
>> I assume that you are aware of the various chaining facilities that
exist,
> including moreover/ultimately. And the ability to refer to facts using
> backquotes, as in `k>0`.
>>
>> With those, I find that I don't need many labels, so that usually the
name
> of the variable involved is sufficient, for example,
>>
>>     assumes k: "k>0"
>>
>>
>> Larry Paulson
>>
>>
>> On 22 May 2012, at 10:33, John Wickerson wrote:
>>
>>> Dear Isabelle,
>>>
>>> When building an Isabelle script, I often have to come up with names for
> facts if I am not using them immediately. Coming up with meaningful names
> all the time is an intellectual burden I could live without when I'm
> concentrating on a proof. More importantly, even if I did come up with
> meaningful names all the time, I reckon they would soon get out-of-sync as
I
> modified my script. I briefly tried *numbering* my steps, but again, the
> numbers quickly get out-of-order as my script evolves, and I have always
to
> bear in mind which number I used last.
>>>
>>> So, my current solution is to have an emacs macro that generates a
> sequence of 5 random letters when I press "C-c d", which I use to name my
> facts. I find this works rather well; I've not had a clash yet, and I
don't
> have to engage my brain at all. Here's a little snippet from my current
> theory, to illustrate:
>>>
>>>> with iecss and "0.prems"(2) have
>>>> dakuy: "set S = set (initials (Graph V \<Lambda> E))" and
>>>> iuqxi: "set (initials (Graph V \<Lambda> E)) = set V" by auto
>>>> from pqshe have wsegy: "set E = {}" by auto
>>>> hence hkimj: "E = []" by auto
>>>
>>>
>>> How do other users approach this issue?
>>>
>>> John
>>>
>>> ps. One final thought: does there exist a tool that processes an
Isabelle
> script to make it more readable, renaming steps with (say) ascending
natural
> numbers, and removing unused names? I think that would be rather nice.
>>
>
>
>
>





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