Re: [isabelle] naming facts



Am Dienstag, den 22.05.2012, 10:33 +0100 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

Uhh, why are 5 random letters better than a slightly out of sync name?

 * For short theorems like "E = []" or "set E = {}" you can reference it
   by `E = []` or `set E = {}`.  You can even use patterns if they are
   unique:

     `set S = _`
     `_ = set V`

 * Use the structuring mechanisms of Isar:
   
     have "" ...
     moreover have "" ...
     moreover have "" ...
     ultimately have "" ...

     have "x = y"
     also have "... < c"
     finally have "x < c" 

     have ""
     then have ""
     then have ""
     then show ""

   This avoids names, but also guides the reader through your proof.


 * I prefer to name collections of assumptions when they specify a
   variable:

     fix x assume x: "0 < x" "x < 1" ...

 * Otherwise I think a good idea is to name the theorem after the
   constants appearing:

     S_eq_initials: "set S = set (initials (Graph V \<Lambda> E))"
     initials_eq_V: "set (initials (Graph V \<Lambda> E)) = set V"

   This avoids mostly the burden to find good names.

 * Only sometimes I use *, **, or *** for theorems I immediately reuse,
   like:

     have *: "a b c = 1"
     show ?thesis
       unfolding *


So please delete your 5 random letters script and use one of these
techniques ;-)

 - Johannes


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