merged
authorhuffman
Tue Sep 06 10:30:33 2011 -0700 (2011-09-06)
changeset 447578aae88168599
parent 44756 efcd71fbaeec
parent 44754 265174356212
child 44758 deb929f002b8
merged
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 10:30:00 2011 -0700
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 10:30:33 2011 -0700
     1.3 @@ -60074,3 +60074,483 @@
     1.4  #110 := [asserted]: #38
     1.5  [mp #110 #120]: false
     1.6  unsat
     1.7 +8021f8e09eb3e47791aed2bed0dafccd5948187d 69 0
     1.8 +#2 := false
     1.9 +decl f4 :: (-> S2 S1)
    1.10 +decl f5 :: S2
    1.11 +#16 := f5
    1.12 +#19 := (f4 f5)
    1.13 +decl f1 :: S1
    1.14 +#4 := f1
    1.15 +#66 := (= f1 #19)
    1.16 +#70 := (not #66)
    1.17 +#20 := (= #19 f1)
    1.18 +#21 := (not #20)
    1.19 +#71 := (iff #21 #70)
    1.20 +#68 := (iff #20 #66)
    1.21 +#69 := [rewrite]: #68
    1.22 +#72 := [monotonicity #69]: #71
    1.23 +#65 := [asserted]: #21
    1.24 +#75 := [mp #65 #72]: #70
    1.25 +decl f3 :: (-> S2 S1)
    1.26 +#17 := (f3 f5)
    1.27 +#61 := (= f1 #17)
    1.28 +#18 := (= #17 f1)
    1.29 +#63 := (iff #18 #61)
    1.30 +#64 := [rewrite]: #63
    1.31 +#60 := [asserted]: #18
    1.32 +#67 := [mp #60 #64]: #61
    1.33 +#8 := (:var 0 S2)
    1.34 +#9 := (f3 #8)
    1.35 +#10 := (pattern #9)
    1.36 +#12 := (f4 #8)
    1.37 +#45 := (= f1 #12)
    1.38 +#42 := (= f1 #9)
    1.39 +#51 := (not #42)
    1.40 +#52 := (or #51 #45)
    1.41 +#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
    1.42 +#85 := (~ #57 #57)
    1.43 +#83 := (~ #52 #52)
    1.44 +#84 := [refl]: #83
    1.45 +#86 := [nnf-pos #84]: #85
    1.46 +#13 := (= #12 f1)
    1.47 +#11 := (= #9 f1)
    1.48 +#14 := (implies #11 #13)
    1.49 +#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
    1.50 +#58 := (iff #15 #57)
    1.51 +#55 := (iff #14 #52)
    1.52 +#48 := (implies #42 #45)
    1.53 +#53 := (iff #48 #52)
    1.54 +#54 := [rewrite]: #53
    1.55 +#49 := (iff #14 #48)
    1.56 +#46 := (iff #13 #45)
    1.57 +#47 := [rewrite]: #46
    1.58 +#43 := (iff #11 #42)
    1.59 +#44 := [rewrite]: #43
    1.60 +#50 := [monotonicity #44 #47]: #49
    1.61 +#56 := [trans #50 #54]: #55
    1.62 +#59 := [quant-intro #56]: #58
    1.63 +#41 := [asserted]: #15
    1.64 +#62 := [mp #41 #59]: #57
    1.65 +#74 := [mp~ #62 #86]: #57
    1.66 +#137 := (not #61)
    1.67 +#139 := (not #57)
    1.68 +#226 := (or #139 #137 #66)
    1.69 +#224 := (or #137 #66)
    1.70 +#217 := (or #139 #224)
    1.71 +#229 := (iff #217 #226)
    1.72 +#157 := [rewrite]: #229
    1.73 +#228 := [quant-inst #16]: #217
    1.74 +#230 := [mp #228 #157]: #226
    1.75 +[unit-resolution #230 #74 #67 #75]: false
    1.76 +unsat
    1.77 +51102b6663906c70b84f1c6e3a1a2e429b49188d 112 0
    1.78 +#2 := false
    1.79 +decl f5 :: (-> S2 S1)
    1.80 +decl f6 :: S2
    1.81 +#19 := f6
    1.82 +#24 := (f5 f6)
    1.83 +decl f1 :: S1
    1.84 +#4 := f1
    1.85 +#82 := (= f1 #24)
    1.86 +#86 := (not #82)
    1.87 +#25 := (= #24 f1)
    1.88 +#26 := (not #25)
    1.89 +#87 := (iff #26 #86)
    1.90 +#84 := (iff #25 #82)
    1.91 +#85 := [rewrite]: #84
    1.92 +#88 := [monotonicity #85]: #87
    1.93 +#81 := [asserted]: #26
    1.94 +#91 := [mp #81 #88]: #86
    1.95 +decl f4 :: (-> S2 S1)
    1.96 +#22 := (f4 f6)
    1.97 +#77 := (= f1 #22)
    1.98 +#23 := (= #22 f1)
    1.99 +#79 := (iff #23 #77)
   1.100 +#80 := [rewrite]: #79
   1.101 +#76 := [asserted]: #23
   1.102 +#83 := [mp #76 #80]: #77
   1.103 +decl f3 :: (-> S2 S1)
   1.104 +#20 := (f3 f6)
   1.105 +#72 := (= f1 #20)
   1.106 +#21 := (= #20 f1)
   1.107 +#74 := (iff #21 #72)
   1.108 +#75 := [rewrite]: #74
   1.109 +#71 := [asserted]: #21
   1.110 +#78 := [mp #71 #75]: #72
   1.111 +#8 := (:var 0 S2)
   1.112 +#10 := (f4 #8)
   1.113 +#9 := (f3 #8)
   1.114 +#11 := (pattern #9 #10)
   1.115 +#15 := (f5 #8)
   1.116 +#56 := (= f1 #15)
   1.117 +#50 := (= f1 #10)
   1.118 +#105 := (not #50)
   1.119 +#47 := (= f1 #9)
   1.120 +#92 := (not #47)
   1.121 +#112 := (or #92 #105 #56)
   1.122 +#117 := (forall (vars (?v0 S2)) (:pat #11) #112)
   1.123 +#53 := (and #47 #50)
   1.124 +#62 := (not #53)
   1.125 +#63 := (or #62 #56)
   1.126 +#68 := (forall (vars (?v0 S2)) (:pat #11) #63)
   1.127 +#118 := (iff #68 #117)
   1.128 +#115 := (iff #63 #112)
   1.129 +#93 := (or #92 #105)
   1.130 +#109 := (or #93 #56)
   1.131 +#113 := (iff #109 #112)
   1.132 +#114 := [rewrite]: #113
   1.133 +#110 := (iff #63 #109)
   1.134 +#107 := (iff #62 #93)
   1.135 +#94 := (not #93)
   1.136 +#97 := (not #94)
   1.137 +#96 := (iff #97 #93)
   1.138 +#106 := [rewrite]: #96
   1.139 +#98 := (iff #62 #97)
   1.140 +#99 := (iff #53 #94)
   1.141 +#100 := [rewrite]: #99
   1.142 +#95 := [monotonicity #100]: #98
   1.143 +#108 := [trans #95 #106]: #107
   1.144 +#111 := [monotonicity #108]: #110
   1.145 +#116 := [trans #111 #114]: #115
   1.146 +#119 := [quant-intro #116]: #118
   1.147 +#103 := (~ #68 #68)
   1.148 +#101 := (~ #63 #63)
   1.149 +#102 := [refl]: #101
   1.150 +#104 := [nnf-pos #102]: #103
   1.151 +#16 := (= #15 f1)
   1.152 +#13 := (= #10 f1)
   1.153 +#12 := (= #9 f1)
   1.154 +#14 := (and #12 #13)
   1.155 +#17 := (implies #14 #16)
   1.156 +#18 := (forall (vars (?v0 S2)) (:pat #11) #17)
   1.157 +#69 := (iff #18 #68)
   1.158 +#66 := (iff #17 #63)
   1.159 +#59 := (implies #53 #56)
   1.160 +#64 := (iff #59 #63)
   1.161 +#65 := [rewrite]: #64
   1.162 +#60 := (iff #17 #59)
   1.163 +#57 := (iff #16 #56)
   1.164 +#58 := [rewrite]: #57
   1.165 +#54 := (iff #14 #53)
   1.166 +#51 := (iff #13 #50)
   1.167 +#52 := [rewrite]: #51
   1.168 +#48 := (iff #12 #47)
   1.169 +#49 := [rewrite]: #48
   1.170 +#55 := [monotonicity #49 #52]: #54
   1.171 +#61 := [monotonicity #55 #58]: #60
   1.172 +#67 := [trans #61 #65]: #66
   1.173 +#70 := [quant-intro #67]: #69
   1.174 +#46 := [asserted]: #18
   1.175 +#73 := [mp #46 #70]: #68
   1.176 +#90 := [mp~ #73 #104]: #68
   1.177 +#120 := [mp #90 #119]: #117
   1.178 +#178 := (not #77)
   1.179 +#265 := (not #72)
   1.180 +#267 := (not #117)
   1.181 +#258 := (or #267 #265 #178 #82)
   1.182 +#179 := (or #265 #178 #82)
   1.183 +#269 := (or #267 #179)
   1.184 +#198 := (iff #269 #258)
   1.185 +#271 := [rewrite]: #198
   1.186 +#270 := [quant-inst #19]: #269
   1.187 +#268 := [mp #270 #271]: #258
   1.188 +[unit-resolution #268 #120 #78 #83 #91]: false
   1.189 +unsat
   1.190 +1191e209015c2f2f439f124434700d861e089600 149 0
   1.191 +#2 := false
   1.192 +decl f3 :: (-> S2 S1)
   1.193 +decl f6 :: S2
   1.194 +#21 := f6
   1.195 +#22 := (f3 f6)
   1.196 +decl f1 :: S1
   1.197 +#4 := f1
   1.198 +#84 := (= f1 #22)
   1.199 +#264 := (not #84)
   1.200 +decl f5 :: (-> S2 S1)
   1.201 +#27 := (f5 f6)
   1.202 +#95 := (= f1 #27)
   1.203 +#178 := (or #264 #95)
   1.204 +decl f4 :: (-> S2 S1)
   1.205 +#24 := (f4 f6)
   1.206 +#88 := (= f1 #24)
   1.207 +#176 := (not #88)
   1.208 +#268 := (or #176 #95)
   1.209 +#266 := (not #268)
   1.210 +#265 := (not #178)
   1.211 +#586 := (or #265 #266)
   1.212 +#375 := (not #586)
   1.213 +#579 := [hypothesis]: #586
   1.214 +#8 := (:var 0 S2)
   1.215 +#11 := (f4 #8)
   1.216 +#12 := (pattern #11)
   1.217 +#9 := (f3 #8)
   1.218 +#10 := (pattern #9)
   1.219 +#65 := (= f1 #11)
   1.220 +#71 := (not #65)
   1.221 +#14 := (f5 #8)
   1.222 +#53 := (= f1 #14)
   1.223 +#72 := (or #53 #71)
   1.224 +#116 := (not #72)
   1.225 +#50 := (= f1 #9)
   1.226 +#59 := (not #50)
   1.227 +#60 := (or #59 #53)
   1.228 +#105 := (not #60)
   1.229 +#106 := (or #105 #116)
   1.230 +#107 := (not #106)
   1.231 +#108 := (forall (vars (?v0 S2)) (:pat #10 #12) #107)
   1.232 +#77 := (and #60 #72)
   1.233 +#80 := (forall (vars (?v0 S2)) (:pat #10 #12) #77)
   1.234 +#109 := (iff #80 #108)
   1.235 +#110 := (iff #77 #107)
   1.236 +#111 := [rewrite]: #110
   1.237 +#117 := [quant-intro #111]: #109
   1.238 +#114 := (~ #80 #80)
   1.239 +#112 := (~ #77 #77)
   1.240 +#113 := [refl]: #112
   1.241 +#115 := [nnf-pos #113]: #114
   1.242 +#15 := (= #14 f1)
   1.243 +#17 := (= #11 f1)
   1.244 +#18 := (implies #17 #15)
   1.245 +#13 := (= #9 f1)
   1.246 +#16 := (implies #13 #15)
   1.247 +#19 := (and #16 #18)
   1.248 +#20 := (forall (vars (?v0 S2)) (:pat #10 #12) #19)
   1.249 +#81 := (iff #20 #80)
   1.250 +#78 := (iff #19 #77)
   1.251 +#75 := (iff #18 #72)
   1.252 +#68 := (implies #65 #53)
   1.253 +#73 := (iff #68 #72)
   1.254 +#74 := [rewrite]: #73
   1.255 +#69 := (iff #18 #68)
   1.256 +#54 := (iff #15 #53)
   1.257 +#55 := [rewrite]: #54
   1.258 +#66 := (iff #17 #65)
   1.259 +#67 := [rewrite]: #66
   1.260 +#70 := [monotonicity #67 #55]: #69
   1.261 +#76 := [trans #70 #74]: #75
   1.262 +#63 := (iff #16 #60)
   1.263 +#56 := (implies #50 #53)
   1.264 +#61 := (iff #56 #60)
   1.265 +#62 := [rewrite]: #61
   1.266 +#57 := (iff #16 #56)
   1.267 +#51 := (iff #13 #50)
   1.268 +#52 := [rewrite]: #51
   1.269 +#58 := [monotonicity #52 #55]: #57
   1.270 +#64 := [trans #58 #62]: #63
   1.271 +#79 := [monotonicity #64 #76]: #78
   1.272 +#82 := [quant-intro #79]: #81
   1.273 +#49 := [asserted]: #20
   1.274 +#85 := [mp #49 #82]: #80
   1.275 +#103 := [mp~ #85 #115]: #80
   1.276 +#118 := [mp #103 #117]: #108
   1.277 +#255 := (not #108)
   1.278 +#589 := (or #255 #375)
   1.279 +#263 := (or #95 #176)
   1.280 +#177 := (not #263)
   1.281 +#256 := (or #265 #177)
   1.282 +#267 := (not #256)
   1.283 +#590 := (or #255 #267)
   1.284 +#592 := (iff #590 #589)
   1.285 +#593 := (iff #589 #589)
   1.286 +#583 := [rewrite]: #593
   1.287 +#582 := (iff #267 #375)
   1.288 +#588 := (iff #256 #586)
   1.289 +#270 := (iff #177 #266)
   1.290 +#196 := (iff #263 #268)
   1.291 +#269 := [rewrite]: #196
   1.292 +#249 := [monotonicity #269]: #270
   1.293 +#243 := [monotonicity #249]: #588
   1.294 +#254 := [monotonicity #243]: #582
   1.295 +#587 := [monotonicity #254]: #592
   1.296 +#241 := [trans #587 #583]: #592
   1.297 +#591 := [quant-inst #21]: #590
   1.298 +#246 := [mp #591 #241]: #589
   1.299 +#217 := [unit-resolution #246 #118 #579]: false
   1.300 +#218 := [lemma #217]: #375
   1.301 +#574 := (or #586 #178)
   1.302 +#575 := [def-axiom]: #574
   1.303 +#580 := [unit-resolution #575 #218]: #178
   1.304 +#578 := (or #265 #264)
   1.305 +#99 := (not #95)
   1.306 +#28 := (= #27 f1)
   1.307 +#29 := (not #28)
   1.308 +#100 := (iff #29 #99)
   1.309 +#97 := (iff #28 #95)
   1.310 +#98 := [rewrite]: #97
   1.311 +#101 := [monotonicity #98]: #100
   1.312 +#94 := [asserted]: #29
   1.313 +#104 := [mp #94 #101]: #99
   1.314 +#569 := (or #265 #264 #95)
   1.315 +#230 := [def-axiom]: #569
   1.316 +#581 := [unit-resolution #230 #104]: #578
   1.317 +#567 := [unit-resolution #581 #580]: #264
   1.318 +#570 := (or #586 #268)
   1.319 +#576 := [def-axiom]: #570
   1.320 +#568 := [unit-resolution #576 #218]: #268
   1.321 +#274 := (or #266 #176)
   1.322 +#572 := (or #266 #176 #95)
   1.323 +#573 := [def-axiom]: #572
   1.324 +#290 := [unit-resolution #573 #104]: #274
   1.325 +#291 := [unit-resolution #290 #568]: #176
   1.326 +#91 := (or #84 #88)
   1.327 +#25 := (= #24 f1)
   1.328 +#23 := (= #22 f1)
   1.329 +#26 := (or #23 #25)
   1.330 +#92 := (iff #26 #91)
   1.331 +#89 := (iff #25 #88)
   1.332 +#90 := [rewrite]: #89
   1.333 +#86 := (iff #23 #84)
   1.334 +#87 := [rewrite]: #86
   1.335 +#93 := [monotonicity #87 #90]: #92
   1.336 +#83 := [asserted]: #26
   1.337 +#96 := [mp #83 #93]: #91
   1.338 +[unit-resolution #96 #291 #567]: false
   1.339 +unsat
   1.340 +45f8ffe676ed981a383aaab6faaf520b9ff236c9 69 0
   1.341 +#2 := false
   1.342 +decl f4 :: (-> S2 S1)
   1.343 +decl f5 :: S2
   1.344 +#16 := f5
   1.345 +#19 := (f4 f5)
   1.346 +decl f1 :: S1
   1.347 +#4 := f1
   1.348 +#66 := (= f1 #19)
   1.349 +#70 := (not #66)
   1.350 +#20 := (= #19 f1)
   1.351 +#21 := (not #20)
   1.352 +#71 := (iff #21 #70)
   1.353 +#68 := (iff #20 #66)
   1.354 +#69 := [rewrite]: #68
   1.355 +#72 := [monotonicity #69]: #71
   1.356 +#65 := [asserted]: #21
   1.357 +#75 := [mp #65 #72]: #70
   1.358 +decl f3 :: (-> S2 S1)
   1.359 +#17 := (f3 f5)
   1.360 +#61 := (= f1 #17)
   1.361 +#18 := (= #17 f1)
   1.362 +#63 := (iff #18 #61)
   1.363 +#64 := [rewrite]: #63
   1.364 +#60 := [asserted]: #18
   1.365 +#67 := [mp #60 #64]: #61
   1.366 +#8 := (:var 0 S2)
   1.367 +#9 := (f3 #8)
   1.368 +#10 := (pattern #9)
   1.369 +#12 := (f4 #8)
   1.370 +#45 := (= f1 #12)
   1.371 +#42 := (= f1 #9)
   1.372 +#51 := (not #42)
   1.373 +#52 := (or #51 #45)
   1.374 +#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
   1.375 +#85 := (~ #57 #57)
   1.376 +#83 := (~ #52 #52)
   1.377 +#84 := [refl]: #83
   1.378 +#86 := [nnf-pos #84]: #85
   1.379 +#13 := (= #12 f1)
   1.380 +#11 := (= #9 f1)
   1.381 +#14 := (implies #11 #13)
   1.382 +#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
   1.383 +#58 := (iff #15 #57)
   1.384 +#55 := (iff #14 #52)
   1.385 +#48 := (implies #42 #45)
   1.386 +#53 := (iff #48 #52)
   1.387 +#54 := [rewrite]: #53
   1.388 +#49 := (iff #14 #48)
   1.389 +#46 := (iff #13 #45)
   1.390 +#47 := [rewrite]: #46
   1.391 +#43 := (iff #11 #42)
   1.392 +#44 := [rewrite]: #43
   1.393 +#50 := [monotonicity #44 #47]: #49
   1.394 +#56 := [trans #50 #54]: #55
   1.395 +#59 := [quant-intro #56]: #58
   1.396 +#41 := [asserted]: #15
   1.397 +#62 := [mp #41 #59]: #57
   1.398 +#74 := [mp~ #62 #86]: #57
   1.399 +#137 := (not #61)
   1.400 +#139 := (not #57)
   1.401 +#226 := (or #139 #137 #66)
   1.402 +#224 := (or #137 #66)
   1.403 +#217 := (or #139 #224)
   1.404 +#229 := (iff #217 #226)
   1.405 +#157 := [rewrite]: #229
   1.406 +#228 := [quant-inst #16]: #217
   1.407 +#230 := [mp #228 #157]: #226
   1.408 +[unit-resolution #230 #74 #67 #75]: false
   1.409 +unsat
   1.410 +ceabafba9f0db45264556e8d9525b667725281c7 76 0
   1.411 +#2 := false
   1.412 +decl f4 :: (-> S2 S1)
   1.413 +decl f5 :: S2
   1.414 +#15 := f5
   1.415 +#18 := (f4 f5)
   1.416 +decl f1 :: S1
   1.417 +#4 := f1
   1.418 +#65 := (= f1 #18)
   1.419 +#69 := (not #65)
   1.420 +#19 := (= #18 f1)
   1.421 +#20 := (not #19)
   1.422 +#70 := (iff #20 #69)
   1.423 +#67 := (iff #19 #65)
   1.424 +#68 := [rewrite]: #67
   1.425 +#71 := [monotonicity #68]: #70
   1.426 +#64 := [asserted]: #20
   1.427 +#74 := [mp #64 #71]: #69
   1.428 +decl f3 :: (-> S2 S1)
   1.429 +#16 := (f3 f5)
   1.430 +#60 := (= f1 #16)
   1.431 +#17 := (= #16 f1)
   1.432 +#62 := (iff #17 #60)
   1.433 +#63 := [rewrite]: #62
   1.434 +#59 := [asserted]: #17
   1.435 +#66 := [mp #59 #63]: #60
   1.436 +#8 := (:var 0 S2)
   1.437 +#11 := (f4 #8)
   1.438 +#555 := (pattern #11)
   1.439 +#9 := (f3 #8)
   1.440 +#554 := (pattern #9)
   1.441 +#44 := (= f1 #11)
   1.442 +#41 := (= f1 #9)
   1.443 +#50 := (not #41)
   1.444 +#51 := (or #50 #44)
   1.445 +#556 := (forall (vars (?v0 S2)) (:pat #554 #555) #51)
   1.446 +#56 := (forall (vars (?v0 S2)) #51)
   1.447 +#559 := (iff #56 #556)
   1.448 +#557 := (iff #51 #51)
   1.449 +#558 := [refl]: #557
   1.450 +#560 := [quant-intro #558]: #559
   1.451 +#84 := (~ #56 #56)
   1.452 +#82 := (~ #51 #51)
   1.453 +#83 := [refl]: #82
   1.454 +#85 := [nnf-pos #83]: #84
   1.455 +#12 := (= #11 f1)
   1.456 +#10 := (= #9 f1)
   1.457 +#13 := (implies #10 #12)
   1.458 +#14 := (forall (vars (?v0 S2)) #13)
   1.459 +#57 := (iff #14 #56)
   1.460 +#54 := (iff #13 #51)
   1.461 +#47 := (implies #41 #44)
   1.462 +#52 := (iff #47 #51)
   1.463 +#53 := [rewrite]: #52
   1.464 +#48 := (iff #13 #47)
   1.465 +#45 := (iff #12 #44)
   1.466 +#46 := [rewrite]: #45
   1.467 +#42 := (iff #10 #41)
   1.468 +#43 := [rewrite]: #42
   1.469 +#49 := [monotonicity #43 #46]: #48
   1.470 +#55 := [trans #49 #53]: #54
   1.471 +#58 := [quant-intro #55]: #57
   1.472 +#40 := [asserted]: #14
   1.473 +#61 := [mp #40 #58]: #56
   1.474 +#73 := [mp~ #61 #85]: #56
   1.475 +#561 := [mp #73 #560]: #556
   1.476 +#136 := (not #60)
   1.477 +#138 := (not #556)
   1.478 +#225 := (or #138 #136 #65)
   1.479 +#223 := (or #136 #65)
   1.480 +#216 := (or #138 #223)
   1.481 +#228 := (iff #216 #225)
   1.482 +#156 := [rewrite]: #228
   1.483 +#227 := [quant-inst #15]: #216
   1.484 +#229 := [mp #227 #156]: #225
   1.485 +[unit-resolution #229 #561 #66 #74]: false
   1.486 +unsat
     2.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 10:30:00 2011 -0700
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 10:30:33 2011 -0700
     2.3 @@ -201,6 +201,9 @@
     2.4    "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
     2.5    by smt+
     2.6  
     2.7 +
     2.8 +section {* Guidance for quantifier heuristics: patterns and weights *}
     2.9 +
    2.10  lemma
    2.11    assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
    2.12    shows "f 1 = 1"
    2.13 @@ -211,6 +214,38 @@
    2.14    shows "f 1 = g 2"
    2.15    using assms by smt
    2.16  
    2.17 +lemma
    2.18 +  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
    2.19 +  and "P t"
    2.20 +  shows "Q t"
    2.21 +  using assms by smt
    2.22 +
    2.23 +lemma
    2.24 +  assumes "ALL x. SMT.trigger [[SMT.pat (P x), SMT.pat (Q x)]]
    2.25 +    (P x & Q x --> R x)"
    2.26 +  and "P t" and "Q t"
    2.27 +  shows "R t"
    2.28 +  using assms by smt
    2.29 +
    2.30 +lemma
    2.31 +  assumes "ALL x. SMT.trigger [[SMT.pat (P x)], [SMT.pat (Q x)]]
    2.32 +    ((P x --> R x) & (Q x --> R x))"
    2.33 +  and "P t | Q t"
    2.34 +  shows "R t"
    2.35 +  using assms by smt
    2.36 +
    2.37 +lemma
    2.38 +  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (SMT.weight 2 (P x --> Q x))"
    2.39 +  and "P t"
    2.40 +  shows "Q t"
    2.41 +  using assms by smt
    2.42 +
    2.43 +lemma
    2.44 +  assumes "ALL x. SMT.weight 1 (P x --> Q x)"
    2.45 +  and "P t"
    2.46 +  shows "Q t"
    2.47 +  using assms by smt
    2.48 +
    2.49  
    2.50  
    2.51  section {* Meta logical connectives *}
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 10:30:00 2011 -0700
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 10:30:33 2011 -0700
     3.3 @@ -22,15 +22,15 @@
     3.4      AFun of 'a ho_type * 'a ho_type |
     3.5      ATyAbs of 'a list * 'a ho_type
     3.6  
     3.7 -  datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
     3.8 -  datatype tff_explicitness = TFF_Implicit | TFF_Explicit
     3.9 +  datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
    3.10 +  datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
    3.11    datatype thf_flavor = THF_Without_Choice | THF_With_Choice
    3.12 -  datatype format =
    3.13 +  datatype tptp_format =
    3.14      CNF |
    3.15      CNF_UEQ |
    3.16      FOF |
    3.17 -    TFF of tff_polymorphism * tff_explicitness |
    3.18 -    THF0 of thf_flavor
    3.19 +    TFF of tptp_polymorphism * tptp_explicitness |
    3.20 +    THF of tptp_polymorphism * tptp_explicitness * thf_flavor
    3.21  
    3.22    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    3.23    datatype 'a problem_line =
    3.24 @@ -92,9 +92,9 @@
    3.25      bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
    3.26      -> 'd -> 'd
    3.27    val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
    3.28 -  val is_format_thf : format -> bool
    3.29 -  val is_format_typed : format -> bool
    3.30 -  val tptp_lines_for_atp_problem : format -> string problem -> string list
    3.31 +  val is_format_thf : tptp_format -> bool
    3.32 +  val is_format_typed : tptp_format -> bool
    3.33 +  val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
    3.34    val ensure_cnf_problem :
    3.35      (string * string) problem -> (string * string) problem
    3.36    val filter_cnf_ueq_problem :
    3.37 @@ -130,16 +130,16 @@
    3.38    AFun of 'a ho_type * 'a ho_type |
    3.39    ATyAbs of 'a list * 'a ho_type
    3.40  
    3.41 -datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
    3.42 -datatype tff_explicitness = TFF_Implicit | TFF_Explicit
    3.43 +datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
    3.44 +datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
    3.45  datatype thf_flavor = THF_Without_Choice | THF_With_Choice
    3.46  
    3.47 -datatype format =
    3.48 +datatype tptp_format =
    3.49    CNF |
    3.50    CNF_UEQ |
    3.51    FOF |
    3.52 -  TFF of tff_polymorphism * tff_explicitness |
    3.53 -  THF0 of thf_flavor
    3.54 +  TFF of tptp_polymorphism * tptp_explicitness |
    3.55 +  THF of tptp_polymorphism * tptp_explicitness * thf_flavor
    3.56  
    3.57  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    3.58  datatype 'a problem_line =
    3.59 @@ -224,10 +224,10 @@
    3.60    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
    3.61    | formula_map f (AAtom tm) = AAtom (f tm)
    3.62  
    3.63 -fun is_format_thf (THF0 _) = true
    3.64 +fun is_format_thf (THF _) = true
    3.65    | is_format_thf _ = false
    3.66  fun is_format_typed (TFF _) = true
    3.67 -  | is_format_typed (THF0 _) = true
    3.68 +  | is_format_typed (THF _) = true
    3.69    | is_format_typed _ = false
    3.70  
    3.71  fun string_for_kind Axiom = "axiom"
    3.72 @@ -266,7 +266,7 @@
    3.73                      ss) ^ "]: " ^ str false ty
    3.74    in str true ty end
    3.75  
    3.76 -fun string_for_type (THF0 _) ty = str_for_type ty
    3.77 +fun string_for_type (THF _) ty = str_for_type ty
    3.78    | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
    3.79    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
    3.80  
    3.81 @@ -288,6 +288,9 @@
    3.82     else
    3.83       "")
    3.84  
    3.85 +fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
    3.86 +  | is_format_with_choice _ = false
    3.87 +
    3.88  fun string_for_term _ (ATerm (s, [])) = s
    3.89    | string_for_term format (ATerm (s, ts)) =
    3.90      if s = tptp_empty_list then
    3.91 @@ -298,7 +301,7 @@
    3.92        |> is_format_thf format ? enclose "(" ")"
    3.93      else
    3.94        (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
    3.95 -             s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
    3.96 +             s = tptp_choice andalso is_format_with_choice format, ts) of
    3.97           (true, _, [AAbs ((s', ty), tm)]) =>
    3.98           (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
    3.99              possible, to work around LEO-II 1.2.8 parser limitation. *)
   3.100 @@ -306,8 +309,8 @@
   3.101               (AQuant (if s = tptp_ho_forall then AForall else AExists,
   3.102                        [(s', SOME ty)], AAtom tm))
   3.103         | (_, true, [AAbs ((s', ty), tm)]) =>
   3.104 -         (*There is code in ATP_Translate to ensure that Eps is always applied
   3.105 -           to an abstraction*)
   3.106 +         (* There is code in "ATP_Translate" to ensure that "Eps" is always
   3.107 +            applied to an abstraction. *)
   3.108           tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
   3.109             string_for_term format tm ^ ""
   3.110           |> enclose "(" ")"
   3.111 @@ -319,7 +322,7 @@
   3.112             else
   3.113               s ^ "(" ^ commas ss ^ ")"
   3.114           end)
   3.115 -  | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
   3.116 +  | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
   3.117      "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
   3.118      string_for_term format tm ^ ")"
   3.119    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
   3.120 @@ -352,7 +355,7 @@
   3.121    | string_for_format CNF_UEQ = tptp_cnf
   3.122    | string_for_format FOF = tptp_fof
   3.123    | string_for_format (TFF _) = tptp_tff
   3.124 -  | string_for_format (THF0 _) = tptp_thf
   3.125 +  | string_for_format (THF _) = tptp_thf
   3.126  
   3.127  fun string_for_problem_line format (Decl (ident, sym, ty)) =
   3.128      string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 10:30:00 2011 -0700
     4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 06 10:30:33 2011 -0700
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  signature ATP_SYSTEMS =
     4.6  sig
     4.7 -  type format = ATP_Problem.format
     4.8 +  type tptp_format = ATP_Problem.tptp_format
     4.9    type formula_kind = ATP_Problem.formula_kind
    4.10    type failure = ATP_Proof.failure
    4.11  
    4.12 @@ -22,7 +22,8 @@
    4.13       conj_sym_kind : formula_kind,
    4.14       prem_kind : formula_kind,
    4.15       best_slices :
    4.16 -       Proof.context -> (real * (bool * (int * format * string * string))) list}
    4.17 +       Proof.context
    4.18 +       -> (real * (bool * (int * tptp_format * string * string))) list}
    4.19  
    4.20    val force_sos : bool Config.T
    4.21    val e_smartN : string
    4.22 @@ -41,6 +42,7 @@
    4.23    val e_tofofN : string
    4.24    val leo2N : string
    4.25    val pffN : string
    4.26 +  val phfN : string
    4.27    val satallaxN : string
    4.28    val snarkN : string
    4.29    val spassN : string
    4.30 @@ -51,7 +53,7 @@
    4.31    val remote_atp :
    4.32      string -> string -> string list -> (string * string) list
    4.33      -> (failure * string) list -> formula_kind -> formula_kind
    4.34 -    -> (Proof.context -> int * format * string) -> string * atp_config
    4.35 +    -> (Proof.context -> int * tptp_format * string) -> string * atp_config
    4.36    val add_atp : string * atp_config -> theory -> theory
    4.37    val get_atp : theory -> string -> atp_config
    4.38    val supported_atps : theory -> string list
    4.39 @@ -79,7 +81,8 @@
    4.40     conj_sym_kind : formula_kind,
    4.41     prem_kind : formula_kind,
    4.42     best_slices :
    4.43 -     Proof.context -> (real * (bool * (int * format * string * string))) list}
    4.44 +     Proof.context
    4.45 +     -> (real * (bool * (int * tptp_format * string * string))) list}
    4.46  
    4.47  (* "best_slices" must be found empirically, taking a wholistic approach since
    4.48     the ATPs are run in parallel. The "real" components give the faction of the
    4.49 @@ -105,6 +108,7 @@
    4.50  val e_tofofN = "e_tofof"
    4.51  val leo2N = "leo2"
    4.52  val pffN = "pff"
    4.53 +val phfN = "phf"
    4.54  val satallaxN = "satallax"
    4.55  val snarkN = "snark"
    4.56  val spassN = "spass"
    4.57 @@ -230,6 +234,8 @@
    4.58  
    4.59  (* LEO-II *)
    4.60  
    4.61 +val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
    4.62 +
    4.63  val leo2_config : atp_config =
    4.64    {exec = ("LEO2_HOME", "leo"),
    4.65     required_execs = [],
    4.66 @@ -243,10 +249,8 @@
    4.67     prem_kind = Hypothesis,
    4.68     best_slices = fn ctxt =>
    4.69       (* FUDGE *)
    4.70 -     [(0.667, (false, (150, THF0 THF_Without_Choice,
    4.71 -                       "mono_simple_higher", sosN))),
    4.72 -      (0.333, (true, (50, THF0 THF_Without_Choice,
    4.73 -                      "mono_simple_higher", no_sosN)))]
    4.74 +     [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
    4.75 +      (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
    4.76       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    4.77           else I)}
    4.78  
    4.79 @@ -255,6 +259,8 @@
    4.80  
    4.81  (* Satallax *)
    4.82  
    4.83 +val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
    4.84 +
    4.85  val satallax_config : atp_config =
    4.86    {exec = ("SATALLAX_HOME", "satallax"),
    4.87     required_execs = [],
    4.88 @@ -266,8 +272,8 @@
    4.89     conj_sym_kind = Axiom,
    4.90     prem_kind = Hypothesis,
    4.91     best_slices =
    4.92 -     K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
    4.93 -     (* FUDGE *)}
    4.94 +     (* FUDGE *)
    4.95 +     K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
    4.96  
    4.97  val satallax = (satallaxN, satallax_config)
    4.98  
    4.99 @@ -314,7 +320,7 @@
   4.100  fun is_old_vampire_version () =
   4.101    string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
   4.102  
   4.103 -val vampire_tff = TFF (TFF_Monomorphic, TFF_Implicit)
   4.104 +val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   4.105  
   4.106  val vampire_config : atp_config =
   4.107    {exec = ("VAMPIRE_HOME", "vampire"),
   4.108 @@ -347,9 +353,9 @@
   4.109           (0.333, (false, (500, FOF, "mono_tags?", sosN))),
   4.110           (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
   4.111        else
   4.112 -        [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
   4.113 -         (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
   4.114 -         (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
   4.115 +        [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
   4.116 +         (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
   4.117 +         (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
   4.118       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   4.119           else I)}
   4.120  
   4.121 @@ -358,7 +364,7 @@
   4.122  
   4.123  (* Z3 with TPTP syntax *)
   4.124  
   4.125 -val z3_tff = TFF (TFF_Monomorphic, TFF_Implicit)
   4.126 +val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   4.127  
   4.128  val z3_tptp_config : atp_config =
   4.129    {exec = ("Z3_HOME", "z3"),
   4.130 @@ -377,18 +383,17 @@
   4.131     prem_kind = Hypothesis,
   4.132     best_slices =
   4.133       (* FUDGE *)
   4.134 -     K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
   4.135 -        (0.25, (false, (125, z3_tff, "mono_simple", ""))),
   4.136 -        (0.125, (false, (62, z3_tff, "mono_simple", ""))),
   4.137 -        (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
   4.138 +     K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
   4.139 +        (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
   4.140 +        (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
   4.141 +        (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
   4.142  
   4.143  val z3_tptp = (z3_tptpN, z3_tptp_config)
   4.144  
   4.145 -(* Not really a prover: Experimental PFF (Polymorphic TFF) output *)
   4.146  
   4.147 -val poly_tff = TFF (TFF_Polymorphic, TFF_Implicit)
   4.148 +(* Not really a prover: Experimental Polymorphic TFF and THF output *)
   4.149  
   4.150 -val pff_config : atp_config =
   4.151 +fun dummy_config format type_enc : atp_config =
   4.152    {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
   4.153     required_execs = [],
   4.154     arguments = K (K (K (K (K "")))),
   4.155 @@ -396,10 +401,16 @@
   4.156     known_failures = [(GaveUp, "SZS status Unknown")],
   4.157     conj_sym_kind = Hypothesis,
   4.158     prem_kind = Hypothesis,
   4.159 -   best_slices = K [(1.0, (false, (200, poly_tff, "poly_simple", "")))]}
   4.160 +   best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
   4.161  
   4.162 +val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
   4.163 +val pff_config = dummy_config pff_format "poly_simple"
   4.164  val pff = (pffN, pff_config)
   4.165  
   4.166 +val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
   4.167 +val phf_config = dummy_config phf_format "poly_simple_higher"
   4.168 +val phf = (phfN, phf_config)
   4.169 +
   4.170  
   4.171  (* Remote ATP invocation via SystemOnTPTP *)
   4.172  
   4.173 @@ -475,34 +486,33 @@
   4.174    (remote_prefix ^ name,
   4.175     remotify_config system_name system_versions best_slice config)
   4.176  
   4.177 -val dumb_tff = TFF (TFF_Monomorphic, TFF_Explicit)
   4.178 +val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
   4.179  
   4.180  val remote_e =
   4.181    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   4.182                 (K (750, FOF, "mono_tags?") (* FUDGE *))
   4.183  val remote_leo2 =
   4.184    remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   4.185 -               (K (100, THF0 THF_Without_Choice,
   4.186 -                   "mono_simple_higher") (* FUDGE *))
   4.187 +               (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
   4.188  val remote_satallax =
   4.189    remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   4.190 -               (K (100, THF0 THF_With_Choice,
   4.191 -                   "mono_simple_higher") (* FUDGE *))
   4.192 +               (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
   4.193  val remote_vampire =
   4.194    remotify_atp vampire "Vampire" ["1.8"]
   4.195                 (K (250, FOF, "mono_guards?") (* FUDGE *))
   4.196  val remote_z3_tptp =
   4.197 -  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
   4.198 +  remotify_atp z3_tptp "Z3" ["3.0"]
   4.199 +               (K (250, z3_tff0, "mono_simple") (* FUDGE *))
   4.200  val remote_e_sine =
   4.201    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   4.202               Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
   4.203  val remote_snark =
   4.204    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   4.205               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   4.206 -             (K (100, dumb_tff, "mono_simple") (* FUDGE *))
   4.207 +             (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
   4.208  val remote_e_tofof =
   4.209    remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
   4.210 -             Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
   4.211 +             Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
   4.212  val remote_waldmeister =
   4.213    remote_atp waldmeisterN "Waldmeister" ["710"]
   4.214               [("#START OF PROOF", "Proved Goals:")]
   4.215 @@ -532,7 +542,7 @@
   4.216    Synchronized.change systems (fn _ => get_systems ())
   4.217  
   4.218  val atps =
   4.219 -  [e, leo2, pff, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
   4.220 +  [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
   4.221     remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
   4.222     remote_e_tofof, remote_waldmeister]
   4.223  val setup = fold add_atp atps
     5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 10:30:00 2011 -0700
     5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 10:30:33 2011 -0700
     5.3 @@ -11,7 +11,7 @@
     5.4    type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     5.5    type connective = ATP_Problem.connective
     5.6    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
     5.7 -  type format = ATP_Problem.format
     5.8 +  type tptp_format = ATP_Problem.tptp_format
     5.9    type formula_kind = ATP_Problem.formula_kind
    5.10    type 'a problem = 'a ATP_Problem.problem
    5.11  
    5.12 @@ -92,7 +92,7 @@
    5.13    val level_of_type_enc : type_enc -> type_level
    5.14    val is_type_enc_quasi_sound : type_enc -> bool
    5.15    val is_type_enc_fairly_sound : type_enc -> bool
    5.16 -  val adjust_type_enc : format -> type_enc -> type_enc
    5.17 +  val adjust_type_enc : tptp_format -> type_enc -> type_enc
    5.18    val mk_aconns :
    5.19      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    5.20    val unmangled_const : string -> string * (string, 'b) ho_term list
    5.21 @@ -100,7 +100,7 @@
    5.22    val helper_table : ((string * bool) * thm list) list
    5.23    val factsN : string
    5.24    val prepare_atp_problem :
    5.25 -    Proof.context -> format -> formula_kind -> formula_kind -> type_enc
    5.26 +    Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
    5.27      -> bool -> string -> bool -> bool -> term list -> term
    5.28      -> ((string * locality) * term) list
    5.29      -> string problem * string Symtab.table * int * int
    5.30 @@ -142,7 +142,7 @@
    5.31  (* TFF1 is still in development, and it is still unclear whether symbols will be
    5.32     allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
    5.33     "dummy" type variables. *)
    5.34 -val exploit_tff1_dummy_type_vars = false
    5.35 +val avoid_first_order_dummy_type_vars = true
    5.36  
    5.37  val bound_var_prefix = "B_"
    5.38  val all_bound_var_prefix = "BA_"
    5.39 @@ -325,8 +325,8 @@
    5.40    fun default c = const_prefix ^ lookup_const c
    5.41  in
    5.42    fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
    5.43 -    | make_fixed_const (SOME (THF0 THF_With_Choice)) c =
    5.44 -        if c = choice_const then tptp_choice else default c
    5.45 +    | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
    5.46 +      if c = choice_const then tptp_choice else default c
    5.47      | make_fixed_const _ c = default c
    5.48  end
    5.49  
    5.50 @@ -587,7 +587,9 @@
    5.51              | _ => raise Same.SAME)
    5.52           | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    5.53             (case (poly, level) of
    5.54 -              (_, Noninf_Nonmono_Types _) => raise Same.SAME
    5.55 +              (Polymorphic, All_Types) =>
    5.56 +              Simple_Types (Higher_Order, Polymorphic, All_Types)
    5.57 +            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    5.58              | (Mangled_Monomorphic, _) =>
    5.59                Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    5.60              | _ => raise Same.SAME)
    5.61 @@ -631,12 +633,13 @@
    5.62    | is_type_level_monotonicity_based Fin_Nonmono_Types = true
    5.63    | is_type_level_monotonicity_based _ = false
    5.64  
    5.65 -fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
    5.66 +fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
    5.67 +                    (Simple_Types (order, _, level)) =
    5.68      Simple_Types (order, Mangled_Monomorphic, level)
    5.69 -  | adjust_type_enc (THF0 _) type_enc = type_enc
    5.70 -  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
    5.71 +  | adjust_type_enc (THF _) type_enc = type_enc
    5.72 +  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
    5.73      Simple_Types (First_Order, Mangled_Monomorphic, level)
    5.74 -  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
    5.75 +  | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
    5.76      Simple_Types (First_Order, poly, level)
    5.77    | adjust_type_enc format (Simple_Types (_, poly, level)) =
    5.78      adjust_type_enc format (Guards (poly, level, Uniform))
    5.79 @@ -746,8 +749,9 @@
    5.80  fun type_class_formula type_enc class arg =
    5.81    AAtom (ATerm (class, arg ::
    5.82        (case type_enc of
    5.83 -         Simple_Types (_, Polymorphic, _) =>
    5.84 -         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
    5.85 +         Simple_Types (First_Order, Polymorphic, _) =>
    5.86 +         if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
    5.87 +         else []
    5.88         | _ => [])))
    5.89  fun formulas_for_types type_enc add_sorts_on_typ Ts =
    5.90    [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
    5.91 @@ -1779,18 +1783,19 @@
    5.92  
    5.93  (** Symbol declarations **)
    5.94  
    5.95 -fun decl_line_for_class s =
    5.96 +fun decl_line_for_class order s =
    5.97    let val name as (s, _) = `make_type_class s in
    5.98      Decl (sym_decl_prefix ^ s, name,
    5.99 -          if exploit_tff1_dummy_type_vars then
   5.100 -            AFun (atype_of_types, bool_atype)
   5.101 +          if order = First_Order andalso avoid_first_order_dummy_type_vars then
   5.102 +            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
   5.103            else
   5.104 -            ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)))
   5.105 +            AFun (atype_of_types, bool_atype))
   5.106    end
   5.107  
   5.108  fun decl_lines_for_classes type_enc classes =
   5.109    case type_enc of
   5.110 -    Simple_Types (_, Polymorphic, _) => map decl_line_for_class classes
   5.111 +    Simple_Types (order, Polymorphic, _) =>
   5.112 +    map (decl_line_for_class order) classes
   5.113    | _ => []
   5.114  
   5.115  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   5.116 @@ -2232,7 +2237,8 @@
   5.117              CNF => ensure_cnf_problem
   5.118            | CNF_UEQ => filter_cnf_ueq_problem
   5.119            | FOF => I
   5.120 -          | TFF (_, TFF_Implicit) => I
   5.121 +          | TFF (_, TPTP_Implicit) => I
   5.122 +          | THF (_, TPTP_Implicit, _) => I
   5.123            | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
   5.124                                                          implicit_declsN)
   5.125      val (problem, pool) = problem |> nice_atp_problem readable_names
     6.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 10:30:00 2011 -0700
     6.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Tue Sep 06 10:30:33 2011 -0700
     6.3 @@ -4,7 +4,7 @@
     6.4  import Control.Exception;
     6.5  import System.IO;
     6.6  import System.Exit;
     6.7 -import Code;
     6.8 +import Generated_Code;
     6.9  
    6.10  type Pos = [Int];
    6.11  
     7.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 10:30:00 2011 -0700
     7.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Tue Sep 06 10:30:33 2011 -0700
     7.3 @@ -8,7 +8,7 @@
     7.4  import System.Exit
     7.5  import Maybe
     7.6  import List (partition, findIndex)
     7.7 -import Code
     7.8 +import Generated_Code
     7.9  
    7.10  
    7.11  type Pos = [Int]
     8.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 10:30:00 2011 -0700
     8.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 10:30:33 2011 -0700
     8.3 @@ -235,17 +235,17 @@
     8.4        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     8.5      fun run in_path = 
     8.6        let
     8.7 -        val code_file = Path.append in_path (Path.basic "Code.hs")
     8.8 +        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
     8.9          val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    8.10          val main_file = Path.append in_path (Path.basic "Main.hs")
    8.11          val main = "module Main where {\n\n" ^
    8.12            "import System;\n" ^
    8.13            "import Narrowing_Engine;\n" ^
    8.14 -          "import Code;\n\n" ^
    8.15 -          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
    8.16 +          "import Generated_Code;\n\n" ^
    8.17 +          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
    8.18            "}\n"
    8.19 -        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    8.20 -          (unprefix "module Code where {" code)
    8.21 +        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    8.22 +          (unprefix "module Generated_Code where {" code)
    8.23          val _ = File.write code_file code'
    8.24          val _ = File.write narrowing_engine_file
    8.25            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
     9.1 --- a/src/Tools/Code/code_target.ML	Tue Sep 06 10:30:00 2011 -0700
     9.2 +++ b/src/Tools/Code/code_target.ML	Tue Sep 06 10:30:33 2011 -0700
     9.3 @@ -394,7 +394,7 @@
     9.4  
     9.5  fun check_code_for thy target strict args naming program names_cs =
     9.6    let
     9.7 -    val module_name = "Code";
     9.8 +    val module_name = "Generated_Code";
     9.9      val { env_var, make_destination, make_command } =
    9.10        (#check o the_fundamental thy) target;
    9.11      fun ext_check p =
    9.12 @@ -435,7 +435,7 @@
    9.13  fun evaluator thy target naming program consts =
    9.14    let
    9.15      val (mounted_serializer, prepared_program) = mount_serializer thy
    9.16 -      target NONE "Code" [] naming program consts;
    9.17 +      target NONE "Generated_Code" [] naming program consts;
    9.18    in evaluation mounted_serializer prepared_program consts end;
    9.19  
    9.20  end; (* local *)