Jiahong Lee (Nov 13 2021 at 06:22): 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?
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.
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
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?
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’.
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.
Jiahong Lee (Nov 14 2021 at 12:30):So, I guess my question is solved in some sense.
Notification Bot (Nov 14 2021 at 12:30):Jia Hong Lee has marked this topic as resolved.
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.
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.
Jiahong Lee (Nov 15 2021 at 01:39):Thanks for your input! You make it even clearer for me to comprehend =D
Last updated: Dec 21 2024 at 16:20 UTC