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;
 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` wenzelm@58889 ` 6` ```section {* Examples and regression tests for automated termination proofs *} ``` krauss@29181 ` 7` ``` ``` krauss@29181 ` 8` ```theory Termination ``` wenzelm@41413 ` 9` ```imports Main "~~/src/HOL/Library/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 \ nat \ 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 (\(i,N). N + 1 - i)") auto ``` krauss@32399 ` 21` krauss@32399 ` 22` ```function foo :: "nat \ nat \ 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 [\(i, N). N, \(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 \ nat" ``` krauss@29181 ` 40` ```where ``` krauss@29181 ` 41` ``` "identity n = n" ``` krauss@29181 ` 42` krauss@29181 ` 43` ```fun yaSuc :: "nat \ 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) \ 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) \ 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) \ 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 \ nat \ 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) \ 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` blanchet@58310 ` 121` ```datatype tree = Node | Branch tree tree ``` krauss@29181 ` 122` krauss@29181 ` 123` ```fun g_tree :: "tree * tree \ 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 \ '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 \ 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 \ 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 \ nat \ nat \ 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 \ nat \ nat \ nat" ``` krauss@29181 ` 218` ```where ``` krauss@29181 ` 219` ``` "fun2 x y z = ``` krauss@29181 ` 220` ``` (if x > 1000 \ z > 0 then ``` krauss@29181 ` 221` ``` fun2 (min x y) y (z - 1) ``` krauss@29181 ` 222` ``` else if y > 0 \ 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@47836 ` 232` ```definition negate :: "int \ int" ``` krauss@47836 ` 233` ```where "negate i = - i" ``` krauss@47836 ` 234` krauss@47836 ` 235` ```function fun3 :: "int => nat" ``` krauss@47836 ` 236` ```where ``` krauss@47836 ` 237` ``` "fun3 i = ``` krauss@47836 ` 238` ``` (if i < 0 then fun3 (negate i) ``` krauss@47836 ` 239` ``` else if i = 0 then 0 ``` krauss@47836 ` 240` ``` else fun3 (i - 1))" ``` krauss@47836 ` 241` ```by (pat_completeness) auto ``` krauss@47836 ` 242` ```termination ``` krauss@47836 ` 243` ``` apply size_change ``` krauss@47836 ` 244` ``` apply (simp add: negate_def) ``` krauss@47836 ` 245` ``` apply size_change ``` krauss@47836 ` 246` ``` done ``` krauss@47836 ` 247` krauss@47836 ` 248` krauss@29181 ` 249` ```end ```