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