10
votes
Accepted
How did 'Isabelle' (the theorem prover) get its name?
A little google-fu (and my own memory) tells me it was apparently named by Larry Paulson after Gerard Huet's daughter.
Gerard Huet happens to be one of the people behind the less poetically named Coq ...
- 8,114
8
votes
Accepted
How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over.
Let us compare the situation to the definite integral, for concretness ...
- 30k
5
votes
Accepted
Naming facts exported from blocks in Isabelle/HOL
From section 1.1.2 in the document isar-ref: you can reference facts via explicit name, implicit name and literal position. In this case, the explicit name has not been provided. I believe that the ...
3
votes
Accepted
When can the coinduction hypothesis be used?
First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A ...
- 2,214
3
votes
Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?
I haven't been able to find a good explanation of how these are different and relate to each other. I know that → is part of HOL and ⇒ and ⟹ part of Isabelle, but it seems that they are basically ...
- 163
1
vote
Isabelle (rule disjE) disjunction elimination rule
Thanks to Patrick Browne I got what I was looking for.
...
- 21
1
vote
What are the differences between LCF's Theorem and Automath's Prop?
The difference is in what kind of type theorem/Prop is.
In Isabelle, theorem is a type in ...
Only top scored, non community-wiki answers of a minimum length are eligible