author | haftmann |
Mon, 21 Jan 2008 08:43:29 +0100 | |
changeset 25929 | 6bfef23e26be |
parent 22309 | 87ec1ca65312 |
child 27742 | df552e6027cf |
permissions | -rw-r--r-- |
21131 | 1 |
(* Title: HOL/ex/LexOrds.thy |
2 |
ID: |
|
3 |
Author: Lukas Bulwahn, TU Muenchen |
|
4 |
||
5 |
Examples for functions whose termination is proven by lexicographic order. |
|
6 |
*) |
|
7 |
||
8 |
theory LexOrds |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
12 |
subsection {* Trivial examples *} |
|
13 |
||
22309 | 14 |
fun identity :: "nat \<Rightarrow> nat" |
21131 | 15 |
where |
22309 | 16 |
"identity n = n" |
21131 | 17 |
|
22309 | 18 |
fun yaSuc :: "nat \<Rightarrow> nat" |
21131 | 19 |
where |
22309 | 20 |
"yaSuc 0 = 0" |
21 |
"yaSuc (Suc n) = Suc (yaSuc n)" |
|
21131 | 22 |
|
23 |
||
24 |
subsection {* Examples on natural numbers *} |
|
25 |
||
26 |
fun bin :: "(nat * nat) \<Rightarrow> nat" |
|
27 |
where |
|
28 |
"bin (0, 0) = 1" |
|
29 |
"bin (Suc n, 0) = 0" |
|
30 |
"bin (0, Suc m) = 0" |
|
31 |
"bin (Suc n, Suc m) = bin (n, m) + bin (Suc n, m)" |
|
32 |
||
33 |
||
34 |
fun t :: "(nat * nat) \<Rightarrow> nat" |
|
35 |
where |
|
36 |
"t (0,n) = 0" |
|
37 |
"t (n,0) = 0" |
|
38 |
"t (Suc n, Suc m) = (if (n mod 2 = 0) then (t (Suc n, m)) else (t (n, Suc m)))" |
|
39 |
||
40 |
||
22309 | 41 |
fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat" |
21131 | 42 |
where |
22309 | 43 |
"k ((0,0),(0,0)) = 0" |
44 |
"k ((Suc z, y), (u,v)) = k((z, y), (u, v))" (* z is descending *) |
|
45 |
"k ((0, Suc y), (u,v)) = k((1, y), (u, v))" (* y is descending *) |
|
46 |
"k ((0,0), (Suc u, v)) = k((1, 1), (u, v))" (* u is descending *) |
|
47 |
"k ((0,0), (0, Suc v)) = k((1,1), (1,v))" (* v is descending *) |
|
21131 | 48 |
|
49 |
||
50 |
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
51 |
where |
|
52 |
"gcd2 x 0 = x" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
53 |
"gcd2 0 y = y" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
54 |
"gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) |
21131 | 55 |
else gcd2 (x - y) (Suc y))" |
56 |
||
22309 | 57 |
fun ack :: "(nat * nat) \<Rightarrow> nat" |
21131 | 58 |
where |
59 |
"ack (0, m) = Suc m" |
|
60 |
"ack (Suc n, 0) = ack(n, 1)" |
|
61 |
"ack (Suc n, Suc m) = ack (n, ack (Suc n, m))" |
|
22309 | 62 |
|
21131 | 63 |
|
22309 | 64 |
fun greedy :: "nat * nat * nat * nat * nat => nat" |
65 |
where |
|
66 |
"greedy (Suc a, Suc b, Suc c, Suc d, Suc e) = |
|
67 |
(if (a < 10) then greedy (Suc a, Suc b, c, d + 2, Suc e) else |
|
68 |
(if (a < 20) then greedy (Suc a, b, Suc c, d, Suc e) else |
|
69 |
(if (a < 30) then greedy (Suc a, b, Suc c, d, Suc e) else |
|
70 |
(if (a < 40) then greedy (Suc a, b, Suc c, d, Suc e) else |
|
71 |
(if (a < 50) then greedy (Suc a, b, Suc c, d, Suc e) else |
|
72 |
(if (a < 60) then greedy (a, Suc b, Suc c, d, Suc e) else |
|
73 |
(if (a < 70) then greedy (a, Suc b, Suc c, d, Suc e) else |
|
74 |
(if (a < 80) then greedy (a, Suc b, Suc c, d, Suc e) else |
|
75 |
(if (a < 90) then greedy (Suc a, Suc b, Suc c, d, e) else |
|
76 |
greedy (Suc a, Suc b, Suc c, d, e))))))))))" |
|
77 |
"greedy (a, b, c, d, e) = 0" |
|
21131 | 78 |
|
22309 | 79 |
|
80 |
fun blowup :: "nat => nat => nat => nat => nat => nat => nat => nat => nat => nat" |
|
81 |
where |
|
82 |
"blowup 0 0 0 0 0 0 0 0 0 = 0" |
|
83 |
"blowup 0 0 0 0 0 0 0 0 (Suc i) = Suc (blowup i i i i i i i i i)" |
|
84 |
"blowup 0 0 0 0 0 0 0 (Suc h) i = Suc (blowup h h h h h h h h i)" |
|
85 |
"blowup 0 0 0 0 0 0 (Suc g) h i = Suc (blowup g g g g g g g h i)" |
|
86 |
"blowup 0 0 0 0 0 (Suc f) g h i = Suc (blowup f f f f f f g h i)" |
|
87 |
"blowup 0 0 0 0 (Suc e) f g h i = Suc (blowup e e e e e f g h i)" |
|
88 |
"blowup 0 0 0 (Suc d) e f g h i = Suc (blowup d d d d e f g h i)" |
|
89 |
"blowup 0 0 (Suc c) d e f g h i = Suc (blowup c c c d e f g h i)" |
|
90 |
"blowup 0 (Suc b) c d e f g h i = Suc (blowup b b c d e f g h i)" |
|
91 |
"blowup (Suc a) b c d e f g h i = Suc (blowup a b c d e f g h i)" |
|
92 |
||
93 |
||
21131 | 94 |
subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *} |
95 |
||
96 |
datatype tree = Node | Branch tree tree |
|
97 |
||
98 |
fun g_tree :: "tree * tree \<Rightarrow> tree" |
|
99 |
where |
|
100 |
"g_tree (Node, Node) = Node" |
|
101 |
"g_tree (Node, Branch a b) = Branch Node (g_tree (a,b))" |
|
102 |
"g_tree (Branch a b, Node) = Branch (g_tree (a,Node)) b" |
|
103 |
"g_tree (Branch a b, Branch c d) = Branch (g_tree (a,c)) (g_tree (b,d))" |
|
104 |
||
105 |
||
106 |
fun acklist :: "'a list * 'a list \<Rightarrow> 'a list" |
|
107 |
where |
|
108 |
"acklist ([], m) = ((hd m)#m)" |
|
109 |
| "acklist (n#ns, []) = acklist (ns, [n])" |
|
110 |
| "acklist ((n#ns), (m#ms)) = acklist (ns, acklist ((n#ns), ms))" |
|
111 |
||
112 |
||
113 |
subsection {* Examples with mutual recursion *} |
|
114 |
||
115 |
fun evn od :: "nat \<Rightarrow> bool" |
|
116 |
where |
|
117 |
"evn 0 = True" |
|
118 |
| "od 0 = False" |
|
22309 | 119 |
| "evn (Suc n) = od (Suc n)" |
21131 | 120 |
| "od (Suc n) = evn n" |
121 |
||
122 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
123 |
fun sizechange_f :: "'a list => 'a list => 'a list" and |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
124 |
sizechange_g :: "'a list => 'a list => 'a list => 'a list" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
125 |
where |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
126 |
"sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
127 |
"sizechange_g a b c = sizechange_f a (b @ c)" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
128 |
|
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
129 |
|
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
130 |
fun |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
131 |
prod :: "nat => nat => nat => nat" and |
22309 | 132 |
eprod :: "nat => nat => nat => nat" and |
133 |
oprod :: "nat => nat => nat => nat" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
134 |
where |
22309 | 135 |
"prod x y z = (if y mod 2 = 0 then eprod x y z else oprod x y z)" |
136 |
"oprod x y z = eprod x (y - 1) (z+x)" |
|
137 |
"eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
138 |
|
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
139 |
|
22309 | 140 |
fun |
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
141 |
pedal :: "nat => nat => nat => nat" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
142 |
and |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
143 |
coast :: "nat => nat => nat => nat" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
144 |
where |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
145 |
"pedal 0 m c = c" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
146 |
| "pedal n 0 c = c" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
147 |
| "pedal n m c = |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
148 |
(if n < m then coast (n - 1) (m - 1) (c + m) |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
149 |
else pedal (n - 1) m (c + m))" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
150 |
|
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
151 |
| "coast n m c = |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
152 |
(if n < m then coast n (m - 1) (c + n) |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
153 |
else pedal n m (c + n))" |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
154 |
|
22309 | 155 |
fun ack1 :: "nat => nat => nat" |
156 |
and ack2 :: "nat => nat => nat" |
|
157 |
where |
|
158 |
"ack1 0 m = m+1" | |
|
159 |
"ack1 (Suc n) m = ack2 n m" | |
|
160 |
"ack2 n 0 = ack1 n 1" | |
|
161 |
"ack2 n (Suc m) = ack1 n (ack2 n (Suc m))" |
|
21131 | 162 |
|
163 |
||
164 |
subsection {*Examples for an unprovable termination *} |
|
165 |
||
166 |
text {* If termination cannot be proven, the tactic gives further information about unprovable subgoals on the arguments *} |
|
167 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
168 |
function noterm :: "(nat * nat) \<Rightarrow> nat" |
21131 | 169 |
where |
170 |
"noterm (a,b) = noterm(b,a)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
171 |
by pat_completeness auto |
21131 | 172 |
(* termination by apply lexicographic_order*) |
173 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
174 |
function term_but_no_prove :: "nat * nat \<Rightarrow> nat" |
21131 | 175 |
where |
176 |
"term_but_no_prove (0,0) = 1" |
|
177 |
"term_but_no_prove (0, Suc b) = 0" |
|
178 |
"term_but_no_prove (Suc a, 0) = 0" |
|
179 |
"term_but_no_prove (Suc a, Suc b) = term_but_no_prove (b, a)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
180 |
by pat_completeness auto |
21131 | 181 |
(* termination by lexicographic_order *) |
182 |
||
183 |
text{* The tactic distinguishes between N = not provable AND F = False *} |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
184 |
function no_proof :: "nat \<Rightarrow> nat" |
21131 | 185 |
where |
186 |
"no_proof m = no_proof (Suc m)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
187 |
by pat_completeness auto |
21131 | 188 |
(* termination by lexicographic_order *) |
189 |
||
190 |
end |