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