src/Doc/Prog_Prove/Types_and_funs.thy
 author nipkow Tue Jan 10 14:29:40 2017 +0100 (2017-01-10) changeset 64862 2baa926a958d parent 58860 fee7cfa69c50 child 67406 23307fd33906 permissions -rw-r--r--
tuned
     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 "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 *}

   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{* 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 *}

   281

   282 lemma "itrev xs [] = rev xs"

   283

   284 txt{* There is no choice as to the induction variable:

   285 *}

   286

   287 apply(induction xs)

   288 apply(auto)

   289

   290 txt{*

   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 *}

   303 (*<*)oops(*>*)

   304 lemma "itrev xs ys = rev xs @ ys"

   305 (*<*)apply(induction xs, auto)(*>*)

   306 txt{*

   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 *}

   324 (*<*)oops

   325 lemma "itrev xs ys = rev xs @ ys"

   326 (*>*)

   327 apply(induction xs arbitrary: ys)

   328

   329 txt{* 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 *}

   333

   334 apply auto

   335 done

   336

   337 text{*

   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 *}

   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 {*

   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 *}

   573

   574 datatype exp = Var | Const int | Add exp exp | Mult exp exp

   575

   576 text{*

   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 *}

   593 (*<*)

   594 end

   595 (*>*)