theory Framework
imports Main
begin
chapter {* The Isabelle/Isar Framework \label{ch:isar-framework} *}
text {*
Isabelle/Isar
\cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,Wenzel:2006:Festschrift}
is intended as a generic framework for developing formal
mathematical documents with full proof checking. Definitions and
proofs are organized as theories; an assembly of theory sources may
be presented as a printed document; see also
\chref{ch:document-prep}.
The main objective of Isar is the design of a human-readable
structured proof language, which is called the ``primary proof
format'' in Isar terminology. Such a primary proof language is
somewhere in the middle between the extremes of primitive proof
objects and actual natural language. In this respect, Isar is a bit
more formalistic than Mizar
\cite{Trybulec:1993:MizarFeatures,Rudnicki:1992:MizarOverview,Wiedijk:1999:Mizar},
using logical symbols for certain reasoning schemes where Mizar
would prefer English words; see \cite{Wenzel-Wiedijk:2002} for
further comparisons of these systems.
So Isar challenges the traditional way of recording informal proofs
in mathematical prose, as well as the common tendency to see fully
formal proofs directly as objects of some logical calculus (e.g.\
@{text "\<lambda>"}-terms in a version of type theory). In fact, Isar is
better understood as an interpreter of a simple block-structured
language for describing data flow of local facts and goals,
interspersed with occasional invocations of proof methods.
Everything is reduced to logical inferences internally, but these
steps are somewhat marginal compared to the overall bookkeeping of
the interpretation process. Thanks to careful design of the syntax
and semantics of Isar language elements, a formal record of Isar
instructions may later appear as an intelligible text to the
attentive reader.
The Isar proof language has emerged from careful analysis of some
inherent virtues of the existing logical framework of Isabelle/Pure
\cite{paulson-found,paulson700}, notably composition of higher-order
natural deduction rules, which is a generalization of Gentzen's
original calculus \cite{Gentzen:1935}. The approach of generic
inference systems in Pure is continued by Isar towards actual proof
texts.
Concrete applications require another intermediate layer: an
object-logic. Isabelle/HOL \cite{isa-tutorial} (simply-typed
set-theory) is being used most of the time; Isabelle/ZF
\cite{isabelle-ZF} is less extensively developed, although it would
probably fit better for classical mathematics.
*}
end