reintroduced broken proofs and regenerated certificates
authorblanchet
Mon Mar 26 11:01:04 2012 +0200 (2012-03-26)
changeset 47111a4476e55a241
parent 47109 db5026631799
child 47112 8493d5d0e9b6
reintroduced broken proofs and regenerated certificates
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.certs
src/HOL/SMT_Examples/SMT_Tests.thy
     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Mar 26 10:42:06 2012 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Mar 26 11:01:04 2012 +0200
     1.3 @@ -12775,3 +12775,110 @@
     1.4  #247 := [asserted]: #123
     1.5  [unit-resolution #247 #633]: false
     1.6  unsat
     1.7 +477e29453df08396d997096a4fc4a8771c735880 106 0
     1.8 +#2 := false
     1.9 +decl f7 :: S3
    1.10 +#19 := f7
    1.11 +decl f5 :: (-> S4 S3 S3)
    1.12 +decl f6 :: S4
    1.13 +#14 := f6
    1.14 +#20 := (f5 f6 f7)
    1.15 +#21 := (= #20 f7)
    1.16 +#74 := (not #21)
    1.17 +decl f1 :: S1
    1.18 +#3 := f1
    1.19 +decl f3 :: (-> S2 S1 S1)
    1.20 +decl f4 :: S2
    1.21 +#7 := f4
    1.22 +#22 := (f3 f4 f1)
    1.23 +#23 := (= #22 f1)
    1.24 +#75 := (not #23)
    1.25 +#558 := [hypothesis]: #75
    1.26 +#8 := (:var 0 S1)
    1.27 +#9 := (f3 f4 #8)
    1.28 +#562 := (pattern #9)
    1.29 +#11 := (= #8 f1)
    1.30 +#10 := (= #9 f1)
    1.31 +#12 := (iff #10 #11)
    1.32 +#563 := (forall (vars (?v0 S1)) (:pat #562) #12)
    1.33 +#13 := (forall (vars (?v0 S1)) #12)
    1.34 +#566 := (iff #13 #563)
    1.35 +#564 := (iff #12 #12)
    1.36 +#565 := [refl]: #564
    1.37 +#567 := [quant-intro #565]: #566
    1.38 +#70 := (~ #13 #13)
    1.39 +#68 := (~ #12 #12)
    1.40 +#69 := [refl]: #68
    1.41 +#71 := [nnf-pos #69]: #70
    1.42 +#47 := [asserted]: #13
    1.43 +#59 := [mp~ #47 #71]: #13
    1.44 +#568 := [mp #59 #567]: #563
    1.45 +#239 := (not #563)
    1.46 +#218 := (or #239 #23)
    1.47 +#146 := (= f1 f1)
    1.48 +#147 := (iff #23 #146)
    1.49 +#554 := (or #239 #147)
    1.50 +#212 := (iff #554 #218)
    1.51 +#550 := (iff #218 #218)
    1.52 +#223 := [rewrite]: #550
    1.53 +#238 := (iff #147 #23)
    1.54 +#1 := true
    1.55 +#24 := (iff #23 true)
    1.56 +#50 := (iff #24 #23)
    1.57 +#51 := [rewrite]: #50
    1.58 +#236 := (iff #147 #24)
    1.59 +#232 := (iff #146 true)
    1.60 +#225 := [rewrite]: #232
    1.61 +#237 := [monotonicity #225]: #236
    1.62 +#235 := [trans #237 #51]: #238
    1.63 +#343 := [monotonicity #235]: #212
    1.64 +#224 := [trans #343 #223]: #212
    1.65 +#556 := [quant-inst #3]: #554
    1.66 +#557 := [mp #556 #224]: #218
    1.67 +#559 := [unit-resolution #557 #568 #558]: false
    1.68 +#560 := [lemma #559]: #23
    1.69 +#64 := (or #74 #75)
    1.70 +#52 := (and #21 #23)
    1.71 +#55 := (not #52)
    1.72 +#81 := (iff #55 #64)
    1.73 +#65 := (not #64)
    1.74 +#76 := (not #65)
    1.75 +#79 := (iff #76 #64)
    1.76 +#80 := [rewrite]: #79
    1.77 +#77 := (iff #55 #76)
    1.78 +#66 := (iff #52 #65)
    1.79 +#67 := [rewrite]: #66
    1.80 +#78 := [monotonicity #67]: #77
    1.81 +#82 := [trans #78 #80]: #81
    1.82 +#25 := (and #21 #24)
    1.83 +#26 := (not #25)
    1.84 +#56 := (iff #26 #55)
    1.85 +#53 := (iff #25 #52)
    1.86 +#54 := [monotonicity #51]: #53
    1.87 +#57 := [monotonicity #54]: #56
    1.88 +#49 := [asserted]: #26
    1.89 +#60 := [mp #49 #57]: #55
    1.90 +#83 := [mp #60 #82]: #64
    1.91 +#555 := [unit-resolution #83 #560]: #74
    1.92 +#15 := (:var 0 S3)
    1.93 +#16 := (f5 f6 #15)
    1.94 +#569 := (pattern #16)
    1.95 +#17 := (= #16 #15)
    1.96 +#570 := (forall (vars (?v0 S3)) (:pat #569) #17)
    1.97 +#18 := (forall (vars (?v0 S3)) #17)
    1.98 +#573 := (iff #18 #570)
    1.99 +#571 := (iff #17 #17)
   1.100 +#572 := [refl]: #571
   1.101 +#574 := [quant-intro #572]: #573
   1.102 +#62 := (~ #18 #18)
   1.103 +#61 := (~ #17 #17)
   1.104 +#72 := [refl]: #61
   1.105 +#63 := [nnf-pos #72]: #62
   1.106 +#48 := [asserted]: #18
   1.107 +#73 := [mp~ #48 #63]: #18
   1.108 +#575 := [mp #73 #574]: #570
   1.109 +#551 := (not #570)
   1.110 +#210 := (or #551 #21)
   1.111 +#215 := [quant-inst #19]: #210
   1.112 +[unit-resolution #215 #575 #555]: false
   1.113 +unsat
     2.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Mar 26 10:42:06 2012 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Mar 26 11:01:04 2012 +0200
     2.3 @@ -467,7 +467,7 @@
     2.4  lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
     2.5    by smt
     2.6  
     2.7 -lemma "id x = x \<and> id True = True" (* BROKEN by (smt id_def) *) oops
     2.8 +lemma "id x = x \<and> id True = True" by (smt id_def)
     2.9  
    2.10  lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
    2.11    using fun_upd_same fun_upd_apply
     3.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Mon Mar 26 10:42:06 2012 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Mon Mar 26 11:01:04 2012 +0200
     3.3 @@ -67155,3 +67155,80 @@
     3.4  #139 := [asserted]: #53
     3.5  [mp #139 #149]: false
     3.6  unsat
     3.7 +f09576464eb9a729afbe3fe966b57e4354456502 30 0
     3.8 +#2 := false
     3.9 +decl f4 :: (-> S3 S4)
    3.10 +decl f6 :: S3
    3.11 +#16 := f6
    3.12 +#17 := (f4 f6)
    3.13 +decl f3 :: (-> S2 S4)
    3.14 +decl f5 :: S2
    3.15 +#14 := f5
    3.16 +#15 := (f3 f5)
    3.17 +#18 := (= #15 #17)
    3.18 +#19 := (not #18)
    3.19 +#41 := [asserted]: #19
    3.20 +#9 := (:var 0 S3)
    3.21 +#10 := (f4 #9)
    3.22 +#7 := (:var 1 S2)
    3.23 +#8 := (f3 #7)
    3.24 +#11 := (pattern #8 #10)
    3.25 +#12 := (= #8 #10)
    3.26 +#13 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #11) #12)
    3.27 +#51 := (~ #13 #13)
    3.28 +#49 := (~ #12 #12)
    3.29 +#50 := [refl]: #49
    3.30 +#52 := [nnf-pos #50]: #51
    3.31 +#40 := [asserted]: #13
    3.32 +#43 := [mp~ #40 #52]: #13
    3.33 +#111 := (not #13)
    3.34 +#197 := (or #111 #18)
    3.35 +#112 := [quant-inst #14 #16]: #197
    3.36 +[unit-resolution #112 #43 #41]: false
    3.37 +unsat
    3.38 +5a4509215da405eb20d4081e74524f90aaca407d 1 0
    3.39 +unsat
    3.40 +ec561a73aaf24cad28c298d64ff90ab9419e03b9 1 0
    3.41 +unsat
    3.42 +99895ba337908a50454cc51cd8d58f8c9973a5d8 1 0
    3.43 +unsat
    3.44 +f66af12ea27f7d59df586df568e3d48733d0c2ad 1 0
    3.45 +unsat
    3.46 +98a1d35ce489ce400102751e60b482d34ba4c100 1 0
    3.47 +unsat
    3.48 +997d0c877f7a6af3978a25e9a11fe86be44aa3d7 1 0
    3.49 +unsat
    3.50 +dec47d92e2bc6704596ff538272e4aa7dad033f8 1 0
    3.51 +unsat
    3.52 +79ff64606be9eaf1430551196cf6a56b904cd2f0 1 0
    3.53 +unsat
    3.54 +9ddb2d0aa5571f810dbdcf99f2a9c0dd91892822 1 0
    3.55 +unsat
    3.56 +383af2a9be136c8b9da304961ed7781d6d8b67da 1 0
    3.57 +unsat
    3.58 +8a45fca8152b4b73650f0bdadc7b4837d03b0e4f 1 0
    3.59 +unsat
    3.60 +028cbfc14838b1039241d56404b98b994249bd70 1 0
    3.61 +unsat
    3.62 +0c3c93869b86cd3cceaa64f6505c6b53e5a0d5f5 1 0
    3.63 +unsat
    3.64 +da5a18ce51a6fcaf95a5da1f3cf6ec44d50d2911 1 0
    3.65 +unsat
    3.66 +b326e9b62ea312d34250c299905421b42e169a3d 1 0
    3.67 +unsat
    3.68 +2df9f9573f4c3d690e8e9d39a01fbee0d0dabfca 1 0
    3.69 +unsat
    3.70 +64fe45c879d2ce11b605b7ccbadec44b7474cdb3 1 0
    3.71 +unsat
    3.72 +27388d866d376a195719342119d2c39bddbbda5e 1 0
    3.73 +unsat
    3.74 +4fdb33415d645476800f24bc2645077ed20fbcc7 1 0
    3.75 +unsat
    3.76 +34954aeef00ac521d8d6983ea46bbdde741af613 1 0
    3.77 +unsat
    3.78 +c975ecb6377964929f32ae1b30fbd693a2969c6a 1 0
    3.79 +unsat
    3.80 +5c9a9ffe9941b81f90170c912034e8b681bc281f 1 0
    3.81 +unsat
    3.82 +26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0
    3.83 +unsat
     4.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 10:42:06 2012 +0200
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Mar 26 11:01:04 2012 +0200
     4.3 @@ -212,7 +212,7 @@
     4.4  lemma
     4.5    assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
     4.6    shows "f a = g b"
     4.7 -  using assms (* BROKEN by smt *) oops
     4.8 +  using assms by smt
     4.9  
    4.10  lemma
    4.11    assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
    4.12 @@ -853,7 +853,7 @@
    4.13    using point.simps
    4.14    using [[smt_datatypes, smt_oracle]]
    4.15    using [[z3_options="AUTO_CONFIG=false"]]
    4.16 -  (* BROKEN by smt+ *) oops
    4.17 +  by smt+
    4.18  
    4.19  lemma
    4.20    "cy (p \<lparr> cx := a \<rparr>) = cy p"
    4.21 @@ -862,7 +862,7 @@
    4.22    using point.simps
    4.23    using [[smt_datatypes, smt_oracle]]
    4.24    using [[z3_options="AUTO_CONFIG=false"]]
    4.25 -  (* BROKEN by smt+ *) oops
    4.26 +  by smt+
    4.27  
    4.28  lemma
    4.29    "p1 = p2 \<longrightarrow> cx p1 = cx p2"
    4.30 @@ -891,7 +891,7 @@
    4.31    using point.simps bw_point.simps
    4.32    using [[smt_datatypes, smt_oracle]]
    4.33    using [[z3_options="AUTO_CONFIG=false"]]
    4.34 -  (* BROKEN by smt+ *) oops
    4.35 +  by smt+
    4.36  
    4.37  lemma
    4.38    "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
    4.39 @@ -905,7 +905,7 @@
    4.40    using point.simps bw_point.simps
    4.41    using [[smt_datatypes, smt_oracle]]
    4.42    using [[z3_options="AUTO_CONFIG=false"]]
    4.43 -  (* BROKEN by smt *) oops
    4.44 +  by smt
    4.45  
    4.46  
    4.47  subsubsection {* Type definitions *}
    4.48 @@ -919,7 +919,7 @@
    4.49    using n1_def n2_def n3_def nplus_def
    4.50    using [[smt_datatypes, smt_oracle]]
    4.51    using [[z3_options="AUTO_CONFIG=false"]]
    4.52 -  (* BROKEN by smt+ *) oops
    4.53 +  by smt+
    4.54  
    4.55  
    4.56