src/Doc/Prog_Prove/Types_and_funs.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 64862 2baa926a958d
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)
     2 theory Types_and_funs
     3 imports Main
     4 begin
     5 (*>*)
     6 text{*
     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}}*}
    12 
    13 type_synonym string = "char list"
    14 
    15 text{*
    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 *}
    58 
    59 datatype 'a tree = Tip | Node  "'a tree"  'a  "'a tree"
    60 
    61 text{* with a mirror function: *}
    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{* The following lemma illustrates induction: *}
    68 
    69 lemma "mirror(mirror t) = t"
    70 apply(induction t)
    71 
    72 txt{* 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 *}
    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{*
    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}}*}
   105 
   106 definition sq :: "nat \<Rightarrow> nat" where
   107 "sq n = n * n"
   108 
   109 text{* 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}}*}
   116 
   117 abbreviation sq' :: "nat \<Rightarrow> nat" where
   118 "sq' n \<equiv> n * n"
   119 
   120 text{* 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 *}
   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{* 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 *}
   174 
   175 lemma "div2(n) = n div 2"
   176 apply(induction n rule: div2.induct)
   177 
   178 txt{* (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 "treesum ::"} @{typ "nat tree \<Rightarrow> nat"}
   222 that sums up all values in a tree of natural numbers
   223 and prove @{prop "treesum t = listsum(contents t)"}.
   224 \end{exercise}
   225 
   226 \begin{exercise}
   227 Define a new type @{text "'a tree2"} of binary trees where values are also
   228 stored in the leaves of the tree.  Also reformulate the
   229 @{const mirror} function accordingly. Define two functions
   230 @{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"}
   231 that traverse a tree and collect all stored values in the respective order in
   232 a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}.
   233 \end{exercise}
   234 
   235 \begin{exercise}
   236 Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"}
   237 such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}.
   238 Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}.
   239 \end{exercise}
   240 
   241 
   242 \section{Induction Heuristics}\index{induction heuristics}
   243 
   244 We have already noted that theorems about recursive functions are proved by
   245 induction. In case the function has more than one argument, we have followed
   246 the following heuristic in the proofs about the append function:
   247 \begin{quote}
   248 \emph{Perform induction on argument number $i$\\
   249  if the function is defined by recursion on argument number $i$.}
   250 \end{quote}
   251 The key heuristic, and the main point of this section, is to
   252 \emph{generalize the goal before induction}.
   253 The reason is simple: if the goal is
   254 too specific, the induction hypothesis is too weak to allow the induction
   255 step to go through. Let us illustrate the idea with an example.
   256 
   257 Function @{const rev} has quadratic worst-case running time
   258 because it calls append for each element of the list and
   259 append is linear in its first argument.  A linear time version of
   260 @{const rev} requires an extra argument where the result is accumulated
   261 gradually, using only~@{text"#"}:
   262 *}
   263 (*<*)
   264 apply auto
   265 done
   266 (*>*)
   267 fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   268 "itrev []        ys = ys" |
   269 "itrev (x#xs) ys = itrev xs (x#ys)"
   270 
   271 text{* The behaviour of @{const itrev} is simple: it reverses
   272 its first argument by stacking its elements onto the second argument,
   273 and it returns that second argument when the first one becomes
   274 empty. Note that @{const itrev} is tail-recursive: it can be
   275 compiled into a loop; no stack is necessary for executing it.
   276 
   277 Naturally, we would like to show that @{const itrev} does indeed reverse
   278 its first argument provided the second one is empty:
   279 *}
   280 
   281 lemma "itrev xs [] = rev xs"
   282 
   283 txt{* There is no choice as to the induction variable:
   284 *}
   285 
   286 apply(induction xs)
   287 apply(auto)
   288 
   289 txt{*
   290 Unfortunately, this attempt does not prove
   291 the induction step:
   292 @{subgoals[display,margin=70]}
   293 The induction hypothesis is too weak.  The fixed
   294 argument,~@{term"[]"}, prevents it from rewriting the conclusion.  
   295 This example suggests a heuristic:
   296 \begin{quote}
   297 \emph{Generalize goals for induction by replacing constants by variables.}
   298 \end{quote}
   299 Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
   300 just not true.  The correct generalization is
   301 *}
   302 (*<*)oops(*>*)
   303 lemma "itrev xs ys = rev xs @ ys"
   304 (*<*)apply(induction xs, auto)(*>*)
   305 txt{*
   306 If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to
   307 @{term"rev xs"}, as required.
   308 In this instance it was easy to guess the right generalization.
   309 Other situations can require a good deal of creativity.  
   310 
   311 Although we now have two variables, only @{text xs} is suitable for
   312 induction, and we repeat our proof attempt. Unfortunately, we are still
   313 not there:
   314 @{subgoals[display,margin=65]}
   315 The induction hypothesis is still too weak, but this time it takes no
   316 intuition to generalize: the problem is that the @{text ys}
   317 in the induction hypothesis is fixed,
   318 but the induction hypothesis needs to be applied with
   319 @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
   320 for all @{text ys} instead of a fixed one. We can instruct induction
   321 to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}.
   322 *}
   323 (*<*)oops
   324 lemma "itrev xs ys = rev xs @ ys"
   325 (*>*)
   326 apply(induction xs arbitrary: ys)
   327 
   328 txt{* The induction hypothesis in the induction step is now universally quantified over @{text ys}:
   329 @{subgoals[display,margin=65]}
   330 Thus the proof succeeds:
   331 *}
   332 
   333 apply auto
   334 done
   335 
   336 text{*
   337 This leads to another heuristic for generalization:
   338 \begin{quote}
   339 \emph{Generalize induction by generalizing all free
   340 variables\\ {\em(except the induction variable itself)}.}
   341 \end{quote}
   342 Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. 
   343 This heuristic prevents trivial failures like the one above.
   344 However, it should not be applied blindly.
   345 It is not always required, and the additional quantifiers can complicate
   346 matters in some cases. The variables that need to be quantified are typically
   347 those that change in recursive calls.
   348 
   349 
   350 \subsection*{Exercises}
   351 
   352 \begin{exercise}
   353 Write a tail-recursive variant of the @{text add} function on @{typ nat}:
   354 @{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}.
   355 Tail-recursive means that in the recursive case, @{text itadd} needs to call
   356 itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}.
   357 Prove @{prop "itadd m n = add m n"}.
   358 \end{exercise}
   359 
   360 
   361 \section{Simplification}
   362 
   363 So far we have talked a lot about simplifying terms without explaining the concept.
   364 \conceptidx{Simplification}{simplification} means
   365 \begin{itemize}
   366 \item using equations $l = r$ from left to right (only),
   367 \item as long as possible.
   368 \end{itemize}
   369 To emphasize the directionality, equations that have been given the
   370 @{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}.
   371 Logically, they are still symmetric, but proofs by
   372 simplification use them only in the left-to-right direction.  The proof tool
   373 that performs simplifications is called the \concept{simplifier}. It is the
   374 basis of @{text auto} and other related proof methods.
   375 
   376 The idea of simplification is best explained by an example. Given the
   377 simplification rules
   378 \[
   379 \begin{array}{rcl@ {\quad}l}
   380 @{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\
   381 @{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\
   382 @{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\
   383 @{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4)
   384 \end{array}
   385 \]
   386 the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True}
   387 as follows:
   388 \[
   389 \begin{array}{r@ {}c@ {}l@ {\quad}l}
   390 @{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"}  & \stackrel{(1)}{=} \\
   391 @{text"(Suc 0"}     & \leq & @{text"Suc 0 + x)"}  & \stackrel{(2)}{=} \\
   392 @{text"(Suc 0"}     & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\
   393 @{text"(0"}         & \leq & @{text"0 + x)"}      & \stackrel{(4)}{=} \\[1ex]
   394  & @{const True}
   395 \end{array}
   396 \]
   397 Simplification is often also called \concept{rewriting}
   398 and simplification rules \conceptidx{rewrite rules}{rewrite rule}.
   399 
   400 \subsection{Simplification Rules}
   401 
   402 The attribute @{text"simp"} declares theorems to be simplification rules,
   403 which the simplifier will use automatically. In addition,
   404 \isacom{datatype} and \isacom{fun} commands implicitly declare some
   405 simplification rules: \isacom{datatype} the distinctness and injectivity
   406 rules, \isacom{fun} the defining equations. Definitions are not declared
   407 as simplification rules automatically! Nearly any theorem can become a
   408 simplification rule. The simplifier will try to transform it into an
   409 equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}.
   410 
   411 Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and
   412 @{prop"xs @ [] = xs"}, should be declared as simplification
   413 rules. Equations that may be counterproductive as simplification rules
   414 should only be used in specific proof steps (see \autoref{sec:simp} below).
   415 Distributivity laws, for example, alter the structure of terms
   416 and can produce an exponential blow-up.
   417 
   418 \subsection{Conditional Simplification Rules}
   419 
   420 Simplification rules can be conditional.  Before applying such a rule, the
   421 simplifier will first try to prove the preconditions, again by
   422 simplification. For example, given the simplification rules
   423 \begin{quote}
   424 @{prop"p(0::nat) = True"}\\
   425 @{prop"p(x) \<Longrightarrow> f(x) = g(x)"},
   426 \end{quote}
   427 the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"}
   428 but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"}
   429 is not provable.
   430 
   431 \subsection{Termination}
   432 
   433 Simplification can run forever, for example if both @{prop"f x = g x"} and
   434 @{prop"g(x) = f(x)"} are simplification rules. It is the user's
   435 responsibility not to include simplification rules that can lead to
   436 nontermination, either on their own or in combination with other
   437 simplification rules. The right-hand side of a simplification rule should
   438 always be ``simpler'' than the left-hand side --- in some sense. But since
   439 termination is undecidable, such a check cannot be automated completely
   440 and Isabelle makes little attempt to detect nontermination.
   441 
   442 When conditional simplification rules are applied, their preconditions are
   443 proved first. Hence all preconditions need to be
   444 simpler than the left-hand side of the conclusion. For example
   445 \begin{quote}
   446 @{prop "n < m \<Longrightarrow> (n < Suc m) = True"}
   447 \end{quote}
   448 is suitable as a simplification rule: both @{prop"n<m"} and @{const True}
   449 are simpler than \mbox{@{prop"n < Suc m"}}. But
   450 \begin{quote}
   451 @{prop "Suc n < m \<Longrightarrow> (n < m) = True"}
   452 \end{quote}
   453 leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}
   454 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}.
   455 
   456 \subsection{The \indexed{@{text simp}}{simp} Proof Method}
   457 \label{sec:simp}
   458 
   459 So far we have only used the proof method @{text auto}.  Method @{text simp}
   460 is the key component of @{text auto}, but @{text auto} can do much more. In
   461 some cases, @{text auto} is overeager and modifies the proof state too much.
   462 In such cases the more predictable @{text simp} method should be used.
   463 Given a goal
   464 \begin{quote}
   465 @{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"}
   466 \end{quote}
   467 the command
   468 \begin{quote}
   469 \isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"}
   470 \end{quote}
   471 simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using
   472 \begin{itemize}
   473 \item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun},
   474 \item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and
   475 \item the assumptions.
   476 \end{itemize}
   477 In addition to or instead of @{text add} there is also @{text del} for removing
   478 simplification rules temporarily. Both are optional. Method @{text auto}
   479 can be modified similarly:
   480 \begin{quote}
   481 \isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"}
   482 \end{quote}
   483 Here the modifiers are @{text"simp add"} and @{text"simp del"}
   484 instead of just @{text add} and @{text del} because @{text auto}
   485 does not just perform simplification.
   486 
   487 Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all
   488 subgoals. There is also @{text simp_all}, which applies @{text simp} to
   489 all subgoals.
   490 
   491 \subsection{Rewriting with Definitions}
   492 \label{sec:rewr-defs}
   493 
   494 Definitions introduced by the command \isacom{definition}
   495 can also be used as simplification rules,
   496 but by default they are not: the simplifier does not expand them
   497 automatically. Definitions are intended for introducing abstract concepts and
   498 not merely as abbreviations. Of course, we need to expand the definition
   499 initially, but once we have proved enough abstract properties of the new
   500 constant, we can forget its original definition. This style makes proofs more
   501 robust: if the definition has to be changed, only the proofs of the abstract
   502 properties will be affected.
   503 
   504 The definition of a function @{text f} is a theorem named @{text f_def}
   505 and can be added to a call of @{text simp} like any other theorem:
   506 \begin{quote}
   507 \isacom{apply}@{text"(simp add: f_def)"}
   508 \end{quote}
   509 In particular, let-expressions can be unfolded by
   510 making @{thm[source] Let_def} a simplification rule.
   511 
   512 \subsection{Case Splitting With @{text simp}}
   513 
   514 Goals containing if-expressions are automatically split into two cases by
   515 @{text simp} using the rule
   516 \begin{quote}
   517 @{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"}
   518 \end{quote}
   519 For example, @{text simp} can prove
   520 \begin{quote}
   521 @{prop"(A \<and> B) = (if A then B else False)"}
   522 \end{quote}
   523 because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"}
   524 simplify to @{const True}.
   525 
   526 We can split case-expressions similarly. For @{text nat} the rule looks like this:
   527 @{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)))"}
   528 Case expressions are not split automatically by @{text simp}, but @{text simp}
   529 can be instructed to do so:
   530 \begin{quote}
   531 \isacom{apply}@{text"(simp split: nat.split)"}
   532 \end{quote}
   533 splits all case-expressions over natural numbers. For an arbitrary
   534 datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}.
   535 Method @{text auto} can be modified in exactly the same way.
   536 The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names.
   537 Splitting if or case-expressions in the assumptions requires 
   538 @{text "split: if_splits"} or @{text "split: t.splits"}.
   539 
   540 
   541 \subsection*{Exercises}
   542 
   543 \exercise\label{exe:tree0}
   544 Define a datatype @{text tree0} of binary tree skeletons which do not store
   545 any information, neither in the inner nodes nor in the leaves.
   546 Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of
   547 all nodes (inner nodes and leaves) in such a tree.
   548 Consider the following recursive function:
   549 *}
   550 (*<*)
   551 datatype tree0 = Tip | Node tree0 tree0
   552 (*>*)
   553 fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where
   554 "explode 0 t = t" |
   555 "explode (Suc n) t = explode n (Node t t)"
   556 
   557 text {*
   558 Find an equation expressing the size of a tree after exploding it
   559 (\noquotes{@{term [source] "nodes (explode n t)"}}) as a function
   560 of @{term "nodes t"} and @{text n}. Prove your equation.
   561 You may use the usual arithmetic operators, including the exponentiation
   562 operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}.
   563 
   564 Hint: simplifying with the list of theorems @{thm[source] algebra_simps}
   565 takes care of common algebraic properties of the arithmetic operators.
   566 \endexercise
   567 
   568 \exercise
   569 Define arithmetic expressions in one variable over integers (type @{typ int})
   570 as a data type:
   571 *}
   572 
   573 datatype exp = Var | Const int | Add exp exp | Mult exp exp
   574 
   575 text{*
   576 Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}}
   577 such that @{term"eval e x"} evaluates @{text e} at the value
   578 @{text x}.
   579 
   580 A polynomial can be represented as a list of coefficients, starting with
   581 the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the
   582 polynomial $4 + 2x - x^2 + 3x^3$.
   583 Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}}
   584 that evaluates a polynomial at the given value.
   585 Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}}
   586 that transforms an expression into a polynomial. This may require auxiliary
   587 functions. Prove that @{text coeffs} preserves the value of the expression:
   588 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.}
   589 Hint: consider the hint in Exercise~\ref{exe:tree0}.
   590 \endexercise
   591 *}
   592 (*<*)
   593 end
   594 (*>*)