# HG changeset patch
# User wenzelm
# Date 939667463 -7200
# Node ID f5288e4b95d138f53e9be7a1a6bfdef21fd29123
# Parent  77bac5d8416227e957c43efb6c58fb73acf40dfe
improved presentation;

diff -r 77bac5d84162 -r f5288e4b95d1 src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Mon Oct 11 20:43:38 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Mon Oct 11 20:44:23 1999 +0200
@@ -170,7 +170,7 @@
  This may be avoided using \isacommand{from} to focus on $\idt{prems}$
  (i.e.\ the $A \conj B$ assumption) as the current facts, enabling the
  use of double-dot proofs.  Note that \isacommand{from} already
- involves forward-chaining.
+ does forward-chaining, involving the \name{conjE} rule.
 *};
 
 lemma "A & B --> B & A";
@@ -217,7 +217,7 @@
 qed;
 
 text {*
- We can still push forward reasoning a bit further, even at the danger
+ We can still push forward reasoning a bit further, even at the risk
  of getting ridiculous.  Note that we force the initial proof step to
  do nothing, by referring to the ``-'' proof method.
 *};
@@ -246,7 +246,7 @@
  is no single best way to arrange some pieces of formal reasoning, of
  course.  Depending on the actual applications, the intended audience
  etc., certain aspects such as rules~/ methods vs.\ facts have to be
- emphasised in an appropriate way.  This requires the proof writer to
+ emphasized in an appropriate way.  This requires the proof writer to
  develop good taste, and some practice, of course.
 *};
 
@@ -275,15 +275,58 @@
 
 text {*
  We rephrase some of the basic reasoning examples of
- \cite{isabelle-intro}.
+ \cite{isabelle-intro} (using HOL rather than FOL).
 *};
 
-subsubsection {* Propositional proof *};
+subsubsection {* A propositional proof *};
+
+text {*
+ We consider the proposition $P \disj P \impl P$.  The proof below
+ involves forward-chaining from $P \disj P$, followed by an explicit
+ case-analysis on the two \emph{identical} cases.
+*};
 
 lemma "P | P --> P";
 proof;
   assume "P | P";
-  then; show P;
+  thus P;
+  proof                    -- {*
+    rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
+  *};
+    assume P; show P; .;
+  next;
+    assume P; show P; .;
+  qed;
+qed;
+
+text {*
+ Case splits are \emph{not} hardwired into the Isar language as a
+ special feature.  The \isacommand{next} command used to separate the
+ cases above is just a short form of managing block structure.
+
+ \medskip In general, applying proof methods may split up a goal into
+ separate ``cases'', i.e.\ new subgoals with individual local
+ assumptions.  The corresponding proof text typically mimics this by
+ establishing results in appropriate contexts, separated by blocks.
+
+ In order to avoid too much explicit bracketing, the Isar system
+ implicitly opens an additional block for any new goal, the
+ \isacommand{next} statement then closes one block level, opening a
+ new one.  The resulting behavior is what one might expect from
+ separating cases, only that it is more flexible.  E.g. an induction
+ base case (which does not introduce local assumptions) would
+ \emph{not} require \isacommand{next} to separate the subsequent step
+ case.
+
+ \medskip In our example the situation is even simpler, since the two
+ ``cases'' actually coincide.  Consequently the proof may be rephrased
+ as follows.
+*};
+
+lemma "P | P --> P";
+proof;
+  assume "P | P";
+  thus P;
   proof;
     assume P;
     show P; .;
@@ -291,61 +334,90 @@
   qed;
 qed;
 
+text {*
+ Again, the rather vacuous body of the proof may be collapsed.  Thus
+ the case analysis degenerates into two assumption steps, which
+ are implicitly performed when concluding the single rule step of the
+ double-dot proof below.
+*};
+
 lemma "P | P --> P";
 proof;
   assume "P | P";
-  then; show P; ..;
+  thus P; ..;
 qed;
 
 
-subsubsection {* Quantifier proof *};
+subsubsection {* A quantifier proof *};
+
+text {*
+ To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
+ x)) \impl (\ex x P \ap x)$.  Informally, this holds because any $a$
+ with $P \ap (f \ap a)$ may be taken as a witness for the second
+ existential statement.
 
-lemma "(EX x. P(f(x))) --> (EX x. P(x))";
+ The first proof is rather verbose, exhibiting quite a lot of
+ (redundant) detail.  It gives explicit rules, even with some
+ instantiation.  Furthermore, we encounter two new language elements:
+ the \isacommand{fix} command augments the context by some new
+ ``arbitrary, but fixed'' element; the \isacommand{is} annotation
+ binds term abbreviations by higher-order pattern matching.
+*};
+
+lemma "(EX x. P (f x)) --> (EX x. P x)";
 proof;
-  assume "EX x. P(f(x))";
-  then; show "EX x. P(x)";
-  proof (rule exE);
+  assume "EX x. P (f x)";
+  thus "EX x. P x";
+  proof (rule exE)             -- {*
+    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
+  *};
     fix a;
-    assume "P(f(a))" (is "P(?witness)");
+    assume "P (f a)" (is "P ?witness");
     show ?thesis; by (rule exI [of P ?witness]);
   qed;
 qed;
 
-lemma "(EX x. P(f(x))) --> (EX x. P(x))";
+text {*
+ While explicit rule instantiation may occasionally help to improve
+ the readability of certain aspects of reasoning it is usually quite
+ redundant.  Above, the basic proof outline gives already enough
+ structural clues for the system to infer both the rules and their
+ instances (by higher-order unification).  Thus we may as well prune
+ the text as follows.
+*};
+
+lemma "(EX x. P (f x)) --> (EX x. P x)";
 proof;
-  assume "EX x. P(f(x))";
-  then; show "EX x. P(x)";
+  assume "EX x. P (f x)";
+  thus "EX x. P x";
   proof;
     fix a;
-    assume "P(f(a))";
+    assume "P (f a)";
     show ?thesis; ..;
   qed;
 qed;
 
-lemma "(EX x. P(f(x))) --> (EX x. P(x))";
-  by blast;
-
 
 subsubsection {* Deriving rules in Isabelle *};
 
-text {* We derive the conjunction elimination rule from the
- projections.  The proof below follows the basic reasoning of the
- script given in the Isabelle Intro Manual closely.  Although, the
- actual underlying operations on rules and proof states are quite
- different: Isabelle/Isar supports non-atomic goals and assumptions
- fully transparently, while the original Isabelle classic script
- depends on the primitive goal command to decompose the rule into
- premises and conclusion, with the result emerging by discharging the
- context again later. *};
+text {*
+ We derive the conjunction elimination rule from the projections.  The
+ proof below follows is quite straight-forward, since Isabelle/Isar
+ supports non-atomic goals and assumptions fully transparently.  Note
+ that this is in contrast to classic Isabelle: the corresponding
+ tactic script given in \cite{isabelle-intro} depends on the primitive
+ goal command to decompose the rule into premises and conclusion, with
+ the result emerging by discharging the context again later.
+*};
 
 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
 proof -;
-  assume ab: "A & B";
+  assume "A & B";
   assume ab_c: "A ==> B ==> C";
   show C;
   proof (rule ab_c);
-    from ab; show A; ..;
-    from ab; show B; ..;
+    show A; by (rule conjunct1);
+    show B; by (rule conjunct2);
   qed;
 qed;
 
diff -r 77bac5d84162 -r f5288e4b95d1 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:43:38 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Mon Oct 11 20:44:23 1999 +0200
@@ -5,11 +5,8 @@
 
 header {* Cantor's Theorem *};
 
-theory Cantor = Main:;
-
-text {*
- This is an Isar'ized version of the final example of the Isabelle/HOL
- manual \cite{isabelle-HOL}.
+theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
+ the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
 *};
 
 text {*
diff -r 77bac5d84162 -r f5288e4b95d1 src/HOL/Isar_examples/document/proof.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/document/proof.sty	Mon Oct 11 20:44:23 1999 +0200
@@ -0,0 +1,254 @@
+%       proof.sty       (Proof Figure Macros)
+%
+%       version 1.0
+%       October 13, 1990
+%       Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
+%
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+%
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+%       Usage:
+%               In \documentstyle, specify an optional style `proof', say,
+%                       \documentstyle[proof]{article}.
+%
+%       The following macros are available:
+%
+%       In all the following macros, all the arguments such as
+%       <Lowers> and <Uppers> are processed in math mode.
+%
+%       \infer<Lower><Uppers>
+%               draws an inference.
+%
+%               Use & in <Uppers> to delimit upper formulae.
+%               <Uppers> consists more than 0 formulae.
+%
+%               \infer returns \hbox{ ... } or \vbox{ ... } and
+%               sets \@LeftOffset and \@RightOffset globally.
+%
+%       \infer[<Label>]<Lower><Uppers>
+%               draws an inference labeled with <Label>.
+%
+%       \infer*<Lower><Uppers>
+%               draws a many step deduction.
+%
+%       \infer*[<Label>]<Lower><Uppers>
+%               draws a many step deduction labeled with <Label>.
+%
+%       \deduce<Lower><Uppers>
+%               draws an inference without a rule.
+%
+%       \deduce[<Proof>]<Lower><Uppers>
+%               draws a many step deduction with a proof name.
+%
+%       Example:
+%               If you want to write
+%                           B C
+%                          -----
+%                      A     D
+%                     ----------
+%                         E
+%       use
+%               \infer{E}{
+%                       A
+%                       &
+%                       \infer{D}{B & C}
+%               }
+%
+
+%       Style Parameters
+
+\newdimen\inferLineSkip         \inferLineSkip=2pt
+\newdimen\inferLabelSkip        \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+%       Variables
+
+\newdimen\@LeftOffset   % global
+\newdimen\@RightOffset  % global
+\newdimen\@SavedLeftOffset      % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+%       Flags
+
+\newif\if@inferRule     % whether \@infer draws a rule.
+\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved     % whether inner math mode where \infer or
+                        % \deduce appears.
+
+%       Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+%       Math Save Macros
+%
+%       \@SaveMath is called in the very begining of toplevel macros
+%       which are \infer and \deduce.
+%       \@RestoreMath is called in the very last before toplevel macros end.
+%       Remark \infer and \deduce ends calling \@infer.
+
+%\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
+%        \relax $\relax \@MathSavedtrue \fi\fi }
+%
+%\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+
+\def\@SaveMath{\relax}
+\def\@RestoreMath{\relax}
+
+
+%       Macros
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+        \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
+
+\def\@inferOneStep{\@inferRuletrue
+        \@ifnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
+        {\@inferRulefalse \@infer[\@empty]}}
+
+%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+        \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+
+%       \@infer[<Label>]<Lower><Uppers>
+%               If \@inferRuletrue, draws a rule and <Label> is right to
+%               a rule.
+%               Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+        \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+        \setbox\@LabelPart=\hbox{$#1$}\relax
+        \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+        \global\@LeftOffset=0pt
+        \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+                \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+                \inferTabSkip
+                \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+                #3\cr}}\relax
+%                       Here is a little trick.
+%                       \@ReturnLeftOffsettrue(false) influences on \infer or
+%                       \deduce placed in ## locally
+%                       because of \@SaveMath and \@RestoreMath.
+        \UpperLeftOffset=\@LeftOffset
+        \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+        \LowerWidth=\wd\@LowerPart
+        \LowerHeight=\ht\@LowerPart
+        \LowerCenter=0.5\LowerWidth
+%
+        \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+        \advance\UpperWidth by -\UpperRightOffset
+        \UpperCenter=\UpperLeftOffset
+        \advance\UpperCenter by 0.5\UpperWidth
+%
+        \ifdim \UpperWidth > \LowerWidth
+                % \UpperCenter > \LowerCenter
+        \UpperAdjust=0pt
+        \RuleAdjust=\UpperLeftOffset
+        \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+        \RuleWidth=\UpperWidth
+        \global\@LeftOffset=\LowerAdjust
+%
+        \else   % \UpperWidth <= \LowerWidth
+        \ifdim \UpperCenter > \LowerCenter
+%
+        \UpperAdjust=0pt
+        \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+        \LowerAdjust=\RuleAdjust
+        \RuleWidth=\LowerWidth
+        \global\@LeftOffset=\LowerAdjust
+%
+        \else   % \UpperWidth <= \LowerWidth
+                % \UpperCenter <= \LowerCenter
+%
+        \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+        \RuleAdjust=0pt
+        \LowerAdjust=0pt
+        \RuleWidth=\LowerWidth
+        \global\@LeftOffset=0pt
+%
+        \fi\fi
+% Make a box
+        \if@inferRule
+%
+        \setbox\ResultBox=\vbox{
+                \moveright \UpperAdjust \box\@UpperPart
+                \nointerlineskip \kern\inferLineSkip
+                \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+                \nointerlineskip \kern\inferLineSkip
+                \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+        \@ifEmpty{#1}{}{\relax
+%
+        \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
+        \advance\HLabelAdjust by -\RuleWidth
+        \WidthAdjust=\HLabelAdjust
+        \advance\WidthAdjust by -\inferLabelSkip
+        \advance\WidthAdjust by -\wd\@LabelPart
+        \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+        \VLabelAdjust=\dp\@LabelPart
+        \advance\VLabelAdjust by -\ht\@LabelPart
+        \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
+        \advance\VLabelAdjust by \inferLineSkip
+%
+        \setbox\ResultBox=\hbox{\box\ResultBox
+                \kern -\HLabelAdjust \kern\inferLabelSkip
+                \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+        }\relax % end @ifEmpty
+%
+        \else % \@inferRulefalse
+%
+        \setbox\ResultBox=\vbox{
+                \moveright \UpperAdjust \box\@UpperPart
+                \nointerlineskip \kern\inferLineSkip
+                \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+                        \@ifEmpty{#1}{}{\relax
+                        \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+        \fi
+%
+        \global\@RightOffset=\wd\ResultBox
+        \global\advance\@RightOffset by -\@LeftOffset
+        \global\advance\@RightOffset by -\LowerWidth
+        \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+        \box\ResultBox
+        \@RestoreMath
+}
diff -r 77bac5d84162 -r f5288e4b95d1 src/HOL/Isar_examples/document/style.tex
--- a/src/HOL/Isar_examples/document/style.tex	Mon Oct 11 20:43:38 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex	Mon Oct 11 20:44:23 1999 +0200
@@ -2,12 +2,12 @@
 %% $Id$
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{comment,isabelle,pdfsetup}
+\usepackage{comment,proof,isabelle,pdfsetup}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
 \parindent 0pt \parskip 0.5ex
 
-\newcommand{\name}[1]{\textsf{#1}}
+\newcommand{\name}[1]{\textsl{#1}}
 
 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
 \newcommand{\var}[1]{{?\!#1}}
@@ -22,6 +22,7 @@
 \newcommand{\ex}[1]{\exists #1\dt\;}
 \newcommand{\impl}{\rightarrow}
 \newcommand{\conj}{\land}
+\newcommand{\disj}{\lor}
 
 
 %%% Local Variables: