# HG changeset patch
# User boehmes
# Date 1278980945 -7200
# Node ID 4eb98849c5c059ee800596481cb73b181f3f8ce9
# Parent  173667d73115b186c75d9f0f07bbe4036e3e7b3b
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
added tests for Ball/Bex

diff -r 173667d73115 -r 4eb98849c5c0 src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Mon Jul 12 22:35:41 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Tue Jul 13 02:29:05 2010 +0200
@@ -53952,3 +53952,211 @@
 #60 := [asserted]: #10
 [mp #60 #69]: false
 unsat
+c08976b5943421000363d731a8009a5d8459d100 93 0
+#2 := false
+decl f5 :: (-> S2 S1)
+decl f6 :: S2
+#16 := f6
+#20 := (f5 f6)
+decl f1 :: S1
+#4 := f1
+#65 := (= f1 #20)
+#84 := (not #65)
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+#17 := (f3 f6 f4)
+#59 := (= f1 #17)
+#8 := (:var 0 S2)
+#12 := (f5 #8)
+#44 := (= f1 #12)
+#10 := (f3 #8 f4)
+#41 := (= f1 #10)
+#50 := (not #41)
+#51 := (or #50 #44)
+#56 := (forall (vars (?v0 S2)) #51)
+#62 := (and #56 #59)
+#71 := (not #62)
+#72 := (or #71 #65)
+#77 := (not #72)
+#21 := (= #20 f1)
+#18 := (= #17 f1)
+#13 := (= #12 f1)
+#11 := (= #10 f1)
+#14 := (implies #11 #13)
+#15 := (forall (vars (?v0 S2)) #14)
+#19 := (and #15 #18)
+#22 := (implies #19 #21)
+#23 := (not #22)
+#78 := (iff #23 #77)
+#75 := (iff #22 #72)
+#68 := (implies #62 #65)
+#73 := (iff #68 #72)
+#74 := [rewrite]: #73
+#69 := (iff #22 #68)
+#66 := (iff #21 #65)
+#67 := [rewrite]: #66
+#63 := (iff #19 #62)
+#60 := (iff #18 #59)
+#61 := [rewrite]: #60
+#57 := (iff #15 #56)
+#54 := (iff #14 #51)
+#47 := (implies #41 #44)
+#52 := (iff #47 #51)
+#53 := [rewrite]: #52
+#48 := (iff #14 #47)
+#45 := (iff #13 #44)
+#46 := [rewrite]: #45
+#42 := (iff #11 #41)
+#43 := [rewrite]: #42
+#49 := [monotonicity #43 #46]: #48
+#55 := [trans #49 #53]: #54
+#58 := [quant-intro #55]: #57
+#64 := [monotonicity #58 #61]: #63
+#70 := [monotonicity #64 #67]: #69
+#76 := [trans #70 #74]: #75
+#79 := [monotonicity #76]: #78
+#40 := [asserted]: #23
+#82 := [mp #40 #79]: #77
+#85 := [not-or-elim #82]: #84
+#80 := [not-or-elim #82]: #62
+#83 := [and-elim #80]: #59
+#572 := (pattern #12)
+#571 := (pattern #10)
+#573 := (forall (vars (?v0 S2)) (:pat #571 #572) #51)
+#576 := (iff #56 #573)
+#574 := (iff #51 #51)
+#575 := [refl]: #574
+#577 := [quant-intro #575]: #576
+#97 := (~ #56 #56)
+#95 := (~ #51 #51)
+#96 := [refl]: #95
+#98 := [nnf-pos #96]: #97
+#81 := [and-elim #80]: #56
+#87 := [mp~ #81 #98]: #56
+#578 := [mp #87 #577]: #573
+#155 := (not #59)
+#157 := (not #573)
+#244 := (or #157 #155 #65)
+#242 := (or #155 #65)
+#235 := (or #157 #242)
+#247 := (iff #235 #244)
+#175 := [rewrite]: #247
+#246 := [quant-inst]: #235
+#248 := [mp #246 #175]: #244
+[unit-resolution #248 #578 #83 #85]: false
+unsat
+9970f178c30353ca679caf02fa917fbf2a5e19ef 113 0
+#2 := false
+decl f3 :: (-> S2 S3 S1)
+decl f4 :: S3
+#9 := f4
+decl f6 :: S2
+#16 := f6
+#19 := (f3 f6 f4)
+decl f1 :: S1
+#4 := f1
+#57 := (= f1 #19)
+decl f5 :: (-> S2 S1)
+#17 := (f5 f6)
+#54 := (= f1 #17)
+#60 := (and #54 #57)
+#63 := (not #60)
+#8 := (:var 0 S2)
+#12 := (f5 #8)
+#45 := (= f1 #12)
+#10 := (f3 #8 f4)
+#42 := (= f1 #10)
+#48 := (and #42 #45)
+#51 := (exists (vars (?v0 S2)) #48)
+#66 := (or #51 #63)
+#69 := (not #66)
+#20 := (= #19 f1)
+#18 := (= #17 f1)
+#21 := (and #18 #20)
+#22 := (not #21)
+#13 := (= #12 f1)
+#11 := (= #10 f1)
+#14 := (and #11 #13)
+#15 := (exists (vars (?v0 S2)) #14)
+#23 := (or #15 #22)
+#24 := (not #23)
+#70 := (iff #24 #69)
+#67 := (iff #23 #66)
+#64 := (iff #22 #63)
+#61 := (iff #21 #60)
+#58 := (iff #20 #57)
+#59 := [rewrite]: #58
+#55 := (iff #18 #54)
+#56 := [rewrite]: #55
+#62 := [monotonicity #56 #59]: #61
+#65 := [monotonicity #62]: #64
+#52 := (iff #15 #51)
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#47 := [rewrite]: #46
+#43 := (iff #11 #42)
+#44 := [rewrite]: #43
+#50 := [monotonicity #44 #47]: #49
+#53 := [quant-intro #50]: #52
+#68 := [monotonicity #53 #65]: #67
+#71 := [monotonicity #68]: #70
+#41 := [asserted]: #24
+#74 := [mp #41 #71]: #69
+#75 := [not-or-elim #74]: #60
+#77 := [and-elim #75]: #57
+#76 := [and-elim #75]: #54
+#585 := (pattern #12)
+#584 := (pattern #10)
+#93 := (not #45)
+#92 := (not #42)
+#94 := (or #92 #93)
+#586 := (forall (vars (?v0 S2)) (:pat #584 #585) #94)
+#101 := (forall (vars (?v0 S2)) #94)
+#589 := (iff #101 #586)
+#587 := (iff #94 #94)
+#588 := [refl]: #587
+#590 := [quant-intro #588]: #589
+#87 := (not #48)
+#90 := (forall (vars (?v0 S2)) #87)
+#102 := (iff #90 #101)
+#99 := (iff #87 #94)
+#95 := (not #94)
+#83 := (not #95)
+#97 := (iff #83 #94)
+#98 := [rewrite]: #97
+#84 := (iff #87 #83)
+#85 := (iff #48 #95)
+#86 := [rewrite]: #85
+#96 := [monotonicity #86]: #84
+#100 := [trans #96 #98]: #99
+#103 := [quant-intro #100]: #102
+#72 := (not #51)
+#79 := (~ #72 #90)
+#88 := (~ #87 #87)
+#89 := [refl]: #88
+#80 := [nnf-neg #89]: #79
+#73 := [not-or-elim #74]: #72
+#91 := [mp~ #73 #80]: #90
+#104 := [mp #91 #103]: #101
+#591 := [mp #104 #590]: #586
+#255 := (not #57)
+#168 := (not #54)
+#248 := (not #586)
+#259 := (or #248 #168 #255)
+#169 := (or #255 #168)
+#260 := (or #248 #169)
+#578 := (iff #260 #259)
+#256 := (or #168 #255)
+#261 := (or #248 #256)
+#241 := (iff #261 #259)
+#576 := [rewrite]: #241
+#258 := (iff #260 #261)
+#170 := (iff #169 #256)
+#257 := [rewrite]: #170
+#262 := [monotonicity #257]: #258
+#235 := [trans #262 #576]: #578
+#188 := [quant-inst]: #260
+#365 := [mp #188 #235]: #259
+[unit-resolution #365 #591 #76 #77]: false
+unsat
diff -r 173667d73115 -r 4eb98849c5c0 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Jul 12 22:35:41 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jul 13 02:29:05 2010 +0200
@@ -84,6 +84,7 @@
 
 lemma
   "case P of True \<Rightarrow> P | False \<Rightarrow> \<not>P"
+  "case P of False \<Rightarrow> \<not>P | True \<Rightarrow> P"
   "case \<not>P of True \<Rightarrow> \<not>P | False \<Rightarrow> P"
   "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
   by smt+
@@ -176,6 +177,11 @@
   by smt+
 
 lemma
+  "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
+  "(\<exists>x\<in>M. P x) \<or> \<not>(P c \<and> c \<in> M)"
+  by smt+
+
+lemma
   "let P = True in P"
   "let P = P1 \<or> P2 in P \<or> \<not>P"
   "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"
diff -r 173667d73115 -r 4eb98849c5c0 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Jul 12 22:35:41 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Jul 13 02:29:05 2010 +0200
@@ -41,10 +41,10 @@
         length (HOLogic.dest_list t) <= 2
     | is_trivial_distinct _ = false
 
-  val thms = @{lemma
-    "distinct [] == True"
-    "distinct [x] == True"
-    "distinct [x, y] == (x ~= y)"
+  val thms = map mk_meta_eq @{lemma
+    "distinct [] = True"
+    "distinct [x] = True"
+    "distinct [x, y] = (x ~= y)"
     by simp_all}
   fun distinct_conv _ =
     if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
@@ -63,10 +63,10 @@
       Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
     | _ => false)
 
-  val thms = @{lemma
-    "(case P of True => x | False => y) == (if P then x else y)"
-    "(case P of False => y | True => x) == (if P then x else y)"
-    by (rule eq_reflection, simp)+}
+  val thms = map mk_meta_eq @{lemma
+    "(case P of True => x | False => y) = (if P then x else y)"
+    "(case P of False => y | True => x) = (if P then x else y)"
+    by simp_all}
   val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
 in
 fun rewrite_bool_cases ctxt =
@@ -201,8 +201,8 @@
     (Conv.arg_conv (norm_conv ctxt)) (eta_conv norm_conv ctxt)
   and unfold_conv thm ctxt = Conv.rewr_conv thm then_conv keep_conv ctxt
   and unfold_ex1_conv ctxt = unfold_conv @{thm Ex1_def} ctxt
-  and unfold_ball_conv ctxt = unfold_conv @{thm Ball_def} ctxt
-  and unfold_bex_conv ctxt = unfold_conv @{thm Bex_def} ctxt
+  and unfold_ball_conv ctxt = unfold_conv (mk_meta_eq @{thm Ball_def}) ctxt
+  and unfold_bex_conv ctxt = unfold_conv (mk_meta_eq @{thm Bex_def}) ctxt
   and norm_conv ctxt ct =
     (case Thm.term_of ct of
       Const (@{const_name All}, _) $ Abs _ => keep_conv
diff -r 173667d73115 -r 4eb98849c5c0 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Jul 12 22:35:41 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Jul 13 02:29:05 2010 +0200
@@ -60,9 +60,9 @@
   | Const (@{const_name max}, _) => true
   | _ => false)
 
-val unfold_abs_conv = Conv.rewr_conv @{thm abs_if[THEN eq_reflection]}
-val unfold_min_conv = Conv.rewr_conv @{thm min_def[THEN eq_reflection]}
-val unfold_max_conv = Conv.rewr_conv @{thm max_def[THEN eq_reflection]}
+val unfold_abs_conv = Conv.rewr_conv (mk_meta_eq @{thm abs_if})
+val unfold_min_conv = Conv.rewr_conv (mk_meta_eq @{thm min_def})
+val unfold_max_conv = Conv.rewr_conv (mk_meta_eq @{thm max_def})
 
 fun expand_conv cv = N.eta_expand_conv (K cv)
 fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))