doc-src/IsarAdvanced/Functions/Thy/Functions.thy

 
 theory Functions
 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
   "fib 0 = 1"
 | "fib (Suc 0) = 1"
 | "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
   do then.
 *}
 
 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.
 
   If patterns overlap, the order of the equations is taken into
   account. The following function inserts a fixed element between any

   simplification:
 *}
 
 lemma "sep (0::nat) [1, 2, 3] = [1, 0, 2, 0, 3]"
 by simp
-
-  
 
 subsection {* Induction *}
 
 text {*
 

   @{text "N + 1 - i"} decreases in every recursive call.
 
   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
   these are packed together into a tuple, as it happened in the above
   example.

 *}
 
 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 *}
 
 text {*
   If two or more functions call one another mutually, they have to be defined

   This splitting can significantly increase the number of equations
   involved, and is not always necessary. The following simple example
   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
 
 text {* Then the conjunction of such values can be defined as follows: *}
 
 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 {* 
   This definition is useful, because the equations can directly be used
   as rules to simplify expressions. But the patterns overlap, e.g.~the

 
 text {*
   @{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.
 
   \item The splitting also concerns the induction rule @{text

 
   On the other hand, a definition needs to be consistent and defining
   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
   function definition. In this case, they are:
 

 subsection {* Non-constructor patterns *}
 
 text {* FIXME *}
 
 
-subsection {* Non-constructor patterns *}
-
-text {* FIXME *}
-
-
-
-
 
 
 section {* Partiality *}
 
 text {* 
   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. 
-
-  FIXME
-*}
-
-
-
   
+  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.
+
+  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. *}
   
-
-
-
-
-
- FIXME *}
-
-
-
-
-
-
+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
+
+*}
+
+
+
+
+
+
+
+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}
+
+
+*}
+
+
+
+
+
+
+end