equal
deleted
inserted
replaced
118 Assuming you have input the declarations and definitions of \texttt{ToyList} |
118 Assuming you have input the declarations and definitions of \texttt{ToyList} |
119 presented so far, we are ready to prove a few simple theorems. This will |
119 presented so far, we are ready to prove a few simple theorems. This will |
120 illustrate not just the basic proof commands but also the typical proof |
120 illustrate not just the basic proof commands but also the typical proof |
121 process. |
121 process. |
122 |
122 |
123 \subsubsection*{Main Goal} |
123 \subsubsection*{Main Goal.} |
124 |
124 |
125 Our goal is to show that reversing a list twice produces the original |
125 Our goal is to show that reversing a list twice produces the original |
126 list. |
126 list. |
127 *} |
127 *} |
128 |
128 |
138 It gives that theorem the name @{text"rev_rev"}, for later reference. |
138 It gives that theorem the name @{text"rev_rev"}, for later reference. |
139 \item |
139 \item |
140 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
140 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
141 simplification will replace occurrences of @{term"rev(rev xs)"} by |
141 simplification will replace occurrences of @{term"rev(rev xs)"} by |
142 @{term"xs"}. |
142 @{term"xs"}. |
143 |
143 \end{itemize} |
144 The name and the simplification attribute are optional. |
144 The name and the simplification attribute are optional. |
145 \end{itemize} |
|
146 Isabelle's response is to print |
145 Isabelle's response is to print |
147 \begin{isabelle} |
146 \begin{isabelle} |
148 proof(prove):~step~0\isanewline |
147 proof(prove):~step~0\isanewline |
149 \isanewline |
148 \isanewline |
150 goal~(theorem~rev\_rev):\isanewline |
149 goal~(theorem~rev\_rev):\isanewline |