author | wenzelm |
Wed, 17 Sep 2008 21:27:14 +0200 | |
changeset 28263 | 69eaa97e7e96 |
parent 27742 | df552e6027cf |
permissions | -rw-r--r-- |
21131 | 1 |
(* Title: HOL/ex/LexOrds.thy |
27742 | 2 |
ID: $Id$ |
21131 | 3 |
Author: Lukas Bulwahn, TU Muenchen |
27742 | 4 |
*) |
21131 | 5 |
|
27742 | 6 |
header {* Examples and regression tests for method lexicographic order. *} |
21131 | 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 |
27742 | 16 |
"identity n = n" |
21131 | 17 |
|
22309 | 18 |
fun yaSuc :: "nat \<Rightarrow> nat" |
21131 | 19 |
where |
22309 | 20 |
"yaSuc 0 = 0" |
27742 | 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" |
|
27742 | 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)" |
|
21131 | 32 |
|
33 |
||
34 |
fun t :: "(nat * nat) \<Rightarrow> nat" |
|
35 |
where |
|
36 |
"t (0,n) = 0" |
|
27742 | 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)))" |
|
21131 | 39 |
|
40 |
||
22309 | 41 |
fun k :: "(nat * nat) * (nat * nat) \<Rightarrow> nat" |
21131 | 42 |
where |
22309 | 43 |
"k ((0,0),(0,0)) = 0" |
27742 | 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" |
|
27742 | 53 |
| "gcd2 0 y = y" |
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" |
|
27742 | 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))))))))))" |
|
27742 | 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" |
|
27742 | 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)" |
|
22309 | 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" |
|
27742 | 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))" |
|
21131 | 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 |
27742 | 126 |
"sizechange_f i x = (if i=[] then x else sizechange_g (tl i) x i)" |
127 |
| "sizechange_g a b c = sizechange_f a (b @ c)" |
|
22258
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)" |
27742 | 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 |
|
21131 | 155 |
|
156 |
subsection {*Examples for an unprovable termination *} |
|
157 |
||
158 |
text {* If termination cannot be proven, the tactic gives further information about unprovable subgoals on the arguments *} |
|
159 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
160 |
function noterm :: "(nat * nat) \<Rightarrow> nat" |
21131 | 161 |
where |
162 |
"noterm (a,b) = noterm(b,a)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
163 |
by pat_completeness auto |
21131 | 164 |
(* termination by apply lexicographic_order*) |
165 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
166 |
function term_but_no_prove :: "nat * nat \<Rightarrow> nat" |
21131 | 167 |
where |
168 |
"term_but_no_prove (0,0) = 1" |
|
27742 | 169 |
| "term_but_no_prove (0, Suc b) = 0" |
170 |
| "term_but_no_prove (Suc a, 0) = 0" |
|
171 |
| "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
|
172 |
by pat_completeness auto |
21131 | 173 |
(* termination by lexicographic_order *) |
174 |
||
175 |
text{* The tactic distinguishes between N = not provable AND F = False *} |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
176 |
function no_proof :: "nat \<Rightarrow> nat" |
21131 | 177 |
where |
178 |
"no_proof m = no_proof (Suc m)" |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21131
diff
changeset
|
179 |
by pat_completeness auto |
21131 | 180 |
(* termination by lexicographic_order *) |
181 |
||
182 |
end |