Theory Basics

(*<*)
theory Basics
imports Main
begin
(*>*)
text‹
This chapter introduces HOL as a functional programming language and shows
how to prove properties of functional programs by induction.

\section{Basics}

\subsection{Types, Terms and Formulas}
\label{sec:TypesTermsForms}

HOL is a typed logic whose type system resembles that of functional
programming languages. Thus there are
\begin{description}
\item[base types,] 
in particular typ‹bool›, the type of truth values,
typ‹nat›, the type of natural numbers ($\mathbb{N}$), and \indexed{typ‹int›}{int},
the type of mathematical integers ($\mathbb{Z}$).
\item[type constructors,]
 in particular ‹list›, the type of
lists, and ‹set›, the type of sets. Type constructors are written
postfix, i.e., after their arguments. For example,
typ‹nat list› is the type of lists whose elements are natural numbers.
\item[function types,]
denoted by ‹⇒›.
\item[type variables,]
  denoted by typ‹'a›, typ‹'b›, etc., like in ML\@.
\end{description}
Note that typ‹'a ⇒ 'b list› means \noquotes{@{typ[source]"'a ⇒ ('b list)"}},
not typ‹('a ⇒ 'b) list›: postfix type constructors have precedence
over ‹⇒›.

\conceptidx{Terms}{term} are formed as in functional programming by
applying functions to arguments. If ‹f› is a function of type
‹τ1 ⇒ τ2› and ‹t› is a term of type
‹τ1› then term‹f t› is a term of type ‹τ2›. We write ‹t :: τ› to mean that term ‹t› has type ‹τ›.

\begin{warn}
There are many predefined infix symbols like ‹+› and ‹≤›.
The name of the corresponding binary function is term‹(+)›,
not just ‹+›. That is, term‹x + y› is nice surface syntax
(``syntactic sugar'') for \noquotes{@{term[source]"(+) x y"}}.
\end{warn}

HOL also supports some basic constructs from functional programming:
\begin{quote}
‹(if b then t1 else t2)›\\
‹(let x = t in u)›\\
‹(case t of pat1 ⇒ t1 | … | patn ⇒ tn)›
\end{quote}
\begin{warn}
The above three constructs must always be enclosed in parentheses
if they occur inside other constructs.
\end{warn}
Terms may also contain ‹λ›-abstractions. For example,
term‹λx. x› is the identity function.

\conceptidx{Formulas}{formula} are terms of type ‹bool›.
There are the basic constants term‹True› and term‹False› and
the usual logical connectives (in decreasing order of precedence):
‹¬›, ‹∧›, ‹∨›, ‹⟶›.

\conceptidx{Equality}{equality} is available in the form of the infix function ‹=›
of type typ‹'a ⇒ 'a ⇒ bool›. It also works for formulas, where
it means ``if and only if''.

\conceptidx{Quantifiers}{quantifier} are written prop‹∀x. P› and prop‹∃x. P›.

Isabelle automatically computes the type of each variable in a term. This is
called \concept{type inference}.  Despite type inference, it is sometimes
necessary to attach an explicit \concept{type constraint} (or \concept{type
annotation}) to a variable or term.  The syntax is ‹t :: τ› as in
\mbox{\noquotes{@{term[source] "m + (n::nat)"}}}. Type constraints may be
needed to
disambiguate terms involving overloaded functions such as ‹+›.

Finally there are the universal quantifier ‹⋀›\index{$4@\isasymAnd} and the implication
‹⟹›\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic
HOL. Logically, they agree with their HOL counterparts ‹∀› and
‹⟶›, but operationally they behave differently. This will become
clearer as we go along.
\begin{warn}
Right-arrows of all kinds always associate to the right. In particular,
the formula
‹A1 ⟹ A2 ⟹ A3› means ‹A1 ⟹ (A2 ⟹ A3)›.
The (Isabelle-specific\footnote{To display implications in this style in
Isabelle/jEdit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{‹⟦ A1; …; An ⟧ ⟹ A›}
is short for the iterated implication \mbox{‹A1 ⟹ … ⟹ An ⟹ A›}.
Sometimes we also employ inference rule notation:
\inferrule{\mbox{‹A1›}\\ \mbox{‹…›}\\ \mbox{‹An›}}
{\mbox{‹A›}}
\end{warn}


\subsection{Theories}
\label{sec:Basic:Theories}

Roughly speaking, a \concept{theory} is a named collection of types,
functions, and theorems, much like a module in a programming language.
All Isabelle text needs to go into a theory.
The general format of a theory ‹T› is
\begin{quote}
\indexed{\isacom{theory}}{theory} ‹T›\\
\indexed{\isacom{imports}}{imports} ‹T1 … Tn›\\
\isacom{begin}\\
\emph{definitions, theorems and proofs}\\
\isacom{end}
\end{quote}
where ‹T1 … Tn› are the names of existing
theories that ‹T› is based on. The ‹Ti› are the
direct \conceptidx{parent theories}{parent theory} of ‹T›.
Everything defined in the parent theories (and their parents, recursively) is
automatically visible. Each theory ‹T› must
reside in a \concept{theory file} named ‹T.thy›.

\begin{warn}
HOL contains a theory theory‹Main›\index{Main@theory‹Main›}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.
Unless you know what you are doing, always include ‹Main›
as a direct or indirect parent of all your theories.
\end{warn}

In addition to the theories that come with the Isabelle/HOL distribution
(see 🌐‹https://isabelle.in.tum.de/library/HOL›)
there is also the \emph{Archive of Formal Proofs}
at 🌐‹https://isa-afp.org›, a growing collection of Isabelle theories
that everybody can contribute to.

\subsection{Quotation Marks}

The textual definition of a theory follows a fixed syntax with keywords like
\isacom{begin} and \isacom{datatype}.  Embedded in this syntax are
the types and formulas of HOL.  To distinguish the two levels, everything
HOL-specific (terms and types) must be enclosed in quotation marks:
\texttt{"}\dots\texttt{"}. Quotation marks around a
single identifier can be dropped.  When Isabelle prints a syntax error
message, it refers to the HOL syntax as the \concept{inner syntax} and the
enclosing theory language as the \concept{outer syntax}.

\ifsem\else
\subsection{Proof State}

\begin{warn}
By default Isabelle/jEdit does not show the proof state but this tutorial
refers to it frequently. You should tick the ``Proof state'' box
to see the proof state in the output window.
\end{warn}
\fi
›
(*<*)
end
(*>*)