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

-(*  Title:      Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
-    ID:         $Id$
+(*  Title:      doc-src/IsarAdvanced/Functions/Thy/Fundefs.thy
     Author:     Alexander Krauss, TU Muenchen
 
 Tutorial for function definitions with the new "function" package.
 *)
 

 by pat_completeness auto
 (*<*)declare findzero.simps[simp del](*>*)
 
 text {*
   \noindent Clearly, any attempt of a termination proof must fail. And without
-  that, we do not get the usual rules @{text "findzero.simp"} and 
+  that, we do not get the usual rules @{text "findzero.simps"} and 
   @{text "findzero.induct"}. So what was the definition good for at all?
 *}
 
 subsection {* Domain predicates *}
 

   recursive call.
 
   The predicate @{term "accp findzero_rel"} is the accessible part of
   that relation. An argument belongs to the accessible part, if it can
   be reached in a finite number of steps (cf.~its definition in @{text
-  "Accessible_Part.thy"}).
+  "Wellfounded.thy"}).
 
   Since the domain predicate is just an abbreviation, you can use
   lemmas for @{const accp} and @{const findzero_rel} directly. Some
   lemmas which are occasionally useful are @{text accpI}, @{text
   accp_downward}, and of course the introduction and elimination rules

 
 section {* Higher-Order Recursion *}
 
 text {*
   Higher-order recursion occurs when recursive calls
-  are passed as arguments to higher-order combinators such as @{term
+  are passed as arguments to higher-order combinators such as @{const
   map}, @{term filter} etc.
   As an example, imagine a datatype of n-ary trees:
 *}
 
 datatype 'a tree = 

   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 when mirror is given as an
-  argument to map? Isabelle gives us the
+  argument to @{const map}? Isabelle gives us the
   subgoals
 
   @{subgoals[display,indent=0]} 
 
   So the system seems to know that @{const map} only
   applies the recursive call @{term "mirror"} to elements
   of @{term "l"}, which is essential for the termination proof.
 
-  This knowledge about map is encoded in so-called congruence rules,
+  This knowledge about @{const map} is encoded in so-called congruence rules,
   which are special theorems known to the \cmd{function} command. The
-  rule for map is
+  rule for @{const 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