updated

--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Thu May 17 23:00:06 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Thu May 17 23:03:47 2007 +0200
@@ -9,13 +9,14 @@
 imports Main
 begin
 
-chapter {* Defining Recursive Functions in Isabelle/HOL *}
-
 section {* Function Definition for Dummies *}
 
 text {*
   In most cases, defining a recursive function is just as simple as other definitions:
-  *}
+
+  Like in functional programming, a function definition consists of a 
+
+*}
 
 fun fib :: "nat \<Rightarrow> nat"
 where
@@ -24,11 +25,21 @@
 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
 text {*
-  The function always terminates, since the argument of gets smaller in every
-  recursive call. Termination is an
-  important requirement, since it prevents inconsistencies: From
-  the "definition" @{text "f(n) = f(n) + 1"} we could prove 
-  @{text "0  = 1"} by subtracting @{text "f(n)"} on both sides.
+  The syntax is rather self-explanatory: We introduce a function by
+  giving its name, its type and a set of defining recursive
+  equations. 
+*}
+
+
+
+
+
+text {*
+  The function always terminates, since its argument gets smaller in
+  every recursive call. Termination is an important requirement, since
+  it prevents inconsistencies: From the "definition" @{text "f(n) =
+  f(n) + 1"} we could prove @{text "0 = 1"} by subtracting @{text
+  "f(n)"} on both sides.
 
   Isabelle tries to prove termination automatically when a function is
   defined. We will later look at cases where this fails and see what to
@@ -38,8 +49,8 @@
 subsection {* Pattern matching *}
 
 text {* \label{patmatch}
-  Like in functional programming, functions can be defined by pattern
-  matching. At the moment we will only consider \emph{datatype
+  Like in functional programming, we can use pattern matching to
+  define functions. At the moment we will only consider \emph{constructor
   patterns}, which only consist of datatype constructors and
   variables.
 
@@ -72,8 +83,6 @@
 lemma "sep (0::nat) [1, 2, 3] = [1, 0, 2, 0, 3]"
 by simp
 
-  
-
 subsection {* Induction *}
 
 text {*
@@ -178,10 +187,14 @@
   We can use this expression as a measure function suitable to prove termination.
 *}
 
-termination 
+termination sum
 by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
 
 text {*
+  The \cmd{termination} command sets up the termination goal for the
+  specified function @{text "sum"}. If the function name is omitted it
+  implicitly refers to the last function definition.
+
   The @{text relation} method takes a relation of
   type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of
   the function. If the function has multiple curried arguments, then
@@ -223,6 +236,32 @@
 termination 
 by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
 
+subsection {* Manual Termination Proofs *}
+
+text {*
+  The @{text relation} method is often useful, but not
+  necessary. Since termination proofs are just normal Isabelle proofs,
+  they can also be carried out manually: 
+*}
+
+function id :: "nat \<Rightarrow> nat"
+where
+  "id 0 = 0"
+| "id (Suc n) = Suc (id n)"
+by pat_completeness auto
+
+termination
+proof 
+  show "wf less_than" ..
+next
+  fix n show "(n, Suc n) \<in> less_than" by simp
+qed
+
+text {*
+  Of course this is just a trivial example, but manual proofs can
+  sometimes be the only choice if faced with very hard termination problems.
+*}
+
 
 section {* Mutual Recursion *}
 
@@ -334,8 +373,8 @@
   shows the problem:
   
   Suppose we are modelling incomplete knowledge about the world by a
-  three-valued datatype, which has values for @{term "T"}, @{term "F"}
-  and @{term "X"} for true, false and uncertain propositions. 
+  three-valued datatype, which has values @{term "T"}, @{term "F"}
+  and @{term "X"} for true, false and uncertain propositions, respectively. 
 *}
 
 datatype P3 = T | F | X
@@ -345,10 +384,10 @@
 fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
 where
   "And T p = p"
-  "And p T = p"
-  "And p F = F"
-  "And F p = F"
-  "And X X = X"
+| "And p T = p"
+| "And p F = F"
+| "And F p = F"
+| "And X X = X"
 
 
 text {* 
@@ -365,15 +404,15 @@
   @{thm[indent=4] And.simps}
   
   \vspace*{1em}
-  \noindent There are several problems with this approach:
+  \noindent There are several problems with this:
 
   \begin{enumerate}
   \item When datatypes have many constructors, there can be an
   explosion of equations. For @{const "And"}, we get seven instead of
-  five equation, which can be tolerated, but this is just a small
+  five equations, which can be tolerated, but this is just a small
   example.
 
-  \item Since splitting makes the equations "more special", they
+  \item Since splitting makes the equations "less general", they
   do not always match in rewriting. While the term @{term "And x F"}
   can be simplified to @{term "F"} by the original specification, a
   (manual) case split on @{term "x"} is now necessary.
@@ -390,17 +429,17 @@
   both @{term "f x = True"} and @{term "f x = False"} is a bad
   idea. So if we don't want Isabelle to mangle our definitions, we
   will have to prove that this is not necessary. By using the full
-  definition form withour the \cmd{sequential} option, we get this
+  definition form without the \cmd{sequential} option, we get this
   behaviour: 
 *}
 
 function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
 where
   "And2 T p = p"
-  "And2 p T = p"
-  "And2 p F = F"
-  "And2 F p = F"
-  "And2 X X = X"
+| "And2 p T = p"
+| "And2 p F = F"
+| "And2 F p = F"
+| "And2 X X = X"
 
 txt {*
   Now it is also time to look at the subgoals generated by a
@@ -436,13 +475,6 @@
 text {* FIXME *}
 
 
-subsection {* Non-constructor patterns *}
-
-text {* FIXME *}
-
-
-
-
 
 
 section {* Partiality *}
@@ -451,23 +483,672 @@
   In HOL, all functions are total. A function @{term "f"} applied to
   @{term "x"} always has a value @{term "f x"}, and there is no notion
   of undefinedness. 
+  
+  This property of HOL is the reason why we have to do termination
+  proofs when defining functions: The termination proof justifies the
+  definition of the function by wellfounded recursion.
 
-  FIXME
+  However, the \cmd{function} package still supports partiality. Let's
+  look at the following function which searches for a zero in the
+  function f. 
+*}
+
+function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
+by pat_completeness auto
+(*<*)declare findzero.simps[simp del](*>*)
+
+text {*
+  Clearly, any attempt of a termination proof must fail. And without
+  that, we do not get the usual rules @{text "findzero.simp"} and 
+  @{text "findzero.induct"}. So what was the definition good for at all?
+*}
+
+subsection {* Domain predicates *}
+
+text {*
+  The trick is that Isabelle has not only defined the function @{const findzero}, but also
+  a predicate @{term "findzero_dom"} that characterizes the values where the function
+  terminates: the \emph{domain} of the function. In Isabelle/HOL, a
+  partial function is just a total function with an additional domain
+  predicate. Like with total functions, we get simplification and
+  induction rules, but they are guarded by the domain conditions and
+  called @{text psimps} and @{text pinduct}:
+*}
+
+thm findzero.psimps
+
+text {*
+  @{thm[display] findzero.psimps}
+*}
+
+thm findzero.pinduct
+
+text {*
+  @{thm[display] findzero.pinduct}
+*}
+
+text {*
+  As already mentioned, HOL does not support true partiality. All we
+  are doing here is using some tricks to make a total function appear
+  as if it was partial. We can still write the term @{term "findzero
+  (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
+  to some natural number, although we might not be able to find out
+  which one (we will discuss this further in \S\ref{default}). The
+  function is \emph{underdefined}.
+
+  But it is enough defined to prove something about it. We can prove
+  that if @{term "findzero f n"}
+  it terminates, it indeed returns a zero of @{term f}:
+*}
+
+lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
+
+txt {* We apply induction as usual, but using the partial induction
+  rule: *}
+
+apply (induct f n rule: findzero.pinduct)
+
+txt {* This gives the following subgoals:
+
+  @{subgoals[display,indent=0]}
+
+  The premise in our lemma was used to satisfy the first premise in
+  the induction rule. However, now we can also use @{term
+  "findzero_dom (f, n)"} as an assumption in the induction step. This
+  allows to unfold @{term "findzero f n"} using the @{text psimps}
+  rule, and the rest is trivial. Since @{text psimps} rules carry the
+  @{text "[simp]"} attribute by default, we just need a single step:
+ *}
+apply simp
+done
+
+text {*
+  Proofs about partial functions are often not harder than for total
+  functions. Fig.~\ref{findzero_isar} shows a slightly more
+  complicated proof written in Isar. It is verbose enough to show how
+  partiality comes into play: From the partial induction, we get an
+  additional domain condition hypothesis. Observe how this condition
+  is applied when calls to @{term findzero} are unfolded.
+*}
+
+text_raw {*
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+*}
+lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
+proof (induct rule: findzero.pinduct)
+  fix f n assume dom: "findzero_dom (f, n)"
+    and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n..<findzero f (Suc n)}\<rbrakk>
+             \<Longrightarrow> f x \<noteq> 0"
+    and x_range: "x \<in> {n..<findzero f n}"
+  
+  have "f n \<noteq> 0"
+  proof 
+    assume "f n = 0"
+    with dom have "findzero f n = n" by simp
+    with x_range show False by auto
+  qed
+  
+  from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
+  thus "f x \<noteq> 0"
+  proof
+    assume "x = n"
+    with `f n \<noteq> 0` show ?thesis by simp
+  next
+    assume "x \<in> {Suc n..<findzero f n}"
+    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}"
+      by simp
+    with IH and `f n \<noteq> 0`
+    show ?thesis by simp
+  qed
+qed
+text_raw {*
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{A proof about a partial function}\label{findzero_isar}
+\end{figure}
+*}
+
+subsection {* Partial termination proofs *}
+
+text {*
+  Now that we have proved some interesting properties about our
+  function, we should turn to the domain predicate and see if it is
+  actually true for some values. Otherwise we would have just proved
+  lemmas with @{term False} as a premise.
+
+  Essentially, we need some introduction rules for @{text
+  findzero_dom}. The function package can prove such domain
+  introduction rules automatically. But since they are not used very
+  often (they are almost never needed if the function is total), they
+  are disabled by default for efficiency reasons. So we have to go
+  back and ask for them explicitly by passing the @{text
+  "(domintros)"} option to the function package:
+
+\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
+\cmd{where}\isanewline%
+\ \ \ldots\\
+\cmd{by} @{text "pat_completeness auto"}\\%
+
+
+  Now the package has proved an introduction rule for @{text findzero_dom}:
+*}
+
+thm findzero.domintros
+
+text {*
+  @{thm[display] findzero.domintros}
+
+  Domain introduction rules allow to show that a given value lies in the
+  domain of a function, if the arguments of all recursive calls
+  are in the domain as well. They allow to do a \qt{single step} in a
+  termination proof. Usually, you want to combine them with a suitable
+  induction principle.
+
+  Since our function increases its argument at recursive calls, we
+  need an induction principle which works \qt{backwards}. We will use
+  @{text inc_induct}, which allows to do induction from a fixed number
+  \qt{downwards}:
+
+  @{thm[display] inc_induct}
+
+  Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact
+  that @{text findzero} terminates if there is a zero which is greater
+  or equal to @{term n}. First we derive two useful rules which will
+  solve the base case and the step case of the induction. The
+  induction is then straightforward, except for the unusal induction
+  principle.
+
+*}
+
+text_raw {*
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+*}
+lemma findzero_termination:
+  assumes "x >= n" 
+  assumes "f x = 0"
+  shows "findzero_dom (f, n)"
+proof - 
+  have base: "findzero_dom (f, x)"
+    by (rule findzero.domintros) (simp add:`f x = 0`)
+
+  have step: "\<And>i. findzero_dom (f, Suc i) 
+    \<Longrightarrow> findzero_dom (f, i)"
+    by (rule findzero.domintros) simp
+
+  from `x \<ge> n`
+  show ?thesis
+  proof (induct rule:inc_induct)
+    show "findzero_dom (f, x)"
+      by (rule base)
+  next
+    fix i assume "findzero_dom (f, Suc i)"
+    thus "findzero_dom (f, i)"
+      by (rule step)
+  qed
+qed      
+text_raw {*
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{Termination proof for @{text findzero}}\label{findzero_term}
+\end{figure}
+*}
+      
+text {*
+  Again, the proof given in Fig.~\ref{findzero_term} has a lot of
+  detail in order to explain the principles. Using more automation, we
+  can also have a short proof:
+*}
+
+lemma findzero_termination_short:
+  assumes zero: "x >= n" 
+  assumes [simp]: "f x = 0"
+  shows "findzero_dom (f, n)"
+  using zero
+  by (induct rule:inc_induct) (auto intro: findzero.domintros)
+    
+text {*
+  It is simple to combine the partial correctness result with the
+  termination lemma:
+*}
+
+lemma findzero_total_correctness:
+  "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
+by (blast intro: findzero_zero findzero_termination)
+
+subsection {* Definition of the domain predicate *}
+
+text {*
+  Sometimes it is useful to know what the definition of the domain
+  predicate actually is. Actually, @{text findzero_dom} is just an
+  abbreviation:
+
+  @{abbrev[display] findzero_dom}
+
+  The domain predicate is the accessible part of a relation @{const
+  findzero_rel}, which was also created internally by the function
+  package. @{const findzero_rel} is just a normal
+  inductively defined predicate, so we can inspect its definition by
+  looking at the introduction rules @{text findzero_rel.intros}.
+  In our case there is just a single rule:
+
+  @{thm[display] findzero_rel.intros}
+
+  The relation @{const findzero_rel}, expressed as a binary predicate,
+  describes the \emph{recursion relation} of the function
+  definition. The recursion relation is a binary relation on
+  the arguments of the function that relates each argument to its
+  recursive calls. In general, there is one introduction rule for each
+  recursive call.
+
+  The predicate @{term "acc findzero_rel"} is the \emph{accessible part} of
+  that relation. An argument belongs to the accessible part, if it can
+  be reached in a finite number of steps. 
+
+  Since the domain predicate is just an abbreviation, you can use
+  lemmas for @{const acc} and @{const findzero_rel} directly. Some
+  lemmas which are occasionally useful are @{text accI}, @{text
+  acc_downward}, and of course the introduction and elimination rules
+  for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
+*}
+
+(*lemma findzero_nicer_domintros:
+  "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
+  "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
+by (rule accI, erule findzero_rel.cases, auto)+
+*)
+  
+subsection {* A Useful Special Case: Tail recursion *}
+
+text {*
+  The domain predicate is our trick that allows us to model partiality
+  in a world of total functions. The downside of this is that we have
+  to carry it around all the time. The termination proof above allowed
+  us to replace the abstract @{term "findzero_dom (f, n)"} by the more
+  concrete @{term "(x \<ge> n \<and> f x = 0)"}, but the condition is still
+  there and it won't go away soon. 
+
+  In particular, the domain predicate guard the unfolding of our
+  function, since it is there as a condition in the @{text psimp}
+  rules. 
+
+  On the other hand, we must be happy about the domain predicate,
+  since it guarantees that all this is at all possible without losing
+  consistency. 
+
+  Now there is an important special case: We can actually get rid
+  of the condition in the simplification rules, \emph{if the function
+  is tail-recursive}. The reason is that for all tail-recursive
+  equations there is a total function satisfying them, even if they
+  are non-terminating. 
+
+  The function package internally does the right construction and can
+  derive the unconditional simp rules, if we ask it to do so. Luckily,
+  our @{const "findzero"} function is tail-recursive, so we can just go
+  back and add another option to the \cmd{function} command:
+
+\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
+\cmd{where}\isanewline%
+\ \ \ldots\\%
+
+  
+  Now, we actually get the unconditional simplification rules, even
+  though the function is partial:
+*}
+
+thm findzero.simps
+
+text {*
+  @{thm[display] findzero.simps}
+
+  Of course these would make the simplifier loop, so we better remove
+  them from the simpset:
+*}
+
+declare findzero.simps[simp del]
+
+
+text {* \fixme{Code generation ???} *}
+
+section {* Nested recursion *}
+
+text {*
+  Recursive calls which are nested in one another frequently cause
+  complications, since their termination proof can depend on a partial
+  correctness property of the function itself. 
+
+  As a small example, we define the \qt{nested zero} function:
+*}
+
+function nz :: "nat \<Rightarrow> nat"
+where
+  "nz 0 = 0"
+| "nz (Suc n) = nz (nz n)"
+by pat_completeness auto
+
+text {*
+  If we attempt to prove termination using the identity measure on
+  naturals, this fails:
+*}
+
+termination
+  apply (relation "measure (\<lambda>n. n)")
+  apply auto
+
+txt {*
+  We get stuck with the subgoal
+
+  @{subgoals[display]}
+
+  Of course this statement is true, since we know that @{const nz} is
+  the zero function. And in fact we have no problem proving this
+  property by induction.
+*}
+oops
+
+lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
+  by (induct rule:nz.pinduct) auto
+
+text {*
+  We formulate this as a partial correctness lemma with the condition
+  @{term "nz_dom n"}. This allows us to prove it with the @{text
+  pinduct} rule before we have proved termination. With this lemma,
+  the termination proof works as expected:
+*}
+
+termination
+  by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
+
+text {*
+  As a general strategy, one should prove the statements needed for
+  termination as a partial property first. Then they can be used to do
+  the termination proof. This also works for less trivial
+  examples. Figure \ref{f91} defines the well-known 91-function by
+  McCarthy \cite{?} and proves its termination.
+*}
+
+text_raw {*
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+*}
+
+function f91 :: "nat => nat"
+where
+  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
+by pat_completeness auto
+
+lemma f91_estimate: 
+  assumes trm: "f91_dom n" 
+  shows "n < f91 n + 11"
+using trm by induct auto
+
+termination
+proof
+  let ?R = "measure (\<lambda>x. 101 - x)"
+  show "wf ?R" ..
+
+  fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
+
+  thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
+
+  assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
+  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
+  with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp 
+qed
+
+text_raw {*
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{McCarthy's 91-function}\label{f91}
+\end{figure}
 *}
 
 
+section {* Higher-Order Recursion *}
 
+text {*
+  Higher-order recursion occurs when recursive calls
+  are passed as arguments to higher-order combinators such as @{term
+  map}, @{term filter} etc.
+  As an example, imagine a data type of n-ary trees:
+*}
+
+datatype 'a tree = 
+  Leaf 'a 
+| Branch "'a tree list"
+
+
+text {* \noindent We can define a map function for trees, using the predefined
+  map function for lists. *}
   
-section {* Nested recursion *}
+function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+where
+  "treemap f (Leaf n) = Leaf (f n)"
+| "treemap f (Branch l) = Branch (map (treemap f) l)"
+by pat_completeness auto
 
 text {*
+  We do the termination proof manually, to point out what happens
+  here: 
+*}
+
+termination proof
+  txt {*
+
+  As usual, we have to give a wellfounded relation, such that the
+  arguments of the recursive calls get smaller. But what exactly are
+  the arguments of the recursive calls? Isabelle gives us the
+  subgoals
+
+  @{subgoals[display,indent=0]} 
+
+  So Isabelle seems to know that @{const map} behaves nicely and only
+  applies the recursive call @{term "treemap f"} to elements
+  of @{term "l"}. Before we discuss where this knowledge comes from,
+  let us finish the termination proof:
+  *}
+
+  show "wf (measure (size o snd))" by simp
+next
+  fix f l and x :: "'a tree"
+  assume "x \<in> set l"
+  thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"
+    apply simp
+    txt {*
+      Simplification returns the following subgoal: 
+
+      @{subgoals[display,indent=0]} 
+
+      We are lacking a property about the function @{const
+      tree_list_size}, which was generated automatically at the
+      definition of the @{text tree} type. We should go back and prove
+      it, by induction.
+      *}
+    oops
+
+  lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
+    by (induct l) auto
+
+  text {* 
+    Now the whole termination proof is automatic:
+    *}
+
+  termination 
+    by lexicographic_order
   
 
+subsection {* Congruence Rules *}
+
+text {*
+  Let's come back to the question how Isabelle knows about @{const
+  map}.
+
+  The knowledge about map is encoded in so-called congruence rules,
+  which are special theorems known to the \cmd{function} command. The
+  rule for map is
+
+  @{thm[display] map_cong}
+
+  You can read this in the following way: Two applications of @{const
+  map} are equal, if the list arguments are equal and the functions
+  coincide on the elements of the list. This means that for the value 
+  @{term "map f l"} we only have to know how @{term f} behaves on
+  @{term l}.
+
+  Usually, one such congruence rule is
+  needed for each higher-order construct that is used when defining
+  new functions. In fact, even basic functions like @{const
+  If} and @{const Let} are handeled by this mechanism. The congruence
+  rule for @{const If} states that the @{text then} branch is only
+  relevant if the condition is true, and the @{text else} branch only if it
+  is false:
+
+  @{thm[display] if_cong}
+  
+  Congruence rules can be added to the
+  function package by giving them the @{term fundef_cong} attribute.
+
+  Isabelle comes with predefined congruence rules for most of the
+  definitions.
+  But if you define your own higher-order constructs, you will have to
+  come up with the congruence rules yourself, if you want to use your
+  functions in recursive definitions. Since the structure of
+  congruence rules is a little unintuitive, here are some exercises:
+*}
+(*<*)
+fun mapeven :: "(nat \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat list"
+where
+  "mapeven f [] = []"
+| "mapeven f (x#xs) = (if x mod 2 = 0 then f x # mapeven f xs else x #
+  mapeven f xs)"
+(*>*)
+text {*
+
+  \begin{exercise}
+    Find a suitable congruence rule for the following function which
+  maps only over the even numbers in a list:
+
+  @{thm[display] mapeven.simps}
+  \end{exercise}
+  
+  \begin{exercise}
+  What happens if the congruence rule for @{const If} is
+  disabled by declaring @{text "if_cong[fundef_cong del]"}?
+  \end{exercise}
+
+  Note that in some cases there is no \qt{best} congruence rule.
+  \fixme
+
+*}
+
 
 
 
 
- FIXME *}
+
+
+section {* Appendix: Predefined Congruence Rules *}
+
+(*<*)
+syntax (Rule output)
+  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+definition 
+FixImp :: "prop \<Rightarrow> prop \<Rightarrow> prop" 
+where
+  "FixImp (PROP A) (PROP B) \<equiv> (PROP A \<Longrightarrow> PROP B)"
+notation (output)
+  FixImp (infixr "\<Longrightarrow>" 1)
+
+setup {*
+let
+  val fix_imps = map_aterms (fn Const ("==>", T) => Const ("Functions.FixImp", T) | t => t)
+  fun transform t = Logic.list_implies (map fix_imps (Logic.strip_imp_prems t), Logic.strip_imp_concl t)
+in
+  TermStyle.add_style "topl" (K transform)
+end
+*}
+(*>*)
+
+subsection {* Basic Control Structures *}
+
+text {*
+
+@{thm_style[mode=Rule] topl if_cong}
+
+@{thm_style [mode=Rule] topl let_cong}
+
+*}
+
+subsection {* Data Types *}
+
+text {*
+
+For each \cmd{datatype} definition, a congruence rule for the case
+  combinator is registeres automatically. Here are the rules for
+  @{text "nat"} and @{text "list"}:
+
+\begin{center}@{thm_style[mode=Rule] topl nat.case_cong}\end{center}
+
+\begin{center}@{thm_style[mode=Rule] topl list.case_cong}\end{center}
+
+*}
+
+subsection {* List combinators *}
+
+
+text {*
+
+@{thm_style[mode=Rule] topl map_cong}
+
+@{thm_style[mode=Rule] topl filter_cong}
+
+@{thm_style[mode=Rule] topl foldr_cong}
+
+@{thm_style[mode=Rule] topl foldl_cong}
+
+Similar: takewhile, dropwhile
+
+*}
+
+subsection {* Sets *}
+
+
+text {*
+
+@{thm_style[mode=Rule] topl ball_cong}
+
+@{thm_style[mode=Rule] topl bex_cong}
+
+@{thm_style[mode=Rule] topl UN_cong}
+
+@{thm_style[mode=Rule] topl INT_cong}
+
+@{thm_style[mode=Rule] topl image_cong}
+
+
+*}
 
 
 

--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu May 17 23:00:06 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Thu May 17 23:03:47 2007 +0200
@@ -20,16 +20,14 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Defining Recursive Functions in Isabelle/HOL%
-}
-\isamarkuptrue%
-%
 \isamarkupsection{Function Definition for Dummies%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-In most cases, defining a recursive function is just as simple as other definitions:%
+In most cases, defining a recursive function is just as simple as other definitions:
+
+  Like in functional programming, a function definition consists of a%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{fun}\isamarkupfalse%
@@ -39,11 +37,16 @@
 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-The function always terminates, since the argument of gets smaller in every
-  recursive call. Termination is an
-  important requirement, since it prevents inconsistencies: From
-  the "definition" \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove 
-  \isa{{\isadigit{0}}\ \ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.
+The syntax is rather self-explanatory: We introduce a function by
+  giving its name, its type and a set of defining recursive
+  equations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The function always terminates, since its argument gets smaller in
+  every recursive call. Termination is an important requirement, since
+  it prevents inconsistencies: From the "definition" \isa{f{\isacharparenleft}n{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}n{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}} we could prove \isa{{\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}} by subtracting \isa{f{\isacharparenleft}n{\isacharparenright}} on both sides.
 
   Isabelle tries to prove termination automatically when a function is
   defined. We will later look at cases where this fails and see what to
@@ -57,8 +60,8 @@
 %
 \begin{isamarkuptext}%
 \label{patmatch}
-  Like in functional programming, functions can be defined by pattern
-  matching. At the moment we will only consider \emph{datatype
+  Like in functional programming, we can use pattern matching to
+  define functions. At the moment we will only consider \emph{constructor
   patterns}, which only consist of datatype constructors and
   variables.
 
@@ -235,7 +238,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
-\ \isanewline
+\ sum\isanewline
 %
 \isadelimproof
 %
@@ -252,7 +255,11 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-The \isa{relation} method takes a relation of
+The \cmd{termination} command sets up the termination goal for the
+  specified function \isa{sum}. If the function name is omitted it
+  implicitly refers to the last function definition.
+
+  The \isa{relation} method takes a relation of
   type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}, where \isa{{\isacharprime}a} is the argument type of
   the function. If the function has multiple curried arguments, then
   these are packed together into a tuple, as it happened in the above
@@ -320,6 +327,71 @@
 %
 \endisadelimproof
 %
+\isamarkupsubsection{Manual Termination Proofs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \isa{relation} method is often useful, but not
+  necessary. Since termination proofs are just normal Isabelle proofs,
+  they can also be carried out manually:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{function}\isamarkupfalse%
+\ id\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}id\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}id\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}id\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ pat{\isacharunderscore}completeness\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{termination}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ \isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}wf\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ n\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}n{\isacharcomma}\ Suc\ n{\isacharparenright}\ {\isasymin}\ less{\isacharunderscore}than{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Of course this is just a trivial example, but manual proofs can
+  sometimes be the only choice if faced with very hard termination problems.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Mutual Recursion%
 }
 \isamarkuptrue%
@@ -506,8 +578,8 @@
   shows the problem:
   
   Suppose we are modelling incomplete knowledge about the world by a
-  three-valued datatype, which has values for \isa{T}, \isa{F}
-  and \isa{X} for true, false and uncertain propositions.%
+  three-valued datatype, which has values \isa{T}, \isa{F}
+  and \isa{X} for true, false and uncertain propositions, respectively.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{datatype}\isamarkupfalse%
@@ -520,10 +592,10 @@
 \ And\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline
 \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}And\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
+{\isacharbar}\ {\isachardoublequoteopen}And\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 This definition is useful, because the equations can directly be used
   as rules to simplify expressions. But the patterns overlap, e.g.~the
@@ -544,15 +616,15 @@
 And\ X\ X\ {\isacharequal}\ X}
   
   \vspace*{1em}
-  \noindent There are several problems with this approach:
+  \noindent There are several problems with this:
 
   \begin{enumerate}
   \item When datatypes have many constructors, there can be an
   explosion of equations. For \isa{And}, we get seven instead of
-  five equation, which can be tolerated, but this is just a small
+  five equations, which can be tolerated, but this is just a small
   example.
 
-  \item Since splitting makes the equations "more special", they
+  \item Since splitting makes the equations "less general", they
   do not always match in rewriting. While the term \isa{And\ x\ F}
   can be simplified to \isa{F} by the original specification, a
   (manual) case split on \isa{x} is now necessary.
@@ -568,7 +640,7 @@
   both \isa{f\ x\ {\isacharequal}\ True} and \isa{f\ x\ {\isacharequal}\ False} is a bad
   idea. So if we don't want Isabelle to mangle our definitions, we
   will have to prove that this is not necessary. By using the full
-  definition form withour the \cmd{sequential} option, we get this
+  definition form without the \cmd{sequential} option, we get this
   behaviour:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -576,10 +648,10 @@
 \ And{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}\ {\isasymRightarrow}\ P{\isadigit{3}}{\isachardoublequoteclose}\isanewline
 \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}And{\isadigit{2}}\ T\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
+{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ T\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ p\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ F\ p\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}And{\isadigit{2}}\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}%
 \isadelimproof
 %
 \endisadelimproof
@@ -642,15 +714,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Non-constructor patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Partiality%
 }
 \isamarkuptrue%
@@ -659,8 +722,490 @@
 In HOL, all functions are total. A function \isa{f} applied to
   \isa{x} always has a value \isa{f\ x}, and there is no notion
   of undefinedness. 
+  
+  This property of HOL is the reason why we have to do termination
+  proofs when defining functions: The termination proof justifies the
+  definition of the function by wellfounded recursion.
 
-  FIXME%
+  However, the \cmd{function} package still supports partiality. Let's
+  look at the following function which searches for a zero in the
+  function f.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{function}\isamarkupfalse%
+\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ {\isacharparenleft}if\ f\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ pat{\isacharunderscore}completeness\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Clearly, any attempt of a termination proof must fail. And without
+  that, we do not get the usual rules \isa{findzero{\isachardot}simp} and 
+  \isa{findzero{\isachardot}induct}. So what was the definition good for at all?%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Domain predicates%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The trick is that Isabelle has not only defined the function \isa{findzero}, but also
+  a predicate \isa{findzero{\isacharunderscore}dom} that characterizes the values where the function
+  terminates: the \emph{domain} of the function. In Isabelle/HOL, a
+  partial function is just a total function with an additional domain
+  predicate. Like with total functions, we get simplification and
+  induction rules, but they are guarded by the domain conditions and
+  called \isa{psimps} and \isa{pinduct}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ findzero{\isachardot}psimps%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
+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}%
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ findzero{\isachardot}pinduct%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharparenright}{\isacharsemicolon}\isanewline
+\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
+{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}a{\isadigit{0}}{\isachardot}{\isadigit{0}}\ {\isacharquery}a{\isadigit{1}}{\isachardot}{\isadigit{0}}%
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As already mentioned, HOL does not support true partiality. All we
+  are doing here is using some tricks to make a total function appear
+  as if it was partial. We can still write the term \isa{findzero\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isacharparenright}\ {\isadigit{0}}} and like any other term of type \isa{nat} it is equal
+  to some natural number, although we might not be able to find out
+  which one (we will discuss this further in \S\ref{default}). The
+  function is \emph{underdefined}.
+
+  But it is enough defined to prove something about it. We can prove
+  that if \isa{findzero\ f\ n}
+  it terminates, it indeed returns a zero of \isa{f}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ findzero{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+We apply induction as usual, but using the partial induction
+  rule:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}induct\ f\ n\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}%
+\begin{isamarkuptxt}%
+This gives the following subgoals:
+
+  \begin{isabelle}%
+\ {\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
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}f\ n{\isachardot}\ }{\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}%
+\end{isabelle}
+
+  The premise in our lemma was used to satisfy the first premise in
+  the induction rule. However, now we can also use \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as an assumption in the induction step. This
+  allows to unfold \isa{findzero\ f\ n} using the \isa{psimps}
+  rule, and the rest is trivial. Since \isa{psimps} rules carry the
+  \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Proofs about partial functions are often not harder than for total
+  functions. Fig.~\ref{findzero_isar} shows a slightly more
+  complicated proof written in Isar. It is verbose enough to show how
+  partiality comes into play: From the partial induction, we get an
+  additional domain condition hypothesis. Observe how this condition
+  is applied when calls to \isa{findzero} are unfolded.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymlbrakk}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}induct\ rule{\isacharcolon}\ findzero{\isachardot}pinduct{\isacharparenright}\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ f\ n\ \isacommand{assume}\isamarkupfalse%
+\ dom{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharsemicolon}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ x{\isacharunderscore}range{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ \ \isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ \isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}f\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ dom\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse%
+\ False\ \isacommand{by}\isamarkupfalse%
+\ auto\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\ \ \isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ x{\isacharunderscore}range\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ n\ {\isasymor}\ x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ auto\isanewline
+\ \ \isacommand{thus}\isamarkupfalse%
+\ {\isachardoublequoteopen}f\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n{\isachardot}{\isachardot}{\isacharless}findzero\ f\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{A proof about a partial function}\label{findzero_isar}
+\end{figure}
+%
+\isamarkupsubsection{Partial termination proofs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Now that we have proved some interesting properties about our
+  function, we should turn to the domain predicate and see if it is
+  actually true for some values. Otherwise we would have just proved
+  lemmas with \isa{False} as a premise.
+
+  Essentially, we need some introduction rules for \isa{findzero{\isacharunderscore}dom}. The function package can prove such domain
+  introduction rules automatically. But since they are not used very
+  often (they are almost never needed if the function is total), they
+  are disabled by default for efficiency reasons. So we have to go
+  back and ask for them explicitly by passing the \isa{{\isacharparenleft}domintros{\isacharparenright}} option to the function package:
+
+\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%
+\cmd{where}\isanewline%
+\ \ \ldots\\
+\cmd{by} \isa{pat{\isacharunderscore}completeness\ auto}\\%
+
+
+  Now the package has proved an introduction rule for \isa{findzero{\isacharunderscore}dom}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ findzero{\isachardot}domintros%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+\end{isabelle}
+
+  Domain introduction rules allow to show that a given value lies in the
+  domain of a function, if the arguments of all recursive calls
+  are in the domain as well. They allow to do a \qt{single step} in a
+  termination proof. Usually, you want to combine them with a suitable
+  induction principle.
+
+  Since our function increases its argument at recursive calls, we
+  need an induction principle which works \qt{backwards}. We will use
+  \isa{inc{\isacharunderscore}induct}, which allows to do induction from a fixed number
+  \qt{downwards}:
+
+  \begin{isabelle}%
+{\isasymlbrakk}{\isacharquery}i\ {\isasymle}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}j{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ {\isacharquery}j{\isacharsemicolon}\ {\isacharquery}P\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}i%
+\end{isabelle}
+
+  Fig.~\ref{findzero_term} gives a detailed Isar proof of the fact
+  that \isa{findzero} terminates if there is a zero which is greater
+  or equal to \isa{n}. First we derive two useful rules which will
+  solve the base case and the step case of the induction. The
+  induction is then straightforward, except for the unusal induction
+  principle.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+\isacommand{lemma}\isamarkupfalse%
+\ findzero{\isacharunderscore}termination{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline
+\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\ \isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ base{\isacharcolon}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}{\isacharbackquoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isacharbackquoteclose}{\isacharparenright}\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ step{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i{\isachardot}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}\ \isanewline
+\ \ \ \ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ findzero{\isachardot}domintros{\isacharparenright}\ simp\isanewline
+\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ {\isacharbackquoteopen}x\ {\isasymge}\ n{\isacharbackquoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ base{\isacharparenright}\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ i\ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ Suc\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{thus}\isamarkupfalse%
+\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ i{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ step{\isacharparenright}\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{Termination proof for \isa{findzero}}\label{findzero_term}
+\end{figure}
+%
+\begin{isamarkuptext}%
+Again, the proof given in Fig.~\ref{findzero_term} has a lot of
+  detail in order to explain the principles. Using more automation, we
+  can also have a short proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ findzero{\isacharunderscore}termination{\isacharunderscore}short{\isacharcolon}\isanewline
+\ \ \isakeyword{assumes}\ zero{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isachargreater}{\isacharequal}\ n{\isachardoublequoteclose}\ \isanewline
+\ \ \isakeyword{assumes}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ zero\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ rule{\isacharcolon}inc{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ intro{\isacharcolon}\ findzero{\isachardot}domintros{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+It is simple to combine the partial correctness result with the
+  termination lemma:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ findzero{\isacharunderscore}total{\isacharunderscore}correctness{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}f\ x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}findzero\ f\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}blast\ intro{\isacharcolon}\ findzero{\isacharunderscore}zero\ findzero{\isacharunderscore}termination{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Definition of the domain predicate%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sometimes it is useful to know what the definition of the domain
+  predicate actually is. Actually, \isa{findzero{\isacharunderscore}dom} is just an
+  abbreviation:
+
+  \begin{isabelle}%
+findzero{\isacharunderscore}dom\ {\isasymequiv}\ acc\ findzero{\isacharunderscore}rel%
+\end{isabelle}
+
+  The domain predicate is the accessible part of a relation \isa{findzero{\isacharunderscore}rel}, which was also created internally by the function
+  package. \isa{findzero{\isacharunderscore}rel} is just a normal
+  inductively defined predicate, so we can inspect its definition by
+  looking at the introduction rules \isa{findzero{\isacharunderscore}rel{\isachardot}intros}.
+  In our case there is just a single rule:
+
+  \begin{isabelle}%
+{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}rel\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+\end{isabelle}
+
+  The relation \isa{findzero{\isacharunderscore}rel}, expressed as a binary predicate,
+  describes the \emph{recursion relation} of the function
+  definition. The recursion relation is a binary relation on
+  the arguments of the function that relates each argument to its
+  recursive calls. In general, there is one introduction rule for each
+  recursive call.
+
+  The predicate \isa{findzero{\isacharunderscore}dom} is the \emph{accessible part} of
+  that relation. An argument belongs to the accessible part, if it can
+  be reached in a finite number of steps. 
+
+  Since the domain predicate is just an abbreviation, you can use
+  lemmas for \isa{acc} and \isa{findzero{\isacharunderscore}rel} directly. Some
+  lemmas which are occasionally useful are \isa{accI}, \isa{acc{\isacharunderscore}downward}, and of course the introduction and elimination rules
+  for the recursion relation \isa{findzero{\isachardot}intros} and \isa{findzero{\isachardot}cases}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{A Useful Special Case: Tail recursion%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The domain predicate is our trick that allows us to model partiality
+  in a world of total functions. The downside of this is that we have
+  to carry it around all the time. The termination proof above allowed
+  us to replace the abstract \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} by the more
+  concrete \isa{n\ {\isasymle}\ x\ {\isasymand}\ f\ x\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}b{\isacharparenright}}, but the condition is still
+  there and it won't go away soon. 
+
+  In particular, the domain predicate guard the unfolding of our
+  function, since it is there as a condition in the \isa{psimp}
+  rules. 
+
+  On the other hand, we must be happy about the domain predicate,
+  since it guarantees that all this is at all possible without losing
+  consistency. 
+
+  Now there is an important special case: We can actually get rid
+  of the condition in the simplification rules, \emph{if the function
+  is tail-recursive}. The reason is that for all tail-recursive
+  equations there is a total function satisfying them, even if they
+  are non-terminating. 
+
+  The function package internally does the right construction and can
+  derive the unconditional simp rules, if we ask it to do so. Luckily,
+  our \isa{findzero} function is tail-recursive, so we can just go
+  back and add another option to the \cmd{function} command:
+
+\noindent\cmd{function} \isa{{\isacharparenleft}domintros{\isacharcomma}\ tailrec{\isacharparenright}\ findzero\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}}\\%
+\cmd{where}\isanewline%
+\ \ \ldots\\%
+
+  
+  Now, we actually get the unconditional simplification rules, even
+  though the function is partial:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ findzero{\isachardot}simps%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+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}%
+\end{isabelle}
+
+  Of course these would make the simplifier loop, so we better remove
+  them from the simpset:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ findzero{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
+\begin{isamarkuptext}%
+\fixme{Code generation ???}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -669,7 +1214,507 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+Recursive calls which are nested in one another frequently cause
+  complications, since their termination proof can depend on a partial
+  correctness property of the function itself. 
+
+  As a small example, we define the \qt{nested zero} function:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{function}\isamarkupfalse%
+\ nz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}nz\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}nz\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ nz\ {\isacharparenleft}nz\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ pat{\isacharunderscore}completeness\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+If we attempt to prove termination using the identity measure on
+  naturals, this fails:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{termination}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isacommand{apply}\isamarkupfalse%
+\ auto%
+\begin{isamarkuptxt}%
+We get stuck with the subgoal
+
+  \begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharless}\ Suc\ n%
+\end{isabelle}
+
+  Of course this statement is true, since we know that \isa{nz} is
+  the zero function. And in fact we have no problem proving this
+  property by induction.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharcolon}\ {\isachardoublequoteopen}nz{\isacharunderscore}dom\ n\ {\isasymLongrightarrow}\ nz\ n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+We formulate this as a partial correctness lemma with the condition
+  \isa{nz{\isacharunderscore}dom\ n}. This allows us to prove it with the \isa{pinduct} rule before we have proved termination. With this lemma,
+  the termination proof works as expected:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{termination}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isacharunderscore}is{\isacharunderscore}zero{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+As a general strategy, one should prove the statements needed for
+  termination as a partial property first. Then they can be used to do
+  the termination proof. This also works for less trivial
+  examples. Figure \ref{f91} defines the well-known 91-function by
+  McCarthy \cite{?} and proves its termination.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{figure}
+\begin{center}
+\begin{minipage}{0.8\textwidth}
+\isabellestyle{it}
+\isastyle\isamarkuptrue
+\isacommand{function}\isamarkupfalse%
+\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n\ then\ n\ {\isacharminus}\ {\isadigit{1}}{\isadigit{0}}\ else\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ pat{\isacharunderscore}completeness\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate{\isacharcolon}\ \isanewline
+\ \ \isakeyword{assumes}\ trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ n{\isachardoublequoteclose}\ \isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ trm\ \isacommand{by}\isamarkupfalse%
+\ induct\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{termination}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{let}\isamarkupfalse%
+\ {\isacharquery}R\ {\isacharequal}\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{1}}\ {\isacharminus}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}wf\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isachardoublequoteclose}\ %
+\isamarkupcmt{Assumptions for both calls%
+}
+\isanewline
+\isanewline
+\ \ \isacommand{thus}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharcomma}\ n{\isacharparenright}\ {\isasymin}\ {\isacharquery}R{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\ %
+\isamarkupcmt{Inner call%
+}
+\isanewline
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ inner{\isacharunderscore}trm{\isacharcolon}\ {\isachardoublequoteopen}f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}dom\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ %
+\isamarkupcmt{Outer call%
+}
+\isanewline
+\ \ \isacommand{with}\isamarkupfalse%
+\ f{\isadigit{9}}{\isadigit{1}}{\isacharunderscore}estimate\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}\ {\isacharless}\ f{\isadigit{9}}{\isadigit{1}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{with}\isamarkupfalse%
+\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharless}\ n{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\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%
+\ simp\ \isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupfalse\isabellestyle{tt}
+\end{minipage}\end{center}
+\caption{McCarthy's 91-function}\label{f91}
+\end{figure}
+%
+\isamarkupsection{Higher-Order Recursion%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Higher-order recursion occurs when recursive calls
+  are passed as arguments to higher-order combinators such as \isa{map}, \isa{filter} etc.
+  As an example, imagine a data type of n-ary trees:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ tree\ {\isacharequal}\ \isanewline
+\ \ Leaf\ {\isacharprime}a\ \isanewline
+{\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ list{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent We can define a map function for trees, using the predefined
+  map function for lists.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{function}\isamarkupfalse%
+\ treemap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ {\isacharparenleft}f\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}treemap\ f\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}map\ {\isacharparenleft}treemap\ f{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ pat{\isacharunderscore}completeness\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+We do the termination proof manually, to point out what happens
+  here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+As usual, we have to give a wellfounded relation, such that the
+  arguments of the recursive calls get smaller. But what exactly are
+  the arguments of the recursive calls? Isabelle gives us the
+  subgoals
+
+  \begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ wf\ {\isacharquery}R\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ f{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R%
+\end{isabelle} 
+
+  So Isabelle seems to know that \isa{map} behaves nicely and only
+  applies the recursive call \isa{treemap\ f} to elements
+  of \isa{l}. Before we discuss where this knowledge comes from,
+  let us finish the termination proof:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ f\ l\ \isakeyword{and}\ x\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{thus}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}f{\isacharcomma}\ Branch\ l{\isacharparenright}{\isacharparenright}\ {\isasymin}\ measure\ {\isacharparenleft}size\ o\ snd{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ simp%
+\begin{isamarkuptxt}%
+Simplification returns the following subgoal: 
+
+      \begin{isabelle}%
+\ {\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}%
+\end{isabelle} 
+
+      We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the
+      definition of the \isa{tree} type. We should go back and prove
+      it, by induction.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \ \ \isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\ \ \isacommand{lemma}\isamarkupfalse%
+\ 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
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Now the whole termination proof is automatic:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \isacommand{termination}\isamarkupfalse%
+\ \isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ lexicographic{\isacharunderscore}order%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Congruence Rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Let's come back to the question how Isabelle knows about \isa{map}.
+
+  The knowledge about map is encoded in so-called congruence rules,
+  which are special theorems known to the \cmd{function} command. The
+  rule for map is
+
+  \begin{isabelle}%
+{\isasymlbrakk}{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys%
+\end{isabelle}
+
+  You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions
+  coincide on the elements of the list. This means that for the value 
+  \isa{map\ f\ l} we only have to know how \isa{f} behaves on
+  \isa{l}.
+
+  Usually, one such congruence rule is
+  needed for each higher-order construct that is used when defining
+  new functions. In fact, even basic functions like \isa{If} and \isa{Let} are handeled by this mechanism. The congruence
+  rule for \isa{If} states that the \isa{then} branch is only
+  relevant if the condition is true, and the \isa{else} branch only if it
+  is false:
+
+  \begin{isabelle}%
+{\isasymlbrakk}{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c{\isacharsemicolon}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v{\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}\ {\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}%
+\end{isabelle}
+  
+  Congruence rules can be added to the
+  function package by giving them the \isa{fundef{\isacharunderscore}cong} attribute.
+
+  Isabelle comes with predefined congruence rules for most of the
+  definitions.
+  But if you define your own higher-order constructs, you will have to
+  come up with the congruence rules yourself, if you want to use your
+  functions in recursive definitions. Since the structure of
+  congruence rules is a little unintuitive, here are some exercises:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{exercise}
+    Find a suitable congruence rule for the following function which
+  maps only over the even numbers in a list:
+
+  \begin{isabelle}%
+mapeven\ {\isacharquery}f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isasep\isanewline%
+mapeven\ {\isacharquery}f\ {\isacharparenleft}{\isacharquery}x\ {\isacharhash}\ {\isacharquery}xs{\isacharparenright}\ {\isacharequal}\isanewline
+{\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}%
+\end{isabelle}
+  \end{exercise}
+  
+  \begin{exercise}
+  What happens if the congruence rule for \isa{If} is
+  disabled by declaring \isa{if{\isacharunderscore}cong{\isacharbrackleft}fundef{\isacharunderscore}cong\ del{\isacharbrackright}}?
+  \end{exercise}
+
+  Note that in some cases there is no \qt{best} congruence rule.
+  \fixme%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Appendix: Predefined Congruence Rules%
+}
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsubsection{Basic Control Structures%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}b\ {\isacharequal}\ {\isacharquery}c}\\\ \mbox{{\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}u}\\\ \mbox{{\isasymnot}\ {\isacharquery}c\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isacharequal}\ {\isacharquery}v}}{\mbox{{\isacharparenleft}if\ {\isacharquery}b\ then\ {\isacharquery}x\ else\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharquery}c\ then\ {\isacharquery}u\ else\ {\isacharquery}v{\isacharparenright}}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{Let\ {\isacharquery}M\ {\isacharquery}f\ {\isacharequal}\ Let\ {\isacharquery}N\ {\isacharquery}g}}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Data Types%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For each \cmd{datatype} definition, a congruence rule for the case
+  combinator is registeres automatically. Here are the rules for
+  \isa{nat} and \isa{list}:
+
+\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}nat{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ Suc\ nat\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ nat}}{\mbox{nat{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ nat{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center}
+
+\begin{center}\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}M{\isacharprime}}\\\ \mbox{{\isacharquery}M{\isacharprime}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharequal}\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}}\\\ \mbox{{\isasymAnd}a\ list{\isachardot}\ {\isacharquery}M{\isacharprime}\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list\ {\isacharequal}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ a\ list}}{\mbox{list{\isacharunderscore}case\ {\isacharquery}f{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}f{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M\ {\isacharequal}\ list{\isacharunderscore}case\ {\isacharquery}g{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}g{\isadigit{2}}{\isachardot}{\isadigit{0}}\ {\isacharquery}M{\isacharprime}}}}\end{center}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{List combinators%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{map\ {\isacharquery}f\ {\isacharquery}xs\ {\isacharequal}\ map\ {\isacharquery}g\ {\isacharquery}ys}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}xs\ {\isacharequal}\ {\isacharquery}ys}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}ys\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{filter\ {\isacharquery}P\ {\isacharquery}xs\ {\isacharequal}\ filter\ {\isacharquery}Q\ {\isacharquery}ys}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ a\ {\isacharequal}\ {\isacharquery}g\ x\ a}}{\mbox{foldr\ {\isacharquery}f\ {\isacharquery}l\ {\isacharquery}a\ {\isacharequal}\ foldr\ {\isacharquery}g\ {\isacharquery}k\ {\isacharquery}b}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}a\ {\isacharequal}\ {\isacharquery}b}\\\ \mbox{{\isacharquery}l\ {\isacharequal}\ {\isacharquery}k}\\\ \mbox{{\isasymAnd}a\ x{\isachardot}\ x\ {\isasymin}\ set\ {\isacharquery}l\ {\isasymLongrightarrow}\ {\isacharquery}f\ a\ x\ {\isacharequal}\ {\isacharquery}g\ a\ x}}{\mbox{foldl\ {\isacharquery}f\ {\isacharquery}a\ {\isacharquery}l\ {\isacharequal}\ foldl\ {\isacharquery}g\ {\isacharquery}b\ {\isacharquery}k}}}
+
+Similar: takewhile, dropwhile%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Sets%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ {\isacharequal}\ {\isacharquery}Q\ x}}{\mbox{{\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}A{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}x{\isasymin}{\isacharquery}B{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymUnion}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}A\ {\isacharequal}\ {\isacharquery}B}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}B\ {\isasymLongrightarrow}\ {\isacharquery}C\ x\ {\isacharequal}\ {\isacharquery}D\ x}}{\mbox{{\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}A\isactrlesub \ {\isacharquery}C\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymInter}\isactrlbsub x{\isasymin}{\isacharquery}B\isactrlesub \ {\isacharquery}D\ x{\isacharparenright}}}}
+
+\isa{\mbox{}\inferrule{\mbox{{\isacharquery}M\ {\isacharequal}\ {\isacharquery}N}\\\ \mbox{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}N\ {\isasymLongrightarrow}\ {\isacharquery}f\ x\ {\isacharequal}\ {\isacharquery}g\ x}}{\mbox{{\isacharquery}f\ {\isacharbackquote}\ {\isacharquery}M\ {\isacharequal}\ {\isacharquery}g\ {\isacharbackquote}\ {\isacharquery}N}}}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Thu May 17 23:00:06 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Thu May 17 23:03:47 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip

--- a/doc-src/IsarAdvanced/Functions/functions.tex	Thu May 17 23:00:06 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/functions.tex	Thu May 17 23:03:47 2007 +0200
@@ -1,14 +1,21 @@
 
 %% $Id$
 
-\documentclass[12pt,a4paper,fleqn]{report}
+\documentclass[11pt,a4paper,fleqn]{article}
+\textwidth  15.93cm
+\textheight 24cm
+\oddsidemargin  0.0cm
+\evensidemargin 0.0cm
+\topmargin  0.0cm
+
 \usepackage{latexsym,graphicx}
-\usepackage{listings}
 \usepackage[refpage]{nomencl}
 \usepackage{../../iman,../../extra,../../isar,../../proof}
 \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
 \usepackage{style}
 \usepackage{Thy/document/pdfsetup}
+\usepackage{mathpartir}
+\usepackage{amsthm}
 
 \newcommand{\cmd}[1]{\isacommand{#1}}
 
@@ -45,17 +52,15 @@
 \newcommand{\strong}[1]{{\bfseries #1}}
 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
 
-\lstset{basicstyle=\scriptsize\ttfamily, keywordstyle=\itshape, commentstyle=\itshape\sffamily, frame=shadowbox}
-\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
-\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
+\newtheorem{exercise}{Exercise}{\bf}{\itshape}
+%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}
 
 \hyphenation{Isabelle}
 \hyphenation{Isar}
 
 \isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar}
-  \\[4ex] Defining Recursive Functions in Isabelle/HOL}
-\author{\emph{Alexander Krauss}}
+\title{Defining Recursive Functions in Isabelle/HOL}
+\author{Alexander Krauss}
 
 
 \isabellestyle{tt}
@@ -66,16 +71,19 @@
 
 \begin{abstract}
   This tutorial describes the use of the new \emph{function} package,
-  starting with very simple examples and the proceeding to the more
-  intricate ones. No familiarity with other definition facilities is
-  assumed.
+	which provides general recursive function definitions for Isabelle/HOL.
+	
+
+%  starting with very simple examples and the proceeding to the more
+%  intricate ones.
 \end{abstract}
 
-\thispagestyle{empty}\clearpage
+%\thispagestyle{empty}\clearpage
 
-\pagenumbering{roman}
-\clearfirst
+%\pagenumbering{roman}
+%\clearfirst
 
+\input{intro.tex}
 \input{Thy/document/Functions.tex}
 
 \begingroup

--- a/src/HOL/IsaMakefile	Thu May 17 23:00:06 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu May 17 23:03:47 2007 +0200
@@ -636,9 +636,9 @@
   ex/Reflection.thy ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy		\
   ex/Records.thy ex/Reflected_Presburger.thy ex/Refute_Examples.thy		\
   ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy 			\
-  ex/Sudoku.thy ex/Tarski.thy ex/document/root.bib ex/document/root.tex		\
-  ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML ex/set.thy		\
-  ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
+  ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib		\
+  ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML 	\
+  ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex