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

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