Re: [isabelle] naming facts



On Tue, 22 May 2012, John Wickerson wrote:

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

A funny thing that I've seen recently on some non-prover tool is this: use SHA1 digest on the content and restrict it to a unique prefix according to the totality of such hashes in a certain context. This gives you 1-3 strange letters in most situations.

Lamport has his own naming scheme, with full paths according to proof structure, and compressed versions thereof.

In Isabelle/Isar the basic attitude is that explicit names are relatively rare, so complete naming is avoided by default. You also have implicit "this" and "calculation" to work with.


	Makarius





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