Re: [isabelle] Word vs WordMain



Hi Nils,

On 07/04/2010, at 3:06 AM, Nils Jähnig wrote:
> I'm new to Isabelle/HOL. I'm supposed to understand a theory which
> imports WordMain (and the author of the theory is still in holidays).
> Here comes my first problem:
> 
> 1) Where do I find WordMain.thy?

WordMain has helpfully been renamed to Word in Isabelle2009-1.


> 2) What is the difference between WordMain.thy and Word.thy

The two should be equivalent.


> And now more specific:
> 
> 3) Why does
> types word32 = "32 word"
> give an inner syntax error? it is the first line after "begin" in
> WordExamples.thy and i thought this should work out of the box.

I would have thought so as well. 

The reason is really quite horrible considering the renaming above: if you don't build on the HOL-Word image, but rely on Isabelle loading the theory "Word" interactively, you get the wrong theory (the one in Library). If I remember correctly, this was the reason I called it WordMain in the first place.

To get the right Word theory, either

- run "isabelle make HOL-Word" in the src/HOL directory and tell ProofGeneral to use this logic (in Isabelle->Logics)

or

- interactively load src/HOL/Word/Word.thy and process this file before you process any of the theories that depend on it.


> Where could be my mistake?

Not really yours..

I'm not sure what I would want the fix to be, though. Another renaming of theories back to the old one (it's not that much fun to fix things back and forth) or a renaming of Library/Word or big warning letters in HOL/Word/Word.thy and WordExamples.thy? 

Cheers,
Gerwin

ps: theory name spaces anyone? ;-)




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