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