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