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