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