1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Thu Jul 26 18:23:38 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Aug 03 18:04:55 2001 +0200
     1.3 @@ -3,11 +3,12 @@
     1.4  (*>*)
     1.5  
     1.6  text{*
     1.7 -Once we have succeeded in proving all termination conditions, the recursion
     1.8 -equations become simplification rules, just as with
     1.9 +Once we have proved all the termination conditions, the \isacommand{recdef} 
    1.10 +recursion equations become simplification rules, just as with
    1.11  \isacommand{primrec}. In most cases this works fine, but there is a subtle
    1.12  problem that must be mentioned: simplification may not
    1.13  terminate because of automatic splitting of @{text if}.
    1.14 +\index{*if expressions!splitting of}
    1.15  Let us look at an example:
    1.16  *}
    1.17  
    1.18 @@ -24,8 +25,9 @@
    1.19  rule. Of course the equation is nonterminating if we are allowed to unfold
    1.20  the recursive call inside the @{text else} branch, which is why programming
    1.21  languages and our simplifier don't do that. Unfortunately the simplifier does
    1.22 -something else which leads to the same problem: it splits @{text if}s if the
    1.23 -condition simplifies to neither @{term True} nor @{term False}. For
    1.24 +something else that leads to the same problem: it splits 
    1.25 +each @{text if}-expression unless its
    1.26 +condition simplifies to @{term True} or @{term False}.  For
    1.27  example, simplification reduces
    1.28  @{term[display]"gcd(m,n) = k"}
    1.29  in one step to
    1.30 @@ -37,9 +39,10 @@
    1.31  simplification steps. Fortunately, this problem can be avoided in many
    1.32  different ways.
    1.33  
    1.34 -The most radical solution is to disable the offending @{thm[source]split_if}
    1.35 +The most radical solution is to disable the offending theorem
    1.36 +@{thm[source]split_if},
    1.37  as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    1.38 -because it means you will often have to invoke the rule explicitly when
    1.39 +approach: you will often have to invoke the rule explicitly when
    1.40  @{text if} is involved.
    1.41  
    1.42  If possible, the definition should be given by pattern matching on the left
    1.43 @@ -54,12 +57,12 @@
    1.44  
    1.45  
    1.46  text{*\noindent
    1.47 -Note that the order of equations is important and hides the side condition
    1.48 -@{prop"n ~= 0"}. Unfortunately, in general the case distinction
    1.49 +The order of equations is important: it hides the side condition
    1.50 +@{prop"n ~= 0"}.  Unfortunately, in general the case distinction
    1.51  may not be expressible by pattern matching.
    1.52  
    1.53 -A very simple alternative is to replace @{text if} by @{text case}, which
    1.54 -is also available for @{typ bool} but is not split automatically:
    1.55 +A simple alternative is to replace @{text if} by @{text case}, 
    1.56 +which is also available for @{typ bool} and is not split automatically:
    1.57  *}
    1.58  
    1.59  consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
    1.60 @@ -67,7 +70,8 @@
    1.61    "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
    1.62  
    1.63  text{*\noindent
    1.64 -In fact, this is probably the neatest solution next to pattern matching.
    1.65 +This is probably the neatest solution next to pattern matching, and it is
    1.66 +always available.
    1.67  
    1.68  A final alternative is to replace the offending simplification rules by
    1.69  derived conditional ones. For @{term gcd} it means we have to prove
    1.70 @@ -77,11 +81,14 @@
    1.71  lemma [simp]: "gcd (m, 0) = m";
    1.72  apply(simp);
    1.73  done
    1.74 +
    1.75  lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
    1.76  apply(simp);
    1.77  done
    1.78  
    1.79  text{*\noindent
    1.80 +Simplification terminates for these proofs because the condition of the @{text
    1.81 +if} simplifies to @{term True} or @{term False}.
    1.82  Now we can disable the original simplification rule:
    1.83  *}
    1.84