# HG changeset patch
# User blanchet
# Date 1332752464 -7200
# Node ID a4476e55a2414c6ed4971bdf95ae2a0aa4aa1fe5
# Parent  db502663179986e8be3a29d8dbbc983747a130e2
reintroduced broken proofs and regenerated certificates

diff -r db5026631799 -r a4476e55a241 src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Mar 26 11:01:04 2012 +0200
@@ -12775,3 +12775,110 @@
 #247 := [asserted]: #123
 [unit-resolution #247 #633]: false
 unsat
+477e29453df08396d997096a4fc4a8771c735880 106 0
+#2 := false
+decl f7 :: S3
+#19 := f7
+decl f5 :: (-> S4 S3 S3)
+decl f6 :: S4
+#14 := f6
+#20 := (f5 f6 f7)
+#21 := (= #20 f7)
+#74 := (not #21)
+decl f1 :: S1
+#3 := f1
+decl f3 :: (-> S2 S1 S1)
+decl f4 :: S2
+#7 := f4
+#22 := (f3 f4 f1)
+#23 := (= #22 f1)
+#75 := (not #23)
+#558 := [hypothesis]: #75
+#8 := (:var 0 S1)
+#9 := (f3 f4 #8)
+#562 := (pattern #9)
+#11 := (= #8 f1)
+#10 := (= #9 f1)
+#12 := (iff #10 #11)
+#563 := (forall (vars (?v0 S1)) (:pat #562) #12)
+#13 := (forall (vars (?v0 S1)) #12)
+#566 := (iff #13 #563)
+#564 := (iff #12 #12)
+#565 := [refl]: #564
+#567 := [quant-intro #565]: #566
+#70 := (~ #13 #13)
+#68 := (~ #12 #12)
+#69 := [refl]: #68
+#71 := [nnf-pos #69]: #70
+#47 := [asserted]: #13
+#59 := [mp~ #47 #71]: #13
+#568 := [mp #59 #567]: #563
+#239 := (not #563)
+#218 := (or #239 #23)
+#146 := (= f1 f1)
+#147 := (iff #23 #146)
+#554 := (or #239 #147)
+#212 := (iff #554 #218)
+#550 := (iff #218 #218)
+#223 := [rewrite]: #550
+#238 := (iff #147 #23)
+#1 := true
+#24 := (iff #23 true)
+#50 := (iff #24 #23)
+#51 := [rewrite]: #50
+#236 := (iff #147 #24)
+#232 := (iff #146 true)
+#225 := [rewrite]: #232
+#237 := [monotonicity #225]: #236
+#235 := [trans #237 #51]: #238
+#343 := [monotonicity #235]: #212
+#224 := [trans #343 #223]: #212
+#556 := [quant-inst #3]: #554
+#557 := [mp #556 #224]: #218
+#559 := [unit-resolution #557 #568 #558]: false
+#560 := [lemma #559]: #23
+#64 := (or #74 #75)
+#52 := (and #21 #23)
+#55 := (not #52)
+#81 := (iff #55 #64)
+#65 := (not #64)
+#76 := (not #65)
+#79 := (iff #76 #64)
+#80 := [rewrite]: #79
+#77 := (iff #55 #76)
+#66 := (iff #52 #65)
+#67 := [rewrite]: #66
+#78 := [monotonicity #67]: #77
+#82 := [trans #78 #80]: #81
+#25 := (and #21 #24)
+#26 := (not #25)
+#56 := (iff #26 #55)
+#53 := (iff #25 #52)
+#54 := [monotonicity #51]: #53
+#57 := [monotonicity #54]: #56
+#49 := [asserted]: #26
+#60 := [mp #49 #57]: #55
+#83 := [mp #60 #82]: #64
+#555 := [unit-resolution #83 #560]: #74
+#15 := (:var 0 S3)
+#16 := (f5 f6 #15)
+#569 := (pattern #16)
+#17 := (= #16 #15)
+#570 := (forall (vars (?v0 S3)) (:pat #569) #17)
+#18 := (forall (vars (?v0 S3)) #17)
+#573 := (iff #18 #570)
+#571 := (iff #17 #17)
+#572 := [refl]: #571
+#574 := [quant-intro #572]: #573
+#62 := (~ #18 #18)
+#61 := (~ #17 #17)
+#72 := [refl]: #61
+#63 := [nnf-pos #72]: #62
+#48 := [asserted]: #18
+#73 := [mp~ #48 #63]: #18
+#575 := [mp #73 #574]: #570
+#551 := (not #570)
+#210 := (or #551 #21)
+#215 := [quant-inst #19]: #210
+[unit-resolution #215 #575 #555]: false
+unsat
diff -r db5026631799 -r a4476e55a241 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Mar 26 11:01:04 2012 +0200
@@ -467,7 +467,7 @@
 lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
   by smt
 
-lemma "id x = x \<and> id True = True" (* BROKEN by (smt id_def) *) oops
+lemma "id x = x \<and> id True = True" by (smt id_def)
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
   using fun_upd_same fun_upd_apply
diff -r db5026631799 -r a4476e55a241 src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Mon Mar 26 11:01:04 2012 +0200
@@ -67155,3 +67155,80 @@
 #139 := [asserted]: #53
 [mp #139 #149]: false
 unsat
+f09576464eb9a729afbe3fe966b57e4354456502 30 0
+#2 := false
+decl f4 :: (-> S3 S4)
+decl f6 :: S3
+#16 := f6
+#17 := (f4 f6)
+decl f3 :: (-> S2 S4)
+decl f5 :: S2
+#14 := f5
+#15 := (f3 f5)
+#18 := (= #15 #17)
+#19 := (not #18)
+#41 := [asserted]: #19
+#9 := (:var 0 S3)
+#10 := (f4 #9)
+#7 := (:var 1 S2)
+#8 := (f3 #7)
+#11 := (pattern #8 #10)
+#12 := (= #8 #10)
+#13 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #11) #12)
+#51 := (~ #13 #13)
+#49 := (~ #12 #12)
+#50 := [refl]: #49
+#52 := [nnf-pos #50]: #51
+#40 := [asserted]: #13
+#43 := [mp~ #40 #52]: #13
+#111 := (not #13)
+#197 := (or #111 #18)
+#112 := [quant-inst #14 #16]: #197
+[unit-resolution #112 #43 #41]: false
+unsat
+5a4509215da405eb20d4081e74524f90aaca407d 1 0
+unsat
+ec561a73aaf24cad28c298d64ff90ab9419e03b9 1 0
+unsat
+99895ba337908a50454cc51cd8d58f8c9973a5d8 1 0
+unsat
+f66af12ea27f7d59df586df568e3d48733d0c2ad 1 0
+unsat
+98a1d35ce489ce400102751e60b482d34ba4c100 1 0
+unsat
+997d0c877f7a6af3978a25e9a11fe86be44aa3d7 1 0
+unsat
+dec47d92e2bc6704596ff538272e4aa7dad033f8 1 0
+unsat
+79ff64606be9eaf1430551196cf6a56b904cd2f0 1 0
+unsat
+9ddb2d0aa5571f810dbdcf99f2a9c0dd91892822 1 0
+unsat
+383af2a9be136c8b9da304961ed7781d6d8b67da 1 0
+unsat
+8a45fca8152b4b73650f0bdadc7b4837d03b0e4f 1 0
+unsat
+028cbfc14838b1039241d56404b98b994249bd70 1 0
+unsat
+0c3c93869b86cd3cceaa64f6505c6b53e5a0d5f5 1 0
+unsat
+da5a18ce51a6fcaf95a5da1f3cf6ec44d50d2911 1 0
+unsat
+b326e9b62ea312d34250c299905421b42e169a3d 1 0
+unsat
+2df9f9573f4c3d690e8e9d39a01fbee0d0dabfca 1 0
+unsat
+64fe45c879d2ce11b605b7ccbadec44b7474cdb3 1 0
+unsat
+27388d866d376a195719342119d2c39bddbbda5e 1 0
+unsat
+4fdb33415d645476800f24bc2645077ed20fbcc7 1 0
+unsat
+34954aeef00ac521d8d6983ea46bbdde741af613 1 0
+unsat
+c975ecb6377964929f32ae1b30fbd693a2969c6a 1 0
+unsat
+5c9a9ffe9941b81f90170c912034e8b681bc281f 1 0
+unsat
+26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0
+unsat
diff -r db5026631799 -r a4476e55a241 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 11:01:04 2012 +0200
@@ -212,7 +212,7 @@
 lemma
   assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
   shows "f a = g b"
-  using assms (* BROKEN by smt *) oops
+  using assms by smt
 
 lemma
   assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
@@ -853,7 +853,7 @@
   using point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "cy (p \<lparr> cx := a \<rparr>) = cy p"
@@ -862,7 +862,7 @@
   using point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
@@ -891,7 +891,7 @@
   using point.simps bw_point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+
 
 lemma
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
@@ -905,7 +905,7 @@
   using point.simps bw_point.simps
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt *) oops
+  by smt
 
 
 subsubsection {* Type definitions *}
@@ -919,7 +919,7 @@
   using n1_def n2_def n3_def nplus_def
   using [[smt_datatypes, smt_oracle]]
   using [[z3_options="AUTO_CONFIG=false"]]
-  (* BROKEN by smt+ *) oops
+  by smt+