author nipkow Sat, 17 Apr 2004 16:24:36 +0200 changeset 14617 a2bcb11ce445 parent 14616 b167b1b848d8 child 14618 068bb99f3ebd
--- 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%
+\ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\ \ \ \ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\ \ \ \ %
+\isamarkupcmt{\dots%
+}
+\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
+\ %
+\isamarkupcmt{\dots%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\ \ \ \ %
+\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}}

\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,`