src/HOL/ex/Termination.thy
 author krauss Mon Aug 24 13:59:08 2009 +0200 (2009-08-24) changeset 32399 4dc441c71cce parent 29181 cc177742e607 child 33468 91ea7115da1b permissions -rw-r--r--
some examples for giving measures manually
```     1 (* Title:       HOL/ex/Termination.thy
```
```     2    Author:      Lukas Bulwahn, TU Muenchen
```
```     3    Author:      Alexander Krauss, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Examples and regression tests for automated termination proofs *}
```
```     7
```
```     8 theory Termination
```
```     9 imports Main 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 sizechange} 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 sizechange
```
```   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 sizechange
```
```   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 sizechange
```
```   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 sizechange -- {* requires Multiset *}
```
```   231
```
```   232 end
```