author wenzelm Mon, 09 Feb 2009 12:57:05 +0100 changeset 29717 51ed69c9422b parent 29716 b6266c4c68fe child 29718 cf48beb23a70
updated generated files;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Mon Feb 09 12:57:05 2009 +0100
@@ -0,0 +1,93 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Framework}%
+%
+%
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Framework\isanewline
+\isakeyword{imports}\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+%
+%
+\isamarkupchapter{The Isabelle/Isar Framework \label{ch:isar-framework}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+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
+  \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.\
+  \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-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
+
+  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{isamarkuptext}%
+\isamarkuptrue%
+%
+%
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+%
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Feb 09 12:52:16 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Feb 09 12:57:05 2009 +0100
@@ -3,8 +3,6 @@
\def\isabellecontext{Introduction}%
%
-\isanewline
-\isanewline
%
%
@@ -71,11 +69,11 @@
debugging of structured proofs.  Isabelle/Isar supports a broad

-  \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
-  is generic and should work reasonably well for any Isabelle
-  object-logic that conforms to the natural deduction view of the
-  Isabelle/Pure framework.  Specific language elements introduced by
-  the major object-logics are described in \chref{ch:hol}
+  \medskip The generic Isabelle/Isar framework (see
+  \chref{ch:isar-framework}) should work reasonably well for any
+  Isabelle object-logic that conforms to the natural deduction view of
+  the Isabelle/Pure framework.  Specific language elements introduced
+  by the major object-logics are described in \chref{ch:hol}
(Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
(Isabelle/ZF).  The main language elements are already provided by
the Isabelle/Pure framework. Nevertheless, examples given in the