src/Doc/Tutorial/Recdef/simplification.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 62392 747d36865c2c
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)
     2 theory simplification imports Main begin
     3 (*>*)
     4 
     5 text{*
     6 Once we have proved all the termination conditions, the \isacommand{recdef} 
     7 recursion equations become simplification rules, just as with
     8 \isacommand{primrec}. In most cases this works fine, but there is a subtle
     9 problem that must be mentioned: simplification may not
    10 terminate because of automatic splitting of @{text "if"}.
    11 \index{*if expressions!splitting of}
    12 Let us look at an example:
    13 *}
    14 
    15 consts gcd :: "nat\<times>nat \<Rightarrow> nat"
    16 recdef gcd "measure (\<lambda>(m,n).n)"
    17   "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    18 
    19 text{*\noindent
    20 According to the measure function, the second argument should decrease with
    21 each recursive call. The resulting termination condition
    22 @{term[display]"n ~= (0::nat) ==> m mod n < n"}
    23 is proved automatically because it is already present as a lemma in
    24 HOL\@.  Thus the recursion equation becomes a simplification
    25 rule. Of course the equation is nonterminating if we are allowed to unfold
    26 the recursive call inside the @{text else} branch, which is why programming
    27 languages and our simplifier don't do that. Unfortunately the simplifier does
    28 something else that leads to the same problem: it splits 
    29 each @{text "if"}-expression unless its
    30 condition simplifies to @{term True} or @{term False}.  For
    31 example, simplification reduces
    32 @{term[display]"gcd(m,n) = k"}
    33 in one step to
    34 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
    35 where the condition cannot be reduced further, and splitting leads to
    36 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    37 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    38 an @{text "if"}, it is unfolded again, which leads to an infinite chain of
    39 simplification steps. Fortunately, this problem can be avoided in many
    40 different ways.
    41 
    42 The most radical solution is to disable the offending theorem
    43 @{thm[source]split_if},
    44 as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
    45 approach: you will often have to invoke the rule explicitly when
    46 @{text "if"} is involved.
    47 
    48 If possible, the definition should be given by pattern matching on the left
    49 rather than @{text "if"} on the right. In the case of @{term gcd} the
    50 following alternative definition suggests itself:
    51 *}
    52 
    53 consts gcd1 :: "nat\<times>nat \<Rightarrow> nat"
    54 recdef gcd1 "measure (\<lambda>(m,n).n)"
    55   "gcd1 (m, 0) = m"
    56   "gcd1 (m, n) = gcd1(n, m mod n)"
    57 
    58 
    59 text{*\noindent
    60 The order of equations is important: it hides the side condition
    61 @{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
    62 may not be expressible by pattern matching.
    63 
    64 A simple alternative is to replace @{text "if"} by @{text case}, 
    65 which is also available for @{typ bool} and is not split automatically:
    66 *}
    67 
    68 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat"
    69 recdef gcd2 "measure (\<lambda>(m,n).n)"
    70   "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))"
    71 
    72 text{*\noindent
    73 This is probably the neatest solution next to pattern matching, and it is
    74 always available.
    75 
    76 A final alternative is to replace the offending simplification rules by
    77 derived conditional ones. For @{term gcd} it means we have to prove
    78 these lemmas:
    79 *}
    80 
    81 lemma [simp]: "gcd (m, 0) = m"
    82 apply(simp)
    83 done
    84 
    85 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"
    86 apply(simp)
    87 done
    88 
    89 text{*\noindent
    90 Simplification terminates for these proofs because the condition of the @{text
    91 "if"} simplifies to @{term True} or @{term False}.
    92 Now we can disable the original simplification rule:
    93 *}
    94 
    95 declare gcd.simps [simp del]
    96 
    97 (*<*)
    98 end
    99 (*>*)