# HG changeset patch
# User wenzelm
# Date 1234180336 -3600
# Node ID b6266c4c68fe74df72c9d9f7d0d7768cb376fe85
# Parent  c3233b483287d348a9275183a61e73117505413a
basic setup for chapter "The Isabelle/Isar Framework";

diff -r c3233b483287 -r b6266c4c68fe doc-src/IsarRef/IsaMakefile
--- 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
 
 
diff -r c3233b483287 -r b6266c4c68fe doc-src/IsarRef/Thy/Framework.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
diff -r c3233b483287 -r b6266c4c68fe doc-src/IsarRef/Thy/Introduction.thy
--- 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
diff -r c3233b483287 -r b6266c4c68fe doc-src/IsarRef/Thy/ROOT.ML
--- 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";
diff -r c3233b483287 -r b6266c4c68fe doc-src/IsarRef/isar-ref.tex
--- 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}