Theory Isabelle

(*<*)
theory Isabelle
  imports 
    HOL.HOL
    HOL.Int
    HOL.Nat
begin
(*>*)

chapter ‹Introduction to Isabelle›
text ‹\label{chap:isabelle}›

text ‹Isabelle is an interactive proof assistant and Isabelle/HOL is an implementation of \emph{higher-order logic} in Isabelle. With it, one can interactively prove propositions about theories that are formalised in terms of higher-order \linebreak logic. Many theories have been formalised (and many theorems proven) in Isabelle/HOL and are publicly available.\footnote{see Isabelle's Archive of Formal Proofs at \code{\href{https://www.isa-afp.org}{isa-afp.org}}}

In this appendix, I will give a short introduction into the most important concepts of Isabelle. For an extensive tutorial, see @{cite prog_prove}. A complete documentation can be found in @{cite isar_ref}.
\vspace{-.3cm}›

subsubsection ‹Simple Definitions›

text ‹The command ‹definition› defines a term by establishing an equality, denoted by ‹≡›. This term can be a function or a constant (i.e.\@ 0-ary function). Predicates are functions to Boolean values.

Definitions are annotated by their type. As an example, we define the predicate ‹even›, which maps an integer to a Boolean value.›

definition even :: ‹int ⇒ bool›
  where ‹even n ≡ ∃ m::int . n = 2 * m›

text ‹Functions can be defined in uncurried form (e.g.\@ ‹(int × int) ⇒ bool›) or in curried form (e.g.\@ ‹int ⇒ int ⇒ bool›). As a very trivial example, we can define equality predicates for integers. Compared to the curried version, the uncurried version does not allow for easy pattern matching. This is why, in this thesis, I usually specify functions in curried form.›

definition equal_uncurried :: ‹(int × int) ⇒ bool›
  where ‹equal_uncurried pair ≡ ∃ n m. pair = (n, m) ∧ n = m›

definition equal_curried :: ‹int ⇒ int ⇒ bool›
  where ‹equal_curried n m ≡ n = m›

text ‹We can also use type variables (prefixed with an apostrophe, e.g.\@ ‹'a›) instead of concrete types to get more abstract terms.›

definition equal_abstract :: ‹'a ⇒ 'a ⇒ bool›
  where ‹equal_abstract a b ≡ a = b›

text ‹For a less trivial example, we define a predicate ‹symmetric› that determines whether a given relation is symmetric. An arbitrary homogeneous relation in curried form has the type ‹'a ⇒ 'a ⇒ bool›.›

definition symmetric :: ‹('a ⇒ 'a ⇒ bool) ⇒ bool›
  where ‹symmetric R ≡ ∀ a b. R a b ⟶ R b a›

text ‹We can also assign notation to a term during the definition, where ‹_› is a placeholder (and the numbers behind the notation specification represent priorities for parsing, which may be ignored by the reader).›

definition approx :: ‹int ⇒ int ⇒ bool›
  (‹_ ≈ _› [50, 50] 50)
  where ‹n ≈ m ≡ n=m-1 ∨ n=m ∨ n=m+1›

text ‹Abbreviations are used the same way as definitions, except that, in order to use the equality established by definitions in proofs, we need to explicitly refer to the definition, whereas abbreviations are always expanded internally by the proof system. An example a little further down below should clarify the distinction.›

abbreviation reflexive :: ‹('a ⇒ 'a ⇒ bool) ⇒ bool›
  where ‹reflexive R ≡ ∀ a. R a a›

subsubsection ‹Proving Propositions›

text ‹Propositions can be stated using any of the commands ‹proposition›, ‹lemma›, ‹theorem›, ‹corollary›, and require a proof.

Since Isabelle is an \emph{interactive} proof assistant, proofs are usually meant to be spelled out in code so as to be readable by humans, and the validity of individual steps is verified by certain automated proof methods (e.g.\@ ‹simp›, ‹arith›, ‹auto›, ‹fast›, ‹blast›, \dots). 

As an example, we will show that the relation ‹approx› is ‹symmetric›.

Since ‹symmetric› was defined using the command ‹definition›, we need to explicitly unfold it, where ‹symmetric_def› is the fact (about the equality) introduced by the definition.

The method specified after the command ‹proof› adjusts the proof goal in some way. Ideally, the proof steps should be clear to the reader even without seeing what exactly the automated methods are doing. I have explained each of the steps using comments below.
\pagebreak›

proposition✐‹tag (proof) visible› ‹symmetric approx›
  unfolding symmetric_def
proof (clarify)
  ― ‹We want to show that for any ‹n› and ‹m› with ‹n ≈ m›, we have ‹m ≈ n›.›
  fix n m
  assume ‹n ≈ m›
  ― ‹Using the definition of ‹approx›, we know this about ‹n› and ‹m›.›
  hence ‹n=m-1 ∨ n=m ∨ n=m+1› unfolding approx_def .
  thus ‹m ≈ n›
  ― ‹With disjunction elimination, we examine each case in a sub-proof.›
  proof (elim disjE)
    assume ‹n = m - 1›
    hence ‹m = n + 1› by arith
    thus ‹m ≈ n› unfolding approx_def by blast
  next
    assume ‹n = m›
    thus ‹m ≈ n› using approx_def by blast
  next
    assume ‹n = m + 1›
    hence ‹m = n - 1› by arith
    thus ‹m ≈ n› using approx_def by blast
  qed
qed

text ‹This proof was probably more detailed than was necessary. By unfolding the other definition as well, this proposition can be proven directly with the proof method ‹arith›.›

proposition✐‹tag (proof) visible› ‹symmetric approx›
  unfolding symmetric_def approx_def by arith

text ‹To see the difference between definitions and abbreviations, note that the following proposition is provable without unfolding ‹reflexive_def› (since ‹reflexive› is an abbreviation, there is no such fact in this context).›

proposition✐‹tag (proof) visible› ‹reflexive approx›
  unfolding approx_def by auto

text ‹In practice, of course, one has to strike a balance between transparency/comprehensibility and conciseness of proofs.›

subsubsection ‹Inductive Definitions›

text ‹Inductively defined predicates can be given using premise-conclusion pairs and multiple clauses.›

inductive even_ind :: ‹int ⇒ bool›
  where
    ‹even_ind 0›
  | ‹even_ind n ⟹ even_ind (n+2)›

subsubsection ‹Function Definitions›

text ‹The command ‹function› also establishes equalities, but usually in more complex ways, so that it may not obvious whether a function is well-defined. Hence, the well-definedness needs to be proved explicitly. (These proofs are often solved by the automated proof methods.)

The function is then assumed to be partial. The command ‹termination› introduces proof obligations to show that the function always terminates (and is thus total). For the example below, this is again proved automatically.

After proving well-definedness and totality, we have access to facts about the function that can be used in proofs, e.g.\@ induction principles. More details can be found in \cref{sec:HML}, where we define a non-trivial ‹function›.›

function✐‹tag (proof) visible› factorial :: ‹nat ⇒ nat›
  where
    ‹n = 0 ⟹ factorial n = 1›
  | ‹n > 0 ⟹ factorial n = n * factorial (n-1)›
  by auto

termination✐‹tag (proof) visible› factorial using "termination" by force

subsubsection ‹Data Types›

text ‹With the command ‹datatype›, new types can be defined, possibly in dependence on existing types, by defining a set of (object) constructor functions. For example, we can (re-)define the type of natural numbers.›

datatype natural_number =
  Zero ― ‹0-ary base constructor›
| Suc ‹natural_number› ― ‹unary recursive/inductive constructor›

text ‹We can define type constructors, i.e.\@ types depending on other types (to be distinguished from the object constructors above) by parameterising the type with type variables.›

datatype ('a)list =
  Empty
| Cons ‹'a› ‹('a)list›

subsubsection ‹Locales›

text ‹Locales define a context consisting of type variables, object variables, and assumptions. These can be accessed in the entire context. Locales can be instantiated by specifying concrete types/objects (or variables from another context) for the type/object variables, and extended to form new locales. We can reenter the locale contexts later on, using the command ‹context›. \Cref{sec:LTS} provides a good example for how locales are used in Isabelle to formalise linear transition systems.›

(*<*)
end
(*>*)