Stream: Beginner Questions

Topic: ✔ Name of the Language used in .thy files


view this post on Zulip Jiahong Lee (Nov 13 2021 at 06:22):

Hi, just to make it clear, what is the name of the language that one write inside a .thy file? It is very ML-like, but I'm sure it's not Standard ML.

Is it called the Isabelle/HOL language or HOL language or Isabelle/Pure language or Pure language or Isar language?

view this post on Zulip Wolfgang Jeltsch (Nov 13 2021 at 17:26):

I would say it’s the Isabelle language and would use the name Isabelle/Isar for the extensions for structured specifications and proofs that were introduced perhaps about 15–20 years ago. However, I have the impression that nowadays Isabelle/Isar stands for the whole language, including the less structured parts (the reference manual for what I’d call Isabelle is called The Isabelle/Isar Reference Manual).

Isabelle/Pure is Isabelle’s meta-logic, Isabelle/HOL is one of several object logics built on it.

view this post on Zulip Jiahong Lee (Nov 14 2021 at 01:35):

Thanks, that makes sense, I'll go with the name "Isabelle/Isar" since the project pushes it as the de facto way of writing proof in Isabelle

view this post on Zulip Jiahong Lee (Nov 14 2021 at 01:40):

Isabelle/Pure is Isabelle’s meta-logic, Isabelle/HOL is one of several object logics built on it.

It sounds like one can write other logic type/system(?) in Isabelle/Isar? E.g. can you write Isabelle/FOL or Isabelle/ZF in Isabelle/Isar?

view this post on Zulip Manuel Eberl (Nov 14 2021 at 10:59):

Also note that you can define new commands at any time. All the commands when you see in a typical Isabelle theory (definition, lemma, typedef, fun, but also the Isar ones like have, obtain) are not part of some fixed language, but in a sense ‘user-defined’.

view this post on Zulip Jiahong Lee (Nov 14 2021 at 12:29):

Hi, that's quite a confusing and yet enlightening statement.

That said, after Ctrl-<Left-click> around, I can see that most commands I use in a .thy file are defined in Isabelle/Pure. Then Isabelle/Isar is built on-top of Isabelle/Pure. So, I'll just think that I'm writing Isabelle/Isar (together with commands exposed from the lower Isabelle/Pure level). As you mention, I can defined my own commands in Isabelle/Isar. I'll see this as its language feature.

view this post on Zulip Jiahong Lee (Nov 14 2021 at 12:30):

So, I guess my question is solved in some sense.

view this post on Zulip Notification Bot (Nov 14 2021 at 12:30):

Jia Hong Lee has marked this topic as resolved.

view this post on Zulip Wolfgang Jeltsch (Nov 14 2021 at 16:06):

Jia Hong Lee said:

It sounds like one can write other logic type/system(?) in Isabelle/Isar? E.g. can you write Isabelle/FOL or Isabelle/ZF in Isabelle/Isar?

Yes, you can. The translation of Isar constructs into logical constructs uses only logical operators of Isabelle/Pure.

view this post on Zulip Wolfgang Jeltsch (Nov 14 2021 at 16:07):

Jia Hong Lee said:

Thanks, that makes sense, I'll go with the name "Isabelle/Isar" since the project pushes it as the de facto way of writing proof in Isabelle

If you’re aiming at using the structured constructs whereever possible, which is what I would recommend, it’s perfectly fair to say you’re writing in Isabelle/Isar, I guess.

view this post on Zulip Jiahong Lee (Nov 15 2021 at 01:39):

Thanks for your input! You make it even clearer for me to comprehend =D


Last updated: Mar 29 2024 at 12:28 UTC