src/HOL/ex/InductiveInvariant_examples.thy
 author paulson Wed Mar 30 08:33:41 2005 +0200 (2005-03-30) changeset 15636 57c437b70521 parent 14244 f58598341d30 child 16417 9bc16273c2d4 permissions -rw-r--r--
converted from DOS to UNIX format
```     1 theory InductiveInvariant_examples = InductiveInvariant :
```
```     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`