diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/Fun/document/fun0.tex
--- a/doc-src/TutorialI/Fun/document/fun0.tex	Thu Jul 26 16:08:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,360 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{fun{\isadigit{0}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\subsection{Definition}
-\label{sec:fun-examples}
-
-Here is a simple example, the \rmindex{Fibonacci function}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib\ x\ {\isaliteral{2B}{\isacharplus}}\ fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-This resembles ordinary functional programming languages. Note the obligatory
-\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
-defines the function in one go. Isabelle establishes termination automatically
-because \isa{fib}'s argument decreases in every recursive call.
-
-Slightly more interesting is the insertion of a fixed element
-between any two elements of a list:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ sep\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-This time the length of the list decreases with the
-recursive call; the first argument is irrelevant for termination.
-
-Pattern matching\index{pattern matching!and \isacommand{fun}}
-need not be exhaustive and may employ wildcards:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ last\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-Overlapping patterns are disambiguated by taking the order of equations into
-account, just as in functional programming:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ sep{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ xs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-To guarantee that the second equation can only be applied if the first
-one does not match, Isabelle internally replaces the second equation
-by the two possibilities that are left: \isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and
-\isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}.  Thus the functions \isa{sep} and
-\isa{sep{\isadigit{1}}} are identical.
-
-Because of its pattern matching syntax, \isacommand{fun} is also useful
-for the definition of non-recursive functions:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{23}{\isacharhash}}x{\isaliteral{23}{\isacharhash}}zs{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-After a function~$f$ has been defined via \isacommand{fun},
-its defining equations (or variants derived from them) are available
-under the name $f$\isa{{\isaliteral{2E}{\isachardot}}simps} as theorems.
-For example, look (via \isacommand{thm}) at
-\isa{sep{\isaliteral{2E}{\isachardot}}simps} and \isa{sep{\isadigit{1}}{\isaliteral{2E}{\isachardot}}simps} to see that they define
-the same function. What is more, those equations are automatically declared as
-simplification rules.
-
-\subsection{Termination}
-
-Isabelle's automatic termination prover for \isacommand{fun} has a
-fixed notion of the \emph{size} (of type \isa{nat}) of an
-argument. The size of a natural number is the number itself. The size
-of a list is its length. For the general case see \S\ref{sec:general-datatype}.
-A recursive function is accepted if \isacommand{fun} can
-show that the size of one fixed argument becomes smaller with each
-recursive call.
-
-More generally, \isacommand{fun} allows any \emph{lexicographic
-combination} of size measures in case there are multiple
-arguments. For example, the following version of \rmindex{Ackermann's
-function} is accepted:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ ack{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}ack{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-The order of arguments has no influence on whether
-\isacommand{fun} can prove termination of a function. For more details
-see elsewhere~\cite{bulwahnKN07}.
-
-\subsection{Simplification}
-\label{sec:fun-simplification}
-
-Upon a successful termination proof, the recursion equations become
-simplification rules, just as with \isacommand{primrec}.
-In most cases this works fine, but there is a subtle
-problem that must be mentioned: simplification may not
-terminate because of automatic splitting of \isa{if}.
-\index{*if expressions!splitting of}
-Let us look at an example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ gcd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-The second argument decreases with each recursive call.
-The termination condition
-\begin{isabelle}%
-\ \ \ \ \ n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ mod\ n\ {\isaliteral{3C}{\isacharless}}\ n%
-\end{isabelle}
-is proved automatically because it is already present as a lemma in
-HOL\@.  Thus the recursion equation becomes a simplification
-rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
-languages and our simplifier don't do that. Unfortunately the simplifier does
-something else that leads to the same problem: it splits 
-each \isa{if}-expression unless its
-condition simplifies to \isa{True} or \isa{False}.  For
-example, simplification reduces
-\begin{isabelle}%
-\ \ \ \ \ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ k%
-\end{isabelle}
-in one step to
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k%
-\end{isabelle}
-where the condition cannot be reduced further, and splitting leads to
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-Since the recursive call \isa{gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of
-simplification steps. Fortunately, this problem can be avoided in many
-different ways.
-
-The most radical solution is to disable the offending theorem
-\isa{split{\isaliteral{5F}{\isacharunderscore}}if},
-as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
-approach: you will often have to invoke the rule explicitly when
-\isa{if} is involved.
-
-If possible, the definition should be given by pattern matching on the left
-rather than \isa{if} on the right. In the case of \isa{gcd} the
-following alternative definition suggests itself:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ gcd{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd{\isadigit{1}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-The order of equations is important: it hides the side condition
-\isa{n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}}.  Unfortunately, not all conditionals can be
-expressed by pattern matching.
-
-A simple alternative is to replace \isa{if} by \isa{case}, 
-which is also available for \isa{bool} and is not split automatically:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ gcd{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{2}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ m\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ gcd{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-This is probably the neatest solution next to pattern matching, and it is
-always available.
-
-A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove
-these lemmas:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}.
-Now we can disable the original simplification rule:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ gcd{\isaliteral{2E}{\isachardot}}simps\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}%
-\begin{isamarkuptext}%
-\index{induction!recursion|(}
-\index{recursion induction|(}
-
-\subsection{Induction}
-\label{sec:fun-induction}
-
-Having defined a function we might like to prove something about it.
-Since the function is recursive, the natural proof principle is
-again induction. But this time the structural form of induction that comes
-with datatypes is unlikely to work well --- otherwise we could have defined the
-function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
-proves a suitable induction rule $f$\isa{{\isaliteral{2E}{\isachardot}}induct} that follows the
-recursion pattern of the particular function $f$. We call this
-\textbf{recursion induction}. Roughly speaking, it
-requires you to prove for each \isacommand{fun} equation that the property
-you are trying to establish holds for the left-hand side provided it holds
-for all recursive calls on the right-hand side. Here is a simple example
-involving the predefined \isa{map} functional on lists:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-Note that \isa{map\ f\ xs}
-is the result of applying \isa{f} to all elements of \isa{xs}. We prove
-this lemma by recursion induction over \isa{sep}:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ x\ xs\ rule{\isaliteral{3A}{\isacharcolon}}\ sep{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-The resulting proof state has three subgoals corresponding to the three
-clauses for \isa{sep}:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x\ y\ zs{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
-\isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-The rest is pure simplification:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent The proof goes smoothly because the induction rule
-follows the recursion of \isa{sep}.  Try proving the above lemma by
-structural induction, and you find that you need an additional case
-distinction.
-
-In general, the format of invoking recursion induction is
-\begin{quote}
-\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $x@1 \dots x@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $f$\isa{{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}}
-\end{quote}\index{*induct_tac (method)}%
-where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
-name of a function that takes $n$ arguments. Usually the subgoal will
-contain the term $f x@1 \dots x@n$ but this need not be the case. The
-induction rules do not mention $f$ at all. Here is \isa{sep{\isaliteral{2E}{\isachardot}}induct}:
-\begin{isabelle}
-{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
-~~{\isasymAnd}a~x.~P~a~[x];\isanewline
-~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}~P~u~v%
-\end{isabelle}
-It merely says that in order to prove a property \isa{P} of \isa{u} and
-\isa{v} you need to prove it for the three cases where \isa{v} is the
-empty list, the singleton list, and the list with at least two elements.
-The final case has an induction hypothesis:  you may assume that \isa{P}
-holds for the tail of that list.
-\index{induction!recursion|)}
-\index{recursion induction|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: