27 theory that contains pretty much everything but lists, thus avoiding |
27 theory that contains pretty much everything but lists, thus avoiding |
28 ambiguities caused by defining lists twice.% |
28 ambiguities caused by defining lists twice.% |
29 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
30 \isamarkuptrue% |
30 \isamarkuptrue% |
31 \isacommand{datatype}\isamarkupfalse% |
31 \isacommand{datatype}\isamarkupfalse% |
32 \ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
32 \ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
33 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharhash}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}% |
33 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixr}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{23}{\isacharhash}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}% |
34 \begin{isamarkuptext}% |
34 \begin{isamarkuptext}% |
35 \noindent |
35 \noindent |
36 The datatype\index{datatype@\isacommand {datatype} (command)} |
36 The datatype\index{datatype@\isacommand {datatype} (command)} |
37 \tydx{list} introduces two |
37 \tydx{list} introduces two |
38 constructors \cdx{Nil} and \cdx{Cons}, the |
38 constructors \cdx{Nil} and \cdx{Cons}, the |
40 example, the term \isa{Cons True (Cons False Nil)} is a value of |
40 example, the term \isa{Cons True (Cons False Nil)} is a value of |
41 type \isa{bool\ list}, namely the list with the elements \isa{True} and |
41 type \isa{bool\ list}, namely the list with the elements \isa{True} and |
42 \isa{False}. Because this notation quickly becomes unwieldy, the |
42 \isa{False}. Because this notation quickly becomes unwieldy, the |
43 datatype declaration is annotated with an alternative syntax: instead of |
43 datatype declaration is annotated with an alternative syntax: instead of |
44 \isa{Nil} and \isa{Cons x xs} we can write |
44 \isa{Nil} and \isa{Cons x xs} we can write |
45 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and |
45 \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\index{$HOL2list@\isa{[]}|bold} and |
46 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this |
46 \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this |
47 alternative syntax is the familiar one. Thus the list \isa{Cons True |
47 alternative syntax is the familiar one. Thus the list \isa{Cons True |
48 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation |
48 (Cons False Nil)} becomes \isa{True\ {\isaliteral{23}{\isacharhash}}\ False\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}. The annotation |
49 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
49 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
50 means that \isa{{\isacharhash}} associates to |
50 means that \isa{{\isaliteral{23}{\isacharhash}}} associates to |
51 the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}} |
51 the right: the term \isa{x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ z} is read as \isa{x\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ z{\isaliteral{29}{\isacharparenright}}} |
52 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}. |
52 and not as \isa{{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ z}. |
53 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}. |
53 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isaliteral{23}{\isacharhash}}}. |
54 |
54 |
55 \begin{warn} |
55 \begin{warn} |
56 Syntax annotations can be powerful, but they are difficult to master and |
56 Syntax annotations can be powerful, but they are difficult to master and |
57 are never necessary. You |
57 are never necessary. You |
58 could drop them from theory \isa{ToyList} and go back to the identifiers |
58 could drop them from theory \isa{ToyList} and go back to the identifiers |
62 Next, two functions \isa{app} and \cdx{rev} are defined recursively, |
62 Next, two functions \isa{app} and \cdx{rev} are defined recursively, |
63 in this order, because Isabelle insists on definition before use:% |
63 in this order, because Isabelle insists on definition before use:% |
64 \end{isamarkuptext}% |
64 \end{isamarkuptext}% |
65 \isamarkuptrue% |
65 \isamarkuptrue% |
66 \isacommand{primrec}\isamarkupfalse% |
66 \isacommand{primrec}\isamarkupfalse% |
67 \ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isacharat}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline |
67 \ app\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixr}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{40}{\isacharat}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline |
68 {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
68 {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ ys\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
69 {\isachardoublequoteopen}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline |
69 {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
70 \isanewline |
70 \isanewline |
71 \isacommand{primrec}\isamarkupfalse% |
71 \isacommand{primrec}\isamarkupfalse% |
72 \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
72 \ rev\ {\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 |
73 {\isachardoublequoteopen}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
73 {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
74 {\isachardoublequoteopen}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}% |
74 {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
75 \begin{isamarkuptext}% |
75 \begin{isamarkuptext}% |
76 \noindent |
76 \noindent |
77 Each function definition is of the form |
77 Each function definition is of the form |
78 \begin{center} |
78 \begin{center} |
79 \isacommand{primrec} \textit{name} \isa{{\isacharcolon}{\isacharcolon}} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations} |
79 \isacommand{primrec} \textit{name} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations} |
80 \end{center} |
80 \end{center} |
81 The equations must be separated by \isa{{\isacharbar}}. |
81 The equations must be separated by \isa{{\isaliteral{7C}{\isacharbar}}}. |
82 % |
82 % |
83 Function \isa{app} is annotated with concrete syntax. Instead of the |
83 Function \isa{app} is annotated with concrete syntax. Instead of the |
84 prefix syntax \isa{app\ xs\ ys} the infix |
84 prefix syntax \isa{app\ xs\ ys} the infix |
85 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred |
85 \isa{xs\ {\isaliteral{40}{\isacharat}}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred |
86 form. |
86 form. |
87 |
87 |
88 \index{*rev (constant)|(}\index{append function|(} |
88 \index{*rev (constant)|(}\index{append function|(} |
89 The equations for \isa{app} and \isa{rev} hardly need comments: |
89 The equations for \isa{app} and \isa{rev} hardly need comments: |
90 \isa{app} appends two lists and \isa{rev} reverses a list. The |
90 \isa{app} appends two lists and \isa{rev} reverses a list. The |
131 \index{evaluation} |
131 \index{evaluation} |
132 |
132 |
133 Assuming you have processed the declarations and definitions of |
133 Assuming you have processed the declarations and definitions of |
134 \texttt{ToyList} presented so far, you may want to test your |
134 \texttt{ToyList} presented so far, you may want to test your |
135 functions by running them. For example, what is the value of |
135 functions by running them. For example, what is the value of |
136 \isa{rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}? Command% |
136 \isa{rev\ {\isaliteral{28}{\isacharparenleft}}True\ {\isaliteral{23}{\isacharhash}}\ False\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}}? Command% |
137 \end{isamarkuptext}% |
137 \end{isamarkuptext}% |
138 \isamarkuptrue% |
138 \isamarkuptrue% |
139 \isacommand{value}\isamarkupfalse% |
139 \isacommand{value}\isamarkupfalse% |
140 \ {\isachardoublequoteopen}rev\ {\isacharparenleft}True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}% |
140 \ {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{28}{\isacharparenleft}}True\ {\isaliteral{23}{\isacharhash}}\ False\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
141 \begin{isamarkuptext}% |
141 \begin{isamarkuptext}% |
142 \noindent yields the correct result \isa{False\ {\isacharhash}\ True\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. |
142 \noindent yields the correct result \isa{False\ {\isaliteral{23}{\isacharhash}}\ True\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}. |
143 But we can go beyond mere functional programming and evaluate terms with |
143 But we can go beyond mere functional programming and evaluate terms with |
144 variables in them, executing functions symbolically:% |
144 variables in them, executing functions symbolically:% |
145 \end{isamarkuptext}% |
145 \end{isamarkuptext}% |
146 \isamarkuptrue% |
146 \isamarkuptrue% |
147 \isacommand{value}\isamarkupfalse% |
147 \isacommand{value}\isamarkupfalse% |
148 \ {\isachardoublequoteopen}rev\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ c\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}% |
148 \ {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ b\ {\isaliteral{23}{\isacharhash}}\ c\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
149 \begin{isamarkuptext}% |
149 \begin{isamarkuptext}% |
150 \noindent yields \isa{c\ {\isacharhash}\ b\ {\isacharhash}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. |
150 \noindent yields \isa{c\ {\isaliteral{23}{\isacharhash}}\ b\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}. |
151 |
151 |
152 \section{An Introductory Proof} |
152 \section{An Introductory Proof} |
153 \label{sec:intro-proof} |
153 \label{sec:intro-proof} |
154 |
154 |
155 Having convinced ourselves (as well as one can by testing) that our |
155 Having convinced ourselves (as well as one can by testing) that our |
175 \index{theorem@\isacommand {theorem} (command)|bold}% |
175 \index{theorem@\isacommand {theorem} (command)|bold}% |
176 \noindent |
176 \noindent |
177 This \isacommand{theorem} command does several things: |
177 This \isacommand{theorem} command does several things: |
178 \begin{itemize} |
178 \begin{itemize} |
179 \item |
179 \item |
180 It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. |
180 It establishes a new theorem to be proved, namely \isa{rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs}. |
181 \item |
181 \item |
182 It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference. |
182 It gives that theorem the name \isa{rev{\isaliteral{5F}{\isacharunderscore}}rev}, for later reference. |
183 \item |
183 \item |
184 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
184 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
185 simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by |
185 simplification will replace occurrences of \isa{rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}} by |
186 \isa{xs}. |
186 \isa{xs}. |
187 \end{itemize} |
187 \end{itemize} |
188 The name and the simplification attribute are optional. |
188 The name and the simplification attribute are optional. |
189 Isabelle's response is to print the initial proof state consisting |
189 Isabelle's response is to print the initial proof state consisting |
190 of some header information (like how many subgoals there are) followed by |
190 of some header information (like how many subgoals there are) followed by |
191 \begin{isabelle}% |
191 \begin{isabelle}% |
192 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
192 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs% |
193 \end{isabelle} |
193 \end{isabelle} |
194 For compactness reasons we omit the header in this tutorial. |
194 For compactness reasons we omit the header in this tutorial. |
195 Until we have finished a proof, the \rmindex{proof state} proper |
195 Until we have finished a proof, the \rmindex{proof state} proper |
196 always looks like this: |
196 always looks like this: |
197 \begin{isabelle} |
197 \begin{isabelle} |
204 Initially there is only one subgoal, which is identical with the |
204 Initially there is only one subgoal, which is identical with the |
205 main goal. (If you always want to see the main goal as well, |
205 main goal. (If you always want to see the main goal as well, |
206 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} |
206 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} |
207 --- this flag used to be set by default.) |
207 --- this flag used to be set by default.) |
208 |
208 |
209 Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively |
209 Let us now get back to \isa{rev\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs}. Properties of recursively |
210 defined functions are best established by induction. In this case there is |
210 defined functions are best established by induction. In this case there is |
211 nothing obvious except induction on \isa{xs}:% |
211 nothing obvious except induction on \isa{xs}:% |
212 \end{isamarkuptxt}% |
212 \end{isamarkuptxt}% |
213 \isamarkuptrue% |
213 \isamarkuptrue% |
214 \isacommand{apply}\isamarkupfalse% |
214 \isacommand{apply}\isamarkupfalse% |
215 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% |
215 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}% |
216 \begin{isamarkuptxt}% |
216 \begin{isamarkuptxt}% |
217 \noindent\index{*induct_tac (method)}% |
217 \noindent\index{*induct_tac (method)}% |
218 This tells Isabelle to perform induction on variable \isa{xs}. The suffix |
218 This tells Isabelle to perform induction on variable \isa{xs}. The suffix |
219 \isa{tac} stands for \textbf{tactic},\index{tactics} |
219 \isa{tac} stands for \textbf{tactic},\index{tactics} |
220 a synonym for ``theorem proving function''. |
220 a synonym for ``theorem proving function''. |
221 By default, induction acts on the first subgoal. The new proof state contains |
221 By default, induction acts on the first subgoal. The new proof state contains |
222 two subgoals, namely the base case (\isa{Nil}) and the induction step |
222 two subgoals, namely the base case (\isa{Nil}) and the induction step |
223 (\isa{Cons}): |
223 (\isa{Cons}): |
224 \begin{isabelle}% |
224 \begin{isabelle}% |
225 \ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline |
225 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
226 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
226 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline |
227 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list% |
227 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}rev\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list% |
228 \end{isabelle} |
228 \end{isabelle} |
229 |
229 |
230 The induction step is an example of the general format of a subgoal:\index{subgoals} |
230 The induction step is an example of the general format of a subgoal:\index{subgoals} |
231 \begin{isabelle} |
231 \begin{isabelle} |
232 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
232 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
237 The {\it assumptions}\index{assumptions!of subgoal} |
237 The {\it assumptions}\index{assumptions!of subgoal} |
238 are the local assumptions for this subgoal and {\it |
238 are the local assumptions for this subgoal and {\it |
239 conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. |
239 conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. |
240 Typical proof steps |
240 Typical proof steps |
241 that add new assumptions are induction and case distinction. In our example |
241 that add new assumptions are induction and case distinction. In our example |
242 the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there |
242 the only assumption is the induction hypothesis \isa{rev\ {\isaliteral{28}{\isacharparenleft}}rev\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there |
243 are multiple assumptions, they are enclosed in the bracket pair |
243 are multiple assumptions, they are enclosed in the bracket pair |
244 \indexboldpos{\isasymlbrakk}{$Isabrl} and |
244 \indexboldpos{\isasymlbrakk}{$Isabrl} and |
245 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. |
245 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. |
246 |
246 |
247 Let us try to solve both goals automatically:% |
247 Let us try to solve both goals automatically:% |
248 \end{isamarkuptxt}% |
248 \end{isamarkuptxt}% |
249 \isamarkuptrue% |
249 \isamarkuptrue% |
250 \isacommand{apply}\isamarkupfalse% |
250 \isacommand{apply}\isamarkupfalse% |
251 {\isacharparenleft}auto{\isacharparenright}% |
251 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
252 \begin{isamarkuptxt}% |
252 \begin{isamarkuptxt}% |
253 \noindent |
253 \noindent |
254 This command tells Isabelle to apply a proof strategy called |
254 This command tells Isabelle to apply a proof strategy called |
255 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to |
255 \isa{auto} to all subgoals. Essentially, \isa{auto} tries to |
256 simplify the subgoals. In our case, subgoal~1 is solved completely (thanks |
256 simplify the subgoals. In our case, subgoal~1 is solved completely (thanks |
257 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version |
257 to the equation \isa{rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}) and disappears; the simplified version |
258 of subgoal~2 becomes the new subgoal~1: |
258 of subgoal~2 becomes the new subgoal~1: |
259 \begin{isabelle}% |
259 \begin{isabelle}% |
260 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
260 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline |
261 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list% |
261 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}rev\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ rev\ {\isaliteral{28}{\isacharparenleft}}rev\ list\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list% |
262 \end{isabelle} |
262 \end{isabelle} |
263 In order to simplify this subgoal further, a lemma suggests itself.% |
263 In order to simplify this subgoal further, a lemma suggests itself.% |
264 \end{isamarkuptxt}% |
264 \end{isamarkuptxt}% |
265 \isamarkuptrue% |
265 \isamarkuptrue% |
266 % |
266 % |
294 \commdx{lemma} are interchangeable and merely indicate |
294 \commdx{lemma} are interchangeable and merely indicate |
295 the importance we attach to a proposition. Therefore we use the words |
295 the importance we attach to a proposition. Therefore we use the words |
296 \emph{theorem} and \emph{lemma} pretty much interchangeably, too. |
296 \emph{theorem} and \emph{lemma} pretty much interchangeably, too. |
297 |
297 |
298 There are two variables that we could induct on: \isa{xs} and |
298 There are two variables that we could induct on: \isa{xs} and |
299 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on |
299 \isa{ys}. Because \isa{{\isaliteral{40}{\isacharat}}} is defined by recursion on |
300 the first argument, \isa{xs} is the correct one:% |
300 the first argument, \isa{xs} is the correct one:% |
301 \end{isamarkuptxt}% |
301 \end{isamarkuptxt}% |
302 \isamarkuptrue% |
302 \isamarkuptrue% |
303 \isacommand{apply}\isamarkupfalse% |
303 \isacommand{apply}\isamarkupfalse% |
304 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% |
304 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}% |
305 \begin{isamarkuptxt}% |
305 \begin{isamarkuptxt}% |
306 \noindent |
306 \noindent |
307 This time not even the base case is solved automatically:% |
307 This time not even the base case is solved automatically:% |
308 \end{isamarkuptxt}% |
308 \end{isamarkuptxt}% |
309 \isamarkuptrue% |
309 \isamarkuptrue% |
310 \isacommand{apply}\isamarkupfalse% |
310 \isacommand{apply}\isamarkupfalse% |
311 {\isacharparenleft}auto{\isacharparenright}% |
311 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
312 \begin{isamarkuptxt}% |
312 \begin{isamarkuptxt}% |
313 \begin{isabelle}% |
313 \begin{isabelle}% |
314 \ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}% |
314 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ rev\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ ys\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}% |
315 \end{isabelle} |
315 \end{isabelle} |
316 Again, we need to abandon this proof attempt and prove another simple lemma |
316 Again, we need to abandon this proof attempt and prove another simple lemma |
317 first. In the future the step of abandoning an incomplete proof before |
317 first. In the future the step of abandoning an incomplete proof before |
318 embarking on the proof of a lemma usually remains implicit.% |
318 embarking on the proof of a lemma usually remains implicit.% |
319 \end{isamarkuptxt}% |
319 \end{isamarkuptxt}% |
333 \begin{isamarkuptext}% |
333 \begin{isamarkuptext}% |
334 We again try the canonical proof procedure:% |
334 We again try the canonical proof procedure:% |
335 \end{isamarkuptext}% |
335 \end{isamarkuptext}% |
336 \isamarkuptrue% |
336 \isamarkuptrue% |
337 \isacommand{lemma}\isamarkupfalse% |
337 \isacommand{lemma}\isamarkupfalse% |
338 \ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
338 \ app{\isaliteral{5F}{\isacharunderscore}}Nil{\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
339 % |
339 % |
340 \isadelimproof |
340 \isadelimproof |
341 % |
341 % |
342 \endisadelimproof |
342 \endisadelimproof |
343 % |
343 % |
344 \isatagproof |
344 \isatagproof |
345 \isacommand{apply}\isamarkupfalse% |
345 \isacommand{apply}\isamarkupfalse% |
346 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
346 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}\isanewline |
347 \isacommand{apply}\isamarkupfalse% |
347 \isacommand{apply}\isamarkupfalse% |
348 {\isacharparenleft}auto{\isacharparenright}% |
348 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
349 \begin{isamarkuptxt}% |
349 \begin{isamarkuptxt}% |
350 \noindent |
350 \noindent |
351 It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}: |
351 It works, yielding the desired message \isa{No\ subgoals{\isaliteral{21}{\isacharbang}}}: |
352 \begin{isabelle}% |
352 \begin{isabelle}% |
353 xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline |
353 xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\isanewline |
354 No\ subgoals{\isacharbang}% |
354 No\ subgoals{\isaliteral{21}{\isacharbang}}% |
355 \end{isabelle} |
355 \end{isabelle} |
356 We still need to confirm that the proof is now finished:% |
356 We still need to confirm that the proof is now finished:% |
357 \end{isamarkuptxt}% |
357 \end{isamarkuptxt}% |
358 \isamarkuptrue% |
358 \isamarkuptrue% |
359 \isacommand{done}\isamarkupfalse% |
359 \isacommand{done}\isamarkupfalse% |
371 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
371 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
372 if it is obvious from the context that the proof is finished. |
372 if it is obvious from the context that the proof is finished. |
373 |
373 |
374 % Instead of \isacommand{apply} followed by a dot, you can simply write |
374 % Instead of \isacommand{apply} followed by a dot, you can simply write |
375 % \isacommand{by}\indexbold{by}, which we do most of the time. |
375 % \isacommand{by}\indexbold{by}, which we do most of the time. |
376 Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}, |
376 Notice that in lemma \isa{app{\isaliteral{5F}{\isacharunderscore}}Nil{\isadigit{2}}}, |
377 as printed out after the final \isacommand{done}, the free variable \isa{xs} has been |
377 as printed out after the final \isacommand{done}, the free variable \isa{xs} has been |
378 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in |
378 replaced by the unknown \isa{{\isaliteral{3F}{\isacharquery}}xs}, just as explained in |
379 \S\ref{sec:variables}. |
379 \S\ref{sec:variables}. |
380 |
380 |
381 Going back to the proof of the first lemma% |
381 Going back to the proof of the first lemma% |
382 \end{isamarkuptext}% |
382 \end{isamarkuptext}% |
383 \isamarkuptrue% |
383 \isamarkuptrue% |
384 \isacommand{lemma}\isamarkupfalse% |
384 \isacommand{lemma}\isamarkupfalse% |
385 \ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
385 \ rev{\isaliteral{5F}{\isacharunderscore}}app\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
386 % |
386 % |
387 \isadelimproof |
387 \isadelimproof |
388 % |
388 % |
389 \endisadelimproof |
389 \endisadelimproof |
390 % |
390 % |
391 \isatagproof |
391 \isatagproof |
392 \isacommand{apply}\isamarkupfalse% |
392 \isacommand{apply}\isamarkupfalse% |
393 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
393 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}\isanewline |
394 \isacommand{apply}\isamarkupfalse% |
394 \isacommand{apply}\isamarkupfalse% |
395 {\isacharparenleft}auto{\isacharparenright}% |
395 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
396 \begin{isamarkuptxt}% |
396 \begin{isamarkuptxt}% |
397 \noindent |
397 \noindent |
398 we find that this time \isa{auto} solves the base case, but the |
398 we find that this time \isa{auto} solves the base case, but the |
399 induction step merely simplifies to |
399 induction step merely simplifies to |
400 \begin{isabelle}% |
400 \begin{isabelle}% |
401 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
401 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline |
402 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline |
402 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }rev\ {\isaliteral{28}{\isacharparenleft}}list\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ ys\ {\isaliteral{40}{\isacharat}}\ rev\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline |
403 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}% |
403 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{28}{\isacharparenleft}}rev\ ys\ {\isaliteral{40}{\isacharat}}\ rev\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ ys\ {\isaliteral{40}{\isacharat}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}% |
404 \end{isabelle} |
404 \end{isabelle} |
405 Now we need to remember that \isa{{\isacharat}} associates to the right, and that |
405 Now we need to remember that \isa{{\isaliteral{40}{\isacharat}}} associates to the right, and that |
406 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}} |
406 \isa{{\isaliteral{23}{\isacharhash}}} and \isa{{\isaliteral{40}{\isacharat}}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}} |
407 in their \isacommand{infixr} annotation). Thus the conclusion really is |
407 in their \isacommand{infixr} annotation). Thus the conclusion really is |
408 \begin{isabelle} |
408 \begin{isabelle} |
409 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
409 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
410 \end{isabelle} |
410 \end{isabelle} |
411 and the missing lemma is associativity of \isa{{\isacharat}}.% |
411 and the missing lemma is associativity of \isa{{\isaliteral{40}{\isacharat}}}.% |
412 \end{isamarkuptxt}% |
412 \end{isamarkuptxt}% |
413 \isamarkuptrue% |
413 \isamarkuptrue% |
414 % |
414 % |
415 \endisatagproof |
415 \endisatagproof |
416 {\isafoldproof}% |
416 {\isafoldproof}% |
427 Abandoning the previous attempt, the canonical proof procedure |
427 Abandoning the previous attempt, the canonical proof procedure |
428 succeeds without further ado.% |
428 succeeds without further ado.% |
429 \end{isamarkuptext}% |
429 \end{isamarkuptext}% |
430 \isamarkuptrue% |
430 \isamarkuptrue% |
431 \isacommand{lemma}\isamarkupfalse% |
431 \isacommand{lemma}\isamarkupfalse% |
432 \ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
432 \ app{\isaliteral{5F}{\isacharunderscore}}assoc\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}ys\ {\isaliteral{40}{\isacharat}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
433 % |
433 % |
434 \isadelimproof |
434 \isadelimproof |
435 % |
435 % |
436 \endisadelimproof |
436 \endisadelimproof |
437 % |
437 % |
438 \isatagproof |
438 \isatagproof |
439 \isacommand{apply}\isamarkupfalse% |
439 \isacommand{apply}\isamarkupfalse% |
440 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
440 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}\isanewline |
441 \isacommand{apply}\isamarkupfalse% |
441 \isacommand{apply}\isamarkupfalse% |
442 {\isacharparenleft}auto{\isacharparenright}\isanewline |
442 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline |
443 \isacommand{done}\isamarkupfalse% |
443 \isacommand{done}\isamarkupfalse% |
444 % |
444 % |
445 \endisatagproof |
445 \endisatagproof |
446 {\isafoldproof}% |
446 {\isafoldproof}% |
447 % |
447 % |
453 \noindent |
453 \noindent |
454 Now we can prove the first lemma:% |
454 Now we can prove the first lemma:% |
455 \end{isamarkuptext}% |
455 \end{isamarkuptext}% |
456 \isamarkuptrue% |
456 \isamarkuptrue% |
457 \isacommand{lemma}\isamarkupfalse% |
457 \isacommand{lemma}\isamarkupfalse% |
458 \ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline |
458 \ rev{\isaliteral{5F}{\isacharunderscore}}app\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
459 % |
459 % |
460 \isadelimproof |
460 \isadelimproof |
461 % |
461 % |
462 \endisadelimproof |
462 \endisadelimproof |
463 % |
463 % |
464 \isatagproof |
464 \isatagproof |
465 \isacommand{apply}\isamarkupfalse% |
465 \isacommand{apply}\isamarkupfalse% |
466 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
466 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}\isanewline |
467 \isacommand{apply}\isamarkupfalse% |
467 \isacommand{apply}\isamarkupfalse% |
468 {\isacharparenleft}auto{\isacharparenright}\isanewline |
468 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline |
469 \isacommand{done}\isamarkupfalse% |
469 \isacommand{done}\isamarkupfalse% |
470 % |
470 % |
471 \endisatagproof |
471 \endisatagproof |
472 {\isafoldproof}% |
472 {\isafoldproof}% |
473 % |
473 % |
479 \noindent |
479 \noindent |
480 Finally, we prove our main theorem:% |
480 Finally, we prove our main theorem:% |
481 \end{isamarkuptext}% |
481 \end{isamarkuptext}% |
482 \isamarkuptrue% |
482 \isamarkuptrue% |
483 \isacommand{theorem}\isamarkupfalse% |
483 \isacommand{theorem}\isamarkupfalse% |
484 \ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
484 \ rev{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}rev{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
485 % |
485 % |
486 \isadelimproof |
486 \isadelimproof |
487 % |
487 % |
488 \endisadelimproof |
488 \endisadelimproof |
489 % |
489 % |
490 \isatagproof |
490 \isatagproof |
491 \isacommand{apply}\isamarkupfalse% |
491 \isacommand{apply}\isamarkupfalse% |
492 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline |
492 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}\isanewline |
493 \isacommand{apply}\isamarkupfalse% |
493 \isacommand{apply}\isamarkupfalse% |
494 {\isacharparenleft}auto{\isacharparenright}\isanewline |
494 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline |
495 \isacommand{done}\isamarkupfalse% |
495 \isacommand{done}\isamarkupfalse% |
496 % |
496 % |
497 \endisatagproof |
497 \endisatagproof |
498 {\isafoldproof}% |
498 {\isafoldproof}% |
499 % |
499 % |