Re: [isabelle] naming facts



Am 22/05/2012 11:33, schrieb John Wickerson:
> 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?

Here is the hardliner view: if you need to number your intermediate statements
with more than 0-9, you are doing something wrong. [Unless you want to do
something exotic like recast refutations found by a SAT solver as Isar proofs ;-) ].

Why? Look at a math book, they don't need many labels either. Of course, it
takes a bit of practice and it is a question of style, but Isar has a number of
features that help to avoid names. I find the following most useful:

- In your example, drop wsegy: and hkimj: and refer to them as `set E = {}` and
`E = []`
- use this, then, hence, assms, ?thesis etc
- Introduce abbreviations: let ?t = "big term"

Tobias





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