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