# HG changeset patch # User nipkow # Date 1082211876 -7200 # Node ID a2bcb11ce445dfc9823488660ed46fa8667bd3bc # Parent b167b1b848d8c8a066fde7e0f1f5c51085192fe3 Added case distinction proof pattern. diff -r b167b1b848d8 -r a2bcb11ce445 doc-src/IsarOverview/Isar/Logic.thy --- 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 \ P\<^isub>2 \ 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*} diff -r b167b1b848d8 -r a2bcb11ce445 doc-src/IsarOverview/Isar/document/Induction.tex --- 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% diff -r b167b1b848d8 -r a2bcb11ce445 doc-src/IsarOverview/Isar/document/Logic.tex --- 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% diff -r b167b1b848d8 -r a2bcb11ce445 doc-src/IsarOverview/Isar/document/isabelle.sty --- 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=`\! diff -r b167b1b848d8 -r a2bcb11ce445 doc-src/IsarOverview/Isar/document/root.tex --- 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,