src/Doc/Prog_Prove/Types_and_funs.thy
author wenzelm
Fri Jan 12 14:08:53 2018 +0100 (2018-01-12)
changeset 67406 23307fd33906
parent 64862 2baa926a958d
child 67613 ce654b0e6d69
permissions -rw-r--r--
isabelle update_cartouches -c;
     1 (*<*)
     2 theory Types_and_funs
     3 imports Main
     4 begin
     5 (*>*)
     6 text\<open>
     7 \vspace{-5ex}
     8 \section{Type and Function Definitions}
     9 
    10 Type synonyms are abbreviations for existing types, for example
    11 \index{string@@{text string}}\<close>
    12 
    13 type_synonym string = "char list"
    14 
    15 text\<open>
    16 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
    17 
    18 \subsection{Datatypes}
    19 \label{sec:datatypes}
    20 
    21 The general form of a datatype definition looks like this:
    22 \begin{quote}
    23 \begin{tabular}{@ {}rclcll}
    24 \indexed{\isacom{datatype}}{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}
    25      & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\
    26      & $|$ & \dots \\
    27      & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$
    28 \end{tabular}
    29 \end{quote}
    30 It introduces the constructors \
    31 $C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"} \ and expresses that any value of this type is built from these constructors in a unique manner. Uniqueness is implied by the following
    32 properties of the constructors:
    33 \begin{itemize}
    34 \item \emph{Distinctness:} $C_i\ \ldots \neq C_j\ \dots$ \quad if $i \neq j$
    35 \item \emph{Injectivity:}
    36 \begin{tabular}[t]{l}
    37  $(C_i \ x_1 \dots x_{n_i} = C_i \ y_1 \dots y_{n_i}) =$\\
    38  $(x_1 = y_1 \land \dots \land x_{n_i} = y_{n_i})$
    39 \end{tabular}
    40 \end{itemize}
    41 The fact that any value of the datatype is built from the constructors implies
    42 the \concept{structural induction}\index{induction} rule: to show
    43 $P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"},
    44 one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming
    45 $P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}.
    46 Distinctness and injectivity are applied automatically by @{text auto}
    47 and other proof methods. Induction must be applied explicitly.
    48 
    49 Like in functional programming languages, datatype values can be taken apart
    50 with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example
    51 \begin{quote}
    52 \noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
    53 \end{quote}
    54 Case expressions must be enclosed in parentheses.
    55 
    56 As an example of a datatype beyond @{typ nat} and @{text list}, consider binary trees:
    57 \<close>
    58 
    59 datatype 'a tree = Tip | Node  "'a tree"  'a  "'a tree"
    60 
    61 text\<open>with a mirror function:\<close>
    62 
    63 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
    64 "mirror Tip = Tip" |
    65 "mirror (Node l a r) = Node (mirror r) a (mirror l)"
    66 
    67 text\<open>The following lemma illustrates induction:\<close>
    68 
    69 lemma "mirror(mirror t) = t"
    70 apply(induction t)
    71 
    72 txt\<open>yields
    73 @{subgoals[display]}
    74 The induction step contains two induction hypotheses, one for each subtree.
    75 An application of @{text auto} finishes the proof.
    76 
    77 A very simple but also very useful datatype is the predefined
    78 @{datatype[display] option}\index{option@@{text option}}\index{None@@{const None}}\index{Some@@{const Some}}
    79 Its sole purpose is to add a new element @{const None} to an existing
    80 type @{typ 'a}. To make sure that @{const None} is distinct from all the
    81 elements of @{typ 'a}, you wrap them up in @{const Some} and call
    82 the new type @{typ"'a option"}. A typical application is a lookup function
    83 on a list of key-value pairs, often called an association list:
    84 \<close>
    85 (*<*)
    86 apply auto
    87 done
    88 (*>*)
    89 fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
    90 "lookup [] x = None" |
    91 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
    92 
    93 text\<open>
    94 Note that @{text"\<tau>\<^sub>1 * \<tau>\<^sub>2"} is the type of pairs, also written @{text"\<tau>\<^sub>1 \<times> \<tau>\<^sub>2"}.
    95 Pairs can be taken apart either by pattern matching (as above) or with the
    96 projection functions @{const fst} and @{const snd}: @{thm fst_conv[of x y]} and @{thm snd_conv[of x y]}.
    97 Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
    98 is short for @{text"(a, (b, c))"} and @{text "\<tau>\<^sub>1 \<times> \<tau>\<^sub>2 \<times> \<tau>\<^sub>3"} is short for
    99 @{text "\<tau>\<^sub>1 \<times> (\<tau>\<^sub>2 \<times> \<tau>\<^sub>3)"}.
   100 
   101 \subsection{Definitions}
   102 
   103 Non-recursive functions can be defined as in the following example:
   104 \index{definition@\isacom{definition}}\<close>
   105 
   106 definition sq :: "nat \<Rightarrow> nat" where
   107 "sq n = n * n"
   108 
   109 text\<open>Such definitions do not allow pattern matching but only
   110 @{text"f x\<^sub>1 \<dots> x\<^sub>n = t"}, where @{text f} does not occur in @{text t}.
   111 
   112 \subsection{Abbreviations}
   113 
   114 Abbreviations are similar to definitions:
   115 \index{abbreviation@\isacom{abbreviation}}\<close>
   116 
   117 abbreviation sq' :: "nat \<Rightarrow> nat" where
   118 "sq' n \<equiv> n * n"
   119 
   120 text\<open>The key difference is that @{const sq'} is only syntactic sugar:
   121 after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}};
   122 before printing, every occurrence of @{term"u*u"} is replaced by
   123 \mbox{@{term"sq' u"}}.  Internally, @{const sq'} does not exist.
   124 This is the
   125 advantage of abbreviations over definitions: definitions need to be expanded
   126 explicitly (\autoref{sec:rewr-defs}) whereas abbreviations are already
   127 expanded upon parsing. However, abbreviations should be introduced sparingly:
   128 if abused, they can lead to a confusing discrepancy between the internal and
   129 external view of a term.
   130 
   131 The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}.
   132 
   133 \subsection{Recursive Functions}
   134 \label{sec:recursive-funs}
   135 
   136 Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching
   137 over datatype constructors. The order of equations matters, as in
   138 functional programming languages. However, all HOL functions must be
   139 total. This simplifies the logic --- terms are always defined --- but means
   140 that recursive functions must terminate. Otherwise one could define a
   141 function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by
   142 subtracting @{term"f n"} on both sides.
   143 
   144 Isabelle's automatic termination checker requires that the arguments of
   145 recursive calls on the right-hand side must be strictly smaller than the
   146 arguments on the left-hand side. In the simplest case, this means that one
   147 fixed argument position decreases in size with each recursive call. The size
   148 is measured as the number of constructors (excluding 0-ary ones, e.g., @{text
   149 Nil}). Lexicographic combinations are also recognized. In more complicated
   150 situations, the user may have to prove termination by hand. For details
   151 see~@{cite Krauss}.
   152 
   153 Functions defined with \isacom{fun} come with their own induction schema
   154 that mirrors the recursion schema and is derived from the termination
   155 order. For example,
   156 \<close>
   157 
   158 fun div2 :: "nat \<Rightarrow> nat" where
   159 "div2 0 = 0" |
   160 "div2 (Suc 0) = 0" |
   161 "div2 (Suc(Suc n)) = Suc(div2 n)"
   162 
   163 text\<open>does not just define @{const div2} but also proves a
   164 customized induction rule:
   165 \[
   166 \inferrule{
   167 \mbox{@{thm (prem 1) div2.induct}}\\
   168 \mbox{@{thm (prem 2) div2.induct}}\\
   169 \mbox{@{thm (prem 3) div2.induct}}}
   170 {\mbox{@{thm (concl) div2.induct[of _ "m"]}}}
   171 \]
   172 This customized induction rule can simplify inductive proofs. For example,
   173 \<close>
   174 
   175 lemma "div2(n) = n div 2"
   176 apply(induction n rule: div2.induct)
   177 
   178 txt\<open>(where the infix @{text div} is the predefined division operation)
   179 yields the subgoals
   180 @{subgoals[display,margin=65]}
   181 An application of @{text auto} finishes the proof.
   182 Had we used ordinary structural induction on @{text n},
   183 the proof would have needed an additional
   184 case analysis in the induction step.
   185 
   186 This example leads to the following induction heuristic:
   187 \begin{quote}
   188 \emph{Let @{text f} be a recursive function.
   189 If the definition of @{text f} is more complicated
   190 than having one equation for each constructor of some datatype,
   191 then properties of @{text f} are best proved via @{text "f.induct"}.\index{inductionrule@@{text".induct"}}}
   192 \end{quote}
   193 
   194 The general case is often called \concept{computation induction},
   195 because the induction follows the (terminating!) computation.
   196 For every defining equation
   197 \begin{quote}
   198 @{text "f(e) = \<dots> f(r\<^sub>1) \<dots> f(r\<^sub>k) \<dots>"}
   199 \end{quote}
   200 where @{text"f(r\<^sub>i)"}, @{text"i=1\<dots>k"}, are all the recursive calls,
   201 the induction rule @{text"f.induct"} contains one premise of the form
   202 \begin{quote}
   203 @{text"P(r\<^sub>1) \<Longrightarrow> \<dots> \<Longrightarrow> P(r\<^sub>k) \<Longrightarrow> P(e)"}
   204 \end{quote}
   205 If @{text "f :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this:
   206 \begin{quote}
   207 \isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}\index{inductionrule@@{text"induction ... rule:"}}
   208 \end{quote}
   209 where typically there is a call @{text"f x\<^sub>1 \<dots> x\<^sub>n"} in the goal.
   210 But note that the induction rule does not mention @{text f} at all,
   211 except in its name, and is applicable independently of @{text f}.
   212 
   213 
   214 \subsection*{Exercises}
   215 
   216 \begin{exercise}
   217 Starting from the type @{text "'a tree"} defined in the text, define
   218 a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"}
   219 that collects all values in a tree in a list, in any order,
   220 without removing duplicates.
   221 Then define a function @{text "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"}
   222 that sums up all values in a tree of natural numbers
   223 and prove @{prop "sum_tree t = sum_list(contents t)"}
   224 (where @{const sum_list} is predefined).
   225 \end{exercise}
   226 
   227 \begin{exercise}
   228 Define a new type @{text "'a tree2"} of binary trees where values are also
   229 stored in the leaves of the tree.  Also reformulate the
   230 @{const mirror} function accordingly. Define two functions
   231 @{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"}
   232 that traverse a tree and collect all stored values in the respective order in
   233 a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}.
   234 \end{exercise}
   235 
   236 \begin{exercise}
   237 Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"}
   238 such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}.
   239 Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}.
   240 \end{exercise}
   241 
   242 
   243 \section{Induction Heuristics}\index{induction heuristics}
   244 
   245 We have already noted that theorems about recursive functions are proved by
   246 induction. In case the function has more than one argument, we have followed
   247 the following heuristic in the proofs about the append function:
   248 \begin{quote}
   249 \emph{Perform induction on argument number $i$\\
   250  if the function is defined by recursion on argument number $i$.}
   251 \end{quote}
   252 The key heuristic, and the main point of this section, is to
   253 \emph{generalize the goal before induction}.
   254 The reason is simple: if the goal is
   255 too specific, the induction hypothesis is too weak to allow the induction
   256 step to go through. Let us illustrate the idea with an example.
   257 
   258 Function @{const rev} has quadratic worst-case running time
   259 because it calls append for each element of the list and
   260 append is linear in its first argument.  A linear time version of
   261 @{const rev} requires an extra argument where the result is accumulated
   262 gradually, using only~@{text"#"}:
   263 \<close>
   264 (*<*)
   265 apply auto
   266 done
   267 (*>*)
   268 fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   269 "itrev []        ys = ys" |
   270 "itrev (x#xs) ys = itrev xs (x#ys)"
   271 
   272 text\<open>The behaviour of @{const itrev} is simple: it reverses
   273 its first argument by stacking its elements onto the second argument,
   274 and it returns that second argument when the first one becomes
   275 empty. Note that @{const itrev} is tail-recursive: it can be
   276 compiled into a loop; no stack is necessary for executing it.
   277 
   278 Naturally, we would like to show that @{const itrev} does indeed reverse
   279 its first argument provided the second one is empty:
   280 \<close>
   281 
   282 lemma "itrev xs [] = rev xs"
   283 
   284 txt\<open>There is no choice as to the induction variable:
   285 \<close>
   286 
   287 apply(induction xs)
   288 apply(auto)
   289 
   290 txt\<open>
   291 Unfortunately, this attempt does not prove
   292 the induction step:
   293 @{subgoals[display,margin=70]}
   294 The induction hypothesis is too weak.  The fixed
   295 argument,~@{term"[]"}, prevents it from rewriting the conclusion.  
   296 This example suggests a heuristic:
   297 \begin{quote}
   298 \emph{Generalize goals for induction by replacing constants by variables.}
   299 \end{quote}
   300 Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
   301 just not true.  The correct generalization is
   302 \<close>
   303 (*<*)oops(*>*)
   304 lemma "itrev xs ys = rev xs @ ys"
   305 (*<*)apply(induction xs, auto)(*>*)
   306 txt\<open>
   307 If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to
   308 @{term"rev xs"}, as required.
   309 In this instance it was easy to guess the right generalization.
   310 Other situations can require a good deal of creativity.  
   311 
   312 Although we now have two variables, only @{text xs} is suitable for
   313 induction, and we repeat our proof attempt. Unfortunately, we are still
   314 not there:
   315 @{subgoals[display,margin=65]}
   316 The induction hypothesis is still too weak, but this time it takes no
   317 intuition to generalize: the problem is that the @{text ys}
   318 in the induction hypothesis is fixed,
   319 but the induction hypothesis needs to be applied with
   320 @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
   321 for all @{text ys} instead of a fixed one. We can instruct induction
   322 to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}.
   323 \<close>
   324 (*<*)oops
   325 lemma "itrev xs ys = rev xs @ ys"
   326 (*>*)
   327 apply(induction xs arbitrary: ys)
   328 
   329 txt\<open>The induction hypothesis in the induction step is now universally quantified over @{text ys}:
   330 @{subgoals[display,margin=65]}
   331 Thus the proof succeeds:
   332 \<close>
   333 
   334 apply auto
   335 done
   336 
   337 text\<open>
   338 This leads to another heuristic for generalization:
   339 \begin{quote}
   340 \emph{Generalize induction by generalizing all free
   341 variables\\ {\em(except the induction variable itself)}.}
   342 \end{quote}
   343 Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. 
   344 This heuristic prevents trivial failures like the one above.
   345 However, it should not be applied blindly.
   346 It is not always required, and the additional quantifiers can complicate
   347 matters in some cases. The variables that need to be quantified are typically
   348 those that change in recursive calls.
   349 
   350 
   351 \subsection*{Exercises}
   352 
   353 \begin{exercise}
   354 Write a tail-recursive variant of the @{text add} function on @{typ nat}:
   355 @{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}.
   356 Tail-recursive means that in the recursive case, @{text itadd} needs to call
   357 itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}.
   358 Prove @{prop "itadd m n = add m n"}.
   359 \end{exercise}
   360 
   361 
   362 \section{Simplification}
   363 
   364 So far we have talked a lot about simplifying terms without explaining the concept.
   365 \conceptidx{Simplification}{simplification} means
   366 \begin{itemize}
   367 \item using equations $l = r$ from left to right (only),
   368 \item as long as possible.
   369 \end{itemize}
   370 To emphasize the directionality, equations that have been given the
   371 @{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}.
   372 Logically, they are still symmetric, but proofs by
   373 simplification use them only in the left-to-right direction.  The proof tool
   374 that performs simplifications is called the \concept{simplifier}. It is the
   375 basis of @{text auto} and other related proof methods.
   376 
   377 The idea of simplification is best explained by an example. Given the
   378 simplification rules
   379 \[
   380 \begin{array}{rcl@ {\quad}l}
   381 @{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\
   382 @{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\
   383 @{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\
   384 @{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4)
   385 \end{array}
   386 \]
   387 the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True}
   388 as follows:
   389 \[
   390 \begin{array}{r@ {}c@ {}l@ {\quad}l}
   391 @{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"}  & \stackrel{(1)}{=} \\
   392 @{text"(Suc 0"}     & \leq & @{text"Suc 0 + x)"}  & \stackrel{(2)}{=} \\
   393 @{text"(Suc 0"}     & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\
   394 @{text"(0"}         & \leq & @{text"0 + x)"}      & \stackrel{(4)}{=} \\[1ex]
   395  & @{const True}
   396 \end{array}
   397 \]
   398 Simplification is often also called \concept{rewriting}
   399 and simplification rules \conceptidx{rewrite rules}{rewrite rule}.
   400 
   401 \subsection{Simplification Rules}
   402 
   403 The attribute @{text"simp"} declares theorems to be simplification rules,
   404 which the simplifier will use automatically. In addition,
   405 \isacom{datatype} and \isacom{fun} commands implicitly declare some
   406 simplification rules: \isacom{datatype} the distinctness and injectivity
   407 rules, \isacom{fun} the defining equations. Definitions are not declared
   408 as simplification rules automatically! Nearly any theorem can become a
   409 simplification rule. The simplifier will try to transform it into an
   410 equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}.
   411 
   412 Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and
   413 @{prop"xs @ [] = xs"}, should be declared as simplification
   414 rules. Equations that may be counterproductive as simplification rules
   415 should only be used in specific proof steps (see \autoref{sec:simp} below).
   416 Distributivity laws, for example, alter the structure of terms
   417 and can produce an exponential blow-up.
   418 
   419 \subsection{Conditional Simplification Rules}
   420 
   421 Simplification rules can be conditional.  Before applying such a rule, the
   422 simplifier will first try to prove the preconditions, again by
   423 simplification. For example, given the simplification rules
   424 \begin{quote}
   425 @{prop"p(0::nat) = True"}\\
   426 @{prop"p(x) \<Longrightarrow> f(x) = g(x)"},
   427 \end{quote}
   428 the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"}
   429 but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"}
   430 is not provable.
   431 
   432 \subsection{Termination}
   433 
   434 Simplification can run forever, for example if both @{prop"f x = g x"} and
   435 @{prop"g(x) = f(x)"} are simplification rules. It is the user's
   436 responsibility not to include simplification rules that can lead to
   437 nontermination, either on their own or in combination with other
   438 simplification rules. The right-hand side of a simplification rule should
   439 always be ``simpler'' than the left-hand side --- in some sense. But since
   440 termination is undecidable, such a check cannot be automated completely
   441 and Isabelle makes little attempt to detect nontermination.
   442 
   443 When conditional simplification rules are applied, their preconditions are
   444 proved first. Hence all preconditions need to be
   445 simpler than the left-hand side of the conclusion. For example
   446 \begin{quote}
   447 @{prop "n < m \<Longrightarrow> (n < Suc m) = True"}
   448 \end{quote}
   449 is suitable as a simplification rule: both @{prop"n<m"} and @{const True}
   450 are simpler than \mbox{@{prop"n < Suc m"}}. But
   451 \begin{quote}
   452 @{prop "Suc n < m \<Longrightarrow> (n < m) = True"}
   453 \end{quote}
   454 leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}
   455 one first has to prove \mbox{@{prop"Suc n < m"}}, which can be rewritten to @{const True} provided @{prop"Suc(Suc n) < m"}, \emph{ad infinitum}.
   456 
   457 \subsection{The \indexed{@{text simp}}{simp} Proof Method}
   458 \label{sec:simp}
   459 
   460 So far we have only used the proof method @{text auto}.  Method @{text simp}
   461 is the key component of @{text auto}, but @{text auto} can do much more. In
   462 some cases, @{text auto} is overeager and modifies the proof state too much.
   463 In such cases the more predictable @{text simp} method should be used.
   464 Given a goal
   465 \begin{quote}
   466 @{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"}
   467 \end{quote}
   468 the command
   469 \begin{quote}
   470 \isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"}
   471 \end{quote}
   472 simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using
   473 \begin{itemize}
   474 \item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun},
   475 \item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and
   476 \item the assumptions.
   477 \end{itemize}
   478 In addition to or instead of @{text add} there is also @{text del} for removing
   479 simplification rules temporarily. Both are optional. Method @{text auto}
   480 can be modified similarly:
   481 \begin{quote}
   482 \isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"}
   483 \end{quote}
   484 Here the modifiers are @{text"simp add"} and @{text"simp del"}
   485 instead of just @{text add} and @{text del} because @{text auto}
   486 does not just perform simplification.
   487 
   488 Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all
   489 subgoals. There is also @{text simp_all}, which applies @{text simp} to
   490 all subgoals.
   491 
   492 \subsection{Rewriting with Definitions}
   493 \label{sec:rewr-defs}
   494 
   495 Definitions introduced by the command \isacom{definition}
   496 can also be used as simplification rules,
   497 but by default they are not: the simplifier does not expand them
   498 automatically. Definitions are intended for introducing abstract concepts and
   499 not merely as abbreviations. Of course, we need to expand the definition
   500 initially, but once we have proved enough abstract properties of the new
   501 constant, we can forget its original definition. This style makes proofs more
   502 robust: if the definition has to be changed, only the proofs of the abstract
   503 properties will be affected.
   504 
   505 The definition of a function @{text f} is a theorem named @{text f_def}
   506 and can be added to a call of @{text simp} like any other theorem:
   507 \begin{quote}
   508 \isacom{apply}@{text"(simp add: f_def)"}
   509 \end{quote}
   510 In particular, let-expressions can be unfolded by
   511 making @{thm[source] Let_def} a simplification rule.
   512 
   513 \subsection{Case Splitting With @{text simp}}
   514 
   515 Goals containing if-expressions are automatically split into two cases by
   516 @{text simp} using the rule
   517 \begin{quote}
   518 @{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"}
   519 \end{quote}
   520 For example, @{text simp} can prove
   521 \begin{quote}
   522 @{prop"(A \<and> B) = (if A then B else False)"}
   523 \end{quote}
   524 because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"}
   525 simplify to @{const True}.
   526 
   527 We can split case-expressions similarly. For @{text nat} the rule looks like this:
   528 @{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) & (ALL n. e = Suc n \<longrightarrow> P(b n)))"}
   529 Case expressions are not split automatically by @{text simp}, but @{text simp}
   530 can be instructed to do so:
   531 \begin{quote}
   532 \isacom{apply}@{text"(simp split: nat.split)"}
   533 \end{quote}
   534 splits all case-expressions over natural numbers. For an arbitrary
   535 datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}.
   536 Method @{text auto} can be modified in exactly the same way.
   537 The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names.
   538 Splitting if or case-expressions in the assumptions requires 
   539 @{text "split: if_splits"} or @{text "split: t.splits"}.
   540 
   541 
   542 \subsection*{Exercises}
   543 
   544 \exercise\label{exe:tree0}
   545 Define a datatype @{text tree0} of binary tree skeletons which do not store
   546 any information, neither in the inner nodes nor in the leaves.
   547 Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of
   548 all nodes (inner nodes and leaves) in such a tree.
   549 Consider the following recursive function:
   550 \<close>
   551 (*<*)
   552 datatype tree0 = Tip | Node tree0 tree0
   553 (*>*)
   554 fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where
   555 "explode 0 t = t" |
   556 "explode (Suc n) t = explode n (Node t t)"
   557 
   558 text \<open>
   559 Find an equation expressing the size of a tree after exploding it
   560 (\noquotes{@{term [source] "nodes (explode n t)"}}) as a function
   561 of @{term "nodes t"} and @{text n}. Prove your equation.
   562 You may use the usual arithmetic operators, including the exponentiation
   563 operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}.
   564 
   565 Hint: simplifying with the list of theorems @{thm[source] algebra_simps}
   566 takes care of common algebraic properties of the arithmetic operators.
   567 \endexercise
   568 
   569 \exercise
   570 Define arithmetic expressions in one variable over integers (type @{typ int})
   571 as a data type:
   572 \<close>
   573 
   574 datatype exp = Var | Const int | Add exp exp | Mult exp exp
   575 
   576 text\<open>
   577 Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}}
   578 such that @{term"eval e x"} evaluates @{text e} at the value
   579 @{text x}.
   580 
   581 A polynomial can be represented as a list of coefficients, starting with
   582 the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the
   583 polynomial $4 + 2x - x^2 + 3x^3$.
   584 Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}}
   585 that evaluates a polynomial at the given value.
   586 Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}}
   587 that transforms an expression into a polynomial. This may require auxiliary
   588 functions. Prove that @{text coeffs} preserves the value of the expression:
   589 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.}
   590 Hint: consider the hint in Exercise~\ref{exe:tree0}.
   591 \endexercise
   592 \<close>
   593 (*<*)
   594 end
   595 (*>*)