(*<*) theory Basics imports Main begin (*>*) text‹
chapter introduces HOL as a functional programming language and shows
to prove properties of functional programs by induction.
section{Basics}
subsection{Types, Terms and Formulas}
label{sec:TypesTermsForms}
is a typed logic whose type system resembles that of functional
languages. Thus there are
begin{description}
item[base types,]
particular typ‹bool›, the type of truth values, typ‹nat›, the type of natural numbers ($\mathbb{N}$), and \indexed{typ‹int›}{int},
type of mathematical integers ($\mathbb{Z}$).
item[type constructors,]
in particular ‹list›, the type of
, and ‹set›, the type of sets. Type constructors are written
, i.e., after their arguments. For example, typ‹nat list› is the type of lists whose elements are natural numbers.
item[function types,]
by ‹→›.
item[type variables,]
denoted by typ‹'a›, typ‹'b›, etc., like in ML\@.
end{description}
that typ‹'a → 'b list› means \noquotes{@{typ[source]"'a → ('b list)"}}, typ‹('a → 'b) list›: postfix type constructors have precedence ‹→›.
conceptidx{Terms}{term} are formed as in functional programming by
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}
are many predefined infix symbols like ‹+› and ‹≤›.
name of the corresponding binary function is term‹(+)›,
just ‹+›. That is, term‹x + y› is nice surface syntax
``syntactic sugar'') for \noquotes{@{term[source]"(+) x y"}}.
end{warn}
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}
above three constructs must always be enclosed in parentheses
they occur inside other constructs.
end{warn}
may also contain ‹λ›-abstractions. For example, term‹λx. x› is the identity function.
conceptidx{Formulas}{formula} are terms of type ‹bool›.
are the basic constants term‹True› and term‹False› and
usual logical connectives (in decreasing order of precedence): ‹¬›, ‹∧›, ‹∨›, ‹⟶›.
conceptidx{Equality}{equality} is available in the form of the infix function ‹=›
type typ‹'a → 'a → bool›. It also works for formulas, where
means ``if and only if''.
conceptidx{Quantifiers}{quantifier} are written prop‹∀x. P› and prop‹∃x. P›.
automatically computes the type of each variable in a term. This is \concept{type inference}. Despite type inference, it is sometimes
to attach an explicit \concept{type constraint} (or \concept{type
}) to a variable or term. The syntax is ‹t :: τ› as in
mbox{\noquotes{@{term[source] "m + (n::nat)"}}}. Type constraints may be
to
terms involving overloaded functions such as ‹+›.
there are the universal quantifier ‹∧›\index{$4@\isasymAnd} and the implication ‹==>›\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic
. Logically, they agree with their HOL counterparts ‹∀› and ‹⟶›, but operationally they behave differently. This will become
as we go along.
begin{warn}
-arrows of all kinds always associate to the right. In particular,
formula ‹A1==> A2==> A3› means ‹A1==> (A2==> A3)›.
(Isabelle-specific\footnote{To display implications in this style in
/jEdit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{‹[ A1; …; An]==> A›}
short for the iterated implication \mbox{‹A1==>…==> An==> A›}.
we also employ inference rule notation:
inferrule{\mbox{‹A1›}\\\mbox{‹…›}\\\mbox{‹An›}} \mbox{‹A›}}
end{warn}
subsection{Theories}
label{sec:Basic:Theories}
speaking, a \concept{theory} is a named collection of types,
, and theorems, much like a module in a programming language.
Isabelle text needs to go into a theory.
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} ‹T1… Tn› are the names of existing
that ‹T› is based on. The ‹Ti› are the \conceptidx{parent theories}{parent theory} of ‹T›.
defined in the parent theories (and their parents, recursively) is
visible. Each theory ‹T› must
in a \concept{theory file} named ‹T.thy›.
begin{warn}
contains a theory 🚫‹Main›\index{Main@🚫‹Main›}, the union of all the basic
theories like arithmetic, lists, sets, etc.
you know what you are doing, always include ‹Main›
a direct or indirect parent of all your theories.
end{warn}
addition to the theories that come with the Isabelle/HOL distribution
see 🌐‹https://isabelle.in.tum.de/library/HOL›)
is also the \emph{Archive of Formal Proofs} 🌐‹https://isa-afp.org›, a growing collection of Isabelle theories
everybody can contribute to.
subsection{Quotation Marks}
textual definition of a theory follows a fixed syntax with keywords like
isacom{begin} and \isacom{datatype}. Embedded in this syntax are
types and formulas of HOL. To distinguish the two levels, everything
-specific (terms and types) must be enclosed in quotation marks:
texttt{"}\dots\texttt{"}. Quotation marks around a
identifier can be dropped. When Isabelle prints a syntax error
, it refers to the HOL syntax as the \concept{inner syntax} and the
theory language as the \concept{outer syntax}.
ifsem\else
subsection{Proof State}
begin{warn}
default Isabelle/jEdit does not show the proof state but this tutorial
to it frequently. You should tick the ``Proof state'' box
see the proof state in the output window.
end{warn}
fi › (*<*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet am 2026-08-25)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
