src/HOL/ex/InductiveInvariant_examples.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 19769 c40ce2de2020
child 32960 69916a850301
permissions -rw-r--r--
added lemmas
     1 (*  ID:         $Id$
     2     Author:	Sava Krsti\'{c} and John Matthews
     3 *)
     4 
     5 header {* Example use if an inductive invariant to solve termination conditions *}
     6 
     7 theory InductiveInvariant_examples imports InductiveInvariant  begin
     8 
     9 text "A simple example showing how to use an inductive invariant
    10       to solve termination conditions generated by recdef on
    11       nested recursive function definitions."
    12 
    13 consts g :: "nat => nat"
    14 
    15 recdef (permissive) g "less_than"
    16   "g 0 = 0"
    17   "g (Suc n) = g (g n)"
    18 
    19 text "We can prove the unsolved termination condition for
    20       g by showing it is an inductive invariant."
    21 
    22 recdef_tc g_tc[simp]: g
    23 apply (rule allI)
    24 apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
    25 apply (auto simp add: indinv_def split: nat.split)
    26 apply (frule_tac x=nat in spec)
    27 apply (drule_tac x="f nat" in spec)
    28 by auto
    29 
    30 
    31 text "This declaration invokes Isabelle's simplifier to
    32       remove any termination conditions before adding
    33       g's rules to the simpset."
    34 declare g.simps [simplified, simp]
    35 
    36 
    37 text "This is an example where the termination condition generated
    38       by recdef is not itself an inductive invariant."
    39 
    40 consts g' :: "nat => nat"
    41 recdef (permissive) g' "less_than"
    42   "g' 0 = 0"
    43   "g' (Suc n) = g' n + g' (g' n)"
    44 
    45 thm g'.simps
    46 
    47 
    48 text "The strengthened inductive invariant is as follows
    49       (this invariant also works for the first example above):"
    50 
    51 lemma g'_inv: "g' n = 0"
    52 thm tfl_indinv_wfrec [OF g'_def]
    53 apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
    54 by (auto simp add: indinv_def split: nat.split)
    55 
    56 recdef_tc g'_tc[simp]: g'
    57 by (simp add: g'_inv)
    58 
    59 text "Now we can remove the termination condition from
    60       the rules for g' ."
    61 thm g'.simps [simplified]
    62 
    63 
    64 text {* Sometimes a recursive definition is partial, that is, it
    65         is only meant to be invoked on "good" inputs. As a contrived
    66         example, we will define a new version of g that is only
    67         well defined for even inputs greater than zero. *}
    68 
    69 consts g_even :: "nat => nat"
    70 recdef (permissive) g_even "less_than"
    71   "g_even (Suc (Suc 0)) = 3"
    72   "g_even n = g_even (g_even (n - 2) - 1)"
    73 
    74 
    75 text "We can prove a conditional version of the unsolved termination
    76       condition for @{term g_even} by proving a stronger inductive invariant."
    77 
    78 lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
    79 apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
    80 apply (auto simp add: indinv_on_def split: nat.split)
    81 by (case_tac ka, auto)
    82 
    83 
    84 text "Now we can prove that the second recursion equation for @{term g_even}
    85       holds, provided that n is an even number greater than two."
    86 
    87 theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
    88 apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
    89 by (auto simp add: g_even_indinv, arith)
    90 
    91 
    92 text "McCarthy's ninety-one function. This function requires a
    93       non-standard measure to prove termination."
    94 
    95 consts ninety_one :: "nat => nat"
    96 recdef (permissive) ninety_one "measure (%n. 101 - n)"
    97   "ninety_one x = (if 100 < x
    98                      then x - 10
    99                      else (ninety_one (ninety_one (x+11))))"
   100 
   101 text "To discharge the termination condition, we will prove
   102       a strengthened inductive invariant:
   103          S x y == x < y + 11"
   104 
   105 lemma ninety_one_inv: "n < ninety_one n + 11"
   106 apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
   107 apply force
   108 apply (auto simp add: indinv_def)
   109 apply (frule_tac x="x+11" in spec)
   110 apply (frule_tac x="f (x + 11)" in spec)
   111 by arith
   112 
   113 text "Proving the termination condition using the
   114       strengthened inductive invariant."
   115 
   116 recdef_tc ninety_one_tc[rule_format]: ninety_one
   117 apply clarify
   118 by (cut_tac n="x+11" in ninety_one_inv, arith)
   119 
   120 text "Now we can remove the termination condition from
   121       the simplification rule for @{term ninety_one}."
   122 
   123 theorem def_ninety_one:
   124 "ninety_one x = (if 100 < x
   125                    then x - 10
   126                    else ninety_one (ninety_one (x+11)))"
   127 by (subst ninety_one.simps,
   128     simp add: ninety_one_tc)
   129 
   130 end