I am (re)learning Isabelle right now, and I have a question regarding the difference between = and ≡, and their uses in Isabelle/HOL.
Specifically, in the (allegedly outdated) Isabelle Tutorial, it says that ≡ should be used for constant definitions (see Section 2.7.2 Constant Definitions), and the following example is given:
definition nand :: gate where "nand A B ≡ ¬(A ∧ B)"
In the more recent "Concrete Semantics" (Section 2.3.2 Definitions), definitions are said to use =, and the following example is given:
definition sq :: "nat ⇒ nat" where "sq n = n ∗ n"
It is furthermore said that abbreviations (Section 2.3.3) should use ≡.
My first idea was that maybe ≡ is a meta-theoretic notion, and behaves to = like ==> behaves to -->. But this is somewhat refuted by the fact that the following works (for a suitable definition of lists etc):
lemma "append_list xs  ≡ xs" apply (induction xs) apply (auto) done
where the ≡ is used within a HOL statement (if I understand correctly). Here, interestingly, after the induction the subgoals are stated using = instead of ≡:
goal (2 subgoals): 1. append_list   =  2. ⋀x1 xs. append_list xs  = xs ⟹ append_list (x1 # xs)  = x1 # xs
I would be grateful for any pointers to an explanation of = and ≡.
No, you were right.
≡ is just the meta-logical equivalent of
=. There is no real reason to use it as an Isabelle ‘user’, much less than using e.g.
⟹ (which does have its uses). This is probably explained somewhere in the Isabelle/Isar reference manual (isar-ref), but as I said, it's not really something you have to know about as a user.
I think the only case in which is might crop up is that the
abbreviation command insists on a specification with
= (and will complain otherwise).
Referring to ‘where the ≡ is used within a HOL statement (if I understand correctly)’: where is the HOL statement there? Because no, you cannot write
≡ as a HOL statement, since
≡ returns a
prop (the type of propositions, which you normally do not see as a HOL user and which you cannot use inside HOL terms).
@Manuel Eberl : Thanks a lot for your response. Re using ≡ in HOL statements: I thought my lemma statement above was a HOL statement, since it is in quotes. Am I misunderstanding the quotes then?
The fact that the
≡ becomes a
= suddenly is probably some quirk of the
induction method. I think it turns meta-logical connectives into their object-logical ones because that is required to use the induction rule (which is specified in terms of HOL predicates, not meta-logical ones). This mainly concerns
⟹, but the HOL-ification probably also happens to convert your
Benedikt Ahrens said:
Manuel Eberl : Thanks a lot for your response. Re using ≡ in HOL statements: I thought my lemma statement above was a HOL statement, since it is in quotes. Am I misunderstanding the quotes then?
Yes! The quotes distinguish outer syntax from inner syntax. The inner syntax is what you use to specify terms and types. The outer syntax is what you use to interact with the system.
If you take a look at Isabelle/Pure (
~~/src/Pure/Pure.thy), you will see lots if Isabelle/Pure statements inside quotes as well. In Isabelle/Pure, you have a type
prop of propositions and some built-in connectives like
HOL then axiomatises a
bool type that can be converted to
prop using the function
Trueprop :: bool ⇒ prop. Whenever you write down a proposition in HOL (i.e.
bool-valued), Isabelle implicitly wraps a
Trueprop around it and hides it from you. HOL also has object-level equivalents to all the meta-level equivalents from Pure, and you can convert between the two in both directions as long as the thing you're looking at is of HOL (i.e. not
prop. You can only reason about
prop directly in Isabelle/Pure).
Disclaimer: I'm not really an expert on Isabelle/Pure, so some details of what I said might be a bit off. But I'm fairly certain that it's a good enough ‘working knowledge’ for the average Isabelle user.
Thanks a lot, that has clarified a lot for me!
Last updated: Sep 25 2022 at 23:25 UTC