Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Word vs WordMain

view this post on Zulip Email Gateway (Aug 18 2022 at 15:02):

From: Alexander Krauss <krauss@in.tum.de>
Hi Nils,

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?

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

I suspect that the theory you are working with was built with Isabelle
2008. WordMain.thy was renamed to Word.thy between the 2008 and the 2009
release: http://isabelle.in.tum.de/repos/isabelle/rev/d9294387ab0e

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.
Where could be my mistake?

When you open WordExamples.thy with the normal HOL image loaded, then
Isabelle picks "Library/Word.thy" by default when you say "imports
Word". This is another, incompatible, development.

You can either manually adapt the import and write

imports "~~/src/HOL/Word/Word"

or your built the HOL-Word image, which contains HOL and the Word
library. To do this, go to /src/HOL where is your Isabelle
installation path, and run

isabelle make HOL-Word

After that you can select the image in Proof General under "Isabelle ->
Logics".

Hope this helps,

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 15:02):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
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

or

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? ;-)

view this post on Zulip Email Gateway (Aug 18 2022 at 15:08):

From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hi,

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?

I found Word.thy in Isabelle/HOL/src/Word/
Hence here my second question:

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

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.
Where could be my mistake?

I did the first exercises of the Isabelle HOL tutorial, so the basic
part of my Isabelle system should work.

Greetings from Berlin
Nils

Last updated: Apr 26 2024 at 12:28 UTC