doc-src/TutorialI/ToyList/ToyList.thy
 author nipkow Tue Mar 18 17:54:27 2003 +0100 (2003-03-18) changeset 13868 01b516b64233 parent 13191 05a9929ee10e child 15136 1275417e3930 permissions -rw-r--r--
*** empty log message ***
     1 theory ToyList = PreList:

     2

     3 text{*\noindent

     4 HOL already has a predefined theory of lists called @{text"List"} ---

     5 @{text"ToyList"} is merely a small fragment of it chosen as an example. In

     6 contrast to what is recommended in \S\ref{sec:Basic:Theories},

     7 @{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a

     8 theory that contains pretty much everything but lists, thus avoiding

     9 ambiguities caused by defining lists twice.

    10 *}

    11

    12 datatype 'a list = Nil                          ("[]")

    13                  | Cons 'a "'a list"            (infixr "#" 65);

    14

    15 text{*\noindent

    16 The datatype\index{datatype@\isacommand {datatype} (command)}

    17 \tydx{list} introduces two

    18 constructors \cdx{Nil} and \cdx{Cons}, the

    19 empty~list and the operator that adds an element to the front of a list. For

    20 example, the term \isa{Cons True (Cons False Nil)} is a value of

    21 type @{typ"bool list"}, namely the list with the elements @{term"True"} and

    22 @{term"False"}. Because this notation quickly becomes unwieldy, the

    23 datatype declaration is annotated with an alternative syntax: instead of

    24 @{term[source]Nil} and \isa{Cons x xs} we can write

    25 @{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and   26 @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this

    27 alternative syntax is the familiar one.  Thus the list \isa{Cons True

    28 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation

    29 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}

    30 means that @{text"#"} associates to

    31 the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"}

    32 and not as @{text"(x # y) # z"}.

    33 The @{text 65} is the priority of the infix @{text"#"}.

    34

    35 \begin{warn}

    36   Syntax annotations can be powerful, but they are difficult to master and

    37   are never necessary.  You

    38   could drop them from theory @{text"ToyList"} and go back to the identifiers

    39   @{term[source]Nil} and @{term[source]Cons}.

    40   Novices should avoid using

    41   syntax annotations in their own theories.

    42 \end{warn}

    43 Next, two functions @{text"app"} and \cdx{rev} are declared:

    44 *}

    45

    46 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)

    47        rev :: "'a list \<Rightarrow> 'a list";

    48

    49 text{*

    50 \noindent

    51 In contrast to many functional programming languages,

    52 Isabelle insists on explicit declarations of all functions

    53 (keyword \commdx{consts}).  Apart from the declaration-before-use

    54 restriction, the order of items in a theory file is unconstrained. Function

    55 @{text"app"} is annotated with concrete syntax too. Instead of the

    56 prefix syntax @{text"app xs ys"} the infix

    57 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred   58 form. Both functions are defined recursively:   59 *}   60   61 primrec   62 "[] @ ys = ys"   63 "(x # xs) @ ys = x # (xs @ ys)";   64   65 primrec   66 "rev [] = []"   67 "rev (x # xs) = (rev xs) @ (x # [])";   68   69 text{*   70 \noindent\index{*rev (constant)|(}\index{append function|(}   71 The equations for @{text"app"} and @{term"rev"} hardly need comments:   72 @{text"app"} appends two lists and @{term"rev"} reverses a list. The   73 keyword \commdx{primrec} indicates that the recursion is   74 of a particularly primitive kind where each recursive call peels off a datatype   75 constructor from one of the arguments. Thus the   76 recursion always terminates, i.e.\ the function is \textbf{total}.   77 \index{functions!total}   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}   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}%   96 A remark about syntax. The textual definition of a theory follows a fixed   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).   99 Embedded in this syntax are the types and formulae of HOL, whose syntax is   100 extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators.   101 To distinguish the two levels, everything   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   105 dropped, unless the identifier happens to be a keyword, as in   106 *}   107   108 consts "end" :: "'a list \<Rightarrow> 'a"   109   110 text{*\noindent   111 When Isabelle prints a syntax error message, it refers to the HOL syntax as   112 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.   113   114   115 \section{An Introductory Proof}   116 \label{sec:intro-proof}   117   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   120 illustrate not just the basic proof commands but also the typical proof   121 process.   122   123 \subsubsection*{Main Goal.}   124   125 Our goal is to show that reversing a list twice produces the original   126 list.   127 *}   128   129 theorem rev_rev [simp]: "rev(rev xs) = xs";   130   131 txt{*\index{theorem@\isacommand {theorem} (command)|bold}%   132 \noindent   133 This \isacommand{theorem} command does several things:   134 \begin{itemize}   135 \item   136 It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.   137 \item   138 It gives that theorem the name @{text"rev_rev"}, for later reference.   139 \item   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   142 @{term"xs"}.   143 \end{itemize}   144 The name and the simplification attribute are optional.   145 Isabelle's response is to print the initial proof state consisting   146 of some header information (like how many subgoals there are) followed by   147 @{subgoals[display,indent=0]}   148 For compactness reasons we omit the header in this tutorial.   149 Until we have finished a proof, the \rmindex{proof state} proper   150 always looks like this:   151 \begin{isabelle}   152 ~1.~$G\sb{1}$\isanewline   153 ~~\vdots~~\isanewline   154 ~$n$.~$G\sb{n}$  155 \end{isabelle}   156 The numbered lines contain the subgoals$G\sb{1}$, \dots,$G\sb{n}$  157 that we need to prove to establish the main goal.\index{subgoals}   158 Initially there is only one subgoal, which is identical with the   159 main goal. (If you always want to see the main goal as well,   160 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}   161 --- this flag used to be set by default.)   162   163 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively   164 defined functions are best established by induction. In this case there is   165 nothing obvious except induction on @{term"xs"}:   166 *}   167   168 apply(induct_tac xs);   169   170 txt{*\noindent\index{*induct_tac (method)}%   171 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix   172 @{term"tac"} stands for \textbf{tactic},\index{tactics}   173 a synonym for theorem proving function''.   174 By default, induction acts on the first subgoal. The new proof state contains   175 two subgoals, namely the base case (@{term[source]Nil}) and the induction step   176 (@{term[source]Cons}):   177 @{subgoals[display,indent=0,margin=65]}   178   179 The induction step is an example of the general format of a subgoal:\index{subgoals}   180 \begin{isabelle}   181 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}   182 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}

   183 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be

   184 ignored most of the time, or simply treated as a list of variables local to

   185 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.

   186 The {\it assumptions}\index{assumptions!of subgoal}

   187 are the local assumptions for this subgoal and {\it

   188   conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.

   189 Typical proof steps

   190 that add new assumptions are induction and case distinction. In our example

   191 the only assumption is the induction hypothesis @{term"rev (rev list) =

   192   list"}, where @{term"list"} is a variable name chosen by Isabelle. If there

   193 are multiple assumptions, they are enclosed in the bracket pair

   194 \indexboldpos{\isasymlbrakk}{$Isabrl} and   195 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.

   196

   197 Let us try to solve both goals automatically:

   198 *}

   199

   200 apply(auto);

   201

   202 txt{*\noindent

   203 This command tells Isabelle to apply a proof strategy called

   204 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to

   205 simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks

   206 to the equation @{prop"rev [] = []"}) and disappears; the simplified version

   207 of subgoal~2 becomes the new subgoal~1:

   208 @{subgoals[display,indent=0,margin=70]}

   209 In order to simplify this subgoal further, a lemma suggests itself.

   210 *}

   211 (*<*)

   212 oops

   213 (*>*)

   214

   215 subsubsection{*First Lemma*}

   216

   217 text{*

   218 \indexbold{abandoning a proof}\indexbold{proofs!abandoning}

   219 After abandoning the above proof attempt (at the shell level type

   220 \commdx{oops}) we start a new proof:

   221 *}

   222

   223 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";

   224

   225 txt{*\noindent The keywords \commdx{theorem} and

   226 \commdx{lemma} are interchangeable and merely indicate

   227 the importance we attach to a proposition.  Therefore we use the words

   228 \emph{theorem} and \emph{lemma} pretty much interchangeably, too.

   229

   230 There are two variables that we could induct on: @{term"xs"} and

   231 @{term"ys"}. Because @{text"@"} is defined by recursion on

   232 the first argument, @{term"xs"} is the correct one:

   233 *}

   234

   235 apply(induct_tac xs);

   236

   237 txt{*\noindent

   238 This time not even the base case is solved automatically:

   239 *}

   240

   241 apply(auto);

   242

   243 txt{*

   244 @{subgoals[display,indent=0,goals_limit=1]}

   245 Again, we need to abandon this proof attempt and prove another simple lemma

   246 first. In the future the step of abandoning an incomplete proof before

   247 embarking on the proof of a lemma usually remains implicit.

   248 *}

   249 (*<*)

   250 oops

   251 (*>*)

   252

   253 subsubsection{*Second Lemma*}

   254

   255 text{*

   256 We again try the canonical proof procedure:

   257 *}

   258

   259 lemma app_Nil2 [simp]: "xs @ [] = xs";

   260 apply(induct_tac xs);

   261 apply(auto);

   262

   263 txt{*

   264 \noindent

   265 It works, yielding the desired message @{text"No subgoals!"}:

   266 @{goals[display,indent=0]}

   267 We still need to confirm that the proof is now finished:

   268 *}

   269

   270 done

   271

   272 text{*\noindent

   273 As a result of that final \commdx{done}, Isabelle associates the lemma just proved

   274 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}

   275 if it is obvious from the context that the proof is finished.

   276

   277 % Instead of \isacommand{apply} followed by a dot, you can simply write

   278 % \isacommand{by}\indexbold{by}, which we do most of the time.

   279 Notice that in lemma @{thm[source]app_Nil2},

   280 as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been

   281 replaced by the unknown @{text"?xs"}, just as explained in

   282 \S\ref{sec:variables}.

   283

   284 Going back to the proof of the first lemma

   285 *}

   286

   287 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";

   288 apply(induct_tac xs);

   289 apply(auto);

   290

   291 txt{*

   292 \noindent

   293 we find that this time @{text"auto"} solves the base case, but the

   294 induction step merely simplifies to

   295 @{subgoals[display,indent=0,goals_limit=1]}

   296 Now we need to remember that @{text"@"} associates to the right, and that

   297 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}

   298 in their \isacommand{infixr} annotation). Thus the conclusion really is

   299 \begin{isabelle}

   300 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))

   301 \end{isabelle}

   302 and the missing lemma is associativity of @{text"@"}.

   303 *}

   304 (*<*)oops(*>*)

   305

   306 subsubsection{*Third Lemma*}

   307

   308 text{*

   309 Abandoning the previous attempt, the canonical proof procedure

   310 succeeds without further ado.

   311 *}

   312

   313 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";

   314 apply(induct_tac xs);

   315 apply(auto);

   316 done

   317

   318 text{*

   319 \noindent

   320 Now we can prove the first lemma:

   321 *}

   322

   323 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";

   324 apply(induct_tac xs);

   325 apply(auto);

   326 done

   327

   328 text{*\noindent

   329 Finally, we prove our main theorem:

   330 *}

   331

   332 theorem rev_rev [simp]: "rev(rev xs) = xs";

   333 apply(induct_tac xs);

   334 apply(auto);

   335 done

   336

   337 text{*\noindent

   338 The final \commdx{end} tells Isabelle to close the current theory because

   339 we are finished with its development:%

   340 \index{*rev (constant)|)}\index{append function|)}

   341 *}

   342

   343 end