src/HOL/ex/InductiveInvariant_examples.thy
changeset 14244 f58598341d30
child 15636 57c437b70521
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Oct 22 10:52:36 2003 +0200
     1.3 @@ -0,0 +1,127 @@
     1.4 +theory InductiveInvariant_examples = InductiveInvariant :
     1.5 +
     1.6 +(** Authors: Sava Krsti\'{c} and John Matthews **)
     1.7 +(**    Date: Oct 17, 2003                      **)
     1.8 +
     1.9 +text "A simple example showing how to use an inductive invariant
    1.10 +      to solve termination conditions generated by recdef on
    1.11 +      nested recursive function definitions."
    1.12 +
    1.13 +consts g :: "nat => nat"
    1.14 +
    1.15 +recdef (permissive) g "less_than"
    1.16 +  "g 0 = 0"
    1.17 +  "g (Suc n) = g (g n)"
    1.18 +
    1.19 +text "We can prove the unsolved termination condition for
    1.20 +      g by showing it is an inductive invariant."
    1.21 +
    1.22 +recdef_tc g_tc[simp]: g
    1.23 +apply (rule allI)
    1.24 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
    1.25 +apply (auto simp add: indinv_def split: nat.split)
    1.26 +apply (frule_tac x=nat in spec)
    1.27 +apply (drule_tac x="f nat" in spec)
    1.28 +by auto
    1.29 +
    1.30 +
    1.31 +text "This declaration invokes Isabelle's simplifier to
    1.32 +      remove any termination conditions before adding
    1.33 +      g's rules to the simpset."
    1.34 +declare g.simps [simplified, simp]
    1.35 +
    1.36 +
    1.37 +text "This is an example where the termination condition generated
    1.38 +      by recdef is not itself an inductive invariant."
    1.39 +
    1.40 +consts g' :: "nat => nat"
    1.41 +recdef (permissive) g' "less_than"
    1.42 +  "g' 0 = 0"
    1.43 +  "g' (Suc n) = g' n + g' (g' n)"
    1.44 +
    1.45 +thm g'.simps
    1.46 +
    1.47 +
    1.48 +text "The strengthened inductive invariant is as follows
    1.49 +      (this invariant also works for the first example above):"
    1.50 +
    1.51 +lemma g'_inv: "g' n = 0"
    1.52 +thm tfl_indinv_wfrec [OF g'_def]
    1.53 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
    1.54 +by (auto simp add: indinv_def split: nat.split)
    1.55 +
    1.56 +recdef_tc g'_tc[simp]: g'
    1.57 +by (simp add: g'_inv)
    1.58 +
    1.59 +text "Now we can remove the termination condition from
    1.60 +      the rules for g' ."
    1.61 +thm g'.simps [simplified]
    1.62 +
    1.63 +
    1.64 +text {* Sometimes a recursive definition is partial, that is, it
    1.65 +        is only meant to be invoked on "good" inputs. As a contrived
    1.66 +        example, we will define a new version of g that is only
    1.67 +        well defined for even inputs greater than zero. *}
    1.68 +
    1.69 +consts g_even :: "nat => nat"
    1.70 +recdef (permissive) g_even "less_than"
    1.71 +  "g_even (Suc (Suc 0)) = 3"
    1.72 +  "g_even n = g_even (g_even (n - 2) - 1)"
    1.73 +
    1.74 +
    1.75 +text "We can prove a conditional version of the unsolved termination
    1.76 +      condition for @{term g_even} by proving a stronger inductive invariant."
    1.77 +
    1.78 +lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
    1.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])
    1.80 +apply (auto simp add: indinv_on_def split: nat.split)
    1.81 +by (case_tac ka, auto)
    1.82 +
    1.83 +
    1.84 +text "Now we can prove that the second recursion equation for @{term g_even}
    1.85 +      holds, provided that n is an even number greater than two."
    1.86 +
    1.87 +theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
    1.88 +apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
    1.89 +by (auto simp add: g_even_indinv, arith)
    1.90 +
    1.91 +
    1.92 +text "McCarthy's ninety-one function. This function requires a
    1.93 +      non-standard measure to prove termination."
    1.94 +
    1.95 +consts ninety_one :: "nat => nat"
    1.96 +recdef (permissive) ninety_one "measure (%n. 101 - n)"
    1.97 +  "ninety_one x = (if 100 < x
    1.98 +                     then x - 10
    1.99 +                     else (ninety_one (ninety_one (x+11))))"
   1.100 +
   1.101 +text "To discharge the termination condition, we will prove
   1.102 +      a strengthened inductive invariant:
   1.103 +         S x y == x < y + 11"
   1.104 +
   1.105 +lemma ninety_one_inv: "n < ninety_one n + 11"
   1.106 +apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
   1.107 +apply force
   1.108 +apply (auto simp add: indinv_def measure_def inv_image_def)
   1.109 +apply (frule_tac x="x+11" in spec)
   1.110 +apply (frule_tac x="f (x + 11)" in spec)
   1.111 +by arith
   1.112 +
   1.113 +text "Proving the termination condition using the
   1.114 +      strengthened inductive invariant."
   1.115 +
   1.116 +recdef_tc ninety_one_tc[rule_format]: ninety_one
   1.117 +apply clarify
   1.118 +by (cut_tac n="x+11" in ninety_one_inv, arith)
   1.119 +
   1.120 +text "Now we can remove the termination condition from
   1.121 +      the simplification rule for @{term ninety_one}."
   1.122 +
   1.123 +theorem def_ninety_one:
   1.124 +"ninety_one x = (if 100 < x
   1.125 +                   then x - 10
   1.126 +                   else ninety_one (ninety_one (x+11)))"
   1.127 +by (subst ninety_one.simps,
   1.128 +    simp add: ninety_one_tc measure_def inv_image_def)
   1.129 +
   1.130 +end
   1.131 \ No newline at end of file