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