The Isabelle definition command is a safer way to define constants than the axiomatization command. The syntax is similiar:

However, there are several differences:

• Only one constant (my_const above) can be defined.
• Only one axiom can be defined, and it must be an equation of the format my_const ... = ..., describing the meaning of my_const in terms of other, already-defined constants.

If no name is given to the defining equation, the default name produced by appending _def to the name of the constant is used (e.g. my_const_def)

Given a theorem r: A = B (typically a defining equation given by the definition command), apply (unfold r) replaces every occurrence of A in the current goal with B.

If the theorem r has premises, then all of those premises must be directly satisfied by assumptions in the current goal for unfold to succeed.

We use the unfold method with the lemma generated by Definition [isa-001D] to replace nand with its definition in our goal:

The Isabelle simplifier, or simp, is one of the most powerful proof automation features in Isabelle, but it is a very simple idea. Given a set of equations, apply (simp) will (almost) blindly rewrite the goal by all of those equations (as well as any equations that are local assumptions in the goal) left-to-right. Given a sufficiently expressive set of equations, this allows the simplifier to solve many goals (including all of the theorems in Example [isa-001E]) on its own.

The default set of equations that simp uses is called the simpset. We can add theorems to the simpset by attaching the [simp] attribute to them.

We can also adjust the simpset locally when we invoke the simp method:

The datatype defines a new type (like typedecl) but also defines some special constants, called constructors, which make values of that type. Constructors may optionally take arguments, and these data types may be recursive.

These datatypes are analogous to the algebraic data types found in many functional programming languages.

The datatype command automatically proves many lemmas about these types for you, chiefly:

• Disjointness: Values made with one constructor are not equal to values made with another constructor.
• Exhaustivity: The only values of this type are those made by the listed constructors.
• Injectivity: Two values of the same constructor are equal iff their arguments are equal.

This defines a type called oot with two values, ONE : oot and TWO : oot. The print_theorems command here allows us to see all of the theorems automatically created by the datatype command, chiefly that the constants ONE and TWO are disjoint (i.e. ONE ≠ TWO) and exhaustive (i.e. that there are no other values of type oot apart from ONE and TWO)

The case_tac method splits the current goal into multiple cases. Given a term t of type \tau , apply (case_tac t) will produce a new goal for each possible case of t according to the .cases theorem for the type \tau .

This works for all types defined with datatype, as well as for natural numbers (type nat) and bools — often an easier way to do classical reasoning than using rule ccontr.

Isabelle/HOL's theory of natural numbers defines natural numbers in a different way, but they behave much as if they were defined with the datatype command.

The fun command can be used to define functions in Isabelle. Unlike definitions, functions can be defined by multiple pattern-matching equations, they may be recursive, and their equations are automatically added to the simpset.

The print_theorems command allows us to see all of the lemmas generated by this command.

In cases where the recursion and pattern matching follows exactly the structure of the datatype in one argument, primrec can be used instead of fun, which is a bit more efficient:

While it is possible to use rule or erule with the generated .induct theorem from a datatype, it is usually much simpler and more convenient to use the induct proof method. Similar to the case_tac method, apply (induct t) splits the goal into various cases, one for each constructor of the type of t. The difference is that for recursive cases of the datatype, we also get an inductive hypothesis added to our assumptions.

The above function is given another function as an input.

This type encodes a sequence of oot values. For example, the value ONEs 3 (TWOs 2 (ONEs 1 Empty)) encodes the sequence [ONE, ONE, ONE, TWO, TWO, ONE].

Methods can be combined using the ; operator:

This applies m2 to every subgoal that results from applying m1 to the current goal. It can be chained together multiple times. For example, the entire proof of Theorem [isa-001W] can be much more succinctly expressed as one line:

This function uses the prepend function to concatenate two oots sequences together.

The Isabelle/HOL theory of Lists defines lists as follows:

This is an example of a polymorphic data type, where the type variable 'a stands for a type. For example, the type nat list is the type of lists of nat, and oot list is the type of a list of oots.

The notation x#xs is syntax sugar for Cons x xs and [] is syntax sugar for Nil. Lists can also be written in square brackets, so:

is equivalent to:

which is equivalent to:

Some provided functions are useful, including replicate :: nat ⇒ 'a ⇒ 'a list, which produces a list of n copies of the given value, and append :: 'a list ⇒ 'a list ⇒ 'a list which joins two lists together into one. The append function also has special notation, so a @ b is equivalent to append a b