--- a/doc-src/ProgProve/Thys/document/Isar.tex Mon Aug 27 21:46:00 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1682 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Isar}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-Apply-scripts are unreadable and hard to maintain. The language of choice
-for larger proofs is \concept{Isar}. The two key features of Isar are:
-\begin{itemize}
-\item It is structured, not linear.
-\item It is readable without running it because
-you need to state what you are proving at any given point.
-\end{itemize}
-Whereas apply-scripts are like assembly language programs, Isar proofs
-are like structured programs with comments. A typical Isar proof looks like this:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{tabular}{@ {}l}
-\isacom{proof}\\
-\quad\isacom{assume} \isa{{\isaliteral{22}{\isachardoublequote}}}$\mathit{formula}_0$\isa{{\isaliteral{22}{\isachardoublequote}}}\\
-\quad\isacom{have} \isa{{\isaliteral{22}{\isachardoublequote}}}$\mathit{formula}_1$\isa{{\isaliteral{22}{\isachardoublequote}}} \quad\isacom{by} \isa{simp}\\
-\quad\vdots\\
-\quad\isacom{have} \isa{{\isaliteral{22}{\isachardoublequote}}}$\mathit{formula}_n$\isa{{\isaliteral{22}{\isachardoublequote}}} \quad\isacom{by} \isa{blast}\\
-\quad\isacom{show} \isa{{\isaliteral{22}{\isachardoublequote}}}$\mathit{formula}_{n+1}$\isa{{\isaliteral{22}{\isachardoublequote}}} \quad\isacom{by} \isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}\\
-\isacom{qed}
-\end{tabular}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$
-(provided each proof step succeeds).
-The intermediate \isacom{have} statements are merely stepping stones
-on the way towards the \isacom{show} statement that proves the actual
-goal. In more detail, this is the Isar core syntax:
-\medskip
-
-\begin{tabular}{@ {}lcl@ {}}
-\textit{proof} &=& \isacom{by} \textit{method}\\
- &$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed}
-\end{tabular}
-\medskip
-
-\begin{tabular}{@ {}lcl@ {}}
-\textit{step} &=& \isacom{fix} \textit{variables} \\
- &$\mid$& \isacom{assume} \textit{proposition} \\
- &$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof}
-\end{tabular}
-\medskip
-
-\begin{tabular}{@ {}lcl@ {}}
-\textit{proposition} &=& [\textit{name}:] \isa{{\isaliteral{22}{\isachardoublequote}}}\textit{formula}\isa{{\isaliteral{22}{\isachardoublequote}}}
-\end{tabular}
-\medskip
-
-\begin{tabular}{@ {}lcl@ {}}
-\textit{fact} &=& \textit{name} \ $\mid$ \ \dots
-\end{tabular}
-\medskip
-
-\noindent A proof can either be an atomic \isacom{by} with a single proof
-method which must finish off the statement being proved, for example \isa{auto}. Or it can be a \isacom{proof}--\isacom{qed} block of multiple
-steps. Such a block can optionally begin with a proof method that indicates
-how to start off the proof, e.g.\ \mbox{\isa{{\isaliteral{28}{\isacharparenleft}}induction\ xs{\isaliteral{29}{\isacharparenright}}}}.
-
-A step either assumes a proposition or states a proposition
-together with its proof. The optional \isacom{from} clause
-indicates which facts are to be used in the proof.
-Intermediate propositions are stated with \isacom{have}, the overall goal
-with \isacom{show}. A step can also introduce new local variables with
-\isacom{fix}. Logically, \isacom{fix} introduces \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-quantified
-variables, \isacom{assume} introduces the assumption of an implication
-(\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}) and \isacom{have}/\isacom{show} the conclusion.
-
-Propositions are optionally named formulas. These names can be referred to in
-later \isacom{from} clauses. In the simplest case, a fact is such a name.
-But facts can also be composed with \isa{OF} and \isa{of} as shown in
-\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
-that assumptions, intermediate \isacom{have} statements and global lemmas all
-have the same status and are thus collectively referred to as
-\concept{facts}.
-
-Fact names can stand for whole lists of facts. For example, if \isa{f} is
-defined by command \isacom{fun}, \isa{f{\isaliteral{2E}{\isachardot}}simps} refers to the whole list of
-recursion equations defining \isa{f}. Individual facts can be selected by
-writing \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}, whole sublists by \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}}.
-
-
-\section{Isar by example}
-
-We show a number of proofs of Cantor's theorem that a function from a set to
-its powerset cannot be surjective, illustrating various features of Isar. The
-constant \isa{surj} is predefined.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj{\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}surj\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ {\isadigit{0}}\ \isacommand{have}\isamarkupfalse%
-\ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ surj{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ {\isadigit{1}}\ \isacommand{have}\isamarkupfalse%
-\ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ {\isadigit{2}}\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The \isacom{proof} command lacks an explicit method how to perform
-the proof. In such cases Isabelle tries to use some standard introduction
-rule, in the above case for \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}}:
-\[
-\inferrule{
-\mbox{\isa{P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}}}
-{\mbox{\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}}}
-\]
-In order to prove \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, assume \isa{P} and show \isa{False}.
-Thus we may assume \isa{surj\ f}. The proof shows that names of propositions
-may be (single!) digits---meaningful names are hard to invent and are often
-not necessary. Both \isacom{have} steps are obvious. The second one introduces
-the diagonal set \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}}, the key idea in the proof.
-If you wonder why \isa{{\isadigit{2}}} directly implies \isa{False}: from \isa{{\isadigit{2}}}
-it follows that \isa{{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ f\ a{\isaliteral{29}{\isacharparenright}}}.
-
-\subsection{\isa{this}, \isa{then}, \isa{hence} and \isa{thus}}
-
-Labels should be avoided. They interrupt the flow of the reader who has to
-scan the context for the point where the label was introduced. Ideally, the
-proof is a linear flow, where the output of one step becomes the input of the
-next step, piping the previously proved fact into the next proof, just like
-in a UNIX pipe. In such cases the predefined name \isa{this} can be used
-to refer to the proposition proved in the previous step. This allows us to
-eliminate all labels from our proof (we suppress the \isacom{lemma} statement):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}surj\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ this\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ surj{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ this\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-We have also taken the opportunity to compress the two \isacom{have}
-steps into one.
-
-To compact the text further, Isar has a few convenient abbreviations:
-\medskip
-
-\begin{tabular}{rcl}
-\isacom{then} &=& \isacom{from} \isa{this}\\
-\isacom{thus} &=& \isacom{then} \isacom{show}\\
-\isacom{hence} &=& \isacom{then} \isacom{have}
-\end{tabular}
-\medskip
-
-\noindent
-With the help of these abbreviations the proof becomes%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}surj\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{hence}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ surj{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-There are two further linguistic variations:
-\medskip
-
-\begin{tabular}{rcl}
-(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts}
-&=&
-\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
-\isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this}
-\end{tabular}
-\medskip
-
-\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
-behind the proposition.
-
-\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
-
-Lemmas can also be stated in a more structured fashion. To demonstrate this
-feature with Cantor's theorem, we rephrase \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f}
-a little:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{assumes}\ s{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}surj\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-The optional \isacom{fixes} part allows you to state the types of
-variables up front rather than by decorating one of their occurrences in the
-formula with a type constraint. The key advantage of the structured format is
-the \isacom{assumes} part that allows you to name each assumption; multiple
-assumptions can be separated by \isacom{and}. The
-\isacom{shows} part gives the goal. The actual theorem that will come out of
-the proof is \isa{surj\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}, but during the proof the assumption
-\isa{surj\ f} is available under the name \isa{s} like any other fact.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
-\ s\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ surj{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-In the \isacom{have} step the assumption \isa{surj\ f} is now
-referenced by its name \isa{s}. The duplication of \isa{surj\ f} in the
-above proofs (once in the statement of the lemma, once in its proof) has been
-eliminated.
-
-\begin{warn}
-Note the dash after the \isacom{proof}
-command. It is the null method that does nothing to the goal. Leaving it out
-would ask Isabelle to try some suitable introduction rule on the goal \isa{False}---but there is no suitable introduction rule and \isacom{proof}
-would fail.
-\end{warn}
-
-Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
-name \isa{assms} that stands for the list of all assumptions. You can refer
-to individual assumptions by \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}, \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} etc,
-thus obviating the need to name them individually.
-
-\section{Proof patterns}
-
-We show a number of important basic proof patterns. Many of them arise from
-the rules of natural deduction that are applied by \isacom{proof} by
-default. The patterns are phrased in terms of \isacom{show} but work for
-\isacom{have} and \isacom{lemma}, too.
-
-We start with two forms of \concept{case analysis}:
-starting from a formula \isa{P} we have the two cases \isa{P} and
-\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, and starting from a fact \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}
-we have the two cases \isa{P} and \isa{Q}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ cases\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}Q{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-\end{tabular}
-\medskip
-\begin{isamarkuptext}%
-How to prove a logical equivalence:
-\end{isamarkuptext}%
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}Q{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}Q{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\medskip
-\begin{isamarkuptext}%
-Proofs by contradiction:
-\end{isamarkuptext}%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}rule\ ccontr{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}P{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-\end{tabular}
-\medskip
-\begin{isamarkuptext}%
-The name \isa{ccontr} stands for ``classical contradiction''.
-
-How to prove quantified formulas:
-\end{isamarkuptext}%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}witness{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-\end{tabular}
-\medskip
-\begin{isamarkuptext}%
-In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}},
-the step \isacom{fix}~\isa{x} introduces a locally fixed variable \isa{x}
-into the subproof, the proverbial ``arbitrary but fixed value''.
-Instead of \isa{x} we could have chosen any name in the subproof.
-In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}},
-\isa{witness} is some arbitrary
-term for which we can prove that it satisfies \isa{P}.
-
-How to reason forward from \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}:
-\end{isamarkuptext}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{then}\isamarkupfalse%
-\ \isacommand{obtain}\isamarkupfalse%
-\ x\ \isakeyword{where}\ p{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-After the \isacom{obtain} step, \isa{x} (we could have chosen any name)
-is a fixed local
-variable, and \isa{p} is the name of the fact
-\noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}.
-This pattern works for one or more \isa{x}.
-As an example of the \isacom{obtain} command, here is the proof of
-Cantor's theorem in more detail:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj{\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}surj\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{hence}\isamarkupfalse%
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ surj{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{obtain}\isamarkupfalse%
-\ a\ \isakeyword{where}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{hence}\isamarkupfalse%
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ a\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}False{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-
-Finally, how to prove set equality and subset relationship:
-\end{isamarkuptext}%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-\end{tabular}
-\begin{isamarkuptext}%
-\section{Streamlining proofs}
-
-\subsection{Pattern matching and quotations}
-
-In the proof patterns shown above, formulas are often duplicated.
-This can make the text harder to read, write and maintain. Pattern matching
-is an abbreviation mechanism to avoid such duplication. Writing
-\begin{quote}
-\isacom{show} \ \textit{formula} \isa{{\isaliteral{28}{\isacharparenleft}}}\isacom{is} \textit{pattern}\isa{{\isaliteral{29}{\isacharparenright}}}
-\end{quote}
-matches the pattern against the formula, thus instantiating the unknowns in
-the pattern for later use. As an example, consider the proof pattern for
-\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}}:
-\end{isamarkuptext}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}formula\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ formula\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}L\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}L{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}R{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}R{\isaliteral{22}{\isachardoublequoteclose}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}L{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Instead of duplicating \isa{formula\isaliteral{5C3C5E697375623E}{}\isactrlisub i} in the text, we introduce
-the two abbreviations \isa{{\isaliteral{3F}{\isacharquery}}L} and \isa{{\isaliteral{3F}{\isacharquery}}R} by pattern matching.
-Pattern matching works wherever a formula is stated, in particular
-with \isacom{have} and \isacom{lemma}.
-
-The unknown \isa{{\isaliteral{3F}{\isacharquery}}thesis} is implicitly matched against any goal stated by
-\isacom{lemma} or \isacom{show}. Here is a typical example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}formula{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}%
-\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Unknowns can also be instantiated with \isacom{let} commands
-\begin{quote}
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}t} = \isa{{\isaliteral{22}{\isachardoublequote}}}\textit{some-big-term}\isa{{\isaliteral{22}{\isachardoublequote}}}
-\end{quote}
-Later proof steps can refer to \isa{{\isaliteral{3F}{\isacharquery}}t}:
-\begin{quote}
-\isacom{have} \isa{{\isaliteral{22}{\isachardoublequote}}}\dots \isa{{\isaliteral{3F}{\isacharquery}}t} \dots\isa{{\isaliteral{22}{\isachardoublequote}}}
-\end{quote}
-\begin{warn}
-Names of facts are introduced with \isa{name{\isaliteral{3A}{\isacharcolon}}} and refer to proved
-theorems. Unknowns \isa{{\isaliteral{3F}{\isacharquery}}X} refer to terms or formulas.
-\end{warn}
-
-Although abbreviations shorten the text, the reader needs to remember what
-they stand for. Similarly for names of facts. Names like \isa{{\isadigit{1}}}, \isa{{\isadigit{2}}}
-and \isa{{\isadigit{3}}} are not helpful and should only be used in short proofs. For
-longer proofs, descriptive names are better. But look at this example:
-\begin{quote}
-\isacom{have} \ \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}}\\
-$\vdots$\\
-\isacom{from} \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}} \dots
-\end{quote}
-The name is longer than the fact it stands for! Short facts do not need names,
-one can refer to them easily by quoting them:
-\begin{quote}
-\isacom{have} \ \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}}\\
-$\vdots$\\
-\isacom{from} \isa{{\isaliteral{60}{\isacharbackquote}}x{\isaliteral{3E}{\isachargreater}}{\isadigit{0}}{\isaliteral{60}{\isacharbackquote}}} \dots
-\end{quote}
-Note that the quotes around \isa{x{\isaliteral{3E}{\isachargreater}}{\isadigit{0}}} are \concept{back quotes}.
-They refer to the fact not by name but by value.
-
-\subsection{\isacom{moreover}}
-
-Sometimes one needs a number of facts to enable some deduction. Of course
-one can name these facts individually, as shown on the right,
-but one can also combine them with \isacom{moreover}, as shown on the left:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{moreover}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{moreover}\isamarkupfalse%
-%
-\\$\vdots$\\\hspace{-1.4ex}
-\isacommand{moreover}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{ultimately}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
-\ $\dots$\\
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\qquad
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{have}\isamarkupfalse%
-\ lab\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{have}\isamarkupfalse%
-\ lab\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$
-%
-\\$\vdots$\\\hspace{-1.4ex}
-\isacommand{have}\isamarkupfalse%
-\ lab\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\ $\dots$\\
-\isacommand{from}\isamarkupfalse%
-\ lab\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ lab\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}%
-\ $\dots$\\
-\isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
-\ $\dots$\\
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-\end{tabular}
-\begin{isamarkuptext}%
-The \isacom{moreover} version is no shorter but expresses the structure more
-clearly and avoids new names.
-
-\subsection{Raw proof blocks}
-
-Sometimes one would like to prove some lemma locally within a proof.
-A lemma that shares the current context of assumptions but that
-has its own assumptions and is generalized over its locally fixed
-variables at the end. This is what a \concept{raw proof block} does:
-\begin{quote}
-\isa{{\isaliteral{7B}{\isacharbraceleft}}} \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}\\
-\mbox{}\ \ \ \isacom{assume} \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m}\\
-\mbox{}\ \ \ $\vdots$\\
-\mbox{}\ \ \ \isacom{have} \isa{B}\\
-\isa{{\isaliteral{7D}{\isacharbraceright}}}
-\end{quote}
-proves \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}
-where all \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub i} have been replaced by unknowns \isa{{\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub i}.
-\begin{warn}
-The conclusion of a raw proof block is \emph{not} indicated by \isacom{show}
-but is simply the final \isacom{have}.
-\end{warn}
-
-As an example we prove a simple fact about divisibility on integers.
-The definition of \isa{dvd} is \isa{{\isaliteral{28}{\isacharparenleft}}b\ dvd\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{29}{\isacharparenright}}}.
-\end{isamarkuptext}%
-\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{fixes}\ a\ b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ dvd\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2B}{\isacharplus}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}b\ dvd\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
-\ \isacommand{fix}\isamarkupfalse%
-\ k\ \isacommand{assume}\isamarkupfalse%
-\ k{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}a{\isaliteral{2B}{\isacharplus}}b\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2A}{\isacharasterisk}}k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2A}{\isacharasterisk}}k{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
-\ k\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ algebra{\isaliteral{5F}{\isacharunderscore}}simps{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{using}\isamarkupfalse%
-\ assms\ \isacommand{by}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto\ simp\ add{\isaliteral{3A}{\isacharcolon}}\ dvd{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Note that the result of a raw proof block has no name. In this example
-it was directly piped (via \isacom{then}) into the final proof, but it can
-also be named for later reference: you simply follow the block directly by a
-\isacom{note} command:
-\begin{quote}
-\isacom{note} \ \isa{name\ {\isaliteral{3D}{\isacharequal}}\ this}
-\end{quote}
-This introduces a new name \isa{name} that refers to \isa{this},
-the fact just proved, in this case the preceding block. In general,
-\isacom{note} introduces a new name for one or more facts.
-
-\section{Case analysis and induction}
-
-\subsection{Datatype case analysis}
-
-We have seen case analysis on formulas. Now we want to distinguish
-which form some term takes: is it \isa{{\isadigit{0}}} or of the form \isa{Suc\ n},
-is it \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} or of the form \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, etc. Here is a typical example
-proof by case analysis on the form of \isa{xs}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}length{\isaliteral{28}{\isacharparenleft}}tl\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ xs\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ y\ ys\ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{23}{\isacharhash}}ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Function \isa{tl} (''tail'') is defined by \isa{tl\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and
-\isa{tl\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs}. Note that the result type of \isa{length} is \isa{nat}
-and \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}.
-
-This proof pattern works for any term \isa{t} whose type is a datatype.
-The goal has to be proved for each constructor \isa{C}:
-\begin{quote}
-\isacom{fix} \ \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n} \isacom{assume} \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3D}{\isacharequal}}\ C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}
-\end{quote}
-Each case can be written in a more compact form by means of the \isacom{case}
-command:
-\begin{quote}
-\isacom{case} \isa{{\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}
-\end{quote}
-This is equivalent to the explicit \isacom{fix}-\isacom{assume} line
-but also gives the assumption \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3D}{\isacharequal}}\ C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} a name: \isa{C},
-like the constructor.
-Here is the \isacom{case} version of the proof above:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ Nil\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ ys{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Remember that \isa{Nil} and \isa{Cons} are the alphanumeric names
-for \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and \isa{{\isaliteral{23}{\isacharhash}}}. The names of the assumptions
-are not used because they are directly piped (via \isacom{thus})
-into the proof of the claim.
-
-\subsection{Structural induction}
-
-We illustrate structural induction with an example based on natural numbers:
-the sum (\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}}) of the first \isa{n} natural numbers
-(\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}}) is equal to \mbox{\isa{n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}}}.
-Never mind the details, just focus on the pattern:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induction\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Except for the rewrite steps, everything is explicitly given. This
-makes the proof easily readable, but the duplication means it is tedious to
-write and maintain. Here is how pattern
-matching can completely avoid any duplication:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induction\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The first line introduces an abbreviation \isa{{\isaliteral{3F}{\isacharquery}}P\ n} for the goal.
-Pattern matching \isa{{\isaliteral{3F}{\isacharquery}}P\ n} with the goal instantiates \isa{{\isaliteral{3F}{\isacharquery}}P} to the
-function \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}}. Now the proposition to
-be proved in the base case can be written as \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isadigit{0}}}, the induction
-hypothesis as \isa{{\isaliteral{3F}{\isacharquery}}P\ n}, and the conclusion of the induction step as
-\isa{{\isaliteral{3F}{\isacharquery}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}.
-
-Induction also provides the \isacom{case} idiom that abbreviates
-the \isacom{fix}-\isacom{assume} step. The above proof becomes%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induction\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isadigit{0}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The unknown \isa{{\isaliteral{3F}{\isacharquery}}case} is set in each case to the required
-claim, i.e.\ \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isadigit{0}}} and \mbox{\isa{{\isaliteral{3F}{\isacharquery}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}} in the above proof,
-without requiring the user to define a \isa{{\isaliteral{3F}{\isacharquery}}P}. The general
-pattern for induction over \isa{nat} is shown on the left-hand side:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{tabular}{@ {}ll@ {}}
-\begin{minipage}[t]{.4\textwidth}
-\isa{%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induction\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isadigit{0}}%
-\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
-\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.4\textwidth}
-~\\
-~\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-~\\
-~\\
-~\\[1ex]
-\isacom{fix} \isa{n} \isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\end{minipage}
-\end{tabular}
-\medskip
-%
-\begin{isamarkuptext}%
-On the right side you can see what the \isacom{case} command
-on the left stands for.
-
-In case the goal is an implication, induction does one more thing: the
-proposition to be proved in each case is not the whole implication but only
-its conclusion; the premises of the implication are immediately made
-assumptions of that case. That is, if in the above proof we replace
-\isacom{show}~\isa{P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}} by
-\mbox{\isacom{show}~\isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}}}
-then \isacom{case}~\isa{{\isadigit{0}}} stands for
-\begin{quote}
-\isacom{assume} \ \isa{{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
-\end{quote}
-and \isacom{case}~\isa{{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} stands for
-\begin{quote}
-\isacom{fix} \isa{n}\\
-\isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}}
- \begin{tabular}[t]{l}\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
-\end{quote}
-The list of assumptions \isa{Suc} is actually subdivided
-into \isa{Suc{\isaliteral{2E}{\isachardot}}IH}, the induction hypotheses (here \isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}})
-and \isa{Suc{\isaliteral{2E}{\isachardot}}prems}, the premises of the goal being proved
-(here \isa{A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}).
-
-Induction works for any datatype.
-Proving a goal \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}
-by induction on \isa{x} generates a proof obligation for each constructor
-\isa{C} of the datatype. The command \isa{case\ {\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}
-performs the following steps:
-\begin{enumerate}
-\item \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}
-\item \isacom{assume} the induction hypotheses (calling them \isa{C{\isaliteral{2E}{\isachardot}}IH})
- and the premises \mbox{\isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}} (calling them \isa{C{\isaliteral{2E}{\isachardot}}prems})
- and calling the whole list \isa{C}
-\item \isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
-\end{enumerate}
-
-\subsection{Rule induction}
-
-Recall the inductive and recursive definitions of even numbers in
-\autoref{sec:inductive-defs}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{inductive}\isamarkupfalse%
-\ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-evSS{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{fun}\isamarkupfalse%
-\ even\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ even\ n{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-We recast the proof of \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ even\ n} in Isar. The
-left column shows the actual proof text, the right column shows
-the implicit effect of the two \isacom{case} commands:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{tabular}{@ {}l@ {\qquad}l@ {}}
-\begin{minipage}[t]{.5\textwidth}
-\isa{%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ even\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induction\ rule{\isaliteral{3A}{\isacharcolon}}\ ev{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ ev{\isadigit{0}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ evSS\isanewline
-\isanewline
-\isanewline
-\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-}
-\end{minipage}
-&
-\begin{minipage}[t]{.5\textwidth}
-~\\
-~\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}}\\
-~\\
-~\\
-\isacom{fix} \isa{n}\\
-\isacom{assume} \isa{evSS{\isaliteral{3A}{\isacharcolon}}}
- \begin{tabular}[t]{l} \isa{{\isaliteral{22}{\isachardoublequote}}ev\ n{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}even\ n{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
-\end{minipage}
-\end{tabular}
-\medskip
-%
-\begin{isamarkuptext}%
-The proof resembles structural induction, but the induction rule is given
-explicitly and the names of the cases are the names of the rules in the
-inductive definition.
-Let us examine the two assumptions named \isa{evSS}:
-\isa{ev\ n} is the premise of rule \isa{evSS}, which we may assume
-because we are in the case where that rule was used; \isa{even\ n}
-is the induction hypothesis.
-\begin{warn}
-Because each \isacom{case} command introduces a list of assumptions
-named like the case name, which is the name of a rule of the inductive
-definition, those rules now need to be accessed with a qualified name, here
-\isa{ev{\isaliteral{2E}{\isachardot}}ev{\isadigit{0}}} and \isa{ev{\isaliteral{2E}{\isachardot}}evSS}
-\end{warn}
-
-In the case \isa{evSS} of the proof above we have pretended that the
-system fixes a variable \isa{n}. But unless the user provides the name
-\isa{n}, the system will just invent its own name that cannot be referred
-to. In the above proof, we do not need to refer to it, hence we do not give
-it a specific name. In case one needs to refer to it one writes
-\begin{quote}
-\isacom{case} \isa{{\isaliteral{28}{\isacharparenleft}}evSS\ m{\isaliteral{29}{\isacharparenright}}}
-\end{quote}
-just like \isacom{case}~\isa{{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} in earlier structural inductions.
-The name \isa{m} is an arbitrary choice. As a result,
-case \isa{evSS} is derived from a renamed version of
-rule \isa{evSS}: \isa{ev\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.
-Here is an example with a (contrived) intermediate step that refers to \isa{m}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ even\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induction\ rule{\isaliteral{3A}{\isacharcolon}}\ ev{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ ev{\isadigit{0}}\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}evSS\ m{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ even\ m{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{using}\isamarkupfalse%
-\ {\isaliteral{60}{\isacharbackquoteopen}}even\ m{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\indent
-In general, let \isa{I} be a (for simplicity unary) inductively defined
-predicate and let the rules in the definition of \isa{I}
-be called \isa{rule\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}, \dots, \isa{rule\isaliteral{5C3C5E697375623E}{}\isactrlisub n}. A proof by rule
-induction follows this pattern:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}I\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induction\ rule{\isaliteral{3A}{\isacharcolon}}\ I{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ rule\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}%
-\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ %
-\ $\dots$\\
-\isacommand{next}\isamarkupfalse%
-%
-\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{case}\isamarkupfalse%
-\ rule\isaliteral{5C3C5E697375623E}{}\isactrlisub n%
-\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{3F}{\isacharquery}}case\ %
-\ $\dots$\\
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-One can provide explicit variable names by writing
-\isacom{case}~\isa{{\isaliteral{28}{\isacharparenleft}}rule\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}}, thus renaming the first \isa{k}
-free variables in rule \isa{i} to \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub k},
-going through rule \isa{i} from left to right.
-
-\subsection{Assumption naming}
-
-In any induction, \isacom{case}~\isa{name} sets up a list of assumptions
-also called \isa{name}, which is subdivided into three parts:
-\begin{description}
-\item[\isa{name{\isaliteral{2E}{\isachardot}}IH}] contains the induction hypotheses.
-\item[\isa{name{\isaliteral{2E}{\isachardot}}hyps}] contains all the other hypotheses of this case in the
-induction rule. For rule inductions these are the hypotheses of rule
-\isa{name}, for structural inductions these are empty.
-\item[\isa{name{\isaliteral{2E}{\isachardot}}prems}] contains the (suitably instantiated) premises
-of the statement being proved, i.e. the \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub i} when
-proving \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A}.
-\end{description}
-\begin{warn}
-Proof method \isa{induct} differs from \isa{induction}
-only in this naming policy: \isa{induct} does not distinguish
-\isa{IH} from \isa{hyps} but subsumes \isa{IH} under \isa{hyps}.
-\end{warn}
-
-More complicated inductive proofs than the ones we have seen so far
-often need to refer to specific assumptions---just \isa{name} or even
-\isa{name{\isaliteral{2E}{\isachardot}}prems} and \isa{name{\isaliteral{2E}{\isachardot}}IH} can be too unspecific.
-This is where the indexing of fact lists comes in handy, e.g.\
-\isa{name{\isaliteral{2E}{\isachardot}}IH{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} or \isa{name{\isaliteral{2E}{\isachardot}}prems{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.
-
-\subsection{Rule inversion}
-
-Rule inversion is case analysis of which rule could have been used to
-derive some fact. The name \concept{rule inversion} emphasizes that we are
-reasoning backwards: by which rules could some given fact have been proved?
-For the inductive definition of \isa{ev}, rule inversion can be summarized
-like this:
-\begin{isabelle}%
-ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ev\ k{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-The realisation in Isabelle is a case analysis.
-A simple example is the proof that \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. We
-already went through the details informally in \autoref{sec:Logic:even}. This
-is the Isar proof:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ this\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{proof}\isamarkupfalse%
-\ cases\isanewline
-\ \ \ \ \isacommand{case}\isamarkupfalse%
-\ ev{\isadigit{0}}\ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ ev{\isaliteral{2E}{\isachardot}}ev{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \ \ \isacommand{case}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}evSS\ k{\isaliteral{29}{\isacharparenright}}\ \isacommand{thus}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ ev{\isaliteral{2E}{\isachardot}}evSS{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The key point here is that a case analysis over some inductively
-defined predicate is triggered by piping the given fact
-(here: \isacom{from}~\isa{this}) into a proof by \isa{cases}.
-Let us examine the assumptions available in each case. In case \isa{ev{\isadigit{0}}}
-we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} and in case \isa{evSS} we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}}
-and \isa{ev\ k}. In each case the assumptions are available under the name
-of the case; there is no fine grained naming schema like for induction.
-
-Sometimes some rules could not have been used to derive the given fact
-because constructors clash. As an extreme example consider
-rule inversion applied to \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}: neither rule \isa{ev{\isadigit{0}}} nor
-rule \isa{evSS} can yield \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} because \isa{Suc\ {\isadigit{0}}} unifies
-neither with \isa{{\isadigit{0}}} nor with \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}. Impossible cases do not
-have to be proved. Hence we can prove anything from \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{then}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ P\ \isacommand{by}\isamarkupfalse%
-\ cases%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-That is, \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} is simply not provable:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ ev{\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ False\ \isacommand{by}\isamarkupfalse%
-\ cases\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Normally not all cases will be impossible. As a simple exercise,
-prove that \mbox{\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: