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.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
```