Difference between = and ≡ · Beginner Questions

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"

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

Manuel Eberl (Mar 17 2021 at 19:57):

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 ≡, not = (and will complain otherwise).

Manuel Eberl (Mar 17 2021 at 19:59):

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).

Benedikt Ahrens (Mar 17 2021 at 20:01):

@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?

Manuel Eberl (Mar 17 2021 at 20:02):

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 ⋀ and ⟹, but the HOL-ification probably also happens to convert your ≡.

Manuel Eberl (Mar 17 2021 at 20:06):

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 ⟹, ⋀, and ≡.

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).

Manuel Eberl (Mar 17 2021 at 20:07):

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.

Stream: Beginner Questions

Topic: Difference between = and ≡