doc-src/ProgProve/Thys/Types_and_funs.thy
author nipkow
Mon, 02 Apr 2012 10:49:03 +0200
changeset 47269 29aa0c071875
child 47306 56d72c923281
permissions -rw-r--r--
New manual Programming and Proving in Isabelle/HOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
theory Types_and_funs
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
imports Main
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
begin
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
\vspace{-5ex}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
\section{Type and function definitions}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
Type synonyms are abbreviations for existing types, for example
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
type_synonym string = "char list"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
\subsection{Datatypes}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
The general form of a datatype definition looks like this:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
\begin{tabular}{@ {}rclcll}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
\isacom{datatype} @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
     & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
     & $|$ & \dots \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
     & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
\end{tabular}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
It introduces the constructors \
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>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
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
properties of the constructors:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
\begin{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
\item \emph{Distinctness:} $C_i\ \ldots \neq C_j\ \dots$ \quad if $i \neq j$
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
\item \emph{Injectivity:}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
\begin{tabular}[t]{l}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
 $(C_i \ x_1 \dots x_{n_i} = C_i \ y_1 \dots y_{n_i}) =$\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
 $(x_1 = y_1 \land \dots \land x_{n_i} = y_{n_i})$
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
\end{tabular}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    40
The fact that any value of the datatype is built from the constructors implies
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    41
the structural induction rule: to show
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    42
$P~x$ for all $x$ of type @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
$P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    45
Distinctness and injectivity are applied automatically by @{text auto}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    46
and other proof methods. Induction must be applied explicitly.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    47
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    48
Datatype values can be taken apart with case-expressions, for example
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    49
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    50
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    51
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    52
just like in functional programming languages. Case expressions
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    53
must be enclosed in parentheses.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    54
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    55
As an example, consider binary trees:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    56
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    57
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    58
datatype 'a tree = Tip | Node "('a tree)" 'a "('a tree)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    59
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    60
text{* with a mirror function: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    61
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    62
fun mirror :: "'a tree \<Rightarrow> 'a tree" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    63
"mirror Tip = Tip" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    64
"mirror (Node l a r) = Node (mirror r) a (mirror l)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    65
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    66
text{* The following lemma illustrates induction: *}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    67
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    68
lemma "mirror(mirror t) = t"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    69
apply(induction t)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    70
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    71
txt{* yields
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    72
@{subgoals[display]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    73
The induction step contains two induction hypotheses, one for each subtree.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    74
An application of @{text auto} finishes the proof.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    75
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    76
A very simple but also very useful datatype is the predefined
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    77
@{datatype[display] option}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    78
Its sole purpose is to add a new element @{const None} to an existing
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    79
type @{typ 'a}. To make sure that @{const None} is distinct from all the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    80
elements of @{typ 'a}, you wrap them up in @{const Some} and call
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    81
the new type @{typ"'a option"}. A typical application is a lookup function
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    82
on a list of key-value pairs, often called an association list:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    83
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    84
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    85
apply auto
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    86
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    87
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    88
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    89
"lookup [] x' = None" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    90
"lookup ((x,y) # ps) x' = (if x = x' then Some y else lookup ps x')"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    91
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    92
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    93
Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    94
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    95
\subsection{Definitions}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    96
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    97
Non recursive functions can be defined as in the following example:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    98
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    99
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   100
definition sq :: "nat \<Rightarrow> nat" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   101
"sq n = n * n"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   102
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   103
text{* Such definitions do not allow pattern matching but only
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   104
@{text"f x\<^isub>1 \<dots> x\<^isub>n = t"}, where @{text f} does not occur in @{text t}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   105
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   106
\subsection{Abbreviations}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   107
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   108
Abbreviations are similar to definitions:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   109
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   110
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   111
abbreviation sq' :: "nat \<Rightarrow> nat" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   112
"sq' n == n * n"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   113
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   114
text{* The key difference is that @{const sq'} is only syntactic sugar:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   115
@{term"sq' t"} is replaced by \mbox{@{term"t*t"}} after parsing, and every
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   116
occurrence of a term @{term"u*u"} is replaced by \mbox{@{term"sq' u"}} before
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   117
printing.  Internally, @{const sq'} does not exist.  This is also the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   118
advantage of abbreviations over definitions: definitions need to be expanded
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   119
explicitly (see \autoref{sec:rewr-defs}) whereas abbreviations are already
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   120
expanded upon parsing. However, abbreviations should be introduced sparingly:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   121
if abused, they can lead to a confusing discrepancy between the internal and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   122
external view of a term.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   123
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   124
\subsection{Recursive functions}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   125
\label{sec:recursive-funs}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   126
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   127
Recursive functions are defined with \isacom{fun} by pattern matching
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   128
over datatype constructors. The order of equations matters. Just as in
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   129
functional programming languages. However, all HOL functions must be
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   130
total. This simplifies the logic---terms are always defined---but means
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   131
that recursive functions must terminate. Otherwise one could define a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   132
function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   133
subtracting @{term"f n"} on both sides.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   134
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   135
Isabelle automatic termination checker requires that the arguments of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   136
recursive calls on the right-hand side must be strictly smaller than the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   137
arguments on the left-hand side. In the simplest case, this means that one
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   138
fixed argument position decreases in size with each recursive call. The size
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   139
is measured as the number of constructors (excluding 0-ary ones, e.g.\ @{text
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   140
Nil}). Lexicographic combinations are also recognised. In more complicated
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   141
situations, the user may have to prove termination by hand. For details
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   142
see~\cite{Krauss}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   143
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   144
Functions defined with \isacom{fun} come with their own induction schema
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   145
that mirrors the recursion schema and is derived from the termination
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   146
order. For example,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   147
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   148
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   149
fun div2 :: "nat \<Rightarrow> nat" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   150
"div2 0 = 0" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   151
"div2 (Suc 0) = Suc 0" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   152
"div2 (Suc(Suc n)) = Suc(div2 n)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   153
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   154
text{* does not just define @{const div2} but also proves a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   155
customised induction rule:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   156
\[
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   157
\inferrule{
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   158
\mbox{@{thm (prem 1) div2.induct}}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   159
\mbox{@{thm (prem 2) div2.induct}}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   160
\mbox{@{thm (prem 3) div2.induct}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   161
{\mbox{@{thm (concl) div2.induct[of _ "m"]}}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   162
\]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   163
This customised induction rule can simplify inductive proofs. For example,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   164
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   165
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   166
lemma "div2(n+n) = n"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   167
apply(induction n rule: div2.induct)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   168
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   169
txt{* yields the 3 subgoals
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   170
@{subgoals[display,margin=65]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   171
An application of @{text auto} finishes the proof.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   172
Had we used ordinary structural induction on @{text n},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   173
the proof would have needed an additional
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   174
case distinction in the induction step.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   175
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   176
The general case is often called \concept{computation induction},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   177
because the induction follows the (terminating!) computation.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   178
For every defining equation
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   179
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   180
@{text "f(e) = \<dots> f(r\<^isub>1) \<dots> f(r\<^isub>k) \<dots>"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   181
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   182
where @{text"f(r\<^isub>i)"}, @{text"i=1\<dots>k"}, are all the recursive calls,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   183
the induction rule @{text"f.induct"} contains one premise of the form
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   184
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   185
@{text"P(r\<^isub>1) \<Longrightarrow> \<dots> \<Longrightarrow> P(r\<^isub>k) \<Longrightarrow> P(e)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   186
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   187
If @{text "f :: \<tau>\<^isub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^isub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   188
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   189
\isacom{apply}@{text"(induction x\<^isub>1 \<dots> x\<^isub>n rule: f.induct)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   190
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   191
where typically there is a call @{text"f x\<^isub>1 \<dots> x\<^isub>n"} in the goal.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   192
But note that the induction rule does not mention @{text f} at all,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   193
except in its name, and is applicable independently of @{text f}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   194
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   195
\section{Induction heuristics}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   196
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   197
We have already noted that theorems about recursive functions are proved by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   198
induction. In case the function has more than one argument, we have followed
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   199
the following heuristic in the proofs about the append function:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   200
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   201
\emph{Perform induction on argument number $i$\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   202
 if the function is defined by recursion on argument number $i$.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   203
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   204
The key heuristic, and the main point of this section, is to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   205
\emph{generalise the goal before induction}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   206
The reason is simple: if the goal is
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   207
too specific, the induction hypothesis is too weak to allow the induction
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   208
step to go through. Let us illustrate the idea with an example.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   209
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   210
Function @{const rev} has quadratic worst-case running time
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   211
because it calls append for each element of the list and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   212
append is linear in its first argument.  A linear time version of
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   213
@{const rev} requires an extra argument where the result is accumulated
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   214
gradually, using only~@{text"#"}:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   215
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   216
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   217
apply auto
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   218
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   219
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   220
fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   221
"itrev []     ys = ys" |
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   222
"itrev (x#xs) ys = itrev xs (x#ys)"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   223
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   224
text{* The behaviour of @{const itrev} is simple: it reverses
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   225
its first argument by stacking its elements onto the second argument,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   226
and returning that second argument when the first one becomes
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   227
empty. Note that @{const itrev} is tail-recursive: it can be
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   228
compiled into a loop, no stack is necessary for executing it.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   229
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   230
Naturally, we would like to show that @{const itrev} does indeed reverse
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   231
its first argument provided the second one is empty:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   232
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   233
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   234
lemma "itrev xs [] = rev xs"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   235
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   236
txt{* There is no choice as to the induction variable:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   237
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   238
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   239
apply(induction xs)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   240
apply(auto)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   241
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   242
txt{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   243
Unfortunately, this attempt does not prove
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   244
the induction step:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   245
@{subgoals[display,margin=70]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   246
The induction hypothesis is too weak.  The fixed
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   247
argument,~@{term"[]"}, prevents it from rewriting the conclusion.  
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   248
This example suggests a heuristic:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   249
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   250
\emph{Generalise goals for induction by replacing constants by variables.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   251
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   252
Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   253
just not true.  The correct generalisation is
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   254
*};
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   255
(*<*)oops;(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   256
lemma "itrev xs ys = rev xs @ ys"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   257
(*<*)apply(induction xs, auto)(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   258
txt{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   259
If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   260
@{term"rev xs"}, as required.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   261
In this instance it was easy to guess the right generalisation.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   262
Other situations can require a good deal of creativity.  
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   263
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   264
Although we now have two variables, only @{text xs} is suitable for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   265
induction, and we repeat our proof attempt. Unfortunately, we are still
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   266
not there:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   267
@{subgoals[display,margin=65]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   268
The induction hypothesis is still too weak, but this time it takes no
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   269
intuition to generalise: the problem is that the @{text ys}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   270
in the induction hypothesis is fixed,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   271
but the induction hypothesis needs to be applied with
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   272
@{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   273
for all @{text ys} instead of a fixed one. We can instruct induction
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   274
to perform this generalisation for us by adding @{text "arbitrary: ys"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   275
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   276
(*<*)oops
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   277
lemma "itrev xs ys = rev xs @ ys"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   278
(*>*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   279
apply(induction xs arbitrary: ys)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   280
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   281
txt{* The induction hypothesis in the induction step is now universally quantified over @{text ys}:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   282
@{subgoals[display,margin=65]}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   283
Thus the proof succeeds:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   284
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   285
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   286
apply auto
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   287
done
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   288
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   289
text{*
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   290
This leads to another heuristic for generalisation:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   291
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   292
\emph{Generalise induction by generalising all free
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   293
variables\\ {\em(except the induction variable itself)}.}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   294
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   295
Generalisation is best performed with @{text"arbitrary: y\<^isub>1 \<dots> y\<^isub>k"}. 
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   296
This heuristic prevents trivial failures like the one above.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   297
However, it should not be applied blindly.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   298
It is not always required, and the additional quantifiers can complicate
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   299
matters in some cases. The variables that need to be quantified are typically
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   300
those that change in recursive calls.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   301
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   302
\section{Simplification}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   303
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   304
So far we have talked a lot about simplifying terms without explaining the concept. \concept{Simplification} means
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   305
\begin{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   306
\item using equations $l = r$ from left to right (only),
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   307
\item as long as possible.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   308
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   309
To emphasise the directionality, equations that have been given the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   310
@{text"simp"} attribute are called \concept{simplification}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   311
rules. Logically, they are still symmetric, but proofs by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   312
simplification use them only in the left-to-right direction.  The proof tool
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   313
that performs simplifications is called the \concept{simplifier}. It is the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   314
basis of @{text auto} and other related proof methods.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   315
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   316
The idea of simplification is best explained by an example. Given the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   317
simplification rules
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   318
\[
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   319
\begin{array}{rcl@ {\quad}l}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   320
@{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   321
@{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   322
@{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   323
@{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   324
\end{array}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   325
\]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   326
the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   327
as follows:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   328
\[
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   329
\begin{array}{r@ {}c@ {}l@ {\quad}l}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   330
@{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"}  & \stackrel{(1)}{=} \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   331
@{text"(Suc 0"}     & \leq & @{text"Suc 0 + x)"}  & \stackrel{(2)}{=} \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   332
@{text"(Suc 0"}     & \leq & @{text"Suc (0 + x)"} & \stackrel{(3)}{=} \\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   333
@{text"(0"}         & \leq & @{text"0 + x)"}      & \stackrel{(4)}{=} \\[1ex]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   334
 & @{const True}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   335
\end{array}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   336
\]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   337
Simplification is often also called \concept{rewriting}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   338
and simplification rules \concept{rewrite rules}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   339
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   340
\subsection{Simplification rules}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   341
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   342
The attribute @{text"simp"} declares theorems to be simplification rules,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   343
which the simplifier will use automatically. In addition,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   344
\isacom{datatype} and \isacom{fun} commands implicitly declare some
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   345
simplification rules: \isacom{datatype} the distinctness and injectivity
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   346
rules, \isacom{fun} the defining equations. Definitions are not declared
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   347
as simplification rules automatically! Nearly any theorem can become a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   348
simplification rule. The simplifier will try to transform it into an
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   349
equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   350
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   351
Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   352
@{prop"xs @ [] = xs"}, should be declared as simplification
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   353
rules. Equations that may be counterproductive as simplification rules
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   354
should only be used in specific proof steps (see \S\ref{sec:simp} below).
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   355
Distributivity laws, for example, alter the structure of terms
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   356
and can produce an exponential blow-up.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   357
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   358
\subsection{Conditional simplification rules}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   359
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   360
Simplification rules can be conditional.  Before applying such a rule, the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   361
simplifier will first try to prove the preconditions, again by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   362
simplification. For example, given the simplification rules
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   363
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   364
@{prop"p(0::nat) = True"}\\
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   365
@{prop"p(x) \<Longrightarrow> f(x) = g(x)"},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   366
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   367
the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   368
but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   369
is not provable.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   370
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   371
\subsection{Termination}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   372
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   373
Simplification can run forever, for example if both @{prop"f x = g x"} and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   374
@{prop"g(x) = f(x)"} are simplification rules. It is the user's
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   375
responsibility not to include simplification rules that can lead to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   376
nontermination, either on their own or in combination with other
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   377
simplification rules. The right-hand side of a simplification rule should
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   378
always be ``simpler'' than the left-hand side---in some sense. But since
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   379
termination is undecidable, such a check cannot be automated completely
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   380
and Isabelle makes little attempt to detect nontermination.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   381
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   382
When conditional simplification rules are applied, their preconditions are
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   383
proved first. Hence all preconditions need to be
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   384
simpler than the left-hand side of the conclusion. For example
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   385
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   386
@{prop "n < m \<Longrightarrow> (n < Suc m) = True"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   387
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   388
is suitable as a simplification rule: both @{prop"n<m"} and @{const True}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   389
are simpler than \mbox{@{prop"n < Suc m"}}. But
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   390
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   391
@{prop "Suc n < m \<Longrightarrow> (n < m) = True"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   392
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   393
leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   394
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}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   395
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   396
\subsection{The @{text simp} proof method}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   397
\label{sec:simp}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   398
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   399
So far we have only used the proof method @{text auto}.  Method @{text simp}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   400
is the key component of @{text auto}, but @{text auto} can do much more. In
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   401
some cases, @{text auto} is overeager and modifies the proof state too much.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   402
In such cases the more predictable @{text simp} method should be used.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   403
Given a goal
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   404
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   405
@{text"1. \<lbrakk> P\<^isub>1; \<dots>; P\<^isub>m \<rbrakk> \<Longrightarrow> C"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   406
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   407
the command
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   408
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   409
\isacom{apply}@{text"(simp add: th\<^isub>1 \<dots> th\<^isub>n)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   410
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   411
simplifies the assumptions @{text "P\<^isub>i"} and the conclusion @{text C} using
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   412
\begin{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   413
\item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun},
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   414
\item the additional lemmas @{text"th\<^isub>1 \<dots> th\<^isub>n"}, and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   415
\item the assumptions.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   416
\end{itemize}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   417
In addition to or instead of @{text add} there is also @{text del} for removing
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   418
simplification rules temporarily. Both are optional. Method @{text auto}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   419
can be modified similarly:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   420
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   421
\isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   422
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   423
Here the modifiers are @{text"simp add"} and @{text"simp del"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   424
instead of just @{text add} and @{text del} because @{text auto}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   425
does not just perform simplification.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   426
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   427
Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   428
subgoals. There is also @{text simp_all}, which applies @{text simp} to
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   429
all subgoals.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   430
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   431
\subsection{Rewriting with definitions}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   432
\label{sec:rewr-defs}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   433
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   434
Definitions introduced by the command \isacom{definition}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   435
can also be used as simplification rules,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   436
but by default they are not: the simplifier does not expand them
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   437
automatically. Definitions are intended for introducing abstract concepts and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   438
not merely as abbreviations. Of course, we need to expand the definition
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   439
initially, but once we have proved enough abstract properties of the new
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   440
constant, we can forget its original definition. This style makes proofs more
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   441
robust: if the definition has to be changed, only the proofs of the abstract
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   442
properties will be affected.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   443
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   444
The definition of a function @{text f} is a theorem named @{text f_def}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   445
and can be added to a call of @{text simp} just like any other theorem:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   446
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   447
\isacom{apply}@{text"(simp add: f_def)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   448
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   449
In particular, let-expressions can be unfolded by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   450
making @{thm[source] Let_def} a simplification rule.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   451
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   452
\subsection{Case splitting with @{text simp}}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   453
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   454
Goals containing if-expressions are automatically split into two cases by
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   455
@{text simp} using the rule
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   456
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   457
@{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   458
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   459
For example, @{text simp} can prove
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   460
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   461
@{prop"(A \<and> B) = (if A then B else False)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   462
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   463
because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   464
simplify to @{const True}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   465
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   466
We can split case-expressions similarly. For @{text nat} the rule looks like this:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   467
@{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)))"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   468
Case expressions are not split automatically by @{text simp}, but @{text simp}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   469
can be instructed to do so:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   470
\begin{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   471
\isacom{apply}@{text"(simp split: nat.split)"}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   472
\end{quote}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   473
splits all case-expressions over natural numbers. For an arbitrary
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   474
datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   475
Method @{text auto} can be modified in exactly the same way.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   476
*}
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   477
(*<*)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   478
end
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
   479
(*>*)