--- a/doc-src/IsarOverview/Isar/document/Induction.tex Mon May 02 16:28:33 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Mon May 02 18:29:29 2005 +0200
@@ -26,19 +26,15 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
@@ -55,19 +51,15 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}cases\ {\isachardoublequote}A{\isachardoublequote}{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ True\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ False\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent which is like the previous proof but instantiates
@@ -84,19 +76,15 @@
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Nil\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Cons\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates
@@ -127,32 +115,30 @@
We start with an inductive proof where both cases are proved automatically:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent If we want to expose more of the structure of the
+\noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
+the operations involved are overloaded.
+
+If we want to expose more of the structure of the
proof, we can use pattern matching to avoid having to repeat the goal
statement:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{fix}\ n\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent We could refine this further to show more of the equational
@@ -160,21 +146,17 @@
introducing context via the \isakeyword{case} command:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ Suc\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent The implicitly defined \isa{{\isacharquery}case} refers to the
@@ -189,19 +171,15 @@
\isamarkuptrue%
\isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Of course we could again have written
@@ -233,56 +211,33 @@
\isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
-\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}} \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}m\ {\isacharless}\ Suc\ n{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \ \ \ %
-\isamarkupcmt{\isa{P\ m}%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{proof}\ cases\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ eq{\isacharcolon}\ {\isachardoublequote}m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{from}\ Suc\ \isakeyword{and}\ A\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}P\ n{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ blast\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ eq\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}m\ {\isasymnoteq}\ n{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{with}\ Suc\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}m\ {\isacharless}\ n{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ arith\isanewline
-\ \ \ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Given the explanations above and the comments in the
@@ -329,21 +284,16 @@
\isamarkuptrue%
\isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{using}\ A\isanewline
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{proof}\ induct\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ refl\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ step\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
@@ -358,37 +308,22 @@
\isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{from}\ A\ B\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}thesis\isanewline
-\ \ \isamarkupfalse%
-\isacommand{proof}\ induct\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x\ \isamarkupfalse%
-\isacommand{assume}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \ %
-\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
-}
-\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{thus}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{fix}\ x{\isacharprime}\ x\ y\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{assume}\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequote}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
-\ \ \ \ \isamarkupfalse%
-\isacommand{from}\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step.
@@ -446,38 +381,28 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{proof}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{1}}\ \isamarkupfalse%
-\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isadigit{2}}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{next}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{case}\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
-\isacommand{by}\ simp\isanewline
-\ \ \isamarkupfalse%
-\isacommand{finally}\ \isamarkupfalse%
-\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
-\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -495,7 +420,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%