1 (* Title: HOL/ex/svc_test.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
|
4 Copyright 1999 University of Cambridge |
|
5 |
|
6 Demonstrating svc_tac: the interface to the Stanford Validity Checker |
|
7 |
|
8 SVC is assumed to be present if the environment variable SVC_HOME is non-empty. |
|
9 |
|
10 set Svc.trace; |
|
11 *) |
|
12 |
|
13 (** Propositional Logic **) |
|
14 |
|
15 (*Blast_tac's runtime for this type of problem appears to be exponential |
|
16 in its length, though Fast_tac manages*) |
|
17 Goal "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P"; |
|
18 by (svc_tac 1); |
|
19 qed ""; |
|
20 |
|
21 (** Some big tautologies supplied by John Harrison **) |
|
22 |
|
23 (*Tautology name: puz013_1. Auto_tac manages; Blast_tac and Fast_tac take |
|
24 a minute or more.*) |
|
25 Goal "~(~v12 & \ |
|
26 \ v0 & \ |
|
27 \ v10 & \ |
|
28 \ (v4 | v5) & \ |
|
29 \ (v9 | v2) & \ |
|
30 \ (v8 | v1) & \ |
|
31 \ (v7 | v0) & \ |
|
32 \ (v3 | v12) & \ |
|
33 \ (v11 | v10) & \ |
|
34 \ (~v12 | ~v6 | v7) & \ |
|
35 \ (~v10 | ~v3 | v1) & \ |
|
36 \ (~v10 | ~v0 | ~v4 | v11) & \ |
|
37 \ (~v5 | ~v2 | ~v8) & \ |
|
38 \ (~v12 | ~v9 | ~v7) & \ |
|
39 \ (~v0 | ~v1 | v4) & \ |
|
40 \ (~v4 | v7 | v2) & \ |
|
41 \ (~v12 | ~v3 | v8) & \ |
|
42 \ (~v4 | v5 | v6) & \ |
|
43 \ (~v7 | ~v8 | v9) & \ |
|
44 \ (~v10 | ~v11 | v12))"; |
|
45 by (svc_tac 1); |
|
46 qed ""; |
|
47 |
|
48 (*Tautology name: dk17_be*) |
|
49 Goal "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) & \ |
|
50 \ (GE0 <-> GE17 & ~IN5) & \ |
|
51 \ (GE22 <-> ~IN9 & ~IN7 & ~IN6 & IN0) & \ |
|
52 \ (GE19 <-> ~IN5 & ~IN4 & ~IN3 & ~IN0) & \ |
|
53 \ (GE20 <-> ~IN7 & ~IN6) & \ |
|
54 \ (GE18 <-> ~IN6 & ~IN2 & ~IN1 & ~IN0) & \ |
|
55 \ (GE21 <-> IN9 & ~IN7 & IN6 & ~IN0) & \ |
|
56 \ (GE23 <-> GE22 & GE0) & \ |
|
57 \ (GE25 <-> ~IN9 & ~IN7 & IN6 & ~IN0) & \ |
|
58 \ (GE26 <-> IN9 & ~IN7 & ~IN6 & IN0) & \ |
|
59 \ (GE2 <-> GE20 & GE19) & \ |
|
60 \ (GE1 <-> GE18 & ~IN7) & \ |
|
61 \ (GE24 <-> GE23 | GE21 & GE0) & \ |
|
62 \ (GE5 <-> ~IN5 & IN4 | IN5 & ~IN4) & \ |
|
63 \ (GE6 <-> GE0 & IN7 & ~IN6 & ~IN0) & \ |
|
64 \ (GE12 <-> GE26 & GE0 | GE25 & GE0) & \ |
|
65 \ (GE14 <-> GE2 & IN8 & ~IN2 & IN1) & \ |
|
66 \ (GE27 <-> ~IN8 & IN5 & ~IN4 & ~IN3) & \ |
|
67 \ (GE9 <-> GE1 & ~IN5 & ~IN4 & IN3) & \ |
|
68 \ (GE7 <-> GE24 | GE2 & IN2 & ~IN1) & \ |
|
69 \ (GE10 <-> GE6 | GE5 & GE1 & ~IN3) & \ |
|
70 \ (GE15 <-> ~IN8 | IN9) & \ |
|
71 \ (GE16 <-> GE12 | GE14 & ~IN9) & \ |
|
72 \ (GE4 <-> \ |
|
73 \ GE5 & GE1 & IN8 & ~IN3 | \ |
|
74 \ GE0 & ~IN7 & IN6 & ~IN0 | \ |
|
75 \ GE2 & IN2 & ~IN1) & \ |
|
76 \ (GE13 <-> GE27 & GE1) & \ |
|
77 \ (GE11 <-> GE9 | GE6 & ~IN8) & \ |
|
78 \ (GE8 <-> GE1 & ~IN5 & IN4 & ~IN3 | GE2 & ~IN2 & IN1) & \ |
|
79 \ (OUT0 <-> GE7 & ~IN8) & \ |
|
80 \ (OUT1 <-> GE7 & IN8) & \ |
|
81 \ (OUT2 <-> GE8 & ~IN9 | GE10 & IN8) & \ |
|
82 \ (OUT3 <-> GE8 & IN9 & ~IN8 | GE11 & ~IN9 | GE12 & ~IN8) & \ |
|
83 \ (OUT4 <-> GE11 & IN9 | GE12 & IN8) & \ |
|
84 \ (OUT5 <-> GE14 & IN9) & \ |
|
85 \ (OUT6 <-> GE13 & ~IN9) & \ |
|
86 \ (OUT7 <-> GE13 & IN9) & \ |
|
87 \ (OUT8 <-> GE9 & ~IN8 | GE15 & GE6 | GE4 & IN9) & \ |
|
88 \ (OUT9 <-> GE9 & IN8 | ~GE15 & GE10 | GE16) & \ |
|
89 \ (OUT10 <-> GE7) & \ |
|
90 \ (WRES0 <-> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) & \ |
|
91 \ (WRES1 <-> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) & \ |
|
92 \ (WRES2 <-> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) & \ |
|
93 \ (WRES5 <-> ~IN5 & IN4 | IN5 & ~IN4) & \ |
|
94 \ (WRES6 <-> WRES0 & IN7 & ~IN6 & ~IN0) & \ |
|
95 \ (WRES9 <-> WRES1 & ~IN5 & ~IN4 & IN3) & \ |
|
96 \ (WRES7 <-> \ |
|
97 \ WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0 | \ |
|
98 \ WRES0 & IN9 & ~IN7 & IN6 & ~IN0 | \ |
|
99 \ WRES2 & IN2 & ~IN1) & \ |
|
100 \ (WRES10 <-> WRES6 | WRES5 & WRES1 & ~IN3) & \ |
|
101 \ (WRES12 <-> \ |
|
102 \ WRES0 & IN9 & ~IN7 & ~IN6 & IN0 | \ |
|
103 \ WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) & \ |
|
104 \ (WRES14 <-> WRES2 & IN8 & ~IN2 & IN1) & \ |
|
105 \ (WRES15 <-> ~IN8 | IN9) & \ |
|
106 \ (WRES4 <-> \ |
|
107 \ WRES5 & WRES1 & IN8 & ~IN3 | \ |
|
108 \ WRES2 & IN2 & ~IN1 | \ |
|
109 \ WRES0 & ~IN7 & IN6 & ~IN0) & \ |
|
110 \ (WRES13 <-> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) & \ |
|
111 \ (WRES11 <-> WRES9 | WRES6 & ~IN8) & \ |
|
112 \ (WRES8 <-> WRES1 & ~IN5 & IN4 & ~IN3 | WRES2 & ~IN2 & IN1) \ |
|
113 \ --> (OUT10 <-> WRES7) & \ |
|
114 \ (OUT9 <-> WRES9 & IN8 | WRES12 | WRES14 & ~IN9 | ~WRES15 & WRES10) & \ |
|
115 \ (OUT8 <-> WRES9 & ~IN8 | WRES15 & WRES6 | WRES4 & IN9) & \ |
|
116 \ (OUT7 <-> WRES13 & IN9) & \ |
|
117 \ (OUT6 <-> WRES13 & ~IN9) & \ |
|
118 \ (OUT5 <-> WRES14 & IN9) & \ |
|
119 \ (OUT4 <-> WRES11 & IN9 | WRES12 & IN8) & \ |
|
120 \ (OUT3 <-> WRES8 & IN9 & ~IN8 | WRES11 & ~IN9 | WRES12 & ~IN8) & \ |
|
121 \ (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) & \ |
|
122 \ (OUT1 <-> WRES7 & IN8) & \ |
|
123 \ (OUT0 <-> WRES7 & ~IN8)"; |
|
124 by (svc_tac 1); |
|
125 qed ""; |
|
126 |
|
127 (*Tautology name: sqn_be. Fast_tac only takes a couple of seconds.*) |
|
128 Goal "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) & \ |
|
129 \ (GE8 <-> ~IN3 & ~IN1) & \ |
|
130 \ (GE5 <-> IN6 | IN5) & \ |
|
131 \ (GE9 <-> ~GE0 | IN2 | ~IN5) & \ |
|
132 \ (GE1 <-> IN3 | ~IN0) & \ |
|
133 \ (GE11 <-> GE8 & IN4) & \ |
|
134 \ (GE3 <-> ~IN4 | ~IN2) & \ |
|
135 \ (GE34 <-> ~GE5 & IN4 | ~GE9) & \ |
|
136 \ (GE2 <-> ~IN4 & IN1) & \ |
|
137 \ (GE14 <-> ~GE1 & ~IN4) & \ |
|
138 \ (GE19 <-> GE11 & ~GE5) & \ |
|
139 \ (GE13 <-> GE8 & ~GE3 & ~IN0) & \ |
|
140 \ (GE20 <-> ~IN5 & IN2 | GE34) & \ |
|
141 \ (GE12 <-> GE2 & ~IN3) & \ |
|
142 \ (GE27 <-> GE14 & IN6 | GE19) & \ |
|
143 \ (GE10 <-> ~IN6 | IN5) & \ |
|
144 \ (GE28 <-> GE13 | GE20 & ~GE1) & \ |
|
145 \ (GE6 <-> ~IN5 | IN6) & \ |
|
146 \ (GE15 <-> GE2 & IN2) & \ |
|
147 \ (GE29 <-> GE27 | GE12 & GE5) & \ |
|
148 \ (GE4 <-> IN3 & ~IN0) & \ |
|
149 \ (GE21 <-> ~GE10 & ~IN1 | ~IN5 & ~IN2) & \ |
|
150 \ (GE30 <-> GE28 | GE14 & IN2) & \ |
|
151 \ (GE31 <-> GE29 | GE15 & ~GE6) & \ |
|
152 \ (GE7 <-> ~IN6 | ~IN5) & \ |
|
153 \ (GE17 <-> ~GE3 & ~IN1) & \ |
|
154 \ (GE18 <-> GE4 & IN2) & \ |
|
155 \ (GE16 <-> GE2 & IN0) & \ |
|
156 \ (GE23 <-> GE19 | GE9 & ~GE1) & \ |
|
157 \ (GE32 <-> GE15 & ~IN6 & ~IN0 | GE21 & GE4 & ~IN4 | GE30 | GE31) & \ |
|
158 \ (GE33 <-> \ |
|
159 \ GE18 & ~GE6 & ~IN4 | \ |
|
160 \ GE17 & ~GE7 & IN3 | \ |
|
161 \ ~GE7 & GE4 & ~GE3 | \ |
|
162 \ GE11 & IN5 & ~IN0) & \ |
|
163 \ (GE25 <-> GE14 & ~GE6 | GE13 & ~GE5 | GE16 & ~IN5 | GE15 & GE1) & \ |
|
164 \ (GE26 <-> \ |
|
165 \ GE12 & IN5 & ~IN2 | \ |
|
166 \ GE10 & GE4 & IN1 | \ |
|
167 \ GE17 & ~GE6 & IN0 | \ |
|
168 \ GE2 & ~IN6) & \ |
|
169 \ (GE24 <-> GE23 | GE16 & GE7) & \ |
|
170 \ (OUT0 <-> \ |
|
171 \ GE6 & IN4 & ~IN1 & IN0 | GE18 & GE0 & ~IN5 | GE12 & ~GE10 | GE24) & \ |
|
172 \ (OUT1 <-> GE26 | GE25 | ~GE5 & GE4 & GE3 | GE7 & ~GE1 & IN1) & \ |
|
173 \ (OUT2 <-> GE33 | GE32) & \ |
|
174 \ (WRES8 <-> ~IN3 & ~IN1) & \ |
|
175 \ (WRES0 <-> IN6 & IN1 | ~IN6 & ~IN1) & \ |
|
176 \ (WRES2 <-> ~IN4 & IN1) & \ |
|
177 \ (WRES3 <-> ~IN4 | ~IN2) & \ |
|
178 \ (WRES1 <-> IN3 | ~IN0) & \ |
|
179 \ (WRES4 <-> IN3 & ~IN0) & \ |
|
180 \ (WRES5 <-> IN6 | IN5) & \ |
|
181 \ (WRES11 <-> WRES8 & IN4) & \ |
|
182 \ (WRES9 <-> ~WRES0 | IN2 | ~IN5) & \ |
|
183 \ (WRES10 <-> ~IN6 | IN5) & \ |
|
184 \ (WRES6 <-> ~IN5 | IN6) & \ |
|
185 \ (WRES7 <-> ~IN6 | ~IN5) & \ |
|
186 \ (WRES12 <-> WRES2 & ~IN3) & \ |
|
187 \ (WRES13 <-> WRES8 & ~WRES3 & ~IN0) & \ |
|
188 \ (WRES14 <-> ~WRES1 & ~IN4) & \ |
|
189 \ (WRES15 <-> WRES2 & IN2) & \ |
|
190 \ (WRES17 <-> ~WRES3 & ~IN1) & \ |
|
191 \ (WRES18 <-> WRES4 & IN2) & \ |
|
192 \ (WRES19 <-> WRES11 & ~WRES5) & \ |
|
193 \ (WRES20 <-> ~IN5 & IN2 | ~WRES5 & IN4 | ~WRES9) & \ |
|
194 \ (WRES21 <-> ~WRES10 & ~IN1 | ~IN5 & ~IN2) & \ |
|
195 \ (WRES16 <-> WRES2 & IN0) \ |
|
196 \ --> (OUT2 <-> \ |
|
197 \ WRES11 & IN5 & ~IN0 | \ |
|
198 \ ~WRES7 & WRES4 & ~WRES3 | \ |
|
199 \ WRES12 & WRES5 | \ |
|
200 \ WRES13 | \ |
|
201 \ WRES14 & IN2 | \ |
|
202 \ WRES14 & IN6 | \ |
|
203 \ WRES15 & ~WRES6 | \ |
|
204 \ WRES15 & ~IN6 & ~IN0 | \ |
|
205 \ WRES17 & ~WRES7 & IN3 | \ |
|
206 \ WRES18 & ~WRES6 & ~IN4 | \ |
|
207 \ WRES20 & ~WRES1 | \ |
|
208 \ WRES21 & WRES4 & ~IN4 | \ |
|
209 \ WRES19) & \ |
|
210 \ (OUT1 <-> \ |
|
211 \ ~WRES5 & WRES4 & WRES3 | \ |
|
212 \ WRES7 & ~WRES1 & IN1 | \ |
|
213 \ WRES2 & ~IN6 | \ |
|
214 \ WRES10 & WRES4 & IN1 | \ |
|
215 \ WRES12 & IN5 & ~IN2 | \ |
|
216 \ WRES13 & ~WRES5 | \ |
|
217 \ WRES14 & ~WRES6 | \ |
|
218 \ WRES15 & WRES1 | \ |
|
219 \ WRES16 & ~IN5 | \ |
|
220 \ WRES17 & ~WRES6 & IN0) & \ |
|
221 \ (OUT0 <-> \ |
|
222 \ WRES6 & IN4 & ~IN1 & IN0 | \ |
|
223 \ WRES9 & ~WRES1 | \ |
|
224 \ WRES12 & ~WRES10 | \ |
|
225 \ WRES16 & WRES7 | \ |
|
226 \ WRES18 & WRES0 & ~IN5 | \ |
|
227 \ WRES19)"; |
|
228 by (svc_tac 1); |
|
229 qed ""; |
|
230 |
|
231 |
|
232 (** Linear arithmetic **) |
|
233 |
|
234 Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \ |
|
235 \ x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \ |
|
236 \ x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"; |
|
237 by (svc_tac 1); |
|
238 qed ""; |
|
239 |
|
240 (*merely to test polarity handling in the presence of biconditionals*) |
|
241 Goal "(x < (y::int)) = (x+1 <= y)"; |
|
242 by (svc_tac 1); |
|
243 qed ""; |
|
244 |
|
245 (** Natural number examples requiring implicit "non-negative" assumptions*) |
|
246 |
|
247 Goal "(3::nat)*a <= 2 + 4*b + 6*c & 11 <= 2*a + b + 2*c & \ |
|
248 \ a + 3*b <= 5 + 2*c --> 2 + 3*b <= 2*a + 6*c"; |
|
249 by (svc_tac 1); |
|
250 qed ""; |
|
251 |
|
252 Goal "(n::nat) < 2 ==> (n = 0) | (n = 1)"; |
|
253 by (svc_tac 1); |
|
254 qed ""; |
|