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