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

author | wenzelm |

Mon, 09 Feb 2009 12:52:16 +0100 | |

changeset 29716 | b6266c4c68fe |

parent 29715 | c3233b483287 |

child 29717 | 51ed69c9422b |

basic setup for chapter "The Isabelle/Isar Framework";

--- a/doc-src/IsarRef/IsaMakefile Mon Feb 09 12:49:13 2009 +0100 +++ b/doc-src/IsarRef/IsaMakefile Mon Feb 09 12:52:16 2009 +0100 @@ -22,10 +22,10 @@ HOL-IsarRef: $(LOG)/HOL-IsarRef.gz $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy \ - Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy \ - Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy \ - Thy/Symbols.thy Thy/ML_Tactic.thy + Thy/Framework.thy Thy/Inner_Syntax.thy Thy/Introduction.thy \ + Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy \ + Thy/Document_Preparation.thy Thy/Generic.thy Thy/HOL_Specific.thy \ + Thy/Quick_Reference.thy Thy/Symbols.thy Thy/ML_Tactic.thy @$(USEDIR) -s IsarRef HOL Thy

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/Framework.thy Mon Feb 09 12:52:16 2009 +0100 @@ -0,0 +1,56 @@ +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

--- a/doc-src/IsarRef/Thy/Introduction.thy Mon Feb 09 12:49:13 2009 +0100 +++ b/doc-src/IsarRef/Thy/Introduction.thy Mon Feb 09 12:52:16 2009 +0100 @@ -1,5 +1,3 @@ -(* $Id$ *) - theory Introduction imports Main begin @@ -51,11 +49,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

--- a/doc-src/IsarRef/Thy/ROOT.ML Mon Feb 09 12:49:13 2009 +0100 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Feb 09 12:52:16 2009 +0100 @@ -1,10 +1,9 @@ - -(* $Id$ *) set ThyOutput.source; use "../../antiquote_setup.ML"; use_thy "Introduction"; +use_thy "Framework"; use_thy "Outer_Syntax"; use_thy "Document_Preparation"; use_thy "Spec";

--- a/doc-src/IsarRef/isar-ref.tex Mon Feb 09 12:49:13 2009 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Mon Feb 09 12:52:16 2009 +0100 @@ -1,6 +1,3 @@ - -%% $Id$ - \documentclass[12pt,a4paper,fleqn]{report} \usepackage{amssymb} \usepackage[greek,english]{babel} @@ -83,6 +80,7 @@ \pagenumbering{roman} \tableofcontents \clearfirst \input{Thy/document/Introduction.tex} +\input{Thy/document/Framework.tex} \input{Thy/document/Outer_Syntax.tex} \input{Thy/document/Document_Preparation.tex} \input{Thy/document/Spec.tex}