doc-src/IsarAdvanced/Functions/Thy/Functions.thy
author krauss
Thu, 12 Jul 2007 12:20:39 +0200
changeset 23805 953eb3c5f793
parent 23188 595a0e24bd8e
child 25091 a2ae7f71613d
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     1
(*  Title:      Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     2
    ID:         $Id$
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     4
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     5
Tutorial for function definitions with the new "function" package.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     6
*)
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     7
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     8
theory Functions
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
     9
imports Main
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    10
begin
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    11
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    12
section {* Function Definitions for Dummies *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    13
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    14
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    15
  In most cases, defining a recursive function is just as simple as other definitions:
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    16
*}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    17
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    18
fun fib :: "nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    19
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    20
  "fib 0 = 1"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    21
| "fib (Suc 0) = 1"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    22
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    23
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    24
text {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    25
  The syntax is rather self-explanatory: We introduce a function by
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    26
  giving its name, its type and a set of defining recursive
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    27
  equations.
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    28
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    29
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    30
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    31
  The function always terminates, since its argument gets smaller in
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    32
  every recursive call. 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    33
  Since HOL is a logic of total functions, termination is a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    34
  fundamental requirement to prevent inconsistencies\footnote{From the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    35
  \qt{definition} @{text "f(n) = f(n) + 1"} we could prove 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    36
  @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    37
  Isabelle tries to prove termination automatically when a definition
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    38
  is made. In \S\ref{termination}, we will look at cases where this
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    39
  fails and see what to do then.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    40
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    41
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    42
subsection {* Pattern matching *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    43
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    44
text {* \label{patmatch}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    45
  Like in functional programming, we can use pattern matching to
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    46
  define functions. At the moment we will only consider \emph{constructor
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    47
  patterns}, which only consist of datatype constructors and
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    48
  variables. Furthermore, patterns must be linear, i.e.\ all variables
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    49
  on the left hand side of an equation must be distinct. In
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    50
  \S\ref{genpats} we discuss more general pattern matching.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    51
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    52
  If patterns overlap, the order of the equations is taken into
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    53
  account. The following function inserts a fixed element between any
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    54
  two elements of a list:
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    55
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    56
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    57
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    58
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    59
  "sep a (x#y#xs) = x # a # sep a (y # xs)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    60
| "sep a xs       = xs"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    61
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    62
text {* 
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    63
  Overlapping patterns are interpreted as \qt{increments} to what is
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    64
  already there: The second equation is only meant for the cases where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    65
  the first one does not match. Consequently, Isabelle replaces it
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    66
  internally by the remaining cases, making the patterns disjoint:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    67
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    68
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    69
thm sep.simps
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    70
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    71
text {* @{thm [display] sep.simps[no_vars]} *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    72
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    73
text {* 
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    74
  \noindent The equations from function definitions are automatically used in
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    75
  simplification:
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    76
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    77
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    78
lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    79
by simp
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    80
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    81
subsection {* Induction *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    82
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    83
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    84
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    85
  Isabelle provides customized induction rules for recursive
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    86
  functions. These rules follow the recursive structure of the
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    87
  definition. Here is the rule @{text sep.induct} arising from the
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    88
  above definition of @{const sep}:
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    89
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    90
  @{thm [display] sep.induct}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    91
  
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    92
  We have a step case for list with at least two elements, and two
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    93
  base cases for the zero- and the one-element list. Here is a simple
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    94
  proof about @{const sep} and @{const map}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    95
*}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
    96
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    97
lemma "map f (sep x ys) = sep (f x) (map f ys)"
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    98
apply (induct x ys rule: sep.induct)
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
    99
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   100
txt {*
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   101
  We get three cases, like in the definition.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   102
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   103
  @{subgoals [display]}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   104
*}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   105
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   106
apply auto 
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   107
done
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   108
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   109
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   110
  With the \cmd{fun} command, you can define about 80\% of the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   111
  functions that occur in practice. The rest of this tutorial explains
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   112
  the remaining 20\%.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   113
*}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   114
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   115
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   116
section {* fun vs.\ function *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   117
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   118
text {* 
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   119
  The \cmd{fun} command provides a
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   120
  convenient shorthand notation for simple function definitions. In
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   121
  this mode, Isabelle tries to solve all the necessary proof obligations
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   122
  automatically. If a proof fails, the definition is
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   123
  rejected. This can either mean that the definition is indeed faulty,
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   124
  or that the default proof procedures are just not smart enough (or
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   125
  rather: not designed) to handle the definition.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   126
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   127
  By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   128
  solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   129
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   130
\end{isamarkuptext}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   131
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   132
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   133
\[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   134
\cmd{fun} @{text "f :: \<tau>"}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   135
\cmd{where}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   136
\hspace*{2ex}{\it equations}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   137
\hspace*{2ex}\vdots\vspace*{6pt}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   138
\end{minipage}\right]
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   139
\quad\equiv\quad
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   140
\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   141
\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   142
\cmd{where}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   143
\hspace*{2ex}{\it equations}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   144
\hspace*{2ex}\vdots\\%
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   145
\cmd{by} @{text "pat_completeness auto"}\\%
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   146
\cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   147
\end{minipage}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   148
\right]\]
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   149
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   150
\begin{isamarkuptext}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   151
  \vspace*{1em}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   152
  \noindent Some details have now become explicit:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   153
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   154
  \begin{enumerate}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   155
  \item The \cmd{sequential} option enables the preprocessing of
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   156
  pattern overlaps which we already saw. Without this option, the equations
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   157
  must already be disjoint and complete. The automatic completion only
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   158
  works with constructor patterns.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   159
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   160
  \item A function definition produces a proof obligation which
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   161
  expresses completeness and compatibility of patterns (we talk about
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   162
  this later). The combination of the methods @{text "pat_completeness"} and
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   163
  @{text "auto"} is used to solve this proof obligation.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   164
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   165
  \item A termination proof follows the definition, started by the
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   166
  \cmd{termination} command. This will be explained in \S\ref{termination}.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   167
 \end{enumerate}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   168
  Whenever a \cmd{fun} command fails, it is usually a good idea to
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   169
  expand the syntax to the more verbose \cmd{function} form, to see
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   170
  what is actually going on.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   171
 *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   172
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   173
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   174
section {* Termination *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   175
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   176
text {*\label{termination}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   177
  The method @{text "lexicographic_order"} is the default method for
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   178
  termination proofs. It can prove termination of a
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   179
  certain class of functions by searching for a suitable lexicographic
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   180
  combination of size measures. Of course, not all functions have such
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   181
  a simple termination argument. For them, we can specify the termination
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   182
  relation manually.
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   183
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   184
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   185
subsection {* The {\tt relation} method *}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   186
text{*
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   187
  Consider the following function, which sums up natural numbers up to
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   188
  @{text "N"}, using a counter @{text "i"}:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   189
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   190
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   191
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   192
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   193
  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   194
by pat_completeness auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   195
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   196
text {*
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   197
  \noindent The @{text "lexicographic_order"} method fails on this example, because none of the
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   198
  arguments decreases in the recursive call, with respect to the standard size ordering.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   199
  To prove termination manually, we must provide a custom wellfounded relation.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   200
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   201
  The termination argument for @{text "sum"} is based on the fact that
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   202
  the \emph{difference} between @{text "i"} and @{text "N"} gets
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   203
  smaller in every step, and that the recursion stops when @{text "i"}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   204
  is greater than @{text "N"}. Phrased differently, the expression 
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   205
  @{text "N + 1 - i"} always decreases.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   206
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   207
  We can use this expression as a measure function suitable to prove termination.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   208
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   209
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   210
termination
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   211
apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   212
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   213
txt {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   214
  The \cmd{termination} command sets up the termination goal for the
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   215
  specified function @{text "sum"}. If the function name is omitted, it
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   216
  implicitly refers to the last function definition.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   217
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   218
  The @{text relation} method takes a relation of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   219
  type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   220
  the function. If the function has multiple curried arguments, then
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   221
  these are packed together into a tuple, as it happened in the above
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   222
  example.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   223
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   224
  The predefined function @{term_type "measure"} constructs a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   225
  wellfounded relation from a mapping into the natural numbers (a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   226
  \emph{measure function}). 
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   227
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   228
  After the invocation of @{text "relation"}, we must prove that (a)
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   229
  the relation we supplied is wellfounded, and (b) that the arguments
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   230
  of recursive calls indeed decrease with respect to the
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   231
  relation:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   232
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   233
  @{subgoals[display,indent=0]}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   234
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   235
  These goals are all solved by @{text "auto"}:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   236
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   237
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   238
apply auto
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   239
done
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   240
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   241
text {*
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   242
  Let us complicate the function a little, by adding some more
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   243
  recursive calls: 
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   244
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   245
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   246
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   247
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   248
  "foo i N = (if i > N 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   249
              then (if N = 0 then 0 else foo 0 (N - 1))
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   250
              else i + foo (Suc i) N)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   251
by pat_completeness auto
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   252
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   253
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   254
  When @{text "i"} has reached @{text "N"}, it starts at zero again
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   255
  and @{text "N"} is decremented.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   256
  This corresponds to a nested
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   257
  loop where one index counts up and the other down. Termination can
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   258
  be proved using a lexicographic combination of two measures, namely
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   259
  the value of @{text "N"} and the above difference. The @{const
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   260
  "measures"} combinator generalizes @{text "measure"} by taking a
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   261
  list of measure functions.  
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   262
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   263
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   264
termination 
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   265
by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   266
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   267
subsection {* How @{text "lexicographic_order"} works *}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   268
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   269
(*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   270
where
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   271
  "fails a [] = a"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   272
| "fails a (x#xs) = fails (x + a) (x # xs)"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   273
*)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   274
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   275
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   276
  To see how the automatic termination proofs work, let's look at an
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   277
  example where it fails\footnote{For a detailed discussion of the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   278
  termination prover, see \cite{bulwahnKN07}}:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   279
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   280
\end{isamarkuptext}  
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   281
\cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   282
\cmd{where}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   283
\hspace*{2ex}@{text "\"fails a [] = a\""}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   284
|\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   285
\begin{isamarkuptext}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   286
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   287
\noindent Isabelle responds with the following error:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   288
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   289
\begin{isabelle}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   290
*** Unfinished subgoals:\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   291
*** (a, 1, <):\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   292
*** \ 1.~@{text "\<And>x. x = 0"}\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   293
*** (a, 1, <=):\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   294
*** \ 1.~False\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   295
*** (a, 2, <):\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   296
*** \ 1.~False\newline
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   297
*** Calls:\newline
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   298
*** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   299
*** Measures:\newline
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   300
*** 1) @{text "\<lambda>x. size (fst x)"}\newline
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   301
*** 2) @{text "\<lambda>x. size (snd x)"}\newline
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   302
*** Result matrix:\newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   303
*** \ \ \ \ 1\ \ 2  \newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   304
*** a:  ?   <= \newline
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   305
*** Could not find lexicographic termination order.\newline
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   306
*** At command "fun".\newline
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   307
\end{isabelle}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   308
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   309
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   310
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   311
text {*
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   312
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   313
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   314
  The the key to this error message is the matrix at the bottom. The rows
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   315
  of that matrix correspond to the different recursive calls (In our
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   316
  case, there is just one). The columns are the function's arguments 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   317
  (expressed through different measure functions, which map the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   318
  argument tuple to a natural number). 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   319
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   320
  The contents of the matrix summarize what is known about argument
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   321
  descents: The second argument has a weak descent (@{text "<="}) at the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   322
  recursive call, and for the first argument nothing could be proved,
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   323
  which is expressed by @{text "?"}. In general, there are the values
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   324
  @{text "<"}, @{text "<="} and @{text "?"}.
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   325
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   326
  For the failed proof attempts, the unfinished subgoals are also
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   327
  printed. Looking at these will often point to a missing lemma.
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   328
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   329
%  As a more real example, here is quicksort:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   330
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   331
(*
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   332
function qs :: "nat list \<Rightarrow> nat list"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   333
where
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   334
  "qs [] = []"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   335
| "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   336
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   337
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   338
termination apply lexicographic_order
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   339
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   340
text {* If we try @{text "lexicographic_order"} method, we get the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   341
  following error *}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   342
termination by (lexicographic_order simp:l2)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   343
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   344
lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   345
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   346
function 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   347
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   348
*)
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   349
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   350
section {* Mutual Recursion *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   351
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   352
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   353
  If two or more functions call one another mutually, they have to be defined
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   354
  in one step. Here are @{text "even"} and @{text "odd"}:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   355
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   356
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   357
function even :: "nat \<Rightarrow> bool"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   358
    and odd  :: "nat \<Rightarrow> bool"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   359
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   360
  "even 0 = True"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   361
| "odd 0 = False"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   362
| "even (Suc n) = odd n"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   363
| "odd (Suc n) = even n"
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   364
by pat_completeness auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   365
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   366
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   367
  To eliminate the mutual dependencies, Isabelle internally
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   368
  creates a single function operating on the sum
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   369
  type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   370
  defined as projections. Consequently, termination has to be proved
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   371
  simultaneously for both functions, by specifying a measure on the
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   372
  sum type: 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   373
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   374
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   375
termination 
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   376
by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   377
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   378
text {* 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   379
  We could also have used @{text lexicographic_order}, which
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   380
  supports mutual recursive termination proofs to a certain extent.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   381
*}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   382
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   383
subsection {* Induction for mutual recursion *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   384
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   385
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   386
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   387
  When functions are mutually recursive, proving properties about them
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   388
  generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   389
  generated from the above definition reflects this.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   390
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   391
  Let us prove something about @{const even} and @{const odd}:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   392
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   393
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   394
lemma even_odd_mod2:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   395
  "even n = (n mod 2 = 0)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   396
  "odd n = (n mod 2 = 1)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   397
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   398
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   399
  We apply simultaneous induction, specifying the induction variable
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   400
  for both goals, separated by \cmd{and}:  *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   401
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   402
apply (induct n and n rule: even_odd.induct)
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   403
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   404
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   405
  We get four subgoals, which correspond to the clauses in the
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   406
  definition of @{const even} and @{const odd}:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   407
  @{subgoals[display,indent=0]}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   408
  Simplification solves the first two goals, leaving us with two
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   409
  statements about the @{text "mod"} operation to prove:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   410
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   411
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   412
apply simp_all
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   413
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   414
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   415
  @{subgoals[display,indent=0]} 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   416
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   417
  \noindent These can be handled by Isabelle's arithmetic decision procedures.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   418
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   419
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   420
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   421
apply arith
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   422
apply arith
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   423
done
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   424
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   425
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   426
  In proofs like this, the simultaneous induction is really essential:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   427
  Even if we are just interested in one of the results, the other
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   428
  one is necessary to strengthen the induction hypothesis. If we leave
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   429
  out the statement about @{const odd} (by substituting it with @{term
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   430
  "True"}), the same proof fails:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   431
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   432
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   433
lemma failed_attempt:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   434
  "even n = (n mod 2 = 0)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   435
  "True"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   436
apply (induct n rule: even_odd.induct)
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   437
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   438
txt {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   439
  \noindent Now the third subgoal is a dead end, since we have no
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   440
  useful induction hypothesis available:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   441
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   442
  @{subgoals[display,indent=0]} 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   443
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   444
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   445
oops
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   446
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   447
section {* General pattern matching *}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   448
text{*\label{genpats} *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   449
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   450
subsection {* Avoiding automatic pattern splitting *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   451
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   452
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   453
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   454
  Up to now, we used pattern matching only on datatypes, and the
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   455
  patterns were always disjoint and complete, and if they weren't,
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   456
  they were made disjoint automatically like in the definition of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   457
  @{const "sep"} in \S\ref{patmatch}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   458
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   459
  This automatic splitting can significantly increase the number of
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   460
  equations involved, and this is not always desirable. The following
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   461
  example shows the problem:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   462
  
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   463
  Suppose we are modeling incomplete knowledge about the world by a
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   464
  three-valued datatype, which has values @{term "T"}, @{term "F"}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   465
  and @{term "X"} for true, false and uncertain propositions, respectively. 
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   466
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   467
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   468
datatype P3 = T | F | X
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   469
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   470
text {* \noindent Then the conjunction of such values can be defined as follows: *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   471
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   472
fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   473
where
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   474
  "And T p = p"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   475
| "And p T = p"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   476
| "And p F = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   477
| "And F p = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   478
| "And X X = X"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   479
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   480
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   481
text {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   482
  This definition is useful, because the equations can directly be used
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   483
  as simplification rules rules. But the patterns overlap: For example,
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   484
  the expression @{term "And T T"} is matched by both the first and
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   485
  the second equation. By default, Isabelle makes the patterns disjoint by
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   486
  splitting them up, producing instances:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   487
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   488
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   489
thm And.simps
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   490
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   491
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   492
  @{thm[indent=4] And.simps}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   493
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   494
  \vspace*{1em}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   495
  \noindent There are several problems with this:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   496
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   497
  \begin{enumerate}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   498
  \item If the datatype has many constructors, there can be an
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   499
  explosion of equations. For @{const "And"}, we get seven instead of
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   500
  five equations, which can be tolerated, but this is just a small
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   501
  example.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   502
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   503
  \item Since splitting makes the equations \qt{less general}, they
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   504
  do not always match in rewriting. While the term @{term "And x F"}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   505
  can be simplified to @{term "F"} with the original equations, a
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   506
  (manual) case split on @{term "x"} is now necessary.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   507
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   508
  \item The splitting also concerns the induction rule @{text
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   509
  "And.induct"}. Instead of five premises it now has seven, which
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   510
  means that our induction proofs will have more cases.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   511
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   512
  \item In general, it increases clarity if we get the same definition
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   513
  back which we put in.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   514
  \end{enumerate}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   515
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   516
  If we do not want the automatic splitting, we can switch it off by
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   517
  leaving out the \cmd{sequential} option. However, we will have to
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   518
  prove that our pattern matching is consistent\footnote{This prevents
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   519
  us from defining something like @{term "f x = True"} and @{term "f x
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   520
  = False"} simultaneously.}:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   521
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   522
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   523
function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   524
where
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   525
  "And2 T p = p"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   526
| "And2 p T = p"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   527
| "And2 p F = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   528
| "And2 F p = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   529
| "And2 X X = X"
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   530
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   531
txt {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   532
  \noindent Now let's look at the proof obligations generated by a
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   533
  function definition. In this case, they are:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   534
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   535
  @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   536
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   537
  The first subgoal expresses the completeness of the patterns. It has
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   538
  the form of an elimination rule and states that every @{term x} of
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   539
  the function's input type must match at least one of the patterns\footnote{Completeness could
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   540
  be equivalently stated as a disjunction of existential statements: 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   541
@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   542
  (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   543
  datatypes, we can solve it with the @{text "pat_completeness"}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   544
  method:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   545
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   546
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   547
apply pat_completeness
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   548
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   549
txt {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   550
  The remaining subgoals express \emph{pattern compatibility}. We do
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   551
  allow that an input value matches multiple patterns, but in this
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   552
  case, the result (i.e.~the right hand sides of the equations) must
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   553
  also be equal. For each pair of two patterns, there is one such
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   554
  subgoal. Usually this needs injectivity of the constructors, which
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   555
  is used automatically by @{text "auto"}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   556
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   557
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   558
by auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   559
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   560
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   561
subsection {* Non-constructor patterns *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   562
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   563
text {*
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   564
  Most of Isabelle's basic types take the form of inductive datatypes,
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   565
  and usually pattern matching works on the constructors of such types. 
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   566
  However, this need not be always the case, and the \cmd{function}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   567
  command handles other kind of patterns, too.
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   568
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   569
  One well-known instance of non-constructor patterns are
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   570
  so-called \emph{$n+k$-patterns}, which are a little controversial in
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   571
  the functional programming world. Here is the initial fibonacci
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   572
  example with $n+k$-patterns:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   573
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   574
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   575
function fib2 :: "nat \<Rightarrow> nat"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   576
where
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   577
  "fib2 0 = 1"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   578
| "fib2 1 = 1"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   579
| "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   580
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   581
(*<*)ML "goals_limit := 1"(*>*)
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   582
txt {*
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   583
  This kind of matching is again justified by the proof of pattern
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   584
  completeness and compatibility. 
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   585
  The proof obligation for pattern completeness states that every natural number is
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   586
  either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   587
  (2::nat)"}:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   588
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   589
  @{subgoals[display,indent=0]}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   590
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   591
  This is an arithmetic triviality, but unfortunately the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   592
  @{text arith} method cannot handle this specific form of an
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   593
  elimination rule. However, we can use the method @{text
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   594
  "elim_to_cases"} to do an ad-hoc conversion to a disjunction of
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   595
  existentials, which can then be soved by the arithmetic decision procedure.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   596
  Pattern compatibility and termination are automatic as usual.
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   597
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   598
(*<*)ML "goals_limit := 10"(*>*)
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   599
apply elim_to_cases
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   600
apply arith
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   601
apply auto
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   602
done
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   603
termination by lexicographic_order
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   604
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   605
text {*
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   606
  We can stretch the notion of pattern matching even more. The
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   607
  following function is not a sensible functional program, but a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   608
  perfectly valid mathematical definition:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   609
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   610
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   611
function ev :: "nat \<Rightarrow> bool"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   612
where
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   613
  "ev (2 * n) = True"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   614
| "ev (2 * n + 1) = False"
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   615
apply elim_to_cases
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   616
by arith+
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   617
termination by (relation "{}") simp
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   618
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   619
text {*
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   620
  This general notion of pattern matching gives you the full freedom
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   621
  of mathematical specifications. However, as always, freedom should
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   622
  be used with care:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   623
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   624
  If we leave the area of constructor
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   625
  patterns, we have effectively departed from the world of functional
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   626
  programming. This means that it is no longer possible to use the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   627
  code generator, and expect it to generate ML code for our
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   628
  definitions. Also, such a specification might not work very well together with
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   629
  simplification. Your mileage may vary.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   630
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   631
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   632
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   633
subsection {* Conditional equations *}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   634
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   635
text {* 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   636
  The function package also supports conditional equations, which are
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   637
  similar to guards in a language like Haskell. Here is Euclid's
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   638
  algorithm written with conditional patterns\footnote{Note that the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   639
  patterns are also overlapping in the base case}:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   640
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   641
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   642
function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   643
where
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   644
  "gcd x 0 = x"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   645
| "gcd 0 y = y"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   646
| "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   647
| "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   648
by (elim_to_cases, auto, arith)
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   649
termination by lexicographic_order
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   650
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   651
text {*
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   652
  By now, you can probably guess what the proof obligations for the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   653
  pattern completeness and compatibility look like. 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   654
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   655
  Again, functions with conditional patterns are not supported by the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   656
  code generator.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   657
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   658
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   659
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   660
subsection {* Pattern matching on strings *}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   661
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   662
text {*
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   663
  As strings (as lists of characters) are normal datatypes, pattern
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   664
  matching on them is possible, but somewhat problematic. Consider the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   665
  following definition:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   666
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   667
\end{isamarkuptext}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   668
\noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   669
\cmd{where}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   670
\hspace*{2ex}@{text "\"check (''good'') = True\""}\\%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   671
@{text "| \"check s = False\""}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   672
\begin{isamarkuptext}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   673
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   674
  \noindent An invocation of the above \cmd{fun} command does not
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   675
  terminate. What is the problem? Strings are lists of characters, and
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   676
  characters are a datatype with a lot of constructors. Splitting the
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   677
  catch-all pattern thus leads to an explosion of cases, which cannot
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   678
  be handled by Isabelle.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   679
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   680
  There are two things we can do here. Either we write an explicit
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   681
  @{text "if"} on the right hand side, or we can use conditional patterns:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   682
*}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   683
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   684
function check :: "string \<Rightarrow> bool"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   685
where
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   686
  "check (''good'') = True"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   687
| "s \<noteq> ''good'' \<Longrightarrow> check s = False"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   688
by auto
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   689
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   690
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   691
section {* Partiality *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   692
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   693
text {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   694
  In HOL, all functions are total. A function @{term "f"} applied to
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   695
  @{term "x"} always has the value @{term "f x"}, and there is no notion
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   696
  of undefinedness. 
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   697
  This is why we have to do termination
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   698
  proofs when defining functions: The proof justifies that the
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   699
  function can be defined by wellfounded recursion.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   700
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   701
  However, the \cmd{function} package does support partiality to a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   702
  certain extent. Let's look at the following function which looks
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   703
  for a zero of a given function f. 
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   704
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   705
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   706
function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   707
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   708
  "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   709
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   710
(*<*)declare findzero.simps[simp del](*>*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   711
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   712
text {*
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   713
  \noindent Clearly, any attempt of a termination proof must fail. And without
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   714
  that, we do not get the usual rules @{text "findzero.simp"} and 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   715
  @{text "findzero.induct"}. So what was the definition good for at all?
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   716
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   717
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   718
subsection {* Domain predicates *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   719
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   720
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   721
  The trick is that Isabelle has not only defined the function @{const findzero}, but also
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   722
  a predicate @{term "findzero_dom"} that characterizes the values where the function
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   723
  terminates: the \emph{domain} of the function. If we treat a
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   724
  partial function just as a total function with an additional domain
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   725
  predicate, we can derive simplification and
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   726
  induction rules as we do for total functions. They are guarded
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   727
  by domain conditions and are called @{text psimps} and @{text
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   728
  pinduct}: 
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   729
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   730
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   731
text {*
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   732
  \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   733
  \hfill(@{text "findzero.psimps"})
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   734
  \vspace{1em}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   735
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   736
  \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   737
  \hfill(@{text "findzero.pinduct"})
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   738
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   739
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   740
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   741
  Remember that all we
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   742
  are doing here is use some tricks to make a total function appear
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   743
  as if it was partial. We can still write the term @{term "findzero
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   744
  (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   745
  to some natural number, although we might not be able to find out
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   746
  which one. The function is \emph{underdefined}.
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   747
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   748
  But it is defined enough to prove something interesting about it. We
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   749
  can prove that if @{term "findzero f n"}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   750
  terminates, it indeed returns a zero of @{term f}:
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   751
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   752
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   753
lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   754
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   755
txt {* \noindent We apply induction as usual, but using the partial induction
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   756
  rule: *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   757
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   758
apply (induct f n rule: findzero.pinduct)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   759
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   760
txt {* \noindent This gives the following subgoals:
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   761
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   762
  @{subgoals[display,indent=0]}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   763
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   764
  \noindent The hypothesis in our lemma was used to satisfy the first premise in
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   765
  the induction rule. However, we also get @{term
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   766
  "findzero_dom (f, n)"} as a local assumption in the induction step. This
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   767
  allows to unfold @{term "findzero f n"} using the @{text psimps}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   768
  rule, and the rest is trivial. Since the @{text psimps} rules carry the
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   769
  @{text "[simp]"} attribute by default, we just need a single step:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   770
 *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   771
apply simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   772
done
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   773
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   774
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   775
  Proofs about partial functions are often not harder than for total
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   776
  functions. Fig.~\ref{findzero_isar} shows a slightly more
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   777
  complicated proof written in Isar. It is verbose enough to show how
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   778
  partiality comes into play: From the partial induction, we get an
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   779
  additional domain condition hypothesis. Observe how this condition
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   780
  is applied when calls to @{term findzero} are unfolded.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   781
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   782
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   783
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   784
\begin{figure}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   785
\hrule\vspace{6pt}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   786
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   787
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   788
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   789
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   790
lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   791
proof (induct rule: findzero.pinduct)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   792
  fix f n assume dom: "findzero_dom (f, n)"
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   793
               and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   794
               and x_range: "x \<in> {n ..< findzero f n}"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   795
  have "f n \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   796
  proof 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   797
    assume "f n = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   798
    with dom have "findzero f n = n" by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   799
    with x_range show False by auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   800
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   801
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   802
  from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   803
  thus "f x \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   804
  proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   805
    assume "x = n"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   806
    with `f n \<noteq> 0` show ?thesis by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   807
  next
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   808
    assume "x \<in> {Suc n ..< findzero f n}"
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   809
    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   810
    with IH and `f n \<noteq> 0`
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   811
    show ?thesis by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   812
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   813
qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   814
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   815
\isamarkupfalse\isabellestyle{tt}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   816
\end{minipage}\vspace{6pt}\hrule
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   817
\caption{A proof about a partial function}\label{findzero_isar}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   818
\end{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   819
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   820
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   821
subsection {* Partial termination proofs *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   822
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   823
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   824
  Now that we have proved some interesting properties about our
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   825
  function, we should turn to the domain predicate and see if it is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   826
  actually true for some values. Otherwise we would have just proved
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   827
  lemmas with @{term False} as a premise.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   828
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   829
  Essentially, we need some introduction rules for @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   830
  findzero_dom}. The function package can prove such domain
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   831
  introduction rules automatically. But since they are not used very
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   832
  often (they are almost never needed if the function is total), this
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   833
  functionality is disabled by default for efficiency reasons. So we have to go
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   834
  back and ask for them explicitly by passing the @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   835
  "(domintros)"} option to the function package:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   836
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   837
\vspace{1ex}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   838
\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   839
\cmd{where}\isanewline%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   840
\ \ \ldots\\
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   841
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   842
  \noindent Now the package has proved an introduction rule for @{text findzero_dom}:
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   843
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   844
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   845
thm findzero.domintros
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   846
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   847
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   848
  @{thm[display] findzero.domintros}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   849
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   850
  Domain introduction rules allow to show that a given value lies in the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   851
  domain of a function, if the arguments of all recursive calls
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   852
  are in the domain as well. They allow to do a \qt{single step} in a
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   853
  termination proof. Usually, you want to combine them with a suitable
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   854
  induction principle.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   855
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   856
  Since our function increases its argument at recursive calls, we
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   857
  need an induction principle which works \qt{backwards}. We will use
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   858
  @{text inc_induct}, which allows to do induction from a fixed number
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   859
  \qt{downwards}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   860
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   861
  \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   862
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   863
  Figure \ref{findzero_term} gives a detailed Isar proof of the fact
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   864
  that @{text findzero} terminates if there is a zero which is greater
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   865
  or equal to @{term n}. First we derive two useful rules which will
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   866
  solve the base case and the step case of the induction. The
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   867
  induction is then straightforward, except for the unusual induction
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   868
  principle.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   869
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   870
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   871
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   872
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   873
\begin{figure}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   874
\hrule\vspace{6pt}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   875
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   876
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   877
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   878
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   879
lemma findzero_termination:
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   880
  assumes "x \<ge> n" and "f x = 0"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   881
  shows "findzero_dom (f, n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   882
proof - 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   883
  have base: "findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   884
    by (rule findzero.domintros) (simp add:`f x = 0`)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   885
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   886
  have step: "\<And>i. findzero_dom (f, Suc i) 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   887
    \<Longrightarrow> findzero_dom (f, i)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   888
    by (rule findzero.domintros) simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   889
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   890
  from `x \<ge> n` show ?thesis
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   891
  proof (induct rule:inc_induct)
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   892
    show "findzero_dom (f, x)" by (rule base)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   893
  next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   894
    fix i assume "findzero_dom (f, Suc i)"
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   895
    thus "findzero_dom (f, i)" by (rule step)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   896
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   897
qed      
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   898
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   899
\isamarkupfalse\isabellestyle{tt}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   900
\end{minipage}\vspace{6pt}\hrule
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   901
\caption{Termination proof for @{text findzero}}\label{findzero_term}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   902
\end{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   903
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   904
      
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   905
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   906
  Again, the proof given in Fig.~\ref{findzero_term} has a lot of
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   907
  detail in order to explain the principles. Using more automation, we
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   908
  can also have a short proof:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   909
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   910
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   911
lemma findzero_termination_short:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   912
  assumes zero: "x >= n" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   913
  assumes [simp]: "f x = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   914
  shows "findzero_dom (f, n)"
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   915
using zero
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   916
by (induct rule:inc_induct) (auto intro: findzero.domintros)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   917
    
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   918
text {*
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   919
  \noindent It is simple to combine the partial correctness result with the
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   920
  termination lemma:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   921
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   922
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   923
lemma findzero_total_correctness:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   924
  "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   925
by (blast intro: findzero_zero findzero_termination)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   926
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   927
subsection {* Definition of the domain predicate *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   928
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   929
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   930
  Sometimes it is useful to know what the definition of the domain
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   931
  predicate looks like. Actually, @{text findzero_dom} is just an
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   932
  abbreviation:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   933
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   934
  @{abbrev[display] findzero_dom}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   935
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   936
  The domain predicate is the \emph{accessible part} of a relation @{const
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   937
  findzero_rel}, which was also created internally by the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   938
  package. @{const findzero_rel} is just a normal
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   939
  inductive predicate, so we can inspect its definition by
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   940
  looking at the introduction rules @{text findzero_rel.intros}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   941
  In our case there is just a single rule:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   942
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   943
  @{thm[display] findzero_rel.intros}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   944
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   945
  The predicate @{const findzero_rel}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   946
  describes the \emph{recursion relation} of the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   947
  definition. The recursion relation is a binary relation on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   948
  the arguments of the function that relates each argument to its
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   949
  recursive calls. In general, there is one introduction rule for each
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   950
  recursive call.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   951
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   952
  The predicate @{term "accp findzero_rel"} is the accessible part of
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   953
  that relation. An argument belongs to the accessible part, if it can
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   954
  be reached in a finite number of steps (cf.~its definition in @{text
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   955
  "Accessible_Part.thy"}).
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   956
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   957
  Since the domain predicate is just an abbreviation, you can use
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   958
  lemmas for @{const accp} and @{const findzero_rel} directly. Some
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   959
  lemmas which are occasionally useful are @{text accpI}, @{text
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   960
  accp_downward}, and of course the introduction and elimination rules
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   961
  for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   962
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   963
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   964
(*lemma findzero_nicer_domintros:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   965
  "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   966
  "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
   967
by (rule accpI, erule findzero_rel.cases, auto)+
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   968
*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   969
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   970
subsection {* A Useful Special Case: Tail recursion *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   971
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   972
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   973
  The domain predicate is our trick that allows us to model partiality
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   974
  in a world of total functions. The downside of this is that we have
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   975
  to carry it around all the time. The termination proof above allowed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   976
  us to replace the abstract @{term "findzero_dom (f, n)"} by the more
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   977
  concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   978
  there and can only be discharged for special cases.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   979
  In particular, the domain predicate guards the unfolding of our
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   980
  function, since it is there as a condition in the @{text psimp}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   981
  rules. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   982
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   983
  Now there is an important special case: We can actually get rid
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   984
  of the condition in the simplification rules, \emph{if the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   985
  is tail-recursive}. The reason is that for all tail-recursive
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   986
  equations there is a total function satisfying them, even if they
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   987
  are non-terminating. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   988
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   989
%  A function is tail recursive, if each call to the function is either
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   990
%  equal
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   991
%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   992
%  So the outer form of the 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   993
%
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   994
%if it can be written in the following
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   995
%  form:
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   996
%  {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   997
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
   998
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   999
  The function package internally does the right construction and can
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1000
  derive the unconditional simp rules, if we ask it to do so. Luckily,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1001
  our @{const "findzero"} function is tail-recursive, so we can just go
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1002
  back and add another option to the \cmd{function} command:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1003
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1004
\vspace{1ex}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1005
\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1006
\cmd{where}\isanewline%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1007
\ \ \ldots\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1008
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1009
  
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1010
  \noindent Now, we actually get unconditional simplification rules, even
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1011
  though the function is partial:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1012
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1013
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1014
thm findzero.simps
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1015
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1016
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1017
  @{thm[display] findzero.simps}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1018
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1019
  \noindent Of course these would make the simplifier loop, so we better remove
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1020
  them from the simpset:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1021
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1022
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1023
declare findzero.simps[simp del]
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1024
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1025
text {* 
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1026
  Getting rid of the domain conditions in the simplification rules is
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1027
  not only useful because it simplifies proofs. It is also required in
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1028
  order to use Isabelle's code generator to generate ML code
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1029
  from a function definition.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1030
  Since the code generator only works with equations, it cannot be
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1031
  used with @{text "psimp"} rules. Thus, in order to generate code for
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1032
  partial functions, they must be defined as a tail recursion.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1033
  Luckily, many functions have a relatively natural tail recursive
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1034
  definition.
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1035
*}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1036
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1037
section {* Nested recursion *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1038
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1039
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1040
  Recursive calls which are nested in one another frequently cause
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1041
  complications, since their termination proof can depend on a partial
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1042
  correctness property of the function itself. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1043
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1044
  As a small example, we define the \qt{nested zero} function:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1045
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1046
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1047
function nz :: "nat \<Rightarrow> nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1048
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1049
  "nz 0 = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1050
| "nz (Suc n) = nz (nz n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1051
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1052
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1053
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1054
  If we attempt to prove termination using the identity measure on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1055
  naturals, this fails:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1056
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1057
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1058
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1059
  apply (relation "measure (\<lambda>n. n)")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1060
  apply auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1061
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1062
txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1063
  We get stuck with the subgoal
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1064
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1065
  @{subgoals[display]}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1066
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1067
  Of course this statement is true, since we know that @{const nz} is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1068
  the zero function. And in fact we have no problem proving this
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1069
  property by induction.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1070
*}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1071
(*<*)oops(*>*)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1072
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1073
  by (induct rule:nz.pinduct) auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1074
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1075
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1076
  We formulate this as a partial correctness lemma with the condition
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1077
  @{term "nz_dom n"}. This allows us to prove it with the @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1078
  pinduct} rule before we have proved termination. With this lemma,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1079
  the termination proof works as expected:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1080
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1081
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1082
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1083
  by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1084
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1085
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1086
  As a general strategy, one should prove the statements needed for
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1087
  termination as a partial property first. Then they can be used to do
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1088
  the termination proof. This also works for less trivial
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1089
  examples. Figure \ref{f91} defines the 91-function, a well-known
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1090
  challenge problem due to John McCarthy, and proves its termination.
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1091
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1092
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1093
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1094
\begin{figure}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1095
\hrule\vspace{6pt}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1096
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1097
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1098
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1099
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1100
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1101
function f91 :: "nat \<Rightarrow> nat"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1102
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1103
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1104
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1105
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1106
lemma f91_estimate: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1107
  assumes trm: "f91_dom n" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1108
  shows "n < f91 n + 11"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1109
using trm by induct auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1110
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1111
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1112
proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1113
  let ?R = "measure (\<lambda>x. 101 - x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1114
  show "wf ?R" ..
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1115
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1116
  fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1117
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1118
  thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1119
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1120
  assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1121
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1122
  with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1123
qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1124
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1125
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1126
\isamarkupfalse\isabellestyle{tt}
23188
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1127
\end{minipage}
595a0e24bd8e updated
krauss
parents: 23003
diff changeset
  1128
\vspace{6pt}\hrule
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1129
\caption{McCarthy's 91-function}\label{f91}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1130
\end{figure}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1131
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1132
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1133
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1134
section {* Higher-Order Recursion *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1135
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1136
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1137
  Higher-order recursion occurs when recursive calls
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1138
  are passed as arguments to higher-order combinators such as @{term
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1139
  map}, @{term filter} etc.
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1140
  As an example, imagine a datatype of n-ary trees:
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1141
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1142
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1143
datatype 'a tree = 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1144
  Leaf 'a 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1145
| Branch "'a tree list"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1146
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1147
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1148
text {* \noindent We can define a map function for trees, using the predefined
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1149
  map function for lists. *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1150
  
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1151
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1152
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1153
  "treemap f (Leaf n) = Leaf (f n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1154
| "treemap f (Branch l) = Branch (map (treemap f) l)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1155
by pat_completeness auto
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1156
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1157
text {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1158
  We do the termination proof manually, to point out what happens
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1159
  here: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1160
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1161
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1162
termination proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1163
  txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1164
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1165
  As usual, we have to give a wellfounded relation, such that the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1166
  arguments of the recursive calls get smaller. But what exactly are
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1167
  the arguments of the recursive calls? Isabelle gives us the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1168
  subgoals
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1169
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1170
  @{subgoals[display,indent=0]} 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1171
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1172
  So Isabelle seems to know that @{const map} behaves nicely and only
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1173
  applies the recursive call @{term "treemap f"} to elements
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1174
  of @{term "l"}. Before we discuss where this knowledge comes from,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1175
  let us finish the termination proof:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1176
  *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1177
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1178
  show "wf (measure (size o snd))" by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1179
next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1180
  fix f l and x :: "'a tree"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1181
  assume "x \<in> set l"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1182
  thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1183
    apply simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1184
    txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1185
      Simplification returns the following subgoal: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1186
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1187
      @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"} 
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1188
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1189
      We are lacking a property about the function @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1190
      tree_list_size}, which was generated automatically at the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1191
      definition of the @{text tree} type. We should go back and prove
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1192
      it, by induction.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1193
      *}
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1194
    (*<*)oops(*>*)
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1195
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1196
  lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1197
    by (induct l) auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1198
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1199
  text {* 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1200
    Now the whole termination proof is automatic:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1201
    *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1202
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1203
  termination 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1204
    by lexicographic_order
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1205
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1206
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1207
subsection {* Congruence Rules *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1208
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1209
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1210
  Let's come back to the question how Isabelle knows about @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1211
  map}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1212
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1213
  The knowledge about map is encoded in so-called congruence rules,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1214
  which are special theorems known to the \cmd{function} command. The
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1215
  rule for map is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1216
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1217
  @{thm[display] map_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1218
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1219
  You can read this in the following way: Two applications of @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1220
  map} are equal, if the list arguments are equal and the functions
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1221
  coincide on the elements of the list. This means that for the value 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1222
  @{term "map f l"} we only have to know how @{term f} behaves on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1223
  @{term l}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1224
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1225
  Usually, one such congruence rule is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1226
  needed for each higher-order construct that is used when defining
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1227
  new functions. In fact, even basic functions like @{const
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1228
  If} and @{const Let} are handled by this mechanism. The congruence
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1229
  rule for @{const If} states that the @{text then} branch is only
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1230
  relevant if the condition is true, and the @{text else} branch only if it
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1231
  is false:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1232
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1233
  @{thm[display] if_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1234
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1235
  Congruence rules can be added to the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1236
  function package by giving them the @{term fundef_cong} attribute.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1237
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1238
  The constructs that are predefined in Isabelle, usually
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1239
  come with the respective congruence rules.
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1240
  But if you define your own higher-order functions, you will have to
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1241
  come up with the congruence rules yourself, if you want to use your
23805
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1242
  functions in recursive definitions. 
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1243
*}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1244
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1245
subsection {* Congruence Rules and Evaluation Order *}
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1246
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1247
text {* 
953eb3c5f793 updated
krauss
parents: 23188
diff changeset
  1248
  Higher order logic differs from functional programming languages in
953eb3c5f793 updated
krauss
parents: 23188