author | wenzelm |
Fri, 10 Jul 2020 21:30:21 +0200 | |
changeset 72006 | 751f371d6883 |
parent 69597 | ff784d5a5bfb |
child 74887 | 56247fdb8bbb |
permissions | -rw-r--r-- |
15136 | 1 |
theory ToyList |
58926
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
2 |
imports Main |
15136 | 3 |
begin |
8745 | 4 |
|
67406 | 5 |
text\<open>\noindent |
69505 | 6 |
HOL already has a predefined theory of lists called \<open>List\<close> --- |
7 |
\<open>ToyList\<close> is merely a small fragment of it chosen as an example. |
|
58926
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
8 |
To avoid some ambiguities caused by defining lists twice, we manipulate |
69597 | 9 |
the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows. |
67406 | 10 |
\<close> |
8745 | 11 |
|
58926
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
12 |
no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) |
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
13 |
hide_type list |
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
14 |
hide_const rev |
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58860
diff
changeset
|
15 |
|
8745 | 16 |
datatype 'a list = Nil ("[]") |
58860 | 17 |
| Cons 'a "'a list" (infixr "#" 65) |
8745 | 18 |
|
67406 | 19 |
text\<open>\noindent |
12327 | 20 |
The datatype\index{datatype@\isacommand {datatype} (command)} |
21 |
\tydx{list} introduces two |
|
11428 | 22 |
constructors \cdx{Nil} and \cdx{Cons}, the |
9541 | 23 |
empty~list and the operator that adds an element to the front of a list. For |
9792 | 24 |
example, the term \isa{Cons True (Cons False Nil)} is a value of |
69597 | 25 |
type \<^typ>\<open>bool list\<close>, namely the list with the elements \<^term>\<open>True\<close> and |
26 |
\<^term>\<open>False\<close>. Because this notation quickly becomes unwieldy, the |
|
8745 | 27 |
datatype declaration is annotated with an alternative syntax: instead of |
9792 | 28 |
@{term[source]Nil} and \isa{Cons x xs} we can write |
69597 | 29 |
\<^term>\<open>[]\<close>\index{$HOL2list@\isa{[]}|bold} and |
30 |
\<^term>\<open>x # xs\<close>\index{$HOL2list@\isa{\#}|bold}. In fact, this |
|
11450 | 31 |
alternative syntax is the familiar one. Thus the list \isa{Cons True |
69597 | 32 |
(Cons False Nil)} becomes \<^term>\<open>True # False # []\<close>. The annotation |
11428 | 33 |
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
69505 | 34 |
means that \<open>#\<close> associates to |
69597 | 35 |
the right: the term \<^term>\<open>x # y # z\<close> is read as \<open>x # (y # z)\<close> |
69505 | 36 |
and not as \<open>(x # y) # z\<close>. |
37 |
The \<open>65\<close> is the priority of the infix \<open>#\<close>. |
|
8745 | 38 |
|
39 |
\begin{warn} |
|
13191 | 40 |
Syntax annotations can be powerful, but they are difficult to master and |
11456 | 41 |
are never necessary. You |
69505 | 42 |
could drop them from theory \<open>ToyList\<close> and go back to the identifiers |
27015 | 43 |
@{term[source]Nil} and @{term[source]Cons}. Novices should avoid using |
10795 | 44 |
syntax annotations in their own theories. |
8745 | 45 |
\end{warn} |
69505 | 46 |
Next, two functions \<open>app\<close> and \cdx{rev} are defined recursively, |
27015 | 47 |
in this order, because Isabelle insists on definition before use: |
67406 | 48 |
\<close> |
8745 | 49 |
|
27015 | 50 |
primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where |
51 |
"[] @ ys = ys" | |
|
52 |
"(x # xs) @ ys = x # (xs @ ys)" |
|
53 |
||
54 |
primrec rev :: "'a list \<Rightarrow> 'a list" where |
|
55 |
"rev [] = []" | |
|
56 |
"rev (x # xs) = (rev xs) @ (x # [])" |
|
8745 | 57 |
|
67406 | 58 |
text\<open>\noindent |
27015 | 59 |
Each function definition is of the form |
60 |
\begin{center} |
|
69505 | 61 |
\isacommand{primrec} \textit{name} \<open>::\<close> \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations} |
27015 | 62 |
\end{center} |
69505 | 63 |
The equations must be separated by \<open>|\<close>. |
27015 | 64 |
% |
69505 | 65 |
Function \<open>app\<close> is annotated with concrete syntax. Instead of the |
66 |
prefix syntax \<open>app xs ys\<close> the infix |
|
69597 | 67 |
\<^term>\<open>xs @ ys\<close>\index{$HOL2list@\isa{\at}|bold} becomes the preferred |
27015 | 68 |
form. |
8745 | 69 |
|
27015 | 70 |
\index{*rev (constant)|(}\index{append function|(} |
69597 | 71 |
The equations for \<open>app\<close> and \<^term>\<open>rev\<close> hardly need comments: |
72 |
\<open>app\<close> appends two lists and \<^term>\<open>rev\<close> reverses a list. The |
|
11428 | 73 |
keyword \commdx{primrec} indicates that the recursion is |
10790 | 74 |
of a particularly primitive kind where each recursive call peels off a datatype |
8771 | 75 |
constructor from one of the arguments. Thus the |
10654 | 76 |
recursion always terminates, i.e.\ the function is \textbf{total}. |
11428 | 77 |
\index{functions!total} |
8745 | 78 |
|
79 |
The termination requirement is absolutely essential in HOL, a logic of total |
|
80 |
functions. If we were to drop it, inconsistencies would quickly arise: the |
|
81 |
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting |
|
82 |
$f(n)$ on both sides. |
|
83 |
% However, this is a subtle issue that we cannot discuss here further. |
|
84 |
||
85 |
\begin{warn} |
|
11456 | 86 |
As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only |
8745 | 87 |
because of totality that reasoning in HOL is comparatively easy. More |
11456 | 88 |
generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as |
8745 | 89 |
function definitions whose totality has not been proved) because they |
90 |
quickly lead to inconsistencies. Instead, fixed constructs for introducing |
|
91 |
types and functions are offered (such as \isacommand{datatype} and |
|
92 |
\isacommand{primrec}) which are guaranteed to preserve consistency. |
|
93 |
\end{warn} |
|
94 |
||
11456 | 95 |
\index{syntax}% |
8745 | 96 |
A remark about syntax. The textual definition of a theory follows a fixed |
10971 | 97 |
syntax with keywords like \isacommand{datatype} and \isacommand{end}. |
98 |
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list). |
|
8745 | 99 |
Embedded in this syntax are the types and formulae of HOL, whose syntax is |
12631 | 100 |
extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators. |
10971 | 101 |
To distinguish the two levels, everything |
8745 | 102 |
HOL-specific (terms and types) should be enclosed in |
103 |
\texttt{"}\dots\texttt{"}. |
|
104 |
To lessen this burden, quotation marks around a single identifier can be |
|
27015 | 105 |
dropped, unless the identifier happens to be a keyword, for example |
106 |
\isa{"end"}. |
|
8745 | 107 |
When Isabelle prints a syntax error message, it refers to the HOL syntax as |
11456 | 108 |
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}. |
8745 | 109 |
|
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
110 |
Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}. |
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
111 |
|
25342 | 112 |
\section{Evaluation} |
113 |
\index{evaluation} |
|
114 |
||
115 |
Assuming you have processed the declarations and definitions of |
|
116 |
\texttt{ToyList} presented so far, you may want to test your |
|
117 |
functions by running them. For example, what is the value of |
|
69597 | 118 |
\<^term>\<open>rev(True#False#[])\<close>? Command |
67406 | 119 |
\<close> |
25342 | 120 |
|
121 |
value "rev (True # False # [])" |
|
122 |
||
69597 | 123 |
text\<open>\noindent yields the correct result \<^term>\<open>False # True # []\<close>. |
25342 | 124 |
But we can go beyond mere functional programming and evaluate terms with |
67406 | 125 |
variables in them, executing functions symbolically:\<close> |
25342 | 126 |
|
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
127 |
value "rev (a # b # c # [])" |
25342 | 128 |
|
69597 | 129 |
text\<open>\noindent yields \<^term>\<open>c # b # a # []\<close>. |
38432
439f50a241c1
Using type real does not require a separate logic now.
nipkow
parents:
38430
diff
changeset
|
130 |
|
10885 | 131 |
\section{An Introductory Proof} |
8745 | 132 |
\label{sec:intro-proof} |
133 |
||
25342 | 134 |
Having convinced ourselves (as well as one can by testing) that our |
135 |
definitions capture our intentions, we are ready to prove a few simple |
|
16360 | 136 |
theorems. This will illustrate not just the basic proof commands but |
137 |
also the typical proof process. |
|
8745 | 138 |
|
11457 | 139 |
\subsubsection*{Main Goal.} |
8745 | 140 |
|
141 |
Our goal is to show that reversing a list twice produces the original |
|
11456 | 142 |
list. |
67406 | 143 |
\<close> |
8745 | 144 |
|
58860 | 145 |
theorem rev_rev [simp]: "rev(rev xs) = xs" |
8745 | 146 |
|
67406 | 147 |
txt\<open>\index{theorem@\isacommand {theorem} (command)|bold}% |
10795 | 148 |
\noindent |
11456 | 149 |
This \isacommand{theorem} command does several things: |
8745 | 150 |
\begin{itemize} |
151 |
\item |
|
69597 | 152 |
It establishes a new theorem to be proved, namely \<^prop>\<open>rev(rev xs) = xs\<close>. |
8745 | 153 |
\item |
69505 | 154 |
It gives that theorem the name \<open>rev_rev\<close>, for later reference. |
8745 | 155 |
\item |
11456 | 156 |
It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
69597 | 157 |
simplification will replace occurrences of \<^term>\<open>rev(rev xs)\<close> by |
158 |
\<^term>\<open>xs\<close>. |
|
11457 | 159 |
\end{itemize} |
8745 | 160 |
The name and the simplification attribute are optional. |
12332 | 161 |
Isabelle's response is to print the initial proof state consisting |
162 |
of some header information (like how many subgoals there are) followed by |
|
13868 | 163 |
@{subgoals[display,indent=0]} |
12332 | 164 |
For compactness reasons we omit the header in this tutorial. |
165 |
Until we have finished a proof, the \rmindex{proof state} proper |
|
166 |
always looks like this: |
|
9723 | 167 |
\begin{isabelle} |
8745 | 168 |
~1.~$G\sb{1}$\isanewline |
169 |
~~\vdots~~\isanewline |
|
170 |
~$n$.~$G\sb{n}$ |
|
9723 | 171 |
\end{isabelle} |
13868 | 172 |
The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ |
173 |
that we need to prove to establish the main goal.\index{subgoals} |
|
174 |
Initially there is only one subgoal, which is identical with the |
|
175 |
main goal. (If you always want to see the main goal as well, |
|
176 |
set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} |
|
177 |
--- this flag used to be set by default.) |
|
8745 | 178 |
|
69597 | 179 |
Let us now get back to \<^prop>\<open>rev(rev xs) = xs\<close>. Properties of recursively |
8745 | 180 |
defined functions are best established by induction. In this case there is |
69597 | 181 |
nothing obvious except induction on \<^term>\<open>xs\<close>: |
67406 | 182 |
\<close> |
8745 | 183 |
|
58860 | 184 |
apply(induct_tac xs) |
8745 | 185 |
|
67406 | 186 |
txt\<open>\noindent\index{*induct_tac (method)}% |
69597 | 187 |
This tells Isabelle to perform induction on variable \<^term>\<open>xs\<close>. The suffix |
188 |
\<^term>\<open>tac\<close> stands for \textbf{tactic},\index{tactics} |
|
11428 | 189 |
a synonym for ``theorem proving function''. |
8745 | 190 |
By default, induction acts on the first subgoal. The new proof state contains |
9792 | 191 |
two subgoals, namely the base case (@{term[source]Nil}) and the induction step |
192 |
(@{term[source]Cons}): |
|
10971 | 193 |
@{subgoals[display,indent=0,margin=65]} |
8745 | 194 |
|
11456 | 195 |
The induction step is an example of the general format of a subgoal:\index{subgoals} |
9723 | 196 |
\begin{isabelle} |
12327 | 197 |
~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
10328 | 198 |
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold} |
8745 | 199 |
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
200 |
ignored most of the time, or simply treated as a list of variables local to |
|
10302 | 201 |
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. |
11456 | 202 |
The {\it assumptions}\index{assumptions!of subgoal} |
203 |
are the local assumptions for this subgoal and {\it |
|
204 |
conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. |
|
205 |
Typical proof steps |
|
206 |
that add new assumptions are induction and case distinction. In our example |
|
69597 | 207 |
the only assumption is the induction hypothesis \<^term>\<open>rev (rev list) = |
208 |
list\<close>, where \<^term>\<open>list\<close> is a variable name chosen by Isabelle. If there |
|
8745 | 209 |
are multiple assumptions, they are enclosed in the bracket pair |
210 |
\indexboldpos{\isasymlbrakk}{$Isabrl} and |
|
211 |
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. |
|
212 |
||
213 |
Let us try to solve both goals automatically: |
|
67406 | 214 |
\<close> |
8745 | 215 |
|
58860 | 216 |
apply(auto) |
8745 | 217 |
|
67406 | 218 |
txt\<open>\noindent |
8745 | 219 |
This command tells Isabelle to apply a proof strategy called |
69505 | 220 |
\<open>auto\<close> to all subgoals. Essentially, \<open>auto\<close> tries to |
10978 | 221 |
simplify the subgoals. In our case, subgoal~1 is solved completely (thanks |
69597 | 222 |
to the equation \<^prop>\<open>rev [] = []\<close>) and disappears; the simplified version |
8745 | 223 |
of subgoal~2 becomes the new subgoal~1: |
10971 | 224 |
@{subgoals[display,indent=0,margin=70]} |
8745 | 225 |
In order to simplify this subgoal further, a lemma suggests itself. |
67406 | 226 |
\<close> |
8745 | 227 |
(*<*) |
228 |
oops |
|
229 |
(*>*) |
|
230 |
||
67406 | 231 |
subsubsection\<open>First Lemma\<close> |
9723 | 232 |
|
67406 | 233 |
text\<open> |
11428 | 234 |
\indexbold{abandoning a proof}\indexbold{proofs!abandoning} |
235 |
After abandoning the above proof attempt (at the shell level type |
|
236 |
\commdx{oops}) we start a new proof: |
|
67406 | 237 |
\<close> |
8745 | 238 |
|
58860 | 239 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
8745 | 240 |
|
67406 | 241 |
txt\<open>\noindent The keywords \commdx{theorem} and |
11428 | 242 |
\commdx{lemma} are interchangeable and merely indicate |
10971 | 243 |
the importance we attach to a proposition. Therefore we use the words |
11428 | 244 |
\emph{theorem} and \emph{lemma} pretty much interchangeably, too. |
8745 | 245 |
|
69597 | 246 |
There are two variables that we could induct on: \<^term>\<open>xs\<close> and |
247 |
\<^term>\<open>ys\<close>. Because \<open>@\<close> is defined by recursion on |
|
248 |
the first argument, \<^term>\<open>xs\<close> is the correct one: |
|
67406 | 249 |
\<close> |
8745 | 250 |
|
58860 | 251 |
apply(induct_tac xs) |
8745 | 252 |
|
67406 | 253 |
txt\<open>\noindent |
8745 | 254 |
This time not even the base case is solved automatically: |
67406 | 255 |
\<close> |
8745 | 256 |
|
58860 | 257 |
apply(auto) |
8745 | 258 |
|
67406 | 259 |
txt\<open> |
10362 | 260 |
@{subgoals[display,indent=0,goals_limit=1]} |
261 |
Again, we need to abandon this proof attempt and prove another simple lemma |
|
262 |
first. In the future the step of abandoning an incomplete proof before |
|
263 |
embarking on the proof of a lemma usually remains implicit. |
|
67406 | 264 |
\<close> |
8745 | 265 |
(*<*) |
266 |
oops |
|
267 |
(*>*) |
|
268 |
||
67406 | 269 |
subsubsection\<open>Second Lemma\<close> |
9723 | 270 |
|
67406 | 271 |
text\<open> |
11456 | 272 |
We again try the canonical proof procedure: |
67406 | 273 |
\<close> |
8745 | 274 |
|
58860 | 275 |
lemma app_Nil2 [simp]: "xs @ [] = xs" |
276 |
apply(induct_tac xs) |
|
277 |
apply(auto) |
|
8745 | 278 |
|
67406 | 279 |
txt\<open> |
8745 | 280 |
\noindent |
69505 | 281 |
It works, yielding the desired message \<open>No subgoals!\<close>: |
10362 | 282 |
@{goals[display,indent=0]} |
8745 | 283 |
We still need to confirm that the proof is now finished: |
67406 | 284 |
\<close> |
8745 | 285 |
|
10171 | 286 |
done |
8745 | 287 |
|
67406 | 288 |
text\<open>\noindent |
11428 | 289 |
As a result of that final \commdx{done}, Isabelle associates the lemma just proved |
10171 | 290 |
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
291 |
if it is obvious from the context that the proof is finished. |
|
292 |
||
293 |
% Instead of \isacommand{apply} followed by a dot, you can simply write |
|
294 |
% \isacommand{by}\indexbold{by}, which we do most of the time. |
|
10971 | 295 |
Notice that in lemma @{thm[source]app_Nil2}, |
69597 | 296 |
as printed out after the final \isacommand{done}, the free variable \<^term>\<open>xs\<close> has been |
69505 | 297 |
replaced by the unknown \<open>?xs\<close>, just as explained in |
9792 | 298 |
\S\ref{sec:variables}. |
8745 | 299 |
|
300 |
Going back to the proof of the first lemma |
|
67406 | 301 |
\<close> |
8745 | 302 |
|
58860 | 303 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
304 |
apply(induct_tac xs) |
|
305 |
apply(auto) |
|
8745 | 306 |
|
67406 | 307 |
txt\<open> |
8745 | 308 |
\noindent |
69505 | 309 |
we find that this time \<open>auto\<close> solves the base case, but the |
8745 | 310 |
induction step merely simplifies to |
10362 | 311 |
@{subgoals[display,indent=0,goals_limit=1]} |
69505 | 312 |
Now we need to remember that \<open>@\<close> associates to the right, and that |
313 |
\<open>#\<close> and \<open>@\<close> have the same priority (namely the \<open>65\<close> |
|
8745 | 314 |
in their \isacommand{infixr} annotation). Thus the conclusion really is |
9723 | 315 |
\begin{isabelle} |
9792 | 316 |
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
9723 | 317 |
\end{isabelle} |
69505 | 318 |
and the missing lemma is associativity of \<open>@\<close>. |
67406 | 319 |
\<close> |
9723 | 320 |
(*<*)oops(*>*) |
8745 | 321 |
|
67406 | 322 |
subsubsection\<open>Third Lemma\<close> |
8745 | 323 |
|
67406 | 324 |
text\<open> |
11456 | 325 |
Abandoning the previous attempt, the canonical proof procedure |
326 |
succeeds without further ado. |
|
67406 | 327 |
\<close> |
8745 | 328 |
|
58860 | 329 |
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
330 |
apply(induct_tac xs) |
|
331 |
apply(auto) |
|
10171 | 332 |
done |
8745 | 333 |
|
67406 | 334 |
text\<open> |
8745 | 335 |
\noindent |
11456 | 336 |
Now we can prove the first lemma: |
67406 | 337 |
\<close> |
8745 | 338 |
|
58860 | 339 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" |
340 |
apply(induct_tac xs) |
|
341 |
apply(auto) |
|
10171 | 342 |
done |
8745 | 343 |
|
67406 | 344 |
text\<open>\noindent |
11456 | 345 |
Finally, we prove our main theorem: |
67406 | 346 |
\<close> |
8745 | 347 |
|
58860 | 348 |
theorem rev_rev [simp]: "rev(rev xs) = xs" |
349 |
apply(induct_tac xs) |
|
350 |
apply(auto) |
|
10171 | 351 |
done |
8745 | 352 |
|
67406 | 353 |
text\<open>\noindent |
11456 | 354 |
The final \commdx{end} tells Isabelle to close the current theory because |
355 |
we are finished with its development:% |
|
356 |
\index{*rev (constant)|)}\index{append function|)} |
|
67406 | 357 |
\<close> |
8745 | 358 |
|
359 |
end |