10

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 theorem prover. Small world!


8

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 just from $0$ to $1$. Here is an example: $$\int_0^1 x^2 + 3 x \, dx$$ This is a very archaic way of writing mathematical expressions that mathematicians like ...


4

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 canonical method to provide an explicit name is to reference the fact of interest by its implicit name immediately after the end of the block. For example, lemma ...


3

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 function $f:2^U\to2^U$ (from subsets of $U$ to subsets of $U$) is monotone, if $A\subseteq B$ always implies $f(A)\subseteq f(B)$. A fixed point of $f$ is a set $...


2

Your first goal is provable, but is somewhat non-trivial arithmetic. I believe that the issue is essentially Isabelle not knowing that $$S(x - 2) = x -1$$ is true for arbitrary $x$, and indeed, this property is false in general, if $x<2$! This is because $x-2=0$ in Isabelle for $x=1$. Here this doesn't occur, because $x=2\cdot 2^n$, so $x\geq 2$ for all ...


1

The difference is in what kind of type theorem/Prop is. In Isabelle, theorem is a type in the underlying implementation language, that is made abstract so that the only way to create an inhabitant of that type (i.e. a valid theorem) is in the end to resort to the primitives provided by the kernel. So it is the typing constraints of the implementation ...


Only top voted, non community-wiki answers of a minimum length are eligible