# HG changeset patch
# User boehmes
# Date 1299703238 -3600
# Node ID 83dd157ec9ab800c3c167da67b48962d61859959
# Parent  55d981e1232a8fb2ad363357646c9f591256ec98
finished and tested Z3 proof reconstruction for injective functions;
only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

diff -r 55d981e1232a -r 83dd157ec9ab src/HOL/SMT_Examples/SMT_Tests.certs
--- a/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Mar 09 21:40:38 2011 +0100
@@ -58652,3 +58652,376 @@
 #121 := [asserted]: #43
 [mp #121 #131]: false
 unsat
+e82a6cc10c3ef4d2130dbd751caaaa2ceb41a37f 138 0
+#2 := false
+decl f4 :: S2
+#9 := f4
+decl f3 :: S2
+#8 := f3
+#152 := (= f3 f4)
+decl inj!0 :: (-> S3 S2)
+decl f6 :: (-> S2 S3)
+#22 := (f6 f4)
+#207 := (inj!0 #22)
+#208 := (= #207 f4)
+#209 := (= f4 #207)
+#14 := (:var 0 S2)
+#15 := (f6 #14)
+#89 := (pattern #15)
+#88 := (inj!0 #15)
+#85 := (= #88 #14)
+#570 := (forall (vars (k!0 S2)) (:pat #89) #85)
+#90 := (forall (vars (k!0 S2)) (:pat #89) #85)
+#571 := (iff #90 #570)
+#573 := (iff #570 #570)
+#574 := [rewrite]: #573
+#572 := [rewrite]: #571
+#575 := [trans #572 #574]: #571
+#12 := (:var 1 S2)
+#47 := (= #12 #14)
+#13 := (f6 #12)
+#16 := (= #13 #15)
+#53 := (not #16)
+#54 := (or #53 #47)
+#59 := (forall (vars (?v0 S2) (?v1 S2)) #54)
+#86 := (iff #59 #90)
+#83 := [rewrite]: #86
+#93 := (~ #59 #59)
+#91 := (~ #54 #54)
+#92 := [refl]: #91
+#94 := [nnf-pos #92]: #93
+decl f5 :: S2
+#10 := f5
+#11 := (distinct f3 f4 f5)
+#62 := (and #11 #59)
+#68 := (not #62)
+#21 := (f6 f3)
+#23 := (= #21 #22)
+#24 := (not #23)
+#69 := (or #24 #68)
+#74 := (not #69)
+#17 := (= #14 #12)
+#18 := (implies #16 #17)
+#19 := (forall (vars (?v0 S2) (?v1 S2)) #18)
+#20 := (and #11 #19)
+#25 := (implies #20 #24)
+#26 := (not #25)
+#75 := (iff #26 #74)
+#72 := (iff #25 #69)
+#65 := (implies #62 #24)
+#70 := (iff #65 #69)
+#71 := [rewrite]: #70
+#66 := (iff #25 #65)
+#63 := (iff #20 #62)
+#60 := (iff #19 #59)
+#57 := (iff #18 #54)
+#50 := (implies #16 #47)
+#55 := (iff #50 #54)
+#56 := [rewrite]: #55
+#51 := (iff #18 #50)
+#48 := (iff #17 #47)
+#49 := [rewrite]: #48
+#52 := [monotonicity #49]: #51
+#58 := [trans #52 #56]: #57
+#61 := [quant-intro #58]: #60
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64]: #66
+#73 := [trans #67 #71]: #72
+#76 := [monotonicity #73]: #75
+#46 := [asserted]: #26
+#79 := [mp #46 #76]: #74
+#78 := [not-or-elim #79]: #62
+#81 := [and-elim #78]: #59
+#87 := [mp~ #81 #94]: #59
+#84 := [mp #87 #83]: #90
+#576 := [mp #84 #575]: #570
+#569 := (not #570)
+#549 := (or #569 #209)
+#550 := (or #569 #208)
+#546 := (iff #550 #549)
+#188 := (iff #549 #549)
+#553 := [rewrite]: #188
+#547 := (iff #208 #209)
+#548 := [rewrite]: #547
+#552 := [monotonicity #548]: #546
+#555 := [trans #552 #553]: #546
+#551 := [quant-inst #9]: #550
+#193 := [mp #551 #555]: #549
+#543 := [unit-resolution #193 #576]: #209
+#254 := [symm #543]: #208
+#269 := (= f3 #207)
+#565 := (inj!0 #21)
+#267 := (= #565 #207)
+#250 := (= #207 #565)
+#554 := (= #22 #21)
+#77 := [not-or-elim #79]: #23
+#557 := [symm #77]: #554
+#266 := [monotonicity #557]: #250
+#268 := [symm #266]: #267
+#567 := (= f3 #565)
+#559 := (or #569 #567)
+#566 := (= #565 f3)
+#217 := (or #569 #566)
+#560 := (iff #217 #559)
+#561 := (iff #559 #559)
+#202 := [rewrite]: #561
+#568 := (iff #566 #567)
+#563 := [rewrite]: #568
+#218 := [monotonicity #563]: #560
+#545 := [trans #218 #202]: #560
+#222 := [quant-inst #8]: #217
+#206 := [mp #222 #545]: #559
+#544 := [unit-resolution #206 #576]: #567
+#160 := [trans #544 #268]: #269
+#539 := [trans #160 #254]: #152
+#239 := (not #152)
+#154 := (= f4 f5)
+#241 := (not #154)
+#153 := (= f3 f5)
+#240 := (not #153)
+#232 := (and #239 #240 #241)
+#80 := [and-elim #78]: #11
+#219 := (not #11)
+#351 := (or #219 #232)
+#558 := [def-axiom]: #351
+#194 := [unit-resolution #558 #80]: #232
+#243 := (not #232)
+#244 := (or #243 #239)
+#172 := [def-axiom]: #244
+#556 := [unit-resolution #172 #194]: #239
+[unit-resolution #556 #539]: false
+unsat
+03a4fcd182047beb0b3be329b34440294749812c 117 0
+#2 := false
+decl f5 :: S3
+#18 := f5
+decl f4 :: S3
+#17 := f4
+#19 := (= f4 f5)
+decl inj!0 :: (-> S2 S4 S3)
+decl f3 :: (-> S2 S3 S4)
+decl f6 :: S2
+#22 := f6
+#24 := (f3 f6 f5)
+#565 := (inj!0 f6 #24)
+#220 := (= #565 f5)
+#352 := (= f5 #565)
+#9 := (:var 1 S3)
+#87 := (:var 0 S2)
+#84 := (f3 #87 #9)
+#85 := (pattern #84)
+#88 := (inj!0 #87 #84)
+#89 := (= #88 #9)
+#82 := (forall (vars (k!0 S2) (k!1 S3)) (:pat #85) #89)
+#11 := (:var 0 S3)
+#14 := (= #9 #11)
+#8 := (:var 2 S2)
+#12 := (f3 #8 #11)
+#10 := (f3 #8 #9)
+#13 := (= #10 #12)
+#49 := (not #13)
+#50 := (or #49 #14)
+#53 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #50)
+#83 := (iff #53 #82)
+#94 := [rewrite]: #83
+#92 := (~ #53 #53)
+#90 := (~ #50 #50)
+#91 := [refl]: #90
+#93 := [nnf-pos #91]: #92
+#20 := (not #19)
+#59 := (and #20 #53)
+#67 := (not #59)
+#23 := (f3 f6 f4)
+#25 := (= #23 #24)
+#26 := (not #25)
+#68 := (or #26 #67)
+#73 := (not #68)
+#15 := (implies #13 #14)
+#16 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S3)) #15)
+#21 := (and #16 #20)
+#27 := (implies #21 #26)
+#28 := (not #27)
+#74 := (iff #28 #73)
+#71 := (iff #27 #68)
+#64 := (implies #59 #26)
+#69 := (iff #64 #68)
+#70 := [rewrite]: #69
+#65 := (iff #27 #64)
+#62 := (iff #21 #59)
+#56 := (and #53 #20)
+#60 := (iff #56 #59)
+#61 := [rewrite]: #60
+#57 := (iff #21 #56)
+#54 := (iff #16 #53)
+#51 := (iff #15 #50)
+#52 := [rewrite]: #51
+#55 := [quant-intro #52]: #54
+#58 := [monotonicity #55]: #57
+#63 := [trans #58 #61]: #62
+#66 := [monotonicity #63]: #65
+#72 := [trans #66 #70]: #71
+#75 := [monotonicity #72]: #74
+#48 := [asserted]: #28
+#78 := [mp #48 #75]: #73
+#77 := [not-or-elim #78]: #59
+#80 := [and-elim #77]: #53
+#86 := [mp~ #80 #93]: #53
+#95 := [mp #86 #94]: #82
+#242 := (not #82)
+#232 := (or #242 #352)
+#566 := (or #242 #220)
+#568 := (iff #566 #232)
+#564 := (iff #232 #232)
+#570 := [rewrite]: #564
+#559 := (iff #220 #352)
+#231 := [rewrite]: #559
+#569 := [monotonicity #231]: #568
+#560 := [trans #569 #570]: #568
+#567 := [quant-inst #18 #22]: #566
+#218 := [mp #567 #560]: #232
+#219 := [unit-resolution #218 #95]: #352
+#209 := [symm #219]: #220
+#210 := (= f4 #565)
+#153 := (inj!0 f6 #23)
+#207 := (= #153 #565)
+#203 := (= #565 #153)
+#223 := (= #24 #23)
+#76 := [not-or-elim #78]: #25
+#561 := [symm #76]: #223
+#546 := [monotonicity #561]: #203
+#208 := [symm #546]: #207
+#154 := (= f4 #153)
+#233 := (or #242 #154)
+#240 := (= #153 f4)
+#244 := (or #242 #240)
+#173 := (iff #244 #233)
+#243 := (iff #233 #233)
+#247 := [rewrite]: #243
+#241 := (iff #240 #154)
+#155 := [rewrite]: #241
+#246 := [monotonicity #155]: #173
+#226 := [trans #246 #247]: #173
+#245 := [quant-inst #17 #22]: #244
+#563 := [mp #245 #226]: #233
+#562 := [unit-resolution #563 #95]: #154
+#548 := [trans #562 #208]: #210
+#549 := [trans #548 #209]: #19
+#79 := [and-elim #77]: #20
+[unit-resolution #79 #549]: false
+unsat
+16237d3c6ed6b1b0d94625f503401c43285f9eec 115 0
+#2 := false
+decl f5 :: S2
+#18 := f5
+decl f4 :: S2
+#17 := f4
+#19 := (= f4 f5)
+decl inj!0 :: (-> S3 S4 S2)
+decl f3 :: (-> S2 S3 S4)
+decl f6 :: S3
+#22 := f6
+#24 := (f3 f5 f6)
+#563 := (inj!0 f6 #24)
+#218 := (= #563 f5)
+#350 := (= f5 #563)
+#9 := (:var 1 S3)
+#11 := (:var 0 S2)
+#12 := (f3 #11 #9)
+#88 := (pattern #12)
+#87 := (inj!0 #9 #12)
+#84 := (= #87 #11)
+#89 := (forall (vars (k!0 S2) (k!1 S3)) (:pat #88) #84)
+#8 := (:var 2 S2)
+#14 := (= #8 #11)
+#10 := (f3 #8 #9)
+#13 := (= #10 #12)
+#49 := (not #13)
+#50 := (or #49 #14)
+#53 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2)) #50)
+#85 := (iff #53 #89)
+#82 := [rewrite]: #85
+#92 := (~ #53 #53)
+#90 := (~ #50 #50)
+#91 := [refl]: #90
+#93 := [nnf-pos #91]: #92
+#20 := (not #19)
+#59 := (and #20 #53)
+#67 := (not #59)
+#23 := (f3 f4 f6)
+#25 := (= #23 #24)
+#26 := (not #25)
+#68 := (or #26 #67)
+#73 := (not #68)
+#15 := (implies #13 #14)
+#16 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2)) #15)
+#21 := (and #16 #20)
+#27 := (implies #21 #26)
+#28 := (not #27)
+#74 := (iff #28 #73)
+#71 := (iff #27 #68)
+#64 := (implies #59 #26)
+#69 := (iff #64 #68)
+#70 := [rewrite]: #69
+#65 := (iff #27 #64)
+#62 := (iff #21 #59)
+#56 := (and #53 #20)
+#60 := (iff #56 #59)
+#61 := [rewrite]: #60
+#57 := (iff #21 #56)
+#54 := (iff #16 #53)
+#51 := (iff #15 #50)
+#52 := [rewrite]: #51
+#55 := [quant-intro #52]: #54
+#58 := [monotonicity #55]: #57
+#63 := [trans #58 #61]: #62
+#66 := [monotonicity #63]: #65
+#72 := [trans #66 #70]: #71
+#75 := [monotonicity #72]: #74
+#48 := [asserted]: #28
+#78 := [mp #48 #75]: #73
+#77 := [not-or-elim #78]: #59
+#80 := [and-elim #77]: #53
+#86 := [mp~ #80 #93]: #53
+#83 := [mp #86 #82]: #89
+#240 := (not #89)
+#230 := (or #240 #350)
+#564 := (or #240 #218)
+#566 := (iff #564 #230)
+#562 := (iff #230 #230)
+#568 := [rewrite]: #562
+#557 := (iff #218 #350)
+#229 := [rewrite]: #557
+#567 := [monotonicity #229]: #566
+#558 := [trans #567 #568]: #566
+#565 := [quant-inst #22 #18]: #564
+#216 := [mp #565 #558]: #230
+#217 := [unit-resolution #216 #83]: #350
+#207 := [symm #217]: #218
+#208 := (= f4 #563)
+#151 := (inj!0 f6 #23)
+#205 := (= #151 #563)
+#201 := (= #563 #151)
+#221 := (= #24 #23)
+#76 := [not-or-elim #78]: #25
+#559 := [symm #76]: #221
+#544 := [monotonicity #559]: #201
+#206 := [symm #544]: #205
+#152 := (= f4 #151)
+#231 := (or #240 #152)
+#238 := (= #151 f4)
+#242 := (or #240 #238)
+#171 := (iff #242 #231)
+#241 := (iff #231 #231)
+#245 := [rewrite]: #241
+#239 := (iff #238 #152)
+#153 := [rewrite]: #239
+#244 := [monotonicity #153]: #171
+#224 := [trans #244 #245]: #171
+#243 := [quant-inst #22 #17]: #242
+#561 := [mp #243 #224]: #231
+#560 := [unit-resolution #561 #83]: #152
+#546 := [trans #560 #206]: #208
+#547 := [trans #546 #207]: #19
+#79 := [and-elim #77]: #20
+[unit-resolution #79 #547]: false
+unsat
diff -r 55d981e1232a -r 83dd157ec9ab src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Mar 09 21:40:38 2011 +0100
@@ -194,7 +194,12 @@
 
 lemma
   "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
-  sorry  (* FIXME: injective function *)
+  by smt
+
+lemma
+  "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
+  "(\<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+
 
 lemma
   assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
diff -r 55d981e1232a -r 83dd157ec9ab src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Mar 09 21:40:38 2011 +0100
@@ -64,8 +64,7 @@
   Z3_Proof_Tools.by_tac (
     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
     THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
-    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
-  Thm.elim_implies def
+    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
 
 
 fun expand thm ct =
@@ -100,8 +99,9 @@
   let
     val (lhs, rhs) =
       pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct))
-    val lhs_thm = prove_lhs ctxt rhs lhs
-    val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
+    val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
+    val rhs_thm =
+      Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
   in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
 
 
diff -r 55d981e1232a -r 83dd157ec9ab src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Mar 09 21:40:38 2011 +0100
@@ -716,13 +716,12 @@
   val prove_conj_disj_eq =
     Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
 
-  fun assume_prems ctxt thm =
-    Assumption.add_assumes (Drule.cprems_of thm) ctxt
-    |>> (fn thms => fold Thm.elim_implies thms thm)
+  fun declare_hyps ctxt thm =
+    (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
 in
 
 fun rewrite simpset ths ct ctxt =
-  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
+  apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
     named ctxt "conj/disj/distinct" prove_conj_disj_eq,
     Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
diff -r 55d981e1232a -r 83dd157ec9ab src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Mar 09 10:28:01 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Mar 09 21:40:38 2011 +0100
@@ -177,7 +177,8 @@
   let val (cv, cu) = Thm.dest_abs NONE ct
   in f (cv :: cvs) cu #>> Thm.cabs cv end
 
-val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
+val is_atomic =
+  (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
 
 fun abstract (ext_logic, with_theories) =
   let