Added case distinction proof pattern.

--- a/doc-src/IsarOverview/Isar/Logic.thy	Sat Apr 17 14:57:50 2004 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Sat Apr 17 16:24:36 2004 +0200
@@ -543,7 +543,38 @@
 tactics but state the desired form explicitly and let the tactic verify
 that from this form the original goal follows.
 \end{quote}
-This yields more readable and also more robust proofs. *}
+This yields more readable and also more robust proofs.
+
+\subsubsection{General case distinctions}
+
+As an important application of raw proof blocks we show how to deal
+with general case distinctions --- more specific kinds are treated in
+\S\ref{sec:CaseDistinction}. Imagine that you would like to prove some
+goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that
+the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and
+that each case $P_i$ implies the goal. Taken together, this proves the
+goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:
+*}
+text_raw{*\renewcommand{\isamarkupcmt}[1]{#1}*}
+(*<*)lemma "XXX"(*>*)
+proof -
+  have "P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3" (*<*)sorry(*>*) -- {*\dots*}
+  moreover
+  { assume P\<^isub>1
+    -- {*\dots*}
+    have ?thesis (*<*)sorry(*>*) -- {*\dots*} }
+  moreover
+  { assume P\<^isub>2
+    -- {*\dots*}
+    have ?thesis (*<*)sorry(*>*) -- {*\dots*} }
+  moreover
+  { assume P\<^isub>3
+    -- {*\dots*}
+    have ?thesis (*<*)sorry(*>*) -- {*\dots*} }
+  ultimately show ?thesis by blast
+qed
+text_raw{*\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}*}
+
 
 subsection{*Further refinements*}
 

--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Sat Apr 17 14:57:50 2004 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Sat Apr 17 16:24:36 2004 +0200
@@ -246,7 +246,7 @@
 \isacommand{next}\isanewline
 \ \ \ \ \isamarkupfalse%
 \isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
-\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}%
+\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}} \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}m\ {\isacharless}\ Suc\ n{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}}%
 }
 \isanewline
 \ \ \ \ \isamarkupfalse%

--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Sat Apr 17 14:57:50 2004 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Sat Apr 17 16:24:36 2004 +0200
@@ -931,10 +931,86 @@
 tactics but state the desired form explicitly and let the tactic verify
 that from this form the original goal follows.
 \end{quote}
-This yields more readable and also more robust proofs.%
+This yields more readable and also more robust proofs.
+
+\subsubsection{General case distinctions}
+
+As an important application of raw proof blocks we show how to deal
+with general case distinctions --- more specific kinds are treated in
+\S\ref{sec:CaseDistinction}. Imagine that you would like to prove some
+goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that
+the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and
+that each case $P_i$ implies the goal. Taken together, this proves the
+goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\renewcommand{\isamarkupcmt}[1]{#1}
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline
+\ \ \ \ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline
+\ \ \ \ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline
+\ \ \ \ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{ultimately}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{by}\ blast\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+%
 \isamarkupsubsection{Further refinements%
 }
 \isamarkuptrue%
@@ -1020,7 +1096,7 @@
 \noindent The concrete syntax is dropped at the end of the proof and the
 theorem becomes \begin{isabelle}%
 {\isasymlbrakk}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}f\ x\ y\ {\isacharequal}\ {\isacharquery}f\ y\ x{\isacharsemicolon}\isanewline
-\isaindent{\ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}r\ x\ y\ {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ x\ z{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ y\ z{\isacharparenright}{\isacharsemicolon}\ {\isacharquery}r\ {\isacharquery}x\ {\isacharquery}y{\isasymrbrakk}\isanewline
+\isaindent{\ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}r\ x\ y\ {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ x\ z{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ y\ z{\isacharparenright}{\isacharsemicolon}\ {\isacharquery}r\ {\isacharquery}x\ {\isacharquery}y{\isasymrbrakk}\isanewline
 {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}x{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}y{\isacharparenright}%
 \end{isabelle}
 \tweakskip%

--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Sat Apr 17 14:57:50 2004 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Sat Apr 17 16:24:36 2004 +0200
@@ -24,8 +24,18 @@
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+% somewhat hackish: spanning sub/super scripts (\<^bsub>..\<^esub>)
+\newcommand{\isactrlbsub}{%
+\def\isatext##1{\isastylescript##1}\begin{math}_\bgroup}
+\newcommand{\isactrlesub}{\egroup\end{math}}
+\newcommand{\isactrlbsup}{%
+\def\isatext##1{\isastylescript##1}\begin{math}^\bgroup}
+\newcommand{\isactrlesup}{\egroup\end{math}}
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -42,6 +52,7 @@
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
 \newcommand{\isadigit}[1]{#1}
 
 \chardef\isacharbang=`\!

--- a/doc-src/IsarOverview/Isar/document/root.tex	Sat Apr 17 14:57:50 2004 +0200
+++ b/doc-src/IsarOverview/Isar/document/root.tex	Sat Apr 17 16:24:36 2004 +0200
@@ -7,7 +7,6 @@
 %\isabellestyle{it}
 
 \newcommand{\tweakskip}{\vspace{-\medskipamount}}
-\newcommand{\Tweakskip}{\tweakskip\tweakskip}
 
 \pagestyle{plain}
 
@@ -32,10 +31,8 @@
 
 \input{intro.tex}
 \input{Logic.tex}
-\Tweakskip\Tweakskip
 \input{Induction.tex}
 
-%\Tweakskip
 \small
 \paragraph{Acknowledgement}
 I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,