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