summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 09 Feb 2009 12:57:05 +0100 | |

changeset 29717 | 51ed69c9422b |

parent 29716 | b6266c4c68fe |

child 29718 | cf48beb23a70 |

updated generated files;

doc-src/IsarRef/Thy/document/Framework.tex | file | annotate | diff | comparison | revisions | |

doc-src/IsarRef/Thy/document/Introduction.tex | file | annotate | diff | comparison | revisions |

--- /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}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Framework\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\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 + 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.\ + \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 + 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{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\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}% % \isadelimtheory -\isanewline -\isanewline % \endisadelimtheory % @@ -71,11 +69,11 @@ debugging of structured proofs. Isabelle/Isar supports a broad range of proof styles, both readable and unreadable ones. - \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