# HG changeset patch
# User boehmes
# Date 1315325264 -7200
# Node ID 3c73f40689782e81fe9b694dccc0c02d23a09e7d
# Parent  eaf394237ba700ffdd480bbc5431f7ddeff0fbd4
added some examples for pattern and weight annotations

diff -r eaf394237ba7 -r 3c73f4068978 src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 17:52:00 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Sep 06 18:07:44 2011 +0200
@@ -60074,3 +60074,483 @@
 #110 := [asserted]: #38
 [mp #110 #120]: false
 unsat
+8021f8e09eb3e47791aed2bed0dafccd5948187d 69 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#16 := f5
+#19 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #19)
+#70 := (not #66)
+#20 := (= #19 f1)
+#21 := (not #20)
+#71 := (iff #21 #70)
+#68 := (iff #20 #66)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#65 := [asserted]: #21
+#75 := [mp #65 #72]: #70
+decl f3 :: (-> S2 S1)
+#17 := (f3 f5)
+#61 := (= f1 #17)
+#18 := (= #17 f1)
+#63 := (iff #18 #61)
+#64 := [rewrite]: #63
+#60 := [asserted]: #18
+#67 := [mp #60 #64]: #61
+#8 := (:var 0 S2)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#12 := (f4 #8)
+#45 := (= f1 #12)
+#42 := (= f1 #9)
+#51 := (not #42)
+#52 := (or #51 #45)
+#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
+#85 := (~ #57 #57)
+#83 := (~ #52 #52)
+#84 := [refl]: #83
+#86 := [nnf-pos #84]: #85
+#13 := (= #12 f1)
+#11 := (= #9 f1)
+#14 := (implies #11 #13)
+#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
+#58 := (iff #15 #57)
+#55 := (iff #14 #52)
+#48 := (implies #42 #45)
+#53 := (iff #48 #52)
+#54 := [rewrite]: #53
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#47 := [rewrite]: #46
+#43 := (iff #11 #42)
+#44 := [rewrite]: #43
+#50 := [monotonicity #44 #47]: #49
+#56 := [trans #50 #54]: #55
+#59 := [quant-intro #56]: #58
+#41 := [asserted]: #15
+#62 := [mp #41 #59]: #57
+#74 := [mp~ #62 #86]: #57
+#137 := (not #61)
+#139 := (not #57)
+#226 := (or #139 #137 #66)
+#224 := (or #137 #66)
+#217 := (or #139 #224)
+#229 := (iff #217 #226)
+#157 := [rewrite]: #229
+#228 := [quant-inst #16]: #217
+#230 := [mp #228 #157]: #226
+[unit-resolution #230 #74 #67 #75]: false
+unsat
+51102b6663906c70b84f1c6e3a1a2e429b49188d 112 0
+#2 := false
+decl f5 :: (-> S2 S1)
+decl f6 :: S2
+#19 := f6
+#24 := (f5 f6)
+decl f1 :: S1
+#4 := f1
+#82 := (= f1 #24)
+#86 := (not #82)
+#25 := (= #24 f1)
+#26 := (not #25)
+#87 := (iff #26 #86)
+#84 := (iff #25 #82)
+#85 := [rewrite]: #84
+#88 := [monotonicity #85]: #87
+#81 := [asserted]: #26
+#91 := [mp #81 #88]: #86
+decl f4 :: (-> S2 S1)
+#22 := (f4 f6)
+#77 := (= f1 #22)
+#23 := (= #22 f1)
+#79 := (iff #23 #77)
+#80 := [rewrite]: #79
+#76 := [asserted]: #23
+#83 := [mp #76 #80]: #77
+decl f3 :: (-> S2 S1)
+#20 := (f3 f6)
+#72 := (= f1 #20)
+#21 := (= #20 f1)
+#74 := (iff #21 #72)
+#75 := [rewrite]: #74
+#71 := [asserted]: #21
+#78 := [mp #71 #75]: #72
+#8 := (:var 0 S2)
+#10 := (f4 #8)
+#9 := (f3 #8)
+#11 := (pattern #9 #10)
+#15 := (f5 #8)
+#56 := (= f1 #15)
+#50 := (= f1 #10)
+#105 := (not #50)
+#47 := (= f1 #9)
+#92 := (not #47)
+#112 := (or #92 #105 #56)
+#117 := (forall (vars (?v0 S2)) (:pat #11) #112)
+#53 := (and #47 #50)
+#62 := (not #53)
+#63 := (or #62 #56)
+#68 := (forall (vars (?v0 S2)) (:pat #11) #63)
+#118 := (iff #68 #117)
+#115 := (iff #63 #112)
+#93 := (or #92 #105)
+#109 := (or #93 #56)
+#113 := (iff #109 #112)
+#114 := [rewrite]: #113
+#110 := (iff #63 #109)
+#107 := (iff #62 #93)
+#94 := (not #93)
+#97 := (not #94)
+#96 := (iff #97 #93)
+#106 := [rewrite]: #96
+#98 := (iff #62 #97)
+#99 := (iff #53 #94)
+#100 := [rewrite]: #99
+#95 := [monotonicity #100]: #98
+#108 := [trans #95 #106]: #107
+#111 := [monotonicity #108]: #110
+#116 := [trans #111 #114]: #115
+#119 := [quant-intro #116]: #118
+#103 := (~ #68 #68)
+#101 := (~ #63 #63)
+#102 := [refl]: #101
+#104 := [nnf-pos #102]: #103
+#16 := (= #15 f1)
+#13 := (= #10 f1)
+#12 := (= #9 f1)
+#14 := (and #12 #13)
+#17 := (implies #14 #16)
+#18 := (forall (vars (?v0 S2)) (:pat #11) #17)
+#69 := (iff #18 #68)
+#66 := (iff #17 #63)
+#59 := (implies #53 #56)
+#64 := (iff #59 #63)
+#65 := [rewrite]: #64
+#60 := (iff #17 #59)
+#57 := (iff #16 #56)
+#58 := [rewrite]: #57
+#54 := (iff #14 #53)
+#51 := (iff #13 #50)
+#52 := [rewrite]: #51
+#48 := (iff #12 #47)
+#49 := [rewrite]: #48
+#55 := [monotonicity #49 #52]: #54
+#61 := [monotonicity #55 #58]: #60
+#67 := [trans #61 #65]: #66
+#70 := [quant-intro #67]: #69
+#46 := [asserted]: #18
+#73 := [mp #46 #70]: #68
+#90 := [mp~ #73 #104]: #68
+#120 := [mp #90 #119]: #117
+#178 := (not #77)
+#265 := (not #72)
+#267 := (not #117)
+#258 := (or #267 #265 #178 #82)
+#179 := (or #265 #178 #82)
+#269 := (or #267 #179)
+#198 := (iff #269 #258)
+#271 := [rewrite]: #198
+#270 := [quant-inst #19]: #269
+#268 := [mp #270 #271]: #258
+[unit-resolution #268 #120 #78 #83 #91]: false
+unsat
+1191e209015c2f2f439f124434700d861e089600 149 0
+#2 := false
+decl f3 :: (-> S2 S1)
+decl f6 :: S2
+#21 := f6
+#22 := (f3 f6)
+decl f1 :: S1
+#4 := f1
+#84 := (= f1 #22)
+#264 := (not #84)
+decl f5 :: (-> S2 S1)
+#27 := (f5 f6)
+#95 := (= f1 #27)
+#178 := (or #264 #95)
+decl f4 :: (-> S2 S1)
+#24 := (f4 f6)
+#88 := (= f1 #24)
+#176 := (not #88)
+#268 := (or #176 #95)
+#266 := (not #268)
+#265 := (not #178)
+#586 := (or #265 #266)
+#375 := (not #586)
+#579 := [hypothesis]: #586
+#8 := (:var 0 S2)
+#11 := (f4 #8)
+#12 := (pattern #11)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#65 := (= f1 #11)
+#71 := (not #65)
+#14 := (f5 #8)
+#53 := (= f1 #14)
+#72 := (or #53 #71)
+#116 := (not #72)
+#50 := (= f1 #9)
+#59 := (not #50)
+#60 := (or #59 #53)
+#105 := (not #60)
+#106 := (or #105 #116)
+#107 := (not #106)
+#108 := (forall (vars (?v0 S2)) (:pat #10 #12) #107)
+#77 := (and #60 #72)
+#80 := (forall (vars (?v0 S2)) (:pat #10 #12) #77)
+#109 := (iff #80 #108)
+#110 := (iff #77 #107)
+#111 := [rewrite]: #110
+#117 := [quant-intro #111]: #109
+#114 := (~ #80 #80)
+#112 := (~ #77 #77)
+#113 := [refl]: #112
+#115 := [nnf-pos #113]: #114
+#15 := (= #14 f1)
+#17 := (= #11 f1)
+#18 := (implies #17 #15)
+#13 := (= #9 f1)
+#16 := (implies #13 #15)
+#19 := (and #16 #18)
+#20 := (forall (vars (?v0 S2)) (:pat #10 #12) #19)
+#81 := (iff #20 #80)
+#78 := (iff #19 #77)
+#75 := (iff #18 #72)
+#68 := (implies #65 #53)
+#73 := (iff #68 #72)
+#74 := [rewrite]: #73
+#69 := (iff #18 #68)
+#54 := (iff #15 #53)
+#55 := [rewrite]: #54
+#66 := (iff #17 #65)
+#67 := [rewrite]: #66
+#70 := [monotonicity #67 #55]: #69
+#76 := [trans #70 #74]: #75
+#63 := (iff #16 #60)
+#56 := (implies #50 #53)
+#61 := (iff #56 #60)
+#62 := [rewrite]: #61
+#57 := (iff #16 #56)
+#51 := (iff #13 #50)
+#52 := [rewrite]: #51
+#58 := [monotonicity #52 #55]: #57
+#64 := [trans #58 #62]: #63
+#79 := [monotonicity #64 #76]: #78
+#82 := [quant-intro #79]: #81
+#49 := [asserted]: #20
+#85 := [mp #49 #82]: #80
+#103 := [mp~ #85 #115]: #80
+#118 := [mp #103 #117]: #108
+#255 := (not #108)
+#589 := (or #255 #375)
+#263 := (or #95 #176)
+#177 := (not #263)
+#256 := (or #265 #177)
+#267 := (not #256)
+#590 := (or #255 #267)
+#592 := (iff #590 #589)
+#593 := (iff #589 #589)
+#583 := [rewrite]: #593
+#582 := (iff #267 #375)
+#588 := (iff #256 #586)
+#270 := (iff #177 #266)
+#196 := (iff #263 #268)
+#269 := [rewrite]: #196
+#249 := [monotonicity #269]: #270
+#243 := [monotonicity #249]: #588
+#254 := [monotonicity #243]: #582
+#587 := [monotonicity #254]: #592
+#241 := [trans #587 #583]: #592
+#591 := [quant-inst #21]: #590
+#246 := [mp #591 #241]: #589
+#217 := [unit-resolution #246 #118 #579]: false
+#218 := [lemma #217]: #375
+#574 := (or #586 #178)
+#575 := [def-axiom]: #574
+#580 := [unit-resolution #575 #218]: #178
+#578 := (or #265 #264)
+#99 := (not #95)
+#28 := (= #27 f1)
+#29 := (not #28)
+#100 := (iff #29 #99)
+#97 := (iff #28 #95)
+#98 := [rewrite]: #97
+#101 := [monotonicity #98]: #100
+#94 := [asserted]: #29
+#104 := [mp #94 #101]: #99
+#569 := (or #265 #264 #95)
+#230 := [def-axiom]: #569
+#581 := [unit-resolution #230 #104]: #578
+#567 := [unit-resolution #581 #580]: #264
+#570 := (or #586 #268)
+#576 := [def-axiom]: #570
+#568 := [unit-resolution #576 #218]: #268
+#274 := (or #266 #176)
+#572 := (or #266 #176 #95)
+#573 := [def-axiom]: #572
+#290 := [unit-resolution #573 #104]: #274
+#291 := [unit-resolution #290 #568]: #176
+#91 := (or #84 #88)
+#25 := (= #24 f1)
+#23 := (= #22 f1)
+#26 := (or #23 #25)
+#92 := (iff #26 #91)
+#89 := (iff #25 #88)
+#90 := [rewrite]: #89
+#86 := (iff #23 #84)
+#87 := [rewrite]: #86
+#93 := [monotonicity #87 #90]: #92
+#83 := [asserted]: #26
+#96 := [mp #83 #93]: #91
+[unit-resolution #96 #291 #567]: false
+unsat
+45f8ffe676ed981a383aaab6faaf520b9ff236c9 69 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#16 := f5
+#19 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#66 := (= f1 #19)
+#70 := (not #66)
+#20 := (= #19 f1)
+#21 := (not #20)
+#71 := (iff #21 #70)
+#68 := (iff #20 #66)
+#69 := [rewrite]: #68
+#72 := [monotonicity #69]: #71
+#65 := [asserted]: #21
+#75 := [mp #65 #72]: #70
+decl f3 :: (-> S2 S1)
+#17 := (f3 f5)
+#61 := (= f1 #17)
+#18 := (= #17 f1)
+#63 := (iff #18 #61)
+#64 := [rewrite]: #63
+#60 := [asserted]: #18
+#67 := [mp #60 #64]: #61
+#8 := (:var 0 S2)
+#9 := (f3 #8)
+#10 := (pattern #9)
+#12 := (f4 #8)
+#45 := (= f1 #12)
+#42 := (= f1 #9)
+#51 := (not #42)
+#52 := (or #51 #45)
+#57 := (forall (vars (?v0 S2)) (:pat #10) #52)
+#85 := (~ #57 #57)
+#83 := (~ #52 #52)
+#84 := [refl]: #83
+#86 := [nnf-pos #84]: #85
+#13 := (= #12 f1)
+#11 := (= #9 f1)
+#14 := (implies #11 #13)
+#15 := (forall (vars (?v0 S2)) (:pat #10) #14)
+#58 := (iff #15 #57)
+#55 := (iff #14 #52)
+#48 := (implies #42 #45)
+#53 := (iff #48 #52)
+#54 := [rewrite]: #53
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#47 := [rewrite]: #46
+#43 := (iff #11 #42)
+#44 := [rewrite]: #43
+#50 := [monotonicity #44 #47]: #49
+#56 := [trans #50 #54]: #55
+#59 := [quant-intro #56]: #58
+#41 := [asserted]: #15
+#62 := [mp #41 #59]: #57
+#74 := [mp~ #62 #86]: #57
+#137 := (not #61)
+#139 := (not #57)
+#226 := (or #139 #137 #66)
+#224 := (or #137 #66)
+#217 := (or #139 #224)
+#229 := (iff #217 #226)
+#157 := [rewrite]: #229
+#228 := [quant-inst #16]: #217
+#230 := [mp #228 #157]: #226
+[unit-resolution #230 #74 #67 #75]: false
+unsat
+ceabafba9f0db45264556e8d9525b667725281c7 76 0
+#2 := false
+decl f4 :: (-> S2 S1)
+decl f5 :: S2
+#15 := f5
+#18 := (f4 f5)
+decl f1 :: S1
+#4 := f1
+#65 := (= f1 #18)
+#69 := (not #65)
+#19 := (= #18 f1)
+#20 := (not #19)
+#70 := (iff #20 #69)
+#67 := (iff #19 #65)
+#68 := [rewrite]: #67
+#71 := [monotonicity #68]: #70
+#64 := [asserted]: #20
+#74 := [mp #64 #71]: #69
+decl f3 :: (-> S2 S1)
+#16 := (f3 f5)
+#60 := (= f1 #16)
+#17 := (= #16 f1)
+#62 := (iff #17 #60)
+#63 := [rewrite]: #62
+#59 := [asserted]: #17
+#66 := [mp #59 #63]: #60
+#8 := (:var 0 S2)
+#11 := (f4 #8)
+#555 := (pattern #11)
+#9 := (f3 #8)
+#554 := (pattern #9)
+#44 := (= f1 #11)
+#41 := (= f1 #9)
+#50 := (not #41)
+#51 := (or #50 #44)
+#556 := (forall (vars (?v0 S2)) (:pat #554 #555) #51)
+#56 := (forall (vars (?v0 S2)) #51)
+#559 := (iff #56 #556)
+#557 := (iff #51 #51)
+#558 := [refl]: #557
+#560 := [quant-intro #558]: #559
+#84 := (~ #56 #56)
+#82 := (~ #51 #51)
+#83 := [refl]: #82
+#85 := [nnf-pos #83]: #84
+#12 := (= #11 f1)
+#10 := (= #9 f1)
+#13 := (implies #10 #12)
+#14 := (forall (vars (?v0 S2)) #13)
+#57 := (iff #14 #56)
+#54 := (iff #13 #51)
+#47 := (implies #41 #44)
+#52 := (iff #47 #51)
+#53 := [rewrite]: #52
+#48 := (iff #13 #47)
+#45 := (iff #12 #44)
+#46 := [rewrite]: #45
+#42 := (iff #10 #41)
+#43 := [rewrite]: #42
+#49 := [monotonicity #43 #46]: #48
+#55 := [trans #49 #53]: #54
+#58 := [quant-intro #55]: #57
+#40 := [asserted]: #14
+#61 := [mp #40 #58]: #56
+#73 := [mp~ #61 #85]: #56
+#561 := [mp #73 #560]: #556
+#136 := (not #60)
+#138 := (not #556)
+#225 := (or #138 #136 #65)
+#223 := (or #136 #65)
+#216 := (or #138 #223)
+#228 := (iff #216 #225)
+#156 := [rewrite]: #228
+#227 := [quant-inst #15]: #216
+#229 := [mp #227 #156]: #225
+[unit-resolution #229 #561 #66 #74]: false
+unsat
diff -r eaf394237ba7 -r 3c73f4068978 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 17:52:00 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Sep 06 18:07:44 2011 +0200
@@ -201,6 +201,9 @@
   "(\<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"
   by smt+
 
+
+section {* Guidance for quantifier heuristics: patterns and weights *}
+
 lemma
   assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
   shows "f 1 = 1"
@@ -211,6 +214,38 @@
   shows "f 1 = g 2"
   using assms by smt
 
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x), SMT.pat (Q x)]]
+    (P x & Q x --> R x)"
+  and "P t" and "Q t"
+  shows "R t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)], [SMT.pat (Q x)]]
+    ((P x --> R x) & (Q x --> R x))"
+  and "P t | Q t"
+  shows "R t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (SMT.weight 2 (P x --> Q x))"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
+lemma
+  assumes "ALL x. SMT.weight 1 (P x --> Q x)"
+  and "P t"
+  shows "Q t"
+  using assms by smt
+
 
 
 section {* Meta logical connectives *}