src/HOL/ex/Termination.thy
author krauss
Fri Nov 06 13:36:46 2009 +0100 (2009-11-06)
changeset 33468 91ea7115da1b
parent 32399 4dc441c71cce
child 41413 64cd30d6b0b8
permissions -rw-r--r--
renamed method sizechange to size_change
krauss@29181
     1
(* Title:       HOL/ex/Termination.thy
krauss@29181
     2
   Author:      Lukas Bulwahn, TU Muenchen
krauss@29181
     3
   Author:      Alexander Krauss, TU Muenchen
krauss@29181
     4
*)
krauss@29181
     5
krauss@29181
     6
header {* Examples and regression tests for automated termination proofs *}
krauss@29181
     7
 
krauss@29181
     8
theory Termination
krauss@29181
     9
imports Main Multiset
krauss@29181
    10
begin
krauss@29181
    11
krauss@32399
    12
subsection {* Manually giving termination relations using @{text relation} and
krauss@32399
    13
@{term measure} *}
krauss@32399
    14
krauss@32399
    15
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@32399
    16
where
krauss@32399
    17
  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
krauss@32399
    18
by pat_completeness auto
krauss@32399
    19
krauss@32399
    20
termination by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
krauss@32399
    21
krauss@32399
    22
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@32399
    23
where
krauss@32399
    24
  "foo i N = (if i > N 
krauss@32399
    25
              then (if N = 0 then 0 else foo 0 (N - 1))
krauss@32399
    26
              else i + foo (Suc i) N)"
krauss@32399
    27
by pat_completeness auto
krauss@32399
    28
krauss@32399
    29
termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
krauss@32399
    30
krauss@32399
    31
krauss@32399
    32
subsection {* @{text lexicographic_order}: Trivial examples *}
krauss@32399
    33
krauss@29181
    34
text {*
krauss@32399
    35
  The @{text fun} command uses the method @{text lexicographic_order} by default,
krauss@32399
    36
  so it is not explicitly invoked.
krauss@29181
    37
*}
krauss@29181
    38
krauss@29181
    39
fun identity :: "nat \<Rightarrow> nat"
krauss@29181
    40
where
krauss@29181
    41
  "identity n = n"
krauss@29181
    42
krauss@29181
    43
fun yaSuc :: "nat \<Rightarrow> nat"
krauss@29181
    44
where 
krauss@29181
    45
  "yaSuc 0 = 0"
krauss@29181
    46
| "yaSuc (Suc n) = Suc (yaSuc n)"
krauss@29181
    47
krauss@29181
    48
krauss@29181
    49
subsection {* Examples on natural numbers *}
krauss@29181
    50
krauss@29181
    51
fun bin :: "(nat * nat) \<Rightarrow> nat"
krauss@29181
    52
where
krauss@29181
    53
  "bin (0, 0) = 1"
krauss@29181
    54
| "bin (Suc n, 0) = 0"
krauss@29181
    55
| "bin (0, Suc m) = 0"
krauss@29181
    56
| "bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)"
krauss@29181
    57
krauss@29181
    58
krauss@29181
    59
fun t :: "(nat * nat) \<Rightarrow> nat"
krauss@29181
    60
where
krauss@29181
    61
  "t (0,n) = 0"
krauss@29181
    62
| "t (n,0) = 0"
krauss@29181
    63
| "t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" 
krauss@29181
    64
krauss@29181
    65
krauss@29181
    66
fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat"
krauss@29181
    67
where
krauss@29181
    68
  "k ((0,0),(0,0)) = 0"
krauss@29181
    69
| "k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *)
krauss@29181
    70
| "k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *)
krauss@29181
    71
| "k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *)
krauss@29181
    72
| "k ((0,0), (0, Suc v)) = k((1,1), (1,v))"   (* v is descending *)
krauss@29181
    73
krauss@29181
    74
krauss@29181
    75
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@29181
    76
where
krauss@29181
    77
  "gcd2 x 0 = x"
krauss@29181
    78
| "gcd2 0 y = y"
krauss@29181
    79
| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
krauss@29181
    80
                                    else gcd2 (x - y) (Suc y))"
krauss@29181
    81
krauss@29181
    82
fun ack :: "(nat * nat) \<Rightarrow> nat"
krauss@29181
    83
where
krauss@29181
    84
  "ack (0, m) = Suc m"
krauss@29181
    85
| "ack (Suc n, 0) = ack(n, 1)"
krauss@29181
    86
| "ack (Suc n, Suc m) = ack (n, ack (Suc n, m))"
krauss@29181
    87
krauss@29181
    88
krauss@29181
    89
fun greedy :: "nat * nat * nat * nat * nat => nat"
krauss@29181
    90
where
krauss@29181
    91
  "greedy (Suc a, Suc b, Suc c, Suc d, Suc e) =
krauss@29181
    92
  (if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else
krauss@29181
    93
  (if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else
krauss@29181
    94
  (if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else
krauss@29181
    95
  (if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else
krauss@29181
    96
  (if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else
krauss@29181
    97
  (if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else
krauss@29181
    98
  (if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else
krauss@29181
    99
  (if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else
krauss@29181
   100
  (if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else
krauss@29181
   101
  greedy (Suc a, Suc b, Suc c, d, e))))))))))"
krauss@29181
   102
| "greedy (a, b, c, d, e) = 0"
krauss@29181
   103
krauss@29181
   104
krauss@29181
   105
fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat"
krauss@29181
   106
where
krauss@29181
   107
  "blowup 0 0 0 0 0 0 0 0 0 = 0"
krauss@29181
   108
| "blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)"
krauss@29181
   109
| "blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)"
krauss@29181
   110
| "blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)"
krauss@29181
   111
| "blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)"
krauss@29181
   112
| "blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)"
krauss@29181
   113
| "blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)"
krauss@29181
   114
| "blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)"
krauss@29181
   115
| "blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)"
krauss@29181
   116
| "blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)"
krauss@29181
   117
krauss@29181
   118
  
krauss@29181
   119
subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
krauss@29181
   120
krauss@29181
   121
datatype tree = Node | Branch tree tree
krauss@29181
   122
krauss@29181
   123
fun g_tree :: "tree * tree \<Rightarrow> tree"
krauss@29181
   124
where
krauss@29181
   125
  "g_tree (Node, Node) = Node"
krauss@29181
   126
| "g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))"
krauss@29181
   127
| "g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b"
krauss@29181
   128
| "g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))"
krauss@29181
   129
krauss@29181
   130
krauss@29181
   131
fun acklist :: "'a list * 'a list \<Rightarrow> 'a list"
krauss@29181
   132
where
krauss@29181
   133
  "acklist ([], m) = ((hd m)#m)"
krauss@29181
   134
|  "acklist (n#ns, []) = acklist (ns, [n])"
krauss@29181
   135
|  "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))"
krauss@29181
   136
krauss@29181
   137
krauss@29181
   138
subsection {* Examples with mutual recursion *}
krauss@29181
   139
krauss@29181
   140
fun evn od :: "nat \<Rightarrow> bool"
krauss@29181
   141
where
krauss@29181
   142
  "evn 0 = True"
krauss@29181
   143
| "od 0 = False"
krauss@29181
   144
| "evn (Suc n) = od (Suc n)"
krauss@29181
   145
| "od (Suc n) = evn n"
krauss@29181
   146
krauss@29181
   147
krauss@29181
   148
fun sizechange_f :: "'a list => 'a list => 'a list" and
krauss@29181
   149
sizechange_g :: "'a list => 'a list => 'a list => 'a list"
krauss@29181
   150
where
krauss@29181
   151
  "sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)"
krauss@29181
   152
| "sizechange_g a b c = sizechange_f a (b @ c)"
krauss@29181
   153
krauss@29181
   154
fun
krauss@29181
   155
  pedal :: "nat => nat => nat => nat"
krauss@29181
   156
and
krauss@29181
   157
  coast :: "nat => nat => nat => nat"
krauss@29181
   158
where
krauss@29181
   159
  "pedal 0 m c = c"
krauss@29181
   160
| "pedal n 0 c = c"
krauss@29181
   161
| "pedal n m c =
krauss@29181
   162
     (if n < m then coast (n - 1) (m - 1) (c + m)
krauss@29181
   163
               else pedal (n - 1) m (c + m))"
krauss@29181
   164
krauss@29181
   165
| "coast n m c =
krauss@29181
   166
     (if n < m then coast n (m - 1) (c + n)
krauss@29181
   167
               else pedal n m (c + n))"
krauss@29181
   168
krauss@29181
   169
krauss@29181
   170
krauss@33468
   171
subsection {* Refined analysis: The @{text size_change} method *}
krauss@29181
   172
krauss@29181
   173
text {* Unsolvable for @{text lexicographic_order} *}
krauss@29181
   174
krauss@29181
   175
function fun1 :: "nat * nat \<Rightarrow> nat"
krauss@29181
   176
where
krauss@29181
   177
  "fun1 (0,0) = 1"
krauss@29181
   178
| "fun1 (0, Suc b) = 0"
krauss@29181
   179
| "fun1 (Suc a, 0) = 0"
krauss@29181
   180
| "fun1 (Suc a, Suc b) = fun1 (b, a)"
krauss@29181
   181
by pat_completeness auto
krauss@33468
   182
termination by size_change
krauss@29181
   183
krauss@29181
   184
krauss@29181
   185
text {* 
krauss@29181
   186
  @{text lexicographic_order} can do the following, but it is much slower. 
krauss@29181
   187
*}
krauss@29181
   188
krauss@29181
   189
function
krauss@29181
   190
  prod :: "nat => nat => nat => nat" and
krauss@29181
   191
  eprod :: "nat => nat => nat => nat" and
krauss@29181
   192
  oprod :: "nat => nat => nat => nat"
krauss@29181
   193
where
krauss@29181
   194
  "prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)"
krauss@29181
   195
| "oprod x y z = eprod x (y - 1) (z+x)"
krauss@29181
   196
| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
krauss@29181
   197
by pat_completeness auto
krauss@33468
   198
termination by size_change
krauss@29181
   199
krauss@29181
   200
text {* 
krauss@29181
   201
  Permutations of arguments:
krauss@29181
   202
*}
krauss@29181
   203
krauss@29181
   204
function perm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@29181
   205
where
krauss@29181
   206
  "perm m n r = (if r > 0 then perm m (r - 1) n
krauss@29181
   207
                  else if n > 0 then perm r (n - 1) m
krauss@29181
   208
                  else m)"
krauss@29181
   209
by auto
krauss@33468
   210
termination by size_change
krauss@29181
   211
krauss@29181
   212
text {*
krauss@29181
   213
  Artificial examples and regression tests:
krauss@29181
   214
*}
krauss@29181
   215
krauss@29181
   216
function
krauss@29181
   217
  fun2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@29181
   218
where
krauss@29181
   219
  "fun2 x y z =
krauss@29181
   220
      (if x > 1000 \<and> z > 0 then
krauss@29181
   221
           fun2 (min x y) y (z - 1)
krauss@29181
   222
       else if y > 0 \<and> x > 100 then
krauss@29181
   223
           fun2 x (y - 1) (2 * z)
krauss@29181
   224
       else if z > 0 then
krauss@29181
   225
           fun2 (min y (z - 1)) x x
krauss@29181
   226
       else
krauss@29181
   227
           0
krauss@29181
   228
      )"
krauss@29181
   229
by pat_completeness auto
krauss@33468
   230
termination by size_change -- {* requires Multiset *}
krauss@29181
   231
krauss@29181
   232
end