1.1 --- a/doc-src/IsarRef/IsaMakefile Mon Feb 09 12:49:13 2009 +0100
1.2 +++ b/doc-src/IsarRef/IsaMakefile Mon Feb 09 12:52:16 2009 +0100
1.3 @@ -22,10 +22,10 @@
1.4 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
1.5
1.6 $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.7 - Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy \
1.8 - Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy \
1.9 - Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy \
1.10 - Thy/Symbols.thy Thy/ML_Tactic.thy
1.11 + Thy/Framework.thy Thy/Inner_Syntax.thy Thy/Introduction.thy \
1.12 + Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy \
1.13 + Thy/Document_Preparation.thy Thy/Generic.thy Thy/HOL_Specific.thy \
1.14 + Thy/Quick_Reference.thy Thy/Symbols.thy Thy/ML_Tactic.thy
1.15 @$(USEDIR) -s IsarRef HOL Thy
1.16
1.17
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/IsarRef/Thy/Framework.thy Mon Feb 09 12:52:16 2009 +0100
2.3 @@ -0,0 +1,56 @@
2.4 +theory Framework
2.5 +imports Main
2.6 +begin
2.7 +
2.8 +chapter {* The Isabelle/Isar Framework \label{ch:isar-framework} *}
2.9 +
2.10 +text {*
2.11 + Isabelle/Isar
2.12 + \cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,Wenzel:2006:Festschrift}
2.13 + is intended as a generic framework for developing formal
2.14 + mathematical documents with full proof checking. Definitions and
2.15 + proofs are organized as theories; an assembly of theory sources may
2.16 + be presented as a printed document; see also
2.17 + \chref{ch:document-prep}.
2.18 +
2.19 + The main objective of Isar is the design of a human-readable
2.20 + structured proof language, which is called the ``primary proof
2.21 + format'' in Isar terminology. Such a primary proof language is
2.22 + somewhere in the middle between the extremes of primitive proof
2.23 + objects and actual natural language. In this respect, Isar is a bit
2.24 + more formalistic than Mizar
2.25 + \cite{Trybulec:1993:MizarFeatures,Rudnicki:1992:MizarOverview,Wiedijk:1999:Mizar},
2.26 + using logical symbols for certain reasoning schemes where Mizar
2.27 + would prefer English words; see \cite{Wenzel-Wiedijk:2002} for
2.28 + further comparisons of these systems.
2.29 +
2.30 + So Isar challenges the traditional way of recording informal proofs
2.31 + in mathematical prose, as well as the common tendency to see fully
2.32 + formal proofs directly as objects of some logical calculus (e.g.\
2.33 + @{text "\<lambda>"}-terms in a version of type theory). In fact, Isar is
2.34 + better understood as an interpreter of a simple block-structured
2.35 + language for describing data flow of local facts and goals,
2.36 + interspersed with occasional invocations of proof methods.
2.37 + Everything is reduced to logical inferences internally, but these
2.38 + steps are somewhat marginal compared to the overall bookkeeping of
2.39 + the interpretation process. Thanks to careful design of the syntax
2.40 + and semantics of Isar language elements, a formal record of Isar
2.41 + instructions may later appear as an intelligible text to the
2.42 + attentive reader.
2.43 +
2.44 + The Isar proof language has emerged from careful analysis of some
2.45 + inherent virtues of the existing logical framework of Isabelle/Pure
2.46 + \cite{paulson-found,paulson700}, notably composition of higher-order
2.47 + natural deduction rules, which is a generalization of Gentzen's
2.48 + original calculus \cite{Gentzen:1935}. The approach of generic
2.49 + inference systems in Pure is continued by Isar towards actual proof
2.50 + texts.
2.51 +
2.52 + Concrete applications require another intermediate layer: an
2.53 + object-logic. Isabelle/HOL \cite{isa-tutorial} (simply-typed
2.54 + set-theory) is being used most of the time; Isabelle/ZF
2.55 + \cite{isabelle-ZF} is less extensively developed, although it would
2.56 + probably fit better for classical mathematics.
2.57 +*}
2.58 +
2.59 +end
3.1 --- a/doc-src/IsarRef/Thy/Introduction.thy Mon Feb 09 12:49:13 2009 +0100
3.2 +++ b/doc-src/IsarRef/Thy/Introduction.thy Mon Feb 09 12:52:16 2009 +0100
3.3 @@ -1,5 +1,3 @@
3.4 -(* $Id$ *)
3.5 -
3.6 theory Introduction
3.7 imports Main
3.8 begin
3.9 @@ -51,11 +49,11 @@
3.10 debugging of structured proofs. Isabelle/Isar supports a broad
3.11 range of proof styles, both readable and unreadable ones.
3.12
3.13 - \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
3.14 - is generic and should work reasonably well for any Isabelle
3.15 - object-logic that conforms to the natural deduction view of the
3.16 - Isabelle/Pure framework. Specific language elements introduced by
3.17 - the major object-logics are described in \chref{ch:hol}
3.18 + \medskip The generic Isabelle/Isar framework (see
3.19 + \chref{ch:isar-framework}) should work reasonably well for any
3.20 + Isabelle object-logic that conforms to the natural deduction view of
3.21 + the Isabelle/Pure framework. Specific language elements introduced
3.22 + by the major object-logics are described in \chref{ch:hol}
3.23 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
3.24 (Isabelle/ZF). The main language elements are already provided by
3.25 the Isabelle/Pure framework. Nevertheless, examples given in the
4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Mon Feb 09 12:49:13 2009 +0100
4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Feb 09 12:52:16 2009 +0100
4.3 @@ -1,10 +1,9 @@
4.4 -
4.5 -(* $Id$ *)
4.6
4.7 set ThyOutput.source;
4.8 use "../../antiquote_setup.ML";
4.9
4.10 use_thy "Introduction";
4.11 +use_thy "Framework";
4.12 use_thy "Outer_Syntax";
4.13 use_thy "Document_Preparation";
4.14 use_thy "Spec";
5.1 --- a/doc-src/IsarRef/isar-ref.tex Mon Feb 09 12:49:13 2009 +0100
5.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Feb 09 12:52:16 2009 +0100
5.3 @@ -1,6 +1,3 @@
5.4 -
5.5 -%% $Id$
5.6 -
5.7 \documentclass[12pt,a4paper,fleqn]{report}
5.8 \usepackage{amssymb}
5.9 \usepackage[greek,english]{babel}
5.10 @@ -83,6 +80,7 @@
5.11 \pagenumbering{roman} \tableofcontents \clearfirst
5.12
5.13 \input{Thy/document/Introduction.tex}
5.14 +\input{Thy/document/Framework.tex}
5.15 \input{Thy/document/Outer_Syntax.tex}
5.16 \input{Thy/document/Document_Preparation.tex}
5.17 \input{Thy/document/Spec.tex}