1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Thu Jul 12 11:43:17 2007 +0200
1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Thu Jul 12 12:20:39 2007 +0200
1.3 @@ -24,7 +24,7 @@
1.4 text {*
1.5 The syntax is rather self-explanatory: We introduce a function by
1.6 giving its name, its type and a set of defining recursive
1.7 - equations. Note that the function is not primitive recursive.
1.8 + equations.
1.9 *}
1.10
1.11 text {*
1.12 @@ -34,7 +34,6 @@
1.13 fundamental requirement to prevent inconsistencies\footnote{From the
1.14 \qt{definition} @{text "f(n) = f(n) + 1"} we could prove
1.15 @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.
1.16 -
1.17 Isabelle tries to prove termination automatically when a definition
1.18 is made. In \S\ref{termination}, we will look at cases where this
1.19 fails and see what to do then.
1.20 @@ -46,7 +45,9 @@
1.21 Like in functional programming, we can use pattern matching to
1.22 define functions. At the moment we will only consider \emph{constructor
1.23 patterns}, which only consist of datatype constructors and
1.24 - (linear occurrences of) variables.
1.25 + variables. Furthermore, patterns must be linear, i.e.\ all variables
1.26 + on the left hand side of an equation must be distinct. In
1.27 + \S\ref{genpats} we discuss more general pattern matching.
1.28
1.29 If patterns overlap, the order of the equations is taken into
1.30 account. The following function inserts a fixed element between any
1.31 @@ -70,7 +71,7 @@
1.32 text {* @{thm [display] sep.simps[no_vars]} *}
1.33
1.34 text {*
1.35 - The equations from function definitions are automatically used in
1.36 + \noindent The equations from function definitions are automatically used in
1.37 simplification:
1.38 *}
1.39
1.40 @@ -81,9 +82,30 @@
1.41
1.42 text {*
1.43
1.44 - Isabelle provides customized induction rules for recursive functions.
1.45 - See \cite[\S3.5.4]{isa-tutorial}. \fixme{Cases?}
1.46 + Isabelle provides customized induction rules for recursive
1.47 + functions. These rules follow the recursive structure of the
1.48 + definition. Here is the rule @{text sep.induct} arising from the
1.49 + above definition of @{const sep}:
1.50
1.51 + @{thm [display] sep.induct}
1.52 +
1.53 + We have a step case for list with at least two elements, and two
1.54 + base cases for the zero- and the one-element list. Here is a simple
1.55 + proof about @{const sep} and @{const map}
1.56 +*}
1.57 +
1.58 +lemma "map f (sep x ys) = sep (f x) (map f ys)"
1.59 +apply (induct x ys rule: sep.induct)
1.60 +
1.61 +txt {*
1.62 + We get three cases, like in the definition.
1.63 +
1.64 + @{subgoals [display]}
1.65 +*}
1.66 +
1.67 +apply auto
1.68 +done
1.69 +text {*
1.70
1.71 With the \cmd{fun} command, you can define about 80\% of the
1.72 functions that occur in practice. The rest of this tutorial explains
1.73 @@ -131,7 +153,7 @@
1.74
1.75 \begin{enumerate}
1.76 \item The \cmd{sequential} option enables the preprocessing of
1.77 - pattern overlaps we already saw. Without this option, the equations
1.78 + pattern overlaps which we already saw. Without this option, the equations
1.79 must already be disjoint and complete. The automatic completion only
1.80 works with constructor patterns.
1.81
1.82 @@ -152,10 +174,12 @@
1.83 section {* Termination *}
1.84
1.85 text {*\label{termination}
1.86 - The @{text "lexicographic_order"} method can prove termination of a
1.87 + The method @{text "lexicographic_order"} is the default method for
1.88 + termination proofs. It can prove termination of a
1.89 certain class of functions by searching for a suitable lexicographic
1.90 combination of size measures. Of course, not all functions have such
1.91 - a simple termination argument.
1.92 + a simple termination argument. For them, we can specify the termination
1.93 + relation manually.
1.94 *}
1.95
1.96 subsection {* The {\tt relation} method *}
1.97 @@ -171,23 +195,19 @@
1.98
1.99 text {*
1.100 \noindent The @{text "lexicographic_order"} method fails on this example, because none of the
1.101 - arguments decreases in the recursive call.
1.102 - % FIXME: simps and induct only appear after "termination"
1.103 -
1.104 - The easiest way of doing termination proofs is to supply a wellfounded
1.105 - relation on the argument type, and to show that the argument
1.106 - decreases in every recursive call.
1.107 + arguments decreases in the recursive call, with respect to the standard size ordering.
1.108 + To prove termination manually, we must provide a custom wellfounded relation.
1.109
1.110 The termination argument for @{text "sum"} is based on the fact that
1.111 the \emph{difference} between @{text "i"} and @{text "N"} gets
1.112 smaller in every step, and that the recursion stops when @{text "i"}
1.113 - is greater then @{text "n"}. Phrased differently, the expression
1.114 - @{text "N + 1 - i"} decreases in every recursive call.
1.115 + is greater than @{text "N"}. Phrased differently, the expression
1.116 + @{text "N + 1 - i"} always decreases.
1.117
1.118 We can use this expression as a measure function suitable to prove termination.
1.119 *}
1.120
1.121 -termination sum
1.122 +termination
1.123 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
1.124
1.125 txt {*
1.126 @@ -267,19 +287,22 @@
1.127 \noindent Isabelle responds with the following error:
1.128
1.129 \begin{isabelle}
1.130 -*** Could not find lexicographic termination order:\newline
1.131 -*** \ \ \ \ 1\ \ 2 \newline
1.132 -*** a: N <= \newline
1.133 +*** Unfinished subgoals:\newline
1.134 +*** (a, 1, <):\newline
1.135 +*** \ 1.~@{text "\<And>x. x = 0"}\newline
1.136 +*** (a, 1, <=):\newline
1.137 +*** \ 1.~False\newline
1.138 +*** (a, 2, <):\newline
1.139 +*** \ 1.~False\newline
1.140 *** Calls:\newline
1.141 *** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline
1.142 *** Measures:\newline
1.143 *** 1) @{text "\<lambda>x. size (fst x)"}\newline
1.144 *** 2) @{text "\<lambda>x. size (snd x)"}\newline
1.145 -*** Unfinished subgoals:\newline
1.146 -*** @{text "\<And>a x xs."}\newline
1.147 -*** \quad @{text "(x. size (fst x)) (x + a, x # xs)"}\newline
1.148 -*** \quad @{text "\<le> (\<lambda>x. size (fst x)) (a, x # xs)"}\newline
1.149 -*** @{text "1. \<And>x. x = 0"}\newline
1.150 +*** Result matrix:\newline
1.151 +*** \ \ \ \ 1\ \ 2 \newline
1.152 +*** a: ? <= \newline
1.153 +*** Could not find lexicographic termination order.\newline
1.154 *** At command "fun".\newline
1.155 \end{isabelle}
1.156 *}
1.157 @@ -288,7 +311,7 @@
1.158 text {*
1.159
1.160
1.161 - The the key to this error message is the matrix at the top. The rows
1.162 + The the key to this error message is the matrix at the bottom. The rows
1.163 of that matrix correspond to the different recursive calls (In our
1.164 case, there is just one). The columns are the function's arguments
1.165 (expressed through different measure functions, which map the
1.166 @@ -297,11 +320,11 @@
1.167 The contents of the matrix summarize what is known about argument
1.168 descents: The second argument has a weak descent (@{text "<="}) at the
1.169 recursive call, and for the first argument nothing could be proved,
1.170 - which is expressed by @{text N}. In general, there are the values
1.171 - @{text "<"}, @{text "<="} and @{text "N"}.
1.172 + which is expressed by @{text "?"}. In general, there are the values
1.173 + @{text "<"}, @{text "<="} and @{text "?"}.
1.174
1.175 For the failed proof attempts, the unfinished subgoals are also
1.176 - printed. Looking at these will often point us to a missing lemma.
1.177 + printed. Looking at these will often point to a missing lemma.
1.178
1.179 % As a more real example, here is quicksort:
1.180 *}
1.181 @@ -391,13 +414,12 @@
1.182 txt {*
1.183 @{subgoals[display,indent=0]}
1.184
1.185 - \noindent These can be handeled by the descision procedure for
1.186 - arithmethic.
1.187 + \noindent These can be handled by Isabelle's arithmetic decision procedures.
1.188
1.189 *}
1.190
1.191 -apply presburger -- {* \fixme{arith} *}
1.192 -apply presburger
1.193 +apply arith
1.194 +apply arith
1.195 done
1.196
1.197 text {*
1.198 @@ -423,6 +445,7 @@
1.199 oops
1.200
1.201 section {* General pattern matching *}
1.202 +text{*\label{genpats} *}
1.203
1.204 subsection {* Avoiding automatic pattern splitting *}
1.205
1.206 @@ -437,7 +460,7 @@
1.207 equations involved, and this is not always desirable. The following
1.208 example shows the problem:
1.209
1.210 - Suppose we are modelling incomplete knowledge about the world by a
1.211 + Suppose we are modeling incomplete knowledge about the world by a
1.212 three-valued datatype, which has values @{term "T"}, @{term "F"}
1.213 and @{term "X"} for true, false and uncertain propositions, respectively.
1.214 *}
1.215 @@ -457,7 +480,7 @@
1.216
1.217 text {*
1.218 This definition is useful, because the equations can directly be used
1.219 - as simplifcation rules rules. But the patterns overlap: For example,
1.220 + as simplification rules rules. But the patterns overlap: For example,
1.221 the expression @{term "And T T"} is matched by both the first and
1.222 the second equation. By default, Isabelle makes the patterns disjoint by
1.223 splitting them up, producing instances:
1.224 @@ -538,33 +561,12 @@
1.225 subsection {* Non-constructor patterns *}
1.226
1.227 text {*
1.228 - Most of Isabelle's basic types take the form of inductive data types
1.229 - with constructors. However, this is not true for all of them. The
1.230 - integers, for instance, are defined using the usual algebraic
1.231 - quotient construction, thus they are not an \qt{official} datatype.
1.232 + Most of Isabelle's basic types take the form of inductive datatypes,
1.233 + and usually pattern matching works on the constructors of such types.
1.234 + However, this need not be always the case, and the \cmd{function}
1.235 + command handles other kind of patterns, too.
1.236
1.237 - Of course, we might want to do pattern matching there, too. So
1.238 -
1.239 -
1.240 -
1.241 -*}
1.242 -
1.243 -function Abs :: "int \<Rightarrow> nat"
1.244 -where
1.245 - "Abs (int n) = n"
1.246 -| "Abs (- int (Suc n)) = n"
1.247 -by (erule int_cases) auto
1.248 -termination by (relation "{}") simp
1.249 -
1.250 -text {*
1.251 - This kind of matching is again justified by the proof of pattern
1.252 - completeness and compatibility. Here, the existing lemma @{text
1.253 - int_cases} is used:
1.254 -
1.255 - \begin{center}@{thm int_cases}\hfill(@{text "int_cases"})\end{center}
1.256 -*}
1.257 -text {*
1.258 - One well-known instance of non-constructor patterns are the
1.259 + One well-known instance of non-constructor patterns are
1.260 so-called \emph{$n+k$-patterns}, which are a little controversial in
1.261 the functional programming world. Here is the initial fibonacci
1.262 example with $n+k$-patterns:
1.263 @@ -578,6 +580,8 @@
1.264
1.265 (*<*)ML "goals_limit := 1"(*>*)
1.266 txt {*
1.267 + This kind of matching is again justified by the proof of pattern
1.268 + completeness and compatibility.
1.269 The proof obligation for pattern completeness states that every natural number is
1.270 either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
1.271 (2::nat)"}:
1.272 @@ -586,13 +590,14 @@
1.273
1.274 This is an arithmetic triviality, but unfortunately the
1.275 @{text arith} method cannot handle this specific form of an
1.276 - elimination rule. We have to do a case split on @{text P} first,
1.277 - which can be conveniently done using the @{text
1.278 - classical} rule. Pattern compatibility and termination are automatic as usual.
1.279 + elimination rule. However, we can use the method @{text
1.280 + "elim_to_cases"} to do an ad-hoc conversion to a disjunction of
1.281 + existentials, which can then be soved by the arithmetic decision procedure.
1.282 + Pattern compatibility and termination are automatic as usual.
1.283 *}
1.284 (*<*)ML "goals_limit := 10"(*>*)
1.285 -
1.286 -apply (rule classical, simp, arith)
1.287 +apply elim_to_cases
1.288 +apply arith
1.289 apply auto
1.290 done
1.291 termination by lexicographic_order
1.292 @@ -607,7 +612,8 @@
1.293 where
1.294 "ev (2 * n) = True"
1.295 | "ev (2 * n + 1) = False"
1.296 -by (rule classical, simp) arith+
1.297 +apply elim_to_cases
1.298 +by arith+
1.299 termination by (relation "{}") simp
1.300
1.301 text {*
1.302 @@ -639,7 +645,7 @@
1.303 | "gcd 0 y = y"
1.304 | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
1.305 | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
1.306 -by (rule classical, auto, arith)
1.307 +by (elim_to_cases, auto, arith)
1.308 termination by lexicographic_order
1.309
1.310 text {*
1.311 @@ -654,7 +660,7 @@
1.312 subsection {* Pattern matching on strings *}
1.313
1.314 text {*
1.315 - As strings (as lists of characters) are normal data types, pattern
1.316 + As strings (as lists of characters) are normal datatypes, pattern
1.317 matching on them is possible, but somewhat problematic. Consider the
1.318 following definition:
1.319
1.320 @@ -665,9 +671,9 @@
1.321 @{text "| \"check s = False\""}
1.322 \begin{isamarkuptext}
1.323
1.324 - An invocation of the above \cmd{fun} command does not
1.325 + \noindent An invocation of the above \cmd{fun} command does not
1.326 terminate. What is the problem? Strings are lists of characters, and
1.327 - characters are a data type with a lot of constructors. Splitting the
1.328 + characters are a datatype with a lot of constructors. Splitting the
1.329 catch-all pattern thus leads to an explosion of cases, which cannot
1.330 be handled by Isabelle.
1.331
1.332 @@ -688,7 +694,6 @@
1.333 In HOL, all functions are total. A function @{term "f"} applied to
1.334 @{term "x"} always has the value @{term "f x"}, and there is no notion
1.335 of undefinedness.
1.336 -
1.337 This is why we have to do termination
1.338 proofs when defining functions: The proof justifies that the
1.339 function can be defined by wellfounded recursion.
1.340 @@ -705,7 +710,7 @@
1.341 (*<*)declare findzero.simps[simp del](*>*)
1.342
1.343 text {*
1.344 - Clearly, any attempt of a termination proof must fail. And without
1.345 + \noindent Clearly, any attempt of a termination proof must fail. And without
1.346 that, we do not get the usual rules @{text "findzero.simp"} and
1.347 @{text "findzero.induct"}. So what was the definition good for at all?
1.348 *}
1.349 @@ -723,16 +728,13 @@
1.350 pinduct}:
1.351 *}
1.352
1.353 -thm findzero.psimps
1.354 +text {*
1.355 + \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
1.356 + \hfill(@{text "findzero.psimps"})
1.357 + \vspace{1em}
1.358
1.359 -text {*
1.360 - @{thm[display] findzero.psimps}
1.361 -*}
1.362 -
1.363 -thm findzero.pinduct
1.364 -
1.365 -text {*
1.366 - @{thm[display] findzero.pinduct}
1.367 + \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
1.368 + \hfill(@{text "findzero.pinduct"})
1.369 *}
1.370
1.371 text {*
1.372 @@ -743,23 +745,23 @@
1.373 to some natural number, although we might not be able to find out
1.374 which one. The function is \emph{underdefined}.
1.375
1.376 - But it is enough defined to prove something interesting about it. We
1.377 + But it is defined enough to prove something interesting about it. We
1.378 can prove that if @{term "findzero f n"}
1.379 - it terminates, it indeed returns a zero of @{term f}:
1.380 + terminates, it indeed returns a zero of @{term f}:
1.381 *}
1.382
1.383 lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
1.384
1.385 -txt {* We apply induction as usual, but using the partial induction
1.386 +txt {* \noindent We apply induction as usual, but using the partial induction
1.387 rule: *}
1.388
1.389 apply (induct f n rule: findzero.pinduct)
1.390
1.391 -txt {* This gives the following subgoals:
1.392 +txt {* \noindent This gives the following subgoals:
1.393
1.394 @{subgoals[display,indent=0]}
1.395
1.396 - The hypothesis in our lemma was used to satisfy the first premise in
1.397 + \noindent The hypothesis in our lemma was used to satisfy the first premise in
1.398 the induction rule. However, we also get @{term
1.399 "findzero_dom (f, n)"} as a local assumption in the induction step. This
1.400 allows to unfold @{term "findzero f n"} using the @{text psimps}
1.401 @@ -804,8 +806,7 @@
1.402 with `f n \<noteq> 0` show ?thesis by simp
1.403 next
1.404 assume "x \<in> {Suc n ..< findzero f n}"
1.405 - with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}"
1.406 - by simp
1.407 + with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
1.408 with IH and `f n \<noteq> 0`
1.409 show ?thesis by simp
1.410 qed
1.411 @@ -863,7 +864,7 @@
1.412 that @{text findzero} terminates if there is a zero which is greater
1.413 or equal to @{term n}. First we derive two useful rules which will
1.414 solve the base case and the step case of the induction. The
1.415 - induction is then straightforward, except for the unusal induction
1.416 + induction is then straightforward, except for the unusual induction
1.417 principle.
1.418
1.419 *}
1.420 @@ -911,8 +912,8 @@
1.421 assumes zero: "x >= n"
1.422 assumes [simp]: "f x = 0"
1.423 shows "findzero_dom (f, n)"
1.424 - using zero
1.425 - by (induct rule:inc_induct) (auto intro: findzero.domintros)
1.426 +using zero
1.427 +by (induct rule:inc_induct) (auto intro: findzero.domintros)
1.428
1.429 text {*
1.430 \noindent It is simple to combine the partial correctness result with the
1.431 @@ -927,7 +928,7 @@
1.432
1.433 text {*
1.434 Sometimes it is useful to know what the definition of the domain
1.435 - predicate actually is. Actually, @{text findzero_dom} is just an
1.436 + predicate looks like. Actually, @{text findzero_dom} is just an
1.437 abbreviation:
1.438
1.439 @{abbrev[display] findzero_dom}
1.440 @@ -948,22 +949,22 @@
1.441 recursive calls. In general, there is one introduction rule for each
1.442 recursive call.
1.443
1.444 - The predicate @{term "acc findzero_rel"} is the accessible part of
1.445 + The predicate @{term "accp findzero_rel"} is the accessible part of
1.446 that relation. An argument belongs to the accessible part, if it can
1.447 be reached in a finite number of steps (cf.~its definition in @{text
1.448 "Accessible_Part.thy"}).
1.449
1.450 Since the domain predicate is just an abbreviation, you can use
1.451 - lemmas for @{const acc} and @{const findzero_rel} directly. Some
1.452 - lemmas which are occasionally useful are @{text accI}, @{text
1.453 - acc_downward}, and of course the introduction and elimination rules
1.454 + lemmas for @{const accp} and @{const findzero_rel} directly. Some
1.455 + lemmas which are occasionally useful are @{text accpI}, @{text
1.456 + accp_downward}, and of course the introduction and elimination rules
1.457 for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
1.458 *}
1.459
1.460 (*lemma findzero_nicer_domintros:
1.461 "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
1.462 "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
1.463 -by (rule accI, erule findzero_rel.cases, auto)+
1.464 +by (rule accpI, erule findzero_rel.cases, auto)+
1.465 *)
1.466
1.467 subsection {* A Useful Special Case: Tail recursion *}
1.468 @@ -1067,8 +1068,7 @@
1.469 the zero function. And in fact we have no problem proving this
1.470 property by induction.
1.471 *}
1.472 -oops
1.473 -
1.474 +(*<*)oops(*>*)
1.475 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
1.476 by (induct rule:nz.pinduct) auto
1.477
1.478 @@ -1119,7 +1119,7 @@
1.479
1.480 assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
1.481 with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
1.482 - with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
1.483 + with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
1.484 qed
1.485
1.486 text_raw {*
1.487 @@ -1137,7 +1137,7 @@
1.488 Higher-order recursion occurs when recursive calls
1.489 are passed as arguments to higher-order combinators such as @{term
1.490 map}, @{term filter} etc.
1.491 - As an example, imagine a data type of n-ary trees:
1.492 + As an example, imagine a datatype of n-ary trees:
1.493 *}
1.494
1.495 datatype 'a tree =
1.496 @@ -1184,14 +1184,14 @@
1.497 txt {*
1.498 Simplification returns the following subgoal:
1.499
1.500 - @{subgoals[display,indent=0]}
1.501 + @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"}
1.502
1.503 We are lacking a property about the function @{const
1.504 tree_list_size}, which was generated automatically at the
1.505 definition of the @{text tree} type. We should go back and prove
1.506 it, by induction.
1.507 *}
1.508 - oops
1.509 + (*<*)oops(*>*)
1.510
1.511 lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
1.512 by (induct l) auto
1.513 @@ -1225,7 +1225,7 @@
1.514 Usually, one such congruence rule is
1.515 needed for each higher-order construct that is used when defining
1.516 new functions. In fact, even basic functions like @{const
1.517 - If} and @{const Let} are handeled by this mechanism. The congruence
1.518 + If} and @{const Let} are handled by this mechanism. The congruence
1.519 rule for @{const If} states that the @{text then} branch is only
1.520 relevant if the condition is true, and the @{text else} branch only if it
1.521 is false:
1.522 @@ -1235,20 +1235,82 @@
1.523 Congruence rules can be added to the
1.524 function package by giving them the @{term fundef_cong} attribute.
1.525
1.526 - Isabelle comes with predefined congruence rules for most of the
1.527 - definitions.
1.528 - But if you define your own higher-order constructs, you will have to
1.529 + The constructs that are predefined in Isabelle, usually
1.530 + come with the respective congruence rules.
1.531 + But if you define your own higher-order functions, you will have to
1.532 come up with the congruence rules yourself, if you want to use your
1.533 - functions in recursive definitions. Since the structure of
1.534 + functions in recursive definitions.
1.535 +*}
1.536 +
1.537 +subsection {* Congruence Rules and Evaluation Order *}
1.538 +
1.539 +text {*
1.540 + Higher order logic differs from functional programming languages in
1.541 + that it has no built-in notion of evaluation order. A program is
1.542 + just a set of equations, and it is not specified how they must be
1.543 + evaluated.
1.544 +
1.545 + However for the purpose of function definition, we must talk about
1.546 + evaluation order implicitly, when we reason about termination.
1.547 + Congruence rules express that a certain evaluation order is
1.548 + consistent with the logical definition.
1.549 +
1.550 + Consider the following function.
1.551 +*}
1.552 +
1.553 +function f :: "nat \<Rightarrow> bool"
1.554 +where
1.555 + "f n = (n = 0 \<or> f (n - 1))"
1.556 +(*<*)by pat_completeness auto(*>*)
1.557 +
1.558 +text {*
1.559 + As given above, the definition fails. The default configuration
1.560 + specifies no congruence rule for disjunction. We have to add a
1.561 + congruence rule that specifies left-to-right evaluation order:
1.562 +
1.563 + \vspace{1ex}
1.564 + \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})
1.565 + \vspace{1ex}
1.566 +
1.567 + Now the definition works without problems. Note how the termination
1.568 + proof depends on the extra condition that we get from the congruence
1.569 + rule.
1.570 +
1.571 + However, as evaluation is not a hard-wired concept, we
1.572 + could just turn everything around by declaring a different
1.573 + congruence rule. Then we can make the reverse definition:
1.574 +*}
1.575 +
1.576 +lemma disj_cong2[fundef_cong]:
1.577 + "(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
1.578 + by blast
1.579 +
1.580 +fun f' :: "nat \<Rightarrow> bool"
1.581 +where
1.582 + "f' n = (f' (n - 1) \<or> n = 0)"
1.583 +
1.584 +text {*
1.585 + \noindent These examples show that, in general, there is no \qt{best} set of
1.586 + congruence rules.
1.587 +
1.588 + However, such tweaking should rarely be necessary in
1.589 + practice, as most of the time, the default set of congruence rules
1.590 + works well.
1.591 +*}
1.592 +
1.593 +(*
1.594 +text {*
1.595 +Since the structure of
1.596 congruence rules is a little unintuitive, here are some exercises:
1.597 *}
1.598 -(*<*)
1.599 +
1.600 fun mapeven :: "(nat \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat list"
1.601 where
1.602 "mapeven f [] = []"
1.603 | "mapeven f (x#xs) = (if x mod 2 = 0 then f x # mapeven f xs else x #
1.604 mapeven f xs)"
1.605 -(*>*)
1.606 +
1.607 +
1.608 text {*
1.609
1.610 \begin{exercise}
1.611 @@ -1267,5 +1329,5 @@
1.612 \fixme{}
1.613
1.614 *}
1.615 -
1.616 +*)
1.617 end
2.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Jul 12 11:43:17 2007 +0200
2.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Jul 12 12:20:39 2007 +0200
2.3 @@ -37,7 +37,7 @@
2.4 \begin{isamarkuptext}%
2.5 The syntax is rather self-explanatory: We introduce a function by
2.6 giving its name, its type and a set of defining recursive
2.7 - equations. Note that the function is not primitive recursive.%
2.8 + equations.%
2.9 \end{isamarkuptext}%
2.10 \isamarkuptrue%
2.11 %
2.12 @@ -48,7 +48,6 @@
2.13 fundamental requirement to prevent inconsistencies\footnote{From the
2.14 \qt{definition} \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove
2.15 \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.}.
2.16 -
2.17 Isabelle tries to prove termination automatically when a definition
2.18 is made. In \S\ref{termination}, we will look at cases where this
2.19 fails and see what to do then.%
2.20 @@ -64,7 +63,9 @@
2.21 Like in functional programming, we can use pattern matching to
2.22 define functions. At the moment we will only consider \emph{constructor
2.23 patterns}, which only consist of datatype constructors and
2.24 - (linear occurrences of) variables.
2.25 + variables. Furthermore, patterns must be linear, i.e.\ all variables
2.26 + on the left hand side of an equation must be distinct. In
2.27 + \S\ref{genpats} we discuss more general pattern matching.
2.28
2.29 If patterns overlap, the order of the equations is taken into
2.30 account. The following function inserts a fixed element between any
2.31 @@ -95,7 +96,7 @@
2.32 \isamarkuptrue%
2.33 %
2.34 \begin{isamarkuptext}%
2.35 -The equations from function definitions are automatically used in
2.36 +\noindent The equations from function definitions are automatically used in
2.37 simplification:%
2.38 \end{isamarkuptext}%
2.39 \isamarkuptrue%
2.40 @@ -121,11 +122,56 @@
2.41 \isamarkuptrue%
2.42 %
2.43 \begin{isamarkuptext}%
2.44 -Isabelle provides customized induction rules for recursive functions.
2.45 - See \cite[\S3.5.4]{isa-tutorial}. \fixme{Cases?}
2.46 +Isabelle provides customized induction rules for recursive
2.47 + functions. These rules follow the recursive structure of the
2.48 + definition. Here is the rule \isa{sep{\isachardot}induct} arising from the
2.49 + above definition of \isa{sep}:
2.50
2.51 + \begin{isabelle}%
2.52 +{\isasymlbrakk}{\isasymAnd}a\ x\ y\ xs{\isachardot}\ {\isacharquery}P\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}a{\isachardot}\ {\isacharquery}P\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}a\ v{\isachardot}\ {\isacharquery}P\ a\ {\isacharbrackleft}v{\isacharbrackright}{\isasymrbrakk}\isanewline
2.53 +{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%
2.54 +\end{isabelle}
2.55 +
2.56 + We have a step case for list with at least two elements, and two
2.57 + base cases for the zero- and the one-element list. Here is a simple
2.58 + proof about \isa{sep} and \isa{map}%
2.59 +\end{isamarkuptext}%
2.60 +\isamarkuptrue%
2.61 +\isacommand{lemma}\isamarkupfalse%
2.62 +\ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep\ x\ ys{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}map\ f\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.63 +%
2.64 +\isadelimproof
2.65 +%
2.66 +\endisadelimproof
2.67 +%
2.68 +\isatagproof
2.69 +\isacommand{apply}\isamarkupfalse%
2.70 +\ {\isacharparenleft}induct\ x\ ys\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
2.71 +\begin{isamarkuptxt}%
2.72 +We get three cases, like in the definition.
2.73
2.74 - With the \cmd{fun} command, you can define about 80\% of the
2.75 + \begin{isabelle}%
2.76 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ x\ y\ xs{\isachardot}\isanewline
2.77 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
2.78 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\isanewline
2.79 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
2.80 +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ v{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}v{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}v{\isacharbrackright}{\isacharparenright}%
2.81 +\end{isabelle}%
2.82 +\end{isamarkuptxt}%
2.83 +\isamarkuptrue%
2.84 +\isacommand{apply}\isamarkupfalse%
2.85 +\ auto\ \isanewline
2.86 +\isacommand{done}\isamarkupfalse%
2.87 +%
2.88 +\endisatagproof
2.89 +{\isafoldproof}%
2.90 +%
2.91 +\isadelimproof
2.92 +%
2.93 +\endisadelimproof
2.94 +%
2.95 +\begin{isamarkuptext}%
2.96 +With the \cmd{fun} command, you can define about 80\% of the
2.97 functions that occur in practice. The rest of this tutorial explains
2.98 the remaining 20\%.%
2.99 \end{isamarkuptext}%
2.100 @@ -173,7 +219,7 @@
2.101
2.102 \begin{enumerate}
2.103 \item The \cmd{sequential} option enables the preprocessing of
2.104 - pattern overlaps we already saw. Without this option, the equations
2.105 + pattern overlaps which we already saw. Without this option, the equations
2.106 must already be disjoint and complete. The automatic completion only
2.107 works with constructor patterns.
2.108
2.109 @@ -197,10 +243,12 @@
2.110 %
2.111 \begin{isamarkuptext}%
2.112 \label{termination}
2.113 - The \isa{lexicographic{\isacharunderscore}order} method can prove termination of a
2.114 + The method \isa{lexicographic{\isacharunderscore}order} is the default method for
2.115 + termination proofs. It can prove termination of a
2.116 certain class of functions by searching for a suitable lexicographic
2.117 combination of size measures. Of course, not all functions have such
2.118 - a simple termination argument.%
2.119 + a simple termination argument. For them, we can specify the termination
2.120 + relation manually.%
2.121 \end{isamarkuptext}%
2.122 \isamarkuptrue%
2.123 %
2.124 @@ -234,24 +282,20 @@
2.125 %
2.126 \begin{isamarkuptext}%
2.127 \noindent The \isa{lexicographic{\isacharunderscore}order} method fails on this example, because none of the
2.128 - arguments decreases in the recursive call.
2.129 - % FIXME: simps and induct only appear after "termination"
2.130 -
2.131 - The easiest way of doing termination proofs is to supply a wellfounded
2.132 - relation on the argument type, and to show that the argument
2.133 - decreases in every recursive call.
2.134 + arguments decreases in the recursive call, with respect to the standard size ordering.
2.135 + To prove termination manually, we must provide a custom wellfounded relation.
2.136
2.137 The termination argument for \isa{sum} is based on the fact that
2.138 the \emph{difference} between \isa{i} and \isa{N} gets
2.139 smaller in every step, and that the recursion stops when \isa{i}
2.140 - is greater then \isa{n}. Phrased differently, the expression
2.141 - \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} decreases in every recursive call.
2.142 + is greater than \isa{N}. Phrased differently, the expression
2.143 + \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} always decreases.
2.144
2.145 We can use this expression as a measure function suitable to prove termination.%
2.146 \end{isamarkuptext}%
2.147 \isamarkuptrue%
2.148 \isacommand{termination}\isamarkupfalse%
2.149 -\ sum\isanewline
2.150 +\isanewline
2.151 %
2.152 \isadelimproof
2.153 %
2.154 @@ -371,26 +415,29 @@
2.155 \noindent Isabelle responds with the following error:
2.156
2.157 \begin{isabelle}
2.158 -*** Could not find lexicographic termination order:\newline
2.159 -*** \ \ \ \ 1\ \ 2 \newline
2.160 -*** a: N <= \newline
2.161 +*** Unfinished subgoals:\newline
2.162 +*** (a, 1, <):\newline
2.163 +*** \ 1.~\isa{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isadigit{0}}}\newline
2.164 +*** (a, 1, <=):\newline
2.165 +*** \ 1.~False\newline
2.166 +*** (a, 2, <):\newline
2.167 +*** \ 1.~False\newline
2.168 *** Calls:\newline
2.169 *** a) \isa{{\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}{\isachargreater}\ {\isacharparenleft}x\ {\isacharplus}\ a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}}\newline
2.170 *** Measures:\newline
2.171 *** 1) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}fst\ x{\isacharparenright}}\newline
2.172 *** 2) \isa{{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}snd\ x{\isacharparenright}}\newline
2.173 -*** Unfinished subgoals:\newline
2.174 -*** \isa{{\isasymAnd}a\ x\ xs{\isachardot}}\newline
2.175 -*** \quad \isa{{\isacharparenleft}x{\isachardot}\ size\ {\isacharparenleft}fst\ x{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x\ {\isacharplus}\ a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}}\newline
2.176 -*** \quad \isa{{\isasymle}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ size\ {\isacharparenleft}fst\ x{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ xs{\isacharparenright}}\newline
2.177 -*** \isa{{\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isadigit{0}}}\newline
2.178 +*** Result matrix:\newline
2.179 +*** \ \ \ \ 1\ \ 2 \newline
2.180 +*** a: ? <= \newline
2.181 +*** Could not find lexicographic termination order.\newline
2.182 *** At command "fun".\newline
2.183 \end{isabelle}%
2.184 \end{isamarkuptext}%
2.185 \isamarkuptrue%
2.186 %
2.187 \begin{isamarkuptext}%
2.188 -The the key to this error message is the matrix at the top. The rows
2.189 +The the key to this error message is the matrix at the bottom. The rows
2.190 of that matrix correspond to the different recursive calls (In our
2.191 case, there is just one). The columns are the function's arguments
2.192 (expressed through different measure functions, which map the
2.193 @@ -399,11 +446,11 @@
2.194 The contents of the matrix summarize what is known about argument
2.195 descents: The second argument has a weak descent (\isa{{\isacharless}{\isacharequal}}) at the
2.196 recursive call, and for the first argument nothing could be proved,
2.197 - which is expressed by \isa{N}. In general, there are the values
2.198 - \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{N}.
2.199 + which is expressed by \isa{{\isacharquery}}. In general, there are the values
2.200 + \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
2.201
2.202 For the failed proof attempts, the unfinished subgoals are also
2.203 - printed. Looking at these will often point us to a missing lemma.
2.204 + printed. Looking at these will often point to a missing lemma.
2.205
2.206 % As a more real example, here is quicksort:%
2.207 \end{isamarkuptext}%
2.208 @@ -523,17 +570,13 @@
2.209 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ even\ n\ {\isacharequal}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}n\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Suc\ n\ mod\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isacharparenright}%
2.210 \end{isabelle}
2.211
2.212 - \noindent These can be handeled by the descision procedure for
2.213 - arithmethic.%
2.214 + \noindent These can be handled by Isabelle's arithmetic decision procedures.%
2.215 \end{isamarkuptxt}%
2.216 \isamarkuptrue%
2.217 \isacommand{apply}\isamarkupfalse%
2.218 -\ presburger\ %
2.219 -\isamarkupcmt{\fixme{arith}%
2.220 -}
2.221 -\isanewline
2.222 +\ arith\isanewline
2.223 \isacommand{apply}\isamarkupfalse%
2.224 -\ presburger\isanewline
2.225 +\ arith\isanewline
2.226 \isacommand{done}\isamarkupfalse%
2.227 %
2.228 \endisatagproof
2.229 @@ -587,6 +630,11 @@
2.230 }
2.231 \isamarkuptrue%
2.232 %
2.233 +\begin{isamarkuptext}%
2.234 +\label{genpats}%
2.235 +\end{isamarkuptext}%
2.236 +\isamarkuptrue%
2.237 +%
2.238 \isamarkupsubsection{Avoiding automatic pattern splitting%
2.239 }
2.240 \isamarkuptrue%
2.241 @@ -601,7 +649,7 @@
2.242 equations involved, and this is not always desirable. The following
2.243 example shows the problem:
2.244
2.245 - Suppose we are modelling incomplete knowledge about the world by a
2.246 + Suppose we are modeling incomplete knowledge about the world by a
2.247 three-valued datatype, which has values \isa{T}, \isa{F}
2.248 and \isa{X} for true, false and uncertain propositions, respectively.%
2.249 \end{isamarkuptext}%
2.250 @@ -622,7 +670,7 @@
2.251 {\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
2.252 \begin{isamarkuptext}%
2.253 This definition is useful, because the equations can directly be used
2.254 - as simplifcation rules rules. But the patterns overlap: For example,
2.255 + as simplification rules rules. But the patterns overlap: For example,
2.256 the expression \isa{And\ T\ T} is matched by both the first and
2.257 the second equation. By default, Isabelle makes the patterns disjoint by
2.258 splitting them up, producing instances:%
2.259 @@ -733,60 +781,12 @@
2.260 \isamarkuptrue%
2.261 %
2.262 \begin{isamarkuptext}%
2.263 -Most of Isabelle's basic types take the form of inductive data types
2.264 - with constructors. However, this is not true for all of them. The
2.265 - integers, for instance, are defined using the usual algebraic
2.266 - quotient construction, thus they are not an \qt{official} datatype.
2.267 +Most of Isabelle's basic types take the form of inductive datatypes,
2.268 + and usually pattern matching works on the constructors of such types.
2.269 + However, this need not be always the case, and the \cmd{function}
2.270 + command handles other kind of patterns, too.
2.271
2.272 - Of course, we might want to do pattern matching there, too. So%
2.273 -\end{isamarkuptext}%
2.274 -\isamarkuptrue%
2.275 -\isacommand{function}\isamarkupfalse%
2.276 -\ Abs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
2.277 -\isakeyword{where}\isanewline
2.278 -\ \ {\isachardoublequoteopen}Abs\ {\isacharparenleft}int\ n{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
2.279 -{\isacharbar}\ {\isachardoublequoteopen}Abs\ {\isacharparenleft}{\isacharminus}\ int\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
2.280 -%
2.281 -\isadelimproof
2.282 -%
2.283 -\endisadelimproof
2.284 -%
2.285 -\isatagproof
2.286 -\isacommand{by}\isamarkupfalse%
2.287 -\ {\isacharparenleft}erule\ int{\isacharunderscore}cases{\isacharparenright}\ auto%
2.288 -\endisatagproof
2.289 -{\isafoldproof}%
2.290 -%
2.291 -\isadelimproof
2.292 -\isanewline
2.293 -%
2.294 -\endisadelimproof
2.295 -\isacommand{termination}\isamarkupfalse%
2.296 -%
2.297 -\isadelimproof
2.298 -\ %
2.299 -\endisadelimproof
2.300 -%
2.301 -\isatagproof
2.302 -\isacommand{by}\isamarkupfalse%
2.303 -\ {\isacharparenleft}relation\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ simp%
2.304 -\endisatagproof
2.305 -{\isafoldproof}%
2.306 -%
2.307 -\isadelimproof
2.308 -%
2.309 -\endisadelimproof
2.310 -%
2.311 -\begin{isamarkuptext}%
2.312 -This kind of matching is again justified by the proof of pattern
2.313 - completeness and compatibility. Here, the existing lemma \isa{int{\isacharunderscore}cases} is used:
2.314 -
2.315 - \begin{center}\isa{{\isasymlbrakk}{\isasymAnd}n{\isachardot}\ {\isacharquery}z\ {\isacharequal}\ int\ n\ {\isasymLongrightarrow}\ {\isacharquery}P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isacharquery}z\ {\isacharequal}\ {\isacharminus}\ int\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}\hfill(\isa{int{\isacharunderscore}cases})\end{center}%
2.316 -\end{isamarkuptext}%
2.317 -\isamarkuptrue%
2.318 -%
2.319 -\begin{isamarkuptext}%
2.320 -One well-known instance of non-constructor patterns are the
2.321 + One well-known instance of non-constructor patterns are
2.322 so-called \emph{$n+k$-patterns}, which are a little controversial in
2.323 the functional programming world. Here is the initial fibonacci
2.324 example with $n+k$-patterns:%
2.325 @@ -819,7 +819,9 @@
2.326 \isatagproof
2.327 %
2.328 \begin{isamarkuptxt}%
2.329 -The proof obligation for pattern completeness states that every natural number is
2.330 +This kind of matching is again justified by the proof of pattern
2.331 + completeness and compatibility.
2.332 + The proof obligation for pattern completeness states that every natural number is
2.333 either \isa{{\isadigit{0}}}, \isa{{\isadigit{1}}} or \isa{n\ {\isacharplus}\ {\isadigit{2}}}:
2.334
2.335 \begin{isabelle}%
2.336 @@ -828,8 +830,9 @@
2.337
2.338 This is an arithmetic triviality, but unfortunately the
2.339 \isa{arith} method cannot handle this specific form of an
2.340 - elimination rule. We have to do a case split on \isa{P} first,
2.341 - which can be conveniently done using the \isa{classical} rule. Pattern compatibility and termination are automatic as usual.%
2.342 + elimination rule. However, we can use the method \isa{elim{\isacharunderscore}to{\isacharunderscore}cases} to do an ad-hoc conversion to a disjunction of
2.343 + existentials, which can then be soved by the arithmetic decision procedure.
2.344 + Pattern compatibility and termination are automatic as usual.%
2.345 \end{isamarkuptxt}%
2.346 \isamarkuptrue%
2.347 %
2.348 @@ -852,7 +855,6 @@
2.349 \isadelimML
2.350 %
2.351 \endisadelimML
2.352 -\isanewline
2.353 %
2.354 \isadelimproof
2.355 %
2.356 @@ -860,7 +862,9 @@
2.357 %
2.358 \isatagproof
2.359 \isacommand{apply}\isamarkupfalse%
2.360 -\ {\isacharparenleft}rule\ classical{\isacharcomma}\ simp{\isacharcomma}\ arith{\isacharparenright}\isanewline
2.361 +\ elim{\isacharunderscore}to{\isacharunderscore}cases\isanewline
2.362 +\isacommand{apply}\isamarkupfalse%
2.363 +\ arith\isanewline
2.364 \isacommand{apply}\isamarkupfalse%
2.365 \ auto\isanewline
2.366 \isacommand{done}\isamarkupfalse%
2.367 @@ -905,8 +909,10 @@
2.368 \endisadelimproof
2.369 %
2.370 \isatagproof
2.371 +\isacommand{apply}\isamarkupfalse%
2.372 +\ elim{\isacharunderscore}to{\isacharunderscore}cases\isanewline
2.373 \isacommand{by}\isamarkupfalse%
2.374 -\ {\isacharparenleft}rule\ classical{\isacharcomma}\ simp{\isacharparenright}\ arith{\isacharplus}%
2.375 +\ arith{\isacharplus}%
2.376 \endisatagproof
2.377 {\isafoldproof}%
2.378 %
2.379 @@ -969,7 +975,7 @@
2.380 %
2.381 \isatagproof
2.382 \isacommand{by}\isamarkupfalse%
2.383 -\ {\isacharparenleft}rule\ classical{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}%
2.384 +\ {\isacharparenleft}elim{\isacharunderscore}to{\isacharunderscore}cases{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}%
2.385 \endisatagproof
2.386 {\isafoldproof}%
2.387 %
2.388 @@ -1007,7 +1013,7 @@
2.389 \isamarkuptrue%
2.390 %
2.391 \begin{isamarkuptext}%
2.392 -As strings (as lists of characters) are normal data types, pattern
2.393 +As strings (as lists of characters) are normal datatypes, pattern
2.394 matching on them is possible, but somewhat problematic. Consider the
2.395 following definition:
2.396
2.397 @@ -1018,9 +1024,9 @@
2.398 \isa{{\isacharbar}\ {\isachardoublequote}check\ s\ {\isacharequal}\ False{\isachardoublequote}}
2.399 \begin{isamarkuptext}
2.400
2.401 - An invocation of the above \cmd{fun} command does not
2.402 + \noindent An invocation of the above \cmd{fun} command does not
2.403 terminate. What is the problem? Strings are lists of characters, and
2.404 - characters are a data type with a lot of constructors. Splitting the
2.405 + characters are a datatype with a lot of constructors. Splitting the
2.406 catch-all pattern thus leads to an explosion of cases, which cannot
2.407 be handled by Isabelle.
2.408
2.409 @@ -1056,7 +1062,6 @@
2.410 In HOL, all functions are total. A function \isa{f} applied to
2.411 \isa{x} always has the value \isa{f\ x}, and there is no notion
2.412 of undefinedness.
2.413 -
2.414 This is why we have to do termination
2.415 proofs when defining functions: The proof justifies that the
2.416 function can be defined by wellfounded recursion.
2.417 @@ -1086,7 +1091,7 @@
2.418 \endisadelimproof
2.419 %
2.420 \begin{isamarkuptext}%
2.421 -Clearly, any attempt of a termination proof must fail. And without
2.422 +\noindent Clearly, any attempt of a termination proof must fail. And without
2.423 that, we do not get the usual rules \isa{findzero{\isachardot}simp} and
2.424 \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
2.425 \end{isamarkuptext}%
2.426 @@ -1106,23 +1111,21 @@
2.427 by domain conditions and are called \isa{psimps} and \isa{pinduct}:%
2.428 \end{isamarkuptext}%
2.429 \isamarkuptrue%
2.430 -\isacommand{thm}\isamarkupfalse%
2.431 -\ findzero{\isachardot}psimps%
2.432 +%
2.433 \begin{isamarkuptext}%
2.434 -\begin{isabelle}%
2.435 +\noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}%
2.436 findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
2.437 findzero\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}f\ {\isacharquery}n\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}n\ else\ findzero\ {\isacharquery}f\ {\isacharparenleft}Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}%
2.438 -\end{isabelle}%
2.439 -\end{isamarkuptext}%
2.440 -\isamarkuptrue%
2.441 -\isacommand{thm}\isamarkupfalse%
2.442 -\ findzero{\isachardot}pinduct%
2.443 -\begin{isamarkuptext}%
2.444 -\begin{isabelle}%
2.445 +\end{isabelle}\end{minipage}
2.446 + \hfill(\isa{findzero{\isachardot}psimps})
2.447 + \vspace{1em}
2.448 +
2.449 + \noindent\begin{minipage}{0.79\textwidth}\begin{isabelle}%
2.450 {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline
2.451 \isaindent{\ }{\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ f\ n{\isasymrbrakk}\isanewline
2.452 {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%
2.453 -\end{isabelle}%
2.454 +\end{isabelle}\end{minipage}
2.455 + \hfill(\isa{findzero{\isachardot}pinduct})%
2.456 \end{isamarkuptext}%
2.457 \isamarkuptrue%
2.458 %
2.459 @@ -1133,9 +1136,9 @@
2.460 to some natural number, although we might not be able to find out
2.461 which one. The function is \emph{underdefined}.
2.462
2.463 - But it is enough defined to prove something interesting about it. We
2.464 + But it is defined enough to prove something interesting about it. We
2.465 can prove that if \isa{findzero\ f\ n}
2.466 - it terminates, it indeed returns a zero of \isa{f}:%
2.467 + terminates, it indeed returns a zero of \isa{f}:%
2.468 \end{isamarkuptext}%
2.469 \isamarkuptrue%
2.470 \isacommand{lemma}\isamarkupfalse%
2.471 @@ -1147,21 +1150,21 @@
2.472 \isatagproof
2.473 %
2.474 \begin{isamarkuptxt}%
2.475 -We apply induction as usual, but using the partial induction
2.476 +\noindent We apply induction as usual, but using the partial induction
2.477 rule:%
2.478 \end{isamarkuptxt}%
2.479 \isamarkuptrue%
2.480 \isacommand{apply}\isamarkupfalse%
2.481 \ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}%
2.482 \begin{isamarkuptxt}%
2.483 -This gives the following subgoals:
2.484 +\noindent This gives the following subgoals:
2.485
2.486 \begin{isabelle}%
2.487 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ {\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ f\ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isasymrbrakk}\isanewline
2.488 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}%
2.489 \end{isabelle}
2.490
2.491 - The hypothesis in our lemma was used to satisfy the first premise in
2.492 + \noindent The hypothesis in our lemma was used to satisfy the first premise in
2.493 the induction rule. However, we also get \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as a local assumption in the induction step. This
2.494 allows to unfold \isa{findzero\ f\ n} using the \isa{psimps}
2.495 rule, and the rest is trivial. Since the \isa{psimps} rules carry the
2.496 @@ -1246,8 +1249,7 @@
2.497 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
2.498 \ \ \ \ \isacommand{with}\isamarkupfalse%
2.499 \ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
2.500 -\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
2.501 -\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
2.502 +\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.503 \ simp\isanewline
2.504 \ \ \ \ \isacommand{with}\isamarkupfalse%
2.505 \ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
2.506 @@ -1318,7 +1320,7 @@
2.507 that \isa{findzero} terminates if there is a zero which is greater
2.508 or equal to \isa{n}. First we derive two useful rules which will
2.509 solve the base case and the step case of the induction. The
2.510 - induction is then straightforward, except for the unusal induction
2.511 + induction is then straightforward, except for the unusual induction
2.512 principle.%
2.513 \end{isamarkuptext}%
2.514 \isamarkuptrue%
2.515 @@ -1396,13 +1398,13 @@
2.516 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.517 %
2.518 \isadelimproof
2.519 -\ \ %
2.520 +%
2.521 \endisadelimproof
2.522 %
2.523 \isatagproof
2.524 \isacommand{using}\isamarkupfalse%
2.525 \ zero\isanewline
2.526 -\ \ \isacommand{by}\isamarkupfalse%
2.527 +\isacommand{by}\isamarkupfalse%
2.528 \ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}%
2.529 \endisatagproof
2.530 {\isafoldproof}%
2.531 @@ -1440,11 +1442,11 @@
2.532 %
2.533 \begin{isamarkuptext}%
2.534 Sometimes it is useful to know what the definition of the domain
2.535 - predicate actually is. Actually, \isa{findzero{\isacharunderscore}dom} is just an
2.536 + predicate looks like. Actually, \isa{findzero{\isacharunderscore}dom} is just an
2.537 abbreviation:
2.538
2.539 \begin{isabelle}%
2.540 -findzero{\isacharunderscore}dom\ {\isasymequiv}\ acc\ findzero{\isacharunderscore}rel%
2.541 +findzero{\isacharunderscore}dom\ {\isasymequiv}\ accp\ findzero{\isacharunderscore}rel%
2.542 \end{isabelle}
2.543
2.544 The domain predicate is the \emph{accessible part} of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function
2.545 @@ -1469,8 +1471,8 @@
2.546 be reached in a finite number of steps (cf.~its definition in \isa{Accessible{\isacharunderscore}Part{\isachardot}thy}).
2.547
2.548 Since the domain predicate is just an abbreviation, you can use
2.549 - lemmas for \isa{acc} and \isa{findzero{\isacharunderscore}rel} directly. Some
2.550 - lemmas which are occasionally useful are \isa{accI}, \isa{acc{\isacharunderscore}downward}, and of course the introduction and elimination rules
2.551 + lemmas for \isa{accp} and \isa{findzero{\isacharunderscore}rel} directly. Some
2.552 + lemmas which are occasionally useful are \isa{accpI}, \isa{accp{\isacharunderscore}downward}, and of course the introduction and elimination rules
2.553 for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.%
2.554 \end{isamarkuptext}%
2.555 \isamarkuptrue%
2.556 @@ -1608,16 +1610,13 @@
2.557 property by induction.%
2.558 \end{isamarkuptxt}%
2.559 \isamarkuptrue%
2.560 -\isacommand{oops}\isamarkupfalse%
2.561 %
2.562 \endisatagproof
2.563 {\isafoldproof}%
2.564 %
2.565 \isadelimproof
2.566 -\isanewline
2.567 %
2.568 \endisadelimproof
2.569 -\isanewline
2.570 \isacommand{lemma}\isamarkupfalse%
2.571 \ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
2.572 %
2.573 @@ -1755,7 +1754,7 @@
2.574 \ \ \isacommand{with}\isamarkupfalse%
2.575 \ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
2.576 \ {\isachardoublequoteopen}{\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
2.577 -\ simp\ \isanewline
2.578 +\ simp\isanewline
2.579 \isacommand{qed}\isamarkupfalse%
2.580 %
2.581 \endisatagproof
2.582 @@ -1778,7 +1777,7 @@
2.583 \begin{isamarkuptext}%
2.584 Higher-order recursion occurs when recursive calls
2.585 are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc.
2.586 - As an example, imagine a data type of n-ary trees:%
2.587 + As an example, imagine a datatype of n-ary trees:%
2.588 \end{isamarkuptext}%
2.589 \isamarkuptrue%
2.590 \isacommand{datatype}\isamarkupfalse%
2.591 @@ -1858,7 +1857,7 @@
2.592 Simplification returns the following subgoal:
2.593
2.594 \begin{isabelle}%
2.595 -\ {\isadigit{1}}{\isachardot}\ x{\isacharunderscore}{\isacharunderscore}\ {\isasymin}\ set\ l{\isacharunderscore}{\isacharunderscore}\ {\isasymLongrightarrow}\ size\ x{\isacharunderscore}{\isacharunderscore}\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharunderscore}{\isacharunderscore}{\isacharparenright}%
2.596 +{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}%
2.597 \end{isabelle}
2.598
2.599 We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the
2.600 @@ -1866,8 +1865,7 @@
2.601 it, by induction.%
2.602 \end{isamarkuptxt}%
2.603 \isamarkuptrue%
2.604 -\ \ \ \ \isacommand{oops}\isamarkupfalse%
2.605 -%
2.606 +\ \ \ \ %
2.607 \endisatagproof
2.608 {\isafoldproof}%
2.609 %
2.610 @@ -1875,7 +1873,6 @@
2.611 %
2.612 \endisadelimproof
2.613 \isanewline
2.614 -\isanewline
2.615 \ \ \isacommand{lemma}\isamarkupfalse%
2.616 \ tree{\isacharunderscore}list{\isacharunderscore}size{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}tree{\isacharunderscore}list{\isacharunderscore}size\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.617 %
2.618 @@ -1936,7 +1933,7 @@
2.619
2.620 Usually, one such congruence rule is
2.621 needed for each higher-order construct that is used when defining
2.622 - new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handeled by this mechanism. The congruence
2.623 + new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handled by this mechanism. The congruence
2.624 rule for \isa{If} states that the \isa{then} branch is only
2.625 relevant if the condition is true, and the \isa{else} branch only if it
2.626 is false:
2.627 @@ -1949,34 +1946,97 @@
2.628 Congruence rules can be added to the
2.629 function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute.
2.630
2.631 - Isabelle comes with predefined congruence rules for most of the
2.632 - definitions.
2.633 - But if you define your own higher-order constructs, you will have to
2.634 + The constructs that are predefined in Isabelle, usually
2.635 + come with the respective congruence rules.
2.636 + But if you define your own higher-order functions, you will have to
2.637 come up with the congruence rules yourself, if you want to use your
2.638 - functions in recursive definitions. Since the structure of
2.639 - congruence rules is a little unintuitive, here are some exercises:%
2.640 + functions in recursive definitions.%
2.641 \end{isamarkuptext}%
2.642 \isamarkuptrue%
2.643 %
2.644 +\isamarkupsubsection{Congruence Rules and Evaluation Order%
2.645 +}
2.646 +\isamarkuptrue%
2.647 +%
2.648 \begin{isamarkuptext}%
2.649 -\begin{exercise}
2.650 - Find a suitable congruence rule for the following function which
2.651 - maps only over the even numbers in a list:
2.652 +Higher order logic differs from functional programming languages in
2.653 + that it has no built-in notion of evaluation order. A program is
2.654 + just a set of equations, and it is not specified how they must be
2.655 + evaluated.
2.656
2.657 - \begin{isabelle}%
2.658 -mapeven\ {\isacharquery}f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline%
2.659 -mapeven\ {\isacharquery}f\ {\isacharparenleft}{\isacharquery}x\ {\isacharhash}\ {\isacharquery}xs{\isacharparenright}\ {\isacharequal}\isanewline
2.660 -{\isacharparenleft}if\ {\isacharquery}x\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharquery}f\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs\ else\ {\isacharquery}x\ {\isacharhash}\ mapeven\ {\isacharquery}f\ {\isacharquery}xs{\isacharparenright}%
2.661 -\end{isabelle}
2.662 - \end{exercise}
2.663 -
2.664 - \begin{exercise}
2.665 - Try what happens if the congruence rule for \isa{If} is
2.666 - disabled by declaring \isa{if{\isacharunderscore}cong{\isacharbrackleft}fundef{\isacharunderscore}cong\ del{\isacharbrackright}}?
2.667 - \end{exercise}
2.668 + However for the purpose of function definition, we must talk about
2.669 + evaluation order implicitly, when we reason about termination.
2.670 + Congruence rules express that a certain evaluation order is
2.671 + consistent with the logical definition.
2.672
2.673 - Note that in some cases there is no \qt{best} congruence rule.
2.674 - \fixme{}%
2.675 + Consider the following function.%
2.676 +\end{isamarkuptext}%
2.677 +\isamarkuptrue%
2.678 +\isacommand{function}\isamarkupfalse%
2.679 +\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
2.680 +\isakeyword{where}\isanewline
2.681 +\ \ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ f\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
2.682 +\isadelimproof
2.683 +%
2.684 +\endisadelimproof
2.685 +%
2.686 +\isatagproof
2.687 +%
2.688 +\endisatagproof
2.689 +{\isafoldproof}%
2.690 +%
2.691 +\isadelimproof
2.692 +%
2.693 +\endisadelimproof
2.694 +%
2.695 +\begin{isamarkuptext}%
2.696 +As given above, the definition fails. The default configuration
2.697 + specifies no congruence rule for disjunction. We have to add a
2.698 + congruence rule that specifies left-to-right evaluation order:
2.699 +
2.700 + \vspace{1ex}
2.701 + \noindent \isa{{\isasymlbrakk}{\isacharquery}P\ {\isacharequal}\ {\isacharquery}P{\isacharprime}{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P{\isacharprime}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharequal}\ {\isacharquery}Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}P\ {\isasymor}\ {\isacharquery}Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}P{\isacharprime}\ {\isasymor}\ {\isacharquery}Q{\isacharprime}{\isacharparenright}}\hfill(\isa{disj{\isacharunderscore}cong})
2.702 + \vspace{1ex}
2.703 +
2.704 + Now the definition works without problems. Note how the termination
2.705 + proof depends on the extra condition that we get from the congruence
2.706 + rule.
2.707 +
2.708 + However, as evaluation is not a hard-wired concept, we
2.709 + could just turn everything around by declaring a different
2.710 + congruence rule. Then we can make the reverse definition:%
2.711 +\end{isamarkuptext}%
2.712 +\isamarkuptrue%
2.713 +\isacommand{lemma}\isamarkupfalse%
2.714 +\ disj{\isacharunderscore}cong{\isadigit{2}}{\isacharbrackleft}fundef{\isacharunderscore}cong{\isacharbrackright}{\isacharcolon}\ \isanewline
2.715 +\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymnot}\ Q{\isacharprime}\ {\isasymLongrightarrow}\ P\ {\isacharequal}\ P{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}Q\ {\isacharequal}\ Q{\isacharprime}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymor}\ Q{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.716 +%
2.717 +\isadelimproof
2.718 +\ \ %
2.719 +\endisadelimproof
2.720 +%
2.721 +\isatagproof
2.722 +\isacommand{by}\isamarkupfalse%
2.723 +\ blast%
2.724 +\endisatagproof
2.725 +{\isafoldproof}%
2.726 +%
2.727 +\isadelimproof
2.728 +\isanewline
2.729 +%
2.730 +\endisadelimproof
2.731 +\isanewline
2.732 +\isacommand{fun}\isamarkupfalse%
2.733 +\ f{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
2.734 +\isakeyword{where}\isanewline
2.735 +\ \ {\isachardoublequoteopen}f{\isacharprime}\ n\ {\isacharequal}\ {\isacharparenleft}f{\isacharprime}\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymor}\ n\ {\isacharequal}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}%
2.736 +\begin{isamarkuptext}%
2.737 +\noindent These examples show that, in general, there is no \qt{best} set of
2.738 + congruence rules.
2.739 +
2.740 + However, such tweaking should rarely be necessary in
2.741 + practice, as most of the time, the default set of congruence rules
2.742 + works well.%
2.743 \end{isamarkuptext}%
2.744 \isamarkuptrue%
2.745 %
3.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/session.tex Thu Jul 12 11:43:17 2007 +0200
3.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/session.tex Thu Jul 12 12:20:39 2007 +0200
3.3 @@ -1,7 +1,5 @@
3.4 \input{Functions.tex}
3.5
3.6 -\input{Predefined_Congs.tex}
3.7 -
3.8 %%% Local Variables:
3.9 %%% mode: latex
3.10 %%% TeX-master: "root"
4.1 --- a/doc-src/IsarAdvanced/Functions/functions.tex Thu Jul 12 11:43:17 2007 +0200
4.2 +++ b/doc-src/IsarAdvanced/Functions/functions.tex Thu Jul 12 12:20:39 2007 +0200
4.3 @@ -67,6 +67,7 @@
4.4
4.5 \begin{document}
4.6
4.7 +\date{\ \\}
4.8 \maketitle
4.9
4.10 \begin{abstract}
4.11 @@ -74,7 +75,7 @@
4.12 which provides general recursive function definitions for Isabelle/HOL.
4.13 We start with very simple examples and then gradually move on to more
4.14 advanced topics such as manual termination proofs, nested recursion,
4.15 - partiality and congruence rules.
4.16 + partiality, tail recursion and congruence rules.
4.17 \end{abstract}
4.18
4.19 %\thispagestyle{empty}\clearpage
4.20 @@ -84,7 +85,7 @@
4.21
4.22 \input{intro.tex}
4.23 \input{Thy/document/Functions.tex}
4.24 -\input{conclusion.tex}
4.25 +%\input{conclusion.tex}
4.26
4.27 \begingroup
4.28 %\tocentry{\bibname}
5.1 --- a/doc-src/IsarAdvanced/Functions/intro.tex Thu Jul 12 11:43:17 2007 +0200
5.2 +++ b/doc-src/IsarAdvanced/Functions/intro.tex Thu Jul 12 12:20:39 2007 +0200
5.3 @@ -1,16 +1,37 @@
5.4 \section{Introduction}
5.5
5.6 -In the upcomung release of Isabelle 2007, new facilities for recursive
5.7 -function definitions \cite{krauss2006} will be available.
5.8 +In the upcoming release of Isabelle 2007, new facilities for recursive
5.9 +function definitions \cite{krauss2006} will be available, providing
5.10 +better support for general recursive definitions than previous
5.11 +packages did. But despite all tool support, function definitions can
5.12 +sometimes be a difficult thing.
5.13
5.14 This tutorial is an example-guided introduction to the practical use
5.15 -of the package. We assume that you have mastered the basic concepts of
5.16 -Isabelle/HOL and are able to write basic specifications and
5.17 -proofs. To start out with Isabelle in general, you should read the
5.18 -tutorial \cite{isa-tutorial}.
5.19 +of the package and related tools. It should help you get started with
5.20 +defining functions quickly. For the more difficult definitions we will
5.21 +discuss what problems can arise, and how they can be solved.
5.22
5.23 -% Definitional extension
5.24 +We assume that you have mastered the basics of Isabelle/HOL
5.25 +and are able to write basic specifications and proofs. To start out
5.26 +with Isabelle in general, consult the Isabelle/HOL tutorial
5.27 +\cite{isa-tutorial}.
5.28
5.29 +
5.30 +
5.31 +\paragraph{Structure of this tutorial.}
5.32 +Section 2 introduces the syntax and basic operation of the \cmd{fun}
5.33 +command, which provides full automation with reasonable default
5.34 +behavior. The impatient reader might want to stop after that
5.35 +section, and consult the remaining sections only when needed.
5.36 +Section 3 introduces the more verbose \cmd{function} command which
5.37 +gives fine-grained control to the user. This form should be used
5.38 +whenever the short form fails.
5.39 +After that we discuss different issues that are more specialized:
5.40 +termination, mutual and nested recursion, partiality, pattern matching
5.41 +and others.
5.42 +
5.43 +
5.44 +\paragraph{Some background.}
5.45 Following the LCF tradition, the package is realized as a definitional
5.46 extension: Recursive definitions are internally transformed into a
5.47 non-recursive form, such that the function can be defined using
5.48 @@ -18,7 +39,7 @@
5.49 derived from the primitive definition. This is a complex task, but it
5.50 is fully automated and mostly transparent to the user. Definitional
5.51 extensions are valuable because they are conservative by construction:
5.52 -The new concept of general wellfounded recursion is completely reduced
5.53 +The \qt{new} concept of general wellfounded recursion is completely reduced
5.54 to existing principles.
5.55
5.56