--- 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}
+
+
+*}