src/HOL/ex/InductiveInvariant_examples.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 19623 12e6cc4382ae permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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 measure_def inv_image_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 measure_def inv_image_def)
```
```   129
```
```   130 end
```