[isabelle-dev] HOL/Word

[Florian Haftmann]

Hi Gerwin,

> Is anyone prepared to leak Florian's new email address so I may haunt him?

I am prepared to be haunted ;-), I am still on the users and dev mailing
list and will follow them following the walrus strategy (only dive up
instantly if you think it is necessary).

First, a quick and dirty answer to your question:

> haftmann at scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ hg cat -r 14cabf5fa710 . | grep -oP '^(lemmas?|corollary|theorems?) [A-Za-z0-9_'\'']+' | sort > names1.txt
> haftmann at scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ hg cat -r 56e3520b68b2 . | grep -oP '^(lemmas?|corollary|theorems?) [A-Za-z0-9_'\'']+' | sort > names2.txt
> haftmann at scarlatti:/data/tum/isabelle/blank/src/HOL/Word$ diff names1.txt names2.txt 
> 197c197
> < lemma bl_and_mask
> ---
>> lemma bl_and_mask'
> 663d662
> < lemma shiftl_0
> 676a676
>> lemma shiftl_x_0
> 679d678
> < lemma shiftr_0
> 689a689
>> lemma shiftr_x_0
> 1037d1036
> < lemmas unat_sub
> 1228d1226
> < lemma uint_0
> 1237a1236
>> lemma uint_eq_0
> 1276d1274
> < lemma unat_sub_simple
> 1341d1338
> < lemma word_less_sub1
> 1344d1340
> < lemma word_le_sub1

These should be the only lemma names affected.

I must confess that the changeset I have produced there really does not
follow best Isabelle practice.  So it is not clear to me whether these
have been mere slips or intentional skips due to duplication.  But
giving the quick and dirty queries from above it should not be too
difficult to reassure what case applies.  Is this enough to help to
solve your problem?  Otherwise I will keep on tracking this, but this
might take a while.

> Someone (Florian, I guess) thought it was a good idea to have "one unified Word theory" as the commit log says. I heartily disagree, but whatever. 

The motiviation for this changeset in the first place were the repeated
pleas for adding code generation to the word type.  Examining what was
needed lead me to the conclusion that the previous division of the Word
theories was largely artificial, in particular the very ancient practice
to separate definitions from their corresponding lemmas into different
theories.  For me it was beyond doubt that a theory defining the word
type should be called "Word", but this was already in use for the main
entrance point, so I was also reluctant to further partition that
unified Word theory.

With some irony you could call this an instance of aspect-oriented
programming:  it is difficult to weave the aspect of code generation
into a theory where it is beyond your scope what the original intentions
have been.  What always made me stumble is that  parts of the Word
theories (in particular Bit_Int) are so highly dependent on the
accidental representation of int values as signed binary numerals;  I
always asked myself whether this modelling is really necessary or could
be formulated in a more abstract fashion.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110206/81286b66/attachment.sig>