doc-src/IsarAdvanced/Functions/Thy/Functions.thy
author krauss
Thu, 17 May 2007 23:03:47 +0200
changeset 23003 4b0bf04a4d68
parent 22065 cdd077905eee
child 23188 595a0e24bd8e
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
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    12
section {* Function Definition for Dummies *}
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
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    17
  Like in functional programming, a function definition consists of a 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    18
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    19
*}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    20
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    21
fun fib :: "nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    22
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    23
  "fib 0 = 1"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    24
| "fib (Suc 0) = 1"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    25
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    26
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    27
text {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    28
  The syntax is rather self-explanatory: We introduce a function by
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    29
  giving its name, its type and a set of defining recursive
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    30
  equations. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    31
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    32
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    33
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    34
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    35
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    36
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    37
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    38
  The function always terminates, since its argument gets smaller in
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    39
  every recursive call. Termination is an important requirement, since
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    40
  it prevents inconsistencies: From the "definition" @{text "f(n) =
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    41
  f(n) + 1"} we could prove @{text "0 = 1"} by subtracting @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    42
  "f(n)"} on both sides.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    43
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    44
  Isabelle tries to prove termination automatically when a function is
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    45
  defined. We will later look at cases where this fails and see what to
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    46
  do then.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    47
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    48
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    49
subsection {* Pattern matching *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    50
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    51
text {* \label{patmatch}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    52
  Like in functional programming, we can use pattern matching to
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
    53
  define functions. At the moment we will only consider \emph{constructor
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    54
  patterns}, which only consist of datatype constructors and
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    55
  variables.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    56
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    57
  If patterns overlap, the order of the equations is taken into
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    58
  account. The following function inserts a fixed element between any
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    59
  two elements of a list:
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
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    62
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    63
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    64
  "sep a (x#y#xs) = x # a # sep a (y # xs)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    65
| "sep a xs       = xs"
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
text {* 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    68
  Overlapping patterns are interpreted as "increments" to what is
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    69
  already there: The second equation is only meant for the cases where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    70
  the first one does not match. Consequently, Isabelle replaces it
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    71
  internally by the remaining cases, making the patterns disjoint:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    72
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    73
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    74
thm sep.simps
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    75
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    76
text {* @{thm [display] sep.simps[no_vars]} *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    77
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    78
text {* 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    79
  The equations from function definitions are automatically used in
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    80
  simplification:
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    81
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    82
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    83
lemma "sep (0::nat) [1, 2, 3] = [1, 0, 2, 0, 3]"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    84
by simp
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    85
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    86
subsection {* Induction *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    87
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    88
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    89
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    90
  Isabelle provides customized induction rules for recursive functions.  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    91
  See \cite[\S3.5.4]{isa-tutorial}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    92
*}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    93
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    94
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
    95
section {* Full form definitions *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    96
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    97
text {* 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    98
  Up to now, we were using the \cmd{fun} command, which provides a
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
    99
  convenient shorthand notation for simple function definitions. In
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   100
  this mode, Isabelle tries to solve all the necessary proof obligations
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   101
  automatically. If a proof does not go through, the definition is
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   102
  rejected. This can either mean that the definition is indeed faulty,
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   103
  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
   104
  rather: not designed) to handle the definition.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   105
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   106
  By expanding the abbreviated \cmd{fun} to the full \cmd{function}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   107
  command, the proof obligations become visible and can be analyzed or
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   108
  solved manually.
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
\end{isamarkuptext}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   111
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   112
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   113
\fbox{\parbox{\textwidth}{
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   114
\noindent\cmd{fun} @{text "f :: \<tau>"}\\%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   115
\cmd{where}\isanewline%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   116
\ \ {\it equations}\isanewline%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   117
\ \ \quad\vdots
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   118
}}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   119
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   120
\begin{isamarkuptext}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   121
\vspace*{1em}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   122
\noindent abbreviates
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   123
\end{isamarkuptext}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   124
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   125
\fbox{\parbox{\textwidth}{
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   126
\noindent\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   127
\cmd{where}\isanewline%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   128
\ \ {\it equations}\isanewline%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   129
\ \ \quad\vdots\\%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   130
\cmd{by} @{text "pat_completeness auto"}\\%
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   131
\cmd{termination by} @{text "lexicographic_order"}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   132
}}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   133
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   134
\begin{isamarkuptext}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   135
  \vspace*{1em}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   136
  \noindent Some declarations and proofs have now become explicit:
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   137
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   138
  \begin{enumerate}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   139
  \item The \cmd{sequential} option enables the preprocessing of
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   140
  pattern overlaps we already saw. Without this option, the equations
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   141
  must already be disjoint and complete. The automatic completion only
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   142
  works with datatype patterns.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   143
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   144
  \item A function definition now produces a proof obligation which
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   145
  expresses completeness and compatibility of patterns (We talk about
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   146
  this later). The combination of the methods @{text "pat_completeness"} and
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   147
  @{text "auto"} is used to solve this proof obligation.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   148
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   149
  \item A termination proof follows the definition, started by the
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   150
  \cmd{termination} command, which sets up the goal. The @{text
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   151
  "lexicographic_order"} method can prove termination of a certain
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   152
  class of functions by searching for a suitable lexicographic
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   153
  combination of size measures.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   154
 \end{enumerate}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   155
  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
   156
  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
   157
  what is actually going on.
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   158
 *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   159
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   160
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   161
section {* Proving termination *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   162
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   163
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   164
  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
   165
  @{text "N"}, using a counter @{text "i"}:
21212
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
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   168
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   169
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   170
  "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
   171
by pat_completeness auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   172
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   173
text {*
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   174
  \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
   175
  arguments decreases in the recursive call.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   176
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   177
  A more general method for termination proofs is to supply a wellfounded
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
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   191
by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   192
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   193
text {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   194
  The \cmd{termination} command sets up the termination goal for the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   195
  specified function @{text "sum"}. If the function name is omitted it
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
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   204
  The predefined function @{term_type "measure"} is a very common way of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   205
  specifying termination relations in terms of a mapping into the
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   206
  natural numbers.
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
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   211
  relation. These goals are all solved by the subsequent call to
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   212
  @{text "auto"}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   213
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   214
  Let us complicate the function a little, by adding some more
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   215
  recursive calls: 
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   216
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   217
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   218
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   219
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   220
  "foo i N = (if i > N 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   221
              then (if N = 0 then 0 else foo 0 (N - 1))
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   222
              else i + foo (Suc i) N)"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   223
by pat_completeness auto
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
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   226
  When @{text "i"} has reached @{text "N"}, it starts at zero again
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   227
  and @{text "N"} is decremented.
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   228
  This corresponds to a nested
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   229
  loop where one index counts up and the other down. Termination can
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   230
  be proved using a lexicographic combination of two measures, namely
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   231
  the value of @{text "N"} and the above difference. The @{const
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   232
  "measures"} combinator generalizes @{text "measure"} by taking a
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   233
  list of measure functions.  
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   234
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   235
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   236
termination 
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   237
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
   238
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   239
subsection {* Manual Termination Proofs *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   240
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   241
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   242
  The @{text relation} method is often useful, but not
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   243
  necessary. Since termination proofs are just normal Isabelle proofs,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   244
  they can also be carried out manually: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   245
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   246
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   247
function id :: "nat \<Rightarrow> nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   248
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   249
  "id 0 = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   250
| "id (Suc n) = Suc (id n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   251
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   252
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   253
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   254
proof 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   255
  show "wf less_than" ..
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   256
next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   257
  fix n show "(n, Suc n) \<in> less_than" by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   258
qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   259
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   260
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   261
  Of course this is just a trivial example, but manual proofs can
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   262
  sometimes be the only choice if faced with very hard termination problems.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   263
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   264
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   265
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   266
section {* Mutual Recursion *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   267
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   268
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   269
  If two or more functions call one another mutually, they have to be defined
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   270
  in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   271
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   272
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   273
function even :: "nat \<Rightarrow> bool"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   274
    and odd  :: "nat \<Rightarrow> bool"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   275
where
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   276
  "even 0 = True"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   277
| "odd 0 = False"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   278
| "even (Suc n) = odd n"
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   279
| "odd (Suc n) = even n"
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   280
by pat_completeness auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   281
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   282
text {*
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   283
  To solve the problem of mutual dependencies, Isabelle internally
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   284
  creates a single function operating on the sum
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   285
  type. Then the original functions are defined as
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   286
  projections. Consequently, termination has to be proved
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   287
  simultaneously for both functions, by specifying a measure on the
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   288
  sum type: 
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   289
*}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   290
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   291
termination 
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   292
by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   293
   auto
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   294
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   295
subsection {* Induction for mutual recursion *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   296
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   297
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   298
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   299
  When functions are mutually recursive, proving properties about them
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   300
  generally requires simultaneous induction. The induction rules
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   301
  generated from the definitions reflect this.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   302
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   303
  Let us prove something about @{const even} and @{const odd}:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   304
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   305
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   306
lemma 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   307
  "even n = (n mod 2 = 0)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   308
  "odd n = (n mod 2 = 1)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   309
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   310
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   311
  We apply simultaneous induction, specifying the induction variable
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   312
  for both goals, separated by \cmd{and}:  *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   313
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   314
apply (induct n and n rule: even_odd.induct)
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   315
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   316
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   317
  We get four subgoals, which correspond to the clauses in the
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   318
  definition of @{const even} and @{const odd}:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   319
  @{subgoals[display,indent=0]}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   320
  Simplification solves the first two goals, leaving us with two
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   321
  statements about the @{text "mod"} operation to prove:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   322
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   323
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   324
apply simp_all
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   325
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   326
txt {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   327
  @{subgoals[display,indent=0]} 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   328
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   329
  \noindent These can be handeled by the descision procedure for
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   330
  presburger arithmethic.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   331
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   332
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   333
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   334
apply presburger
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   335
apply presburger
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   336
done
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   337
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   338
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   339
  Even if we were just interested in one of the statements proved by
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   340
  simultaneous induction, the other ones may be necessary to
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   341
  strengthen the induction hypothesis. If we had left out the statement
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   342
  about @{const odd} (by substituting it with @{term "True"}, our
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   343
  proof would have failed:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   344
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   345
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   346
lemma 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   347
  "even n = (n mod 2 = 0)"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   348
  "True"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   349
apply (induct n rule: even_odd.induct)
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   350
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   351
txt {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   352
  \noindent Now the third subgoal is a dead end, since we have no
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   353
  useful induction hypothesis:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   354
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   355
  @{subgoals[display,indent=0]} 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   356
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   357
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   358
oops
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
section {* More general patterns *}
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
subsection {* Avoiding pattern splitting *}
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
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   365
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   366
  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
   367
  patterns were always disjoint and complete, and if they weren't,
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   368
  they were made disjoint automatically like in the definition of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   369
  @{const "sep"} in \S\ref{patmatch}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   370
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   371
  This splitting can significantly increase the number of equations
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   372
  involved, and is not always necessary. The following simple example
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   373
  shows the problem:
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
  Suppose we are modelling incomplete knowledge about the world by a
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   376
  three-valued datatype, which has values @{term "T"}, @{term "F"}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   377
  and @{term "X"} for true, false and uncertain propositions, respectively. 
22065
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
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   380
datatype P3 = T | F | X
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   381
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   382
text {* Then the conjunction of such values can be defined as follows: *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   383
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   384
fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   385
where
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   386
  "And T p = p"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   387
| "And p T = p"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   388
| "And p F = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   389
| "And F p = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   390
| "And X X = X"
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   391
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   392
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   393
text {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   394
  This definition is useful, because the equations can directly be used
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   395
  as rules to simplify expressions. But the patterns overlap, e.g.~the
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   396
  expression @{term "And T T"} is matched by the first two
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   397
  equations. By default, Isabelle makes the patterns disjoint by
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   398
  splitting them up, producing instances:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   399
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   400
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   401
thm And.simps
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   402
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   403
text {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   404
  @{thm[indent=4] And.simps}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   405
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   406
  \vspace*{1em}
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   407
  \noindent There are several problems with this:
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   408
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   409
  \begin{enumerate}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   410
  \item When datatypes have many constructors, there can be an
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   411
  explosion of equations. For @{const "And"}, we get seven instead of
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   412
  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
   413
  example.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   414
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   415
  \item Since splitting makes the equations "less general", they
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   416
  do not always match in rewriting. While the term @{term "And x F"}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   417
  can be simplified to @{term "F"} by the original specification, a
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   418
  (manual) case split on @{term "x"} is now necessary.
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
  \item The splitting also concerns the induction rule @{text
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   421
  "And.induct"}. Instead of five premises it now has seven, which
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   422
  means that our induction proofs will have more cases.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   423
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   424
  \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
   425
  back which we put in.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   426
  \end{enumerate}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   427
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   428
  On the other hand, a definition needs to be consistent and defining
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   429
  both @{term "f x = True"} and @{term "f x = False"} is a bad
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   430
  idea. So if we don't want Isabelle to mangle our definitions, we
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   431
  will have to prove that this is not necessary. By using the full
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   432
  definition form without the \cmd{sequential} option, we get this
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   433
  behaviour: 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   434
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   435
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   436
function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   437
where
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   438
  "And2 T p = p"
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   439
| "And2 p T = p"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   440
| "And2 p F = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   441
| "And2 F p = F"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   442
| "And2 X X = X"
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
txt {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   445
  Now it is also time to look at the subgoals generated by a
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   446
  function definition. In this case, they are:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   447
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   448
  @{subgoals[display,indent=0]} 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   449
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   450
  The first subgoal expresses the completeness of the patterns. It has
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   451
  the form of an elimination rule and states that every @{term x} of
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   452
  the function's input type must match one of the patterns. It could
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   453
  be equivalently stated as a disjunction of existential statements: 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   454
@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   455
  (\<exists>p. x = (F, p)) \<or> (x = (X, X))"} If the patterns just involve
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   456
  datatypes, we can solve it with the @{text "pat_completeness"} method:
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   457
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   458
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   459
apply pat_completeness
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   460
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   461
txt {*
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   462
  The remaining subgoals express \emph{pattern compatibility}. We do
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   463
  allow that a value is matched by more than one patterns, but in this
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   464
  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
   465
  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
   466
  subgoal. Usually this needs injectivity of the constructors, which
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   467
  is used automatically by @{text "auto"}.
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   468
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   469
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   470
by auto
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   471
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   472
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   473
subsection {* Non-constructor patterns *}
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   474
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   475
text {* FIXME *}
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
   476
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   477
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   478
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   479
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   480
section {* Partiality *}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   481
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   482
text {* 
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   483
  In HOL, all functions are total. A function @{term "f"} applied to
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   484
  @{term "x"} always has a value @{term "f x"}, and there is no notion
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   485
  of undefinedness. 
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   486
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   487
  This property of HOL is the reason why we have to do termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   488
  proofs when defining functions: The termination proof justifies the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   489
  definition of the function by wellfounded recursion.
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   490
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   491
  However, the \cmd{function} package still supports partiality. Let's
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   492
  look at the following function which searches for a zero in the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   493
  function f. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   494
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   495
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   496
function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   497
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   498
  "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   499
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   500
(*<*)declare findzero.simps[simp del](*>*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   501
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   502
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   503
  Clearly, any attempt of a termination proof must fail. And without
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   504
  that, we do not get the usual rules @{text "findzero.simp"} and 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   505
  @{text "findzero.induct"}. So what was the definition good for at all?
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   506
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   507
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   508
subsection {* Domain predicates *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   509
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   510
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   511
  The trick is that Isabelle has not only defined the function @{const findzero}, but also
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   512
  a predicate @{term "findzero_dom"} that characterizes the values where the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   513
  terminates: the \emph{domain} of the function. In Isabelle/HOL, a
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   514
  partial function is just a total function with an additional domain
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   515
  predicate. Like with total functions, we get simplification and
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   516
  induction rules, but they are guarded by the domain conditions and
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   517
  called @{text psimps} and @{text pinduct}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   518
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   519
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   520
thm findzero.psimps
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   521
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   522
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   523
  @{thm[display] findzero.psimps}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   524
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   525
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   526
thm findzero.pinduct
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   527
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   528
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   529
  @{thm[display] findzero.pinduct}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   530
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   531
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   532
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   533
  As already mentioned, HOL does not support true partiality. All we
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   534
  are doing here is using some tricks to make a total function appear
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   535
  as if it was partial. We can still write the term @{term "findzero
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   536
  (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   537
  to some natural number, although we might not be able to find out
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   538
  which one (we will discuss this further in \S\ref{default}). The
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   539
  function is \emph{underdefined}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   540
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   541
  But it is enough defined to prove something about it. We can prove
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   542
  that if @{term "findzero f n"}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   543
  it terminates, it indeed returns a zero of @{term f}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   544
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   545
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   546
lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   547
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   548
txt {* We apply induction as usual, but using the partial induction
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   549
  rule: *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   550
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   551
apply (induct f n rule: findzero.pinduct)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   552
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   553
txt {* This gives the following subgoals:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   554
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   555
  @{subgoals[display,indent=0]}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   556
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   557
  The premise in our lemma was used to satisfy the first premise in
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   558
  the induction rule. However, now we can also use @{term
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   559
  "findzero_dom (f, n)"} as an assumption in the induction step. This
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   560
  allows to unfold @{term "findzero f n"} using the @{text psimps}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   561
  rule, and the rest is trivial. Since @{text psimps} rules carry the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   562
  @{text "[simp]"} attribute by default, we just need a single step:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   563
 *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   564
apply simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   565
done
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   566
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   567
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   568
  Proofs about partial functions are often not harder than for total
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   569
  functions. Fig.~\ref{findzero_isar} shows a slightly more
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   570
  complicated proof written in Isar. It is verbose enough to show how
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   571
  partiality comes into play: From the partial induction, we get an
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   572
  additional domain condition hypothesis. Observe how this condition
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   573
  is applied when calls to @{term findzero} are unfolded.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   574
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   575
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   576
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   577
\begin{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   578
\begin{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   579
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   580
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   581
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   582
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   583
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
   584
proof (induct rule: findzero.pinduct)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   585
  fix f n assume dom: "findzero_dom (f, n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   586
    and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n..<findzero f (Suc n)}\<rbrakk>
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   587
             \<Longrightarrow> f x \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   588
    and x_range: "x \<in> {n..<findzero f n}"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   589
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   590
  have "f n \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   591
  proof 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   592
    assume "f n = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   593
    with dom have "findzero f n = n" by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   594
    with x_range show False by auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   595
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   596
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   597
  from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   598
  thus "f x \<noteq> 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   599
  proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   600
    assume "x = n"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   601
    with `f n \<noteq> 0` show ?thesis by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   602
  next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   603
    assume "x \<in> {Suc n..<findzero f n}"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   604
    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   605
      by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   606
    with IH and `f n \<noteq> 0`
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   607
    show ?thesis by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   608
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   609
qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   610
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   611
\isamarkupfalse\isabellestyle{tt}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   612
\end{minipage}\end{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   613
\caption{A proof about a partial function}\label{findzero_isar}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   614
\end{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   615
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   616
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   617
subsection {* Partial termination proofs *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   618
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   619
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   620
  Now that we have proved some interesting properties about our
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   621
  function, we should turn to the domain predicate and see if it is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   622
  actually true for some values. Otherwise we would have just proved
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   623
  lemmas with @{term False} as a premise.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   624
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   625
  Essentially, we need some introduction rules for @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   626
  findzero_dom}. The function package can prove such domain
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   627
  introduction rules automatically. But since they are not used very
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   628
  often (they are almost never needed if the function is total), they
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   629
  are disabled by default for efficiency reasons. So we have to go
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   630
  back and ask for them explicitly by passing the @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   631
  "(domintros)"} option to the function package:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   632
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   633
\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   634
\cmd{where}\isanewline%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   635
\ \ \ldots\\
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   636
\cmd{by} @{text "pat_completeness auto"}\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   637
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   638
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   639
  Now the package has proved an introduction rule for @{text findzero_dom}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   640
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   641
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   642
thm findzero.domintros
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   643
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   644
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   645
  @{thm[display] findzero.domintros}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   646
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   647
  Domain introduction rules allow to show that a given value lies in the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   648
  domain of a function, if the arguments of all recursive calls
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   649
  are in the domain as well. They allow to do a \qt{single step} in a
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   650
  termination proof. Usually, you want to combine them with a suitable
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   651
  induction principle.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   652
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   653
  Since our function increases its argument at recursive calls, we
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   654
  need an induction principle which works \qt{backwards}. We will use
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   655
  @{text inc_induct}, which allows to do induction from a fixed number
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   656
  \qt{downwards}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   657
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   658
  @{thm[display] inc_induct}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   659
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   660
  Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   661
  that @{text findzero} terminates if there is a zero which is greater
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   662
  or equal to @{term n}. First we derive two useful rules which will
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   663
  solve the base case and the step case of the induction. The
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   664
  induction is then straightforward, except for the unusal induction
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   665
  principle.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   666
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   667
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   668
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   669
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   670
\begin{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   671
\begin{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   672
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   673
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   674
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   675
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   676
lemma findzero_termination:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   677
  assumes "x >= n" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   678
  assumes "f x = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   679
  shows "findzero_dom (f, n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   680
proof - 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   681
  have base: "findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   682
    by (rule findzero.domintros) (simp add:`f x = 0`)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   683
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   684
  have step: "\<And>i. findzero_dom (f, Suc i) 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   685
    \<Longrightarrow> findzero_dom (f, i)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   686
    by (rule findzero.domintros) simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   687
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   688
  from `x \<ge> n`
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   689
  show ?thesis
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   690
  proof (induct rule:inc_induct)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   691
    show "findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   692
      by (rule base)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   693
  next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   694
    fix i assume "findzero_dom (f, Suc i)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   695
    thus "findzero_dom (f, i)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   696
      by (rule step)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   697
  qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   698
qed      
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   699
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   700
\isamarkupfalse\isabellestyle{tt}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   701
\end{minipage}\end{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   702
\caption{Termination proof for @{text findzero}}\label{findzero_term}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   703
\end{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   704
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   705
      
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   706
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   707
  Again, the proof given in Fig.~\ref{findzero_term} has a lot of
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   708
  detail in order to explain the principles. Using more automation, we
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   709
  can also have a short proof:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   710
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   711
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   712
lemma findzero_termination_short:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   713
  assumes zero: "x >= n" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   714
  assumes [simp]: "f x = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   715
  shows "findzero_dom (f, n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   716
  using zero
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   717
  by (induct rule:inc_induct) (auto intro: findzero.domintros)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   718
    
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   719
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   720
  It is simple to combine the partial correctness result with the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   721
  termination lemma:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   722
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   723
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   724
lemma findzero_total_correctness:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   725
  "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   726
by (blast intro: findzero_zero findzero_termination)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   727
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   728
subsection {* Definition of the domain predicate *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   729
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   730
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   731
  Sometimes it is useful to know what the definition of the domain
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   732
  predicate actually is. Actually, @{text findzero_dom} is just an
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   733
  abbreviation:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   734
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   735
  @{abbrev[display] findzero_dom}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   736
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   737
  The domain predicate is the accessible part of a relation @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   738
  findzero_rel}, which was also created internally by the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   739
  package. @{const findzero_rel} is just a normal
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   740
  inductively defined predicate, so we can inspect its definition by
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   741
  looking at the introduction rules @{text findzero_rel.intros}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   742
  In our case there is just a single rule:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   743
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   744
  @{thm[display] findzero_rel.intros}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   745
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   746
  The relation @{const findzero_rel}, expressed as a binary predicate,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   747
  describes the \emph{recursion relation} of the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   748
  definition. The recursion relation is a binary relation on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   749
  the arguments of the function that relates each argument to its
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   750
  recursive calls. In general, there is one introduction rule for each
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   751
  recursive call.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   752
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   753
  The predicate @{term "acc findzero_rel"} is the \emph{accessible part} of
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   754
  that relation. An argument belongs to the accessible part, if it can
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   755
  be reached in a finite number of steps. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   756
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   757
  Since the domain predicate is just an abbreviation, you can use
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   758
  lemmas for @{const acc} and @{const findzero_rel} directly. Some
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   759
  lemmas which are occasionally useful are @{text accI}, @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   760
  acc_downward}, and of course the introduction and elimination rules
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   761
  for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   762
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   763
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   764
(*lemma findzero_nicer_domintros:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   765
  "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   766
  "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   767
by (rule accI, erule findzero_rel.cases, auto)+
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   768
*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   769
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   770
subsection {* A Useful Special Case: Tail recursion *}
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
  The domain predicate is our trick that allows us to model partiality
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   774
  in a world of total functions. The downside of this is that we have
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   775
  to carry it around all the time. The termination proof above allowed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   776
  us to replace the abstract @{term "findzero_dom (f, n)"} by the more
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   777
  concrete @{term "(x \<ge> n \<and> f x = 0)"}, but the condition is still
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   778
  there and it won't go away soon. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   779
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   780
  In particular, the domain predicate guard the unfolding of our
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   781
  function, since it is there as a condition in the @{text psimp}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   782
  rules. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   783
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   784
  On the other hand, we must be happy about the domain predicate,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   785
  since it guarantees that all this is at all possible without losing
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   786
  consistency. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   787
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   788
  Now there is an important special case: We can actually get rid
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   789
  of the condition in the simplification rules, \emph{if the function
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   790
  is tail-recursive}. The reason is that for all tail-recursive
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   791
  equations there is a total function satisfying them, even if they
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   792
  are non-terminating. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   793
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   794
  The function package internally does the right construction and can
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   795
  derive the unconditional simp rules, if we ask it to do so. Luckily,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   796
  our @{const "findzero"} function is tail-recursive, so we can just go
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   797
  back and add another option to the \cmd{function} command:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   798
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   799
\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   800
\cmd{where}\isanewline%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   801
\ \ \ldots\\%
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   802
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   803
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   804
  Now, we actually get the unconditional simplification rules, even
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   805
  though the function is partial:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   806
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   807
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   808
thm findzero.simps
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   809
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   810
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   811
  @{thm[display] findzero.simps}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   812
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   813
  Of course these would make the simplifier loop, so we better remove
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   814
  them from the simpset:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   815
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   816
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   817
declare findzero.simps[simp del]
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   818
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   819
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   820
text {* \fixme{Code generation ???} *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   821
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   822
section {* Nested recursion *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   823
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   824
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   825
  Recursive calls which are nested in one another frequently cause
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   826
  complications, since their termination proof can depend on a partial
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   827
  correctness property of the function itself. 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   828
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   829
  As a small example, we define the \qt{nested zero} function:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   830
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   831
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   832
function nz :: "nat \<Rightarrow> nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   833
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   834
  "nz 0 = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   835
| "nz (Suc n) = nz (nz n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   836
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   837
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   838
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   839
  If we attempt to prove termination using the identity measure on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   840
  naturals, this fails:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   841
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   842
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   843
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   844
  apply (relation "measure (\<lambda>n. n)")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   845
  apply auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   846
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   847
txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   848
  We get stuck with the subgoal
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   849
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   850
  @{subgoals[display]}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   851
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   852
  Of course this statement is true, since we know that @{const nz} is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   853
  the zero function. And in fact we have no problem proving this
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   854
  property by induction.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   855
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   856
oops
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   857
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   858
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   859
  by (induct rule:nz.pinduct) auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   860
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   861
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   862
  We formulate this as a partial correctness lemma with the condition
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   863
  @{term "nz_dom n"}. This allows us to prove it with the @{text
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   864
  pinduct} rule before we have proved termination. With this lemma,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   865
  the termination proof works as expected:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   866
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   867
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   868
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   869
  by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   870
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   871
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   872
  As a general strategy, one should prove the statements needed for
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   873
  termination as a partial property first. Then they can be used to do
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   874
  the termination proof. This also works for less trivial
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   875
  examples. Figure \ref{f91} defines the well-known 91-function by
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   876
  McCarthy \cite{?} and proves its termination.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   877
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   878
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   879
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   880
\begin{figure}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   881
\begin{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   882
\begin{minipage}{0.8\textwidth}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   883
\isabellestyle{it}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   884
\isastyle\isamarkuptrue
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   885
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   886
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   887
function f91 :: "nat => nat"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   888
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   889
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   890
by pat_completeness auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   891
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   892
lemma f91_estimate: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   893
  assumes trm: "f91_dom n" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   894
  shows "n < f91 n + 11"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   895
using trm by induct auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   896
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   897
termination
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   898
proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   899
  let ?R = "measure (\<lambda>x. 101 - x)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   900
  show "wf ?R" ..
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   901
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   902
  fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   903
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   904
  thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   905
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   906
  assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   907
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   908
  with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   909
qed
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   910
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   911
text_raw {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   912
\isamarkupfalse\isabellestyle{tt}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   913
\end{minipage}\end{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   914
\caption{McCarthy's 91-function}\label{f91}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   915
\end{figure}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   916
*}
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   917
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   918
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   919
section {* Higher-Order Recursion *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   920
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   921
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   922
  Higher-order recursion occurs when recursive calls
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   923
  are passed as arguments to higher-order combinators such as @{term
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   924
  map}, @{term filter} etc.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   925
  As an example, imagine a data type of n-ary trees:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   926
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   927
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   928
datatype 'a tree = 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   929
  Leaf 'a 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   930
| Branch "'a tree list"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   931
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   932
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   933
text {* \noindent We can define a map function for trees, using the predefined
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   934
  map function for lists. *}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   935
  
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   936
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   937
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   938
  "treemap f (Leaf n) = Leaf (f n)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   939
| "treemap f (Branch l) = Branch (map (treemap f) l)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   940
by pat_completeness auto
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   941
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   942
text {*
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   943
  We do the termination proof manually, to point out what happens
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   944
  here: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   945
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   946
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   947
termination proof
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   948
  txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   949
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   950
  As usual, we have to give a wellfounded relation, such that the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   951
  arguments of the recursive calls get smaller. But what exactly are
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   952
  the arguments of the recursive calls? Isabelle gives us the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   953
  subgoals
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   954
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   955
  @{subgoals[display,indent=0]} 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   956
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   957
  So Isabelle seems to know that @{const map} behaves nicely and only
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   958
  applies the recursive call @{term "treemap f"} to elements
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   959
  of @{term "l"}. Before we discuss where this knowledge comes from,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   960
  let us finish the termination proof:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   961
  *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   962
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   963
  show "wf (measure (size o snd))" by simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   964
next
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   965
  fix f l and x :: "'a tree"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   966
  assume "x \<in> set l"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   967
  thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   968
    apply simp
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   969
    txt {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   970
      Simplification returns the following subgoal: 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   971
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   972
      @{subgoals[display,indent=0]} 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   973
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   974
      We are lacking a property about the function @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   975
      tree_list_size}, which was generated automatically at the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   976
      definition of the @{text tree} type. We should go back and prove
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   977
      it, by induction.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   978
      *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   979
    oops
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   980
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   981
  lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   982
    by (induct l) auto
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   983
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   984
  text {* 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   985
    Now the whole termination proof is automatic:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   986
    *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   987
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   988
  termination 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   989
    by lexicographic_order
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   990
  
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
   991
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   992
subsection {* Congruence Rules *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   993
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   994
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   995
  Let's come back to the question how Isabelle knows about @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   996
  map}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   997
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   998
  The knowledge about map is encoded in so-called congruence rules,
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
   999
  which are special theorems known to the \cmd{function} command. The
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1000
  rule for map is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1001
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1002
  @{thm[display] map_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1004
  You can read this in the following way: Two applications of @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1005
  map} are equal, if the list arguments are equal and the functions
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1006
  coincide on the elements of the list. This means that for the value 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1007
  @{term "map f l"} we only have to know how @{term f} behaves on
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1008
  @{term l}.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1009
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1010
  Usually, one such congruence rule is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1011
  needed for each higher-order construct that is used when defining
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1012
  new functions. In fact, even basic functions like @{const
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1013
  If} and @{const Let} are handeled by this mechanism. The congruence
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1014
  rule for @{const If} states that the @{text then} branch is only
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1015
  relevant if the condition is true, and the @{text else} branch only if it
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1016
  is false:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1017
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1018
  @{thm[display] if_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1019
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1020
  Congruence rules can be added to the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1021
  function package by giving them the @{term fundef_cong} attribute.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1022
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1023
  Isabelle comes with predefined congruence rules for most of the
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1024
  definitions.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1025
  But if you define your own higher-order constructs, you will have to
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1026
  come up with the congruence rules yourself, if you want to use your
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1027
  functions in recursive definitions. Since the structure of
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1028
  congruence rules is a little unintuitive, here are some exercises:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1029
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1030
(*<*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1031
fun mapeven :: "(nat \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat list"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1032
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1033
  "mapeven f [] = []"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1034
| "mapeven f (x#xs) = (if x mod 2 = 0 then f x # mapeven f xs else x #
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1035
  mapeven f xs)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1036
(*>*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1037
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1038
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1039
  \begin{exercise}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1040
    Find a suitable congruence rule for the following function which
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1041
  maps only over the even numbers in a list:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1042
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1043
  @{thm[display] mapeven.simps}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1044
  \end{exercise}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1045
  
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1046
  \begin{exercise}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1047
  What happens if the congruence rule for @{const If} is
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1048
  disabled by declaring @{text "if_cong[fundef_cong del]"}?
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1049
  \end{exercise}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1050
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1051
  Note that in some cases there is no \qt{best} congruence rule.
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1052
  \fixme
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1053
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1054
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1055
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1056
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1057
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1058
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1059
23003
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1060
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1061
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1062
section {* Appendix: Predefined Congruence Rules *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1063
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1064
(*<*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1065
syntax (Rule output)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1066
  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1067
  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1068
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1069
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1070
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1071
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1072
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1073
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1074
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1075
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1076
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1077
definition 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1078
FixImp :: "prop \<Rightarrow> prop \<Rightarrow> prop" 
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1079
where
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1080
  "FixImp (PROP A) (PROP B) \<equiv> (PROP A \<Longrightarrow> PROP B)"
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1081
notation (output)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1082
  FixImp (infixr "\<Longrightarrow>" 1)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1083
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1084
setup {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1085
let
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1086
  val fix_imps = map_aterms (fn Const ("==>", T) => Const ("Functions.FixImp", T) | t => t)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1087
  fun transform t = Logic.list_implies (map fix_imps (Logic.strip_imp_prems t), Logic.strip_imp_concl t)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1088
in
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1089
  TermStyle.add_style "topl" (K transform)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1090
end
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1091
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1092
(*>*)
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1093
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1094
subsection {* Basic Control Structures *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1095
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1096
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1097
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1098
@{thm_style[mode=Rule] topl if_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1099
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1100
@{thm_style [mode=Rule] topl let_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1101
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1102
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1103
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1104
subsection {* Data Types *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1105
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1106
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1107
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1108
For each \cmd{datatype} definition, a congruence rule for the case
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1109
  combinator is registeres automatically. Here are the rules for
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1110
  @{text "nat"} and @{text "list"}:
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1111
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1112
\begin{center}@{thm_style[mode=Rule] topl nat.case_cong}\end{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1113
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1114
\begin{center}@{thm_style[mode=Rule] topl list.case_cong}\end{center}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1115
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1116
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1117
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1118
subsection {* List combinators *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1119
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1120
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1121
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1122
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1123
@{thm_style[mode=Rule] topl map_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1124
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1125
@{thm_style[mode=Rule] topl filter_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1126
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1127
@{thm_style[mode=Rule] topl foldr_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1128
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1129
@{thm_style[mode=Rule] topl foldl_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1130
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1131
Similar: takewhile, dropwhile
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1132
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1133
*}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1134
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1135
subsection {* Sets *}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1136
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1137
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1138
text {*
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1139
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1140
@{thm_style[mode=Rule] topl ball_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1141
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1142
@{thm_style[mode=Rule] topl bex_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1143
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1144
@{thm_style[mode=Rule] topl UN_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1145
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1146
@{thm_style[mode=Rule] topl INT_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1147
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1148
@{thm_style[mode=Rule] topl image_cong}
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1149
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1150
4b0bf04a4d68 updated
krauss
parents: 22065
diff changeset
  1151
*}
22065
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1152
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1153
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1154
cdd077905eee added sections on mutual induction and patterns
krauss
parents: 21346
diff changeset
  1155
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
21212
547224bf9348 Added a (stub of a) function tutorial
krauss
parents:
diff changeset
  1158
end