# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1223571530 14400
# Node ID 2356e5c70d98b5df83c3840b3050c167704e6b5c
# Parent  5ae6a1bb91c9e15024a4b74904c547896e4e0b1f
added a proof and tuned the rest

diff -r 5ae6a1bb91c9 -r 2356e5c70d98 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Mon Oct 06 10:11:08 2008 -0400
+++ b/CookBook/FirstSteps.thy	Thu Oct 09 12:58:50 2008 -0400
@@ -168,10 +168,11 @@
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
 
-  In a similar way you can use antiquotations to refer to theorems:
+  In a similar way you can use antiquotations to refer to theorems or simpsets:
 *}
 
 ML {* @{thm allI} *}
+ML {* @{simpset} *}
 
 text {*
   In the course of this introduction, we will learn more about 
@@ -412,7 +413,7 @@
    shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  on the ML level:\footnote{Note that @{text "|>"} is just reverse
+  on the ML level:\footnote{Note that @{text "|>"} is reverse
   application. This combinator, and several variants are defined in
   @{ML_file "Pure/General/basics.ML"}.}
 
@@ -440,6 +441,22 @@
 
 text {*
 
+  This code-snippet constructs the following proof:
+
+  \[
+  \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
+    {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+       {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+          {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+                 {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
+                 &
+           \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
+          }
+       }
+    }
+  \]
+
+
   \begin{readmore}
   For how the functions @{text "assume"}, @{text "forall_elim"} etc work
   see \isccite{sec:thms}. The basic functions for theorems are defined in
@@ -468,6 +485,8 @@
   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
   prop"} is just the identity function and used as a syntactic marker. 
   
+  (FIXME: maybe show how this is printed on the screen) 
+
   \begin{readmore}
   For more on goals see \isccite{sec:tactical-goals}. 
   \end{readmore}
@@ -502,13 +521,12 @@
 
 
 text {*
-  
-  To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
-  sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
-  the variables @{text params} that will be generalised once the
-  goal is proved; @{text "tac"} is a function that returns a tactic having some funny 
-  input parameters (FIXME by possibly having an explanation in the implementation-manual). 
-
+  To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets 
+  up a goal state for proving the goal @{text C} under the assumptions @{text As} 
+  (empty in the proof at hand) 
+  with the variables @{text xs} that will be generalised once the
+  goal is proved. The @{text "tac"} is the tactic which proves the goal and which 
+  can make use of the local assumptions.
 *}
 
 
@@ -527,6 +545,15 @@
 end
 *}
 
+text {*
+
+  \begin{readmore}
+  To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+  \end{readmore}
+
+*}
+
+
 text {* An alternative way to transcribe this proof is as follows *}
 
 ML {*
@@ -543,10 +570,11 @@
 end
 *}
 
+text {* (FIXME: are there any advantages/disadvantages about this way?) *}
+
 section {* Storing Theorems *}
 
 section {* Theorem Attributes *}
 
-text {* Was changing theorems. *}
 
 end
\ No newline at end of file
diff -r 5ae6a1bb91c9 -r 2356e5c70d98 CookBook/document/proof.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/document/proof.sty	Thu Oct 09 12:58:50 2008 -0400
@@ -0,0 +1,278 @@
+%       proof.sty       (Proof Figure Macros)
+%
+%       version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
+%       Mar 6, 1997
+%       Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.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>.
+%
+%       \infer=<Lower><Uppers>
+%               draws a double-ruled deduction.
+%
+%       \infer=[<Label>]<Lower><Uppers>
+%               draws a double-ruled 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@DoubleRule    % whether \@infer draws doulbe rules.
+\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 }
+
+%       Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+    \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+      \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+          \let\reserved@d\reserved@b\fi
+      \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+       \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
+       \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+       \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+       \@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, it draws a rule and <Label> is right to
+%               a rule. In this case, if \@DoubleRuletrue, it draws
+%               double rules.
+%
+%               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
+               \if@DoubleRule
+               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+                       \kern 1pt\hrule width\RuleWidth}\relax
+               \else
+               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+               \fi
+               \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 5ae6a1bb91c9 -r 2356e5c70d98 CookBook/document/root.tex
--- a/CookBook/document/root.tex	Mon Oct 06 10:11:08 2008 -0400
+++ b/CookBook/document/root.tex	Thu Oct 09 12:58:50 2008 -0400
@@ -4,6 +4,7 @@
 \usepackage{isabellesym}
 \usepackage{charter}
 \usepackage[pdftex]{graphicx}
+\usepackage{proof}
 
 % Cross references to other manuals:
 \usepackage{xr}
diff -r 5ae6a1bb91c9 -r 2356e5c70d98 cookbook.pdf
Binary file cookbook.pdf has changed