added some examples for pattern and weight annotations
authorboehmes
Tue Sep 06 18:07:44 2011 +0200 (2011-09-06)
changeset 447533c73f4068978
parent 44752 eaf394237ba7
child 44754 265174356212
added some examples for pattern and weight annotations
src/HOL/SMT_Examples/SMT_Tests.certs
src/HOL/SMT_Examples/SMT_Tests.thy
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 17:52:00 2011 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 18:07:44 2011 +0200
     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 17:52:00 2011 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 18:07:44 2011 +0200
     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 *}