try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Nov 07 17:54:35 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Nov 07 17:54:38 2011 +0100
@@ -15300,3 +15300,101 @@
 #54 := [not-or-elim #53]: #12
 [th-lemma arith farkas 1 1 1 #54 #58 #56]: false
 unsat
+c5587cced9846bad48f0e98f61ddedd728385b78 97 0
+#2 := false
+decl f1 :: S1
+#3 := f1
+decl f3 :: (-> S3 S2 S1)
+decl f10 :: (-> S5 S3 S2)
+decl f12 :: (-> S6 S3 S3)
+decl f6 :: S3
+#19 := f6
+decl f13 :: S6
+#43 := f13
+#44 := (f12 f13 f6)
+decl f11 :: S5
+#42 := f11
+#45 := (f10 f11 #44)
+decl f8 :: (-> S4 S2 S3)
+decl f9 :: S4
+#29 := f9
+#46 := (f8 f9 #45)
+#54 := (f3 #46 #45)
+#55 := (= #54 f1)
+#56 := (not #55)
+#141 := [asserted]: #56
+decl f4 :: S3
+#7 := f4
+#47 := (f12 f13 f4)
+#48 := (f10 f11 #47)
+#51 := (f8 f9 #48)
+#52 := (f3 #51 #45)
+#53 := (= #52 f1)
+#140 := [asserted]: #53
+#49 := (f3 #46 #48)
+#50 := (= #49 f1)
+#139 := [asserted]: #50
+#8 := (:var 0 S2)
+#12 := (:var 1 S2)
+#34 := (f8 f9 #12)
+#35 := (f3 #34 #8)
+#30 := (:var 2 S2)
+#31 := (f8 f9 #30)
+#32 := (f3 #31 #12)
+#636 := (pattern #32 #35)
+#37 := (f3 #31 #8)
+#38 := (= #37 f1)
+#36 := (= #35 f1)
+#113 := (not #36)
+#33 := (= #32 f1)
+#121 := (not #33)
+#130 := (or #121 #113 #38)
+#637 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S2)) (:pat #636) #130)
+#133 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S2)) #130)
+#640 := (iff #133 #637)
+#638 := (iff #130 #130)
+#639 := [refl]: #638
+#641 := [quant-intro #639]: #640
+#147 := (~ #133 #133)
+#163 := (~ #130 #130)
+#164 := [refl]: #163
+#148 := [nnf-pos #164]: #147
+#39 := (implies #36 #38)
+#40 := (implies #33 #39)
+#41 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S2)) #40)
+#136 := (iff #41 #133)
+#115 := (or #113 #38)
+#122 := (or #121 #115)
+#127 := (forall (vars (?v0 S2) (?v1 S2) (?v2 S2)) #122)
+#134 := (iff #127 #133)
+#131 := (iff #122 #130)
+#132 := [rewrite]: #131
+#135 := [quant-intro #132]: #134
+#128 := (iff #41 #127)
+#125 := (iff #40 #122)
+#118 := (implies #33 #115)
+#123 := (iff #118 #122)
+#124 := [rewrite]: #123
+#119 := (iff #40 #118)
+#116 := (iff #39 #115)
+#117 := [rewrite]: #116
+#120 := [monotonicity #117]: #119
+#126 := [trans #120 #124]: #125
+#129 := [quant-intro #126]: #128
+#137 := [trans #129 #135]: #136
+#112 := [asserted]: #41
+#138 := [mp #112 #137]: #133
+#165 := [mp~ #138 #148]: #133
+#642 := [mp #165 #641]: #637
+#306 := (not #53)
+#220 := (not #50)
+#308 := (not #637)
+#299 := (or #308 #220 #306 #55)
+#221 := (or #220 #306 #55)
+#310 := (or #308 #221)
+#312 := (iff #310 #299)
+#309 := [rewrite]: #312
+#311 := [quant-inst #45 #48 #45]: #310
+#313 := [mp #311 #309]: #299
+[unit-resolution #313 #642 #139 #140 #141]: false
+unsat

--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Nov 07 17:54:35 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Nov 07 17:54:38 2011 +0100
@@ -510,6 +510,19 @@
   by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
 
 
+context complete_lattice
+begin
+
+lemma 
+  assumes "Sup { a | i::bool . True } \<le> Sup { b | i::bool . True }"
+  and     "Sup { b | i::bool . True } \<le> Sup { a | i::bool . True }"
+  shows   "Sup { a | i::bool . True } \<le> Sup { a | i::bool . True }"
+  using assms by (smt order_trans)
+
+end
+
+
+
 section {* Monomorphization examples *}
 
 definition Pred :: "'a \<Rightarrow> bool" where "Pred x = True"

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:54:35 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 07 17:54:38 2011 +0100
@@ -160,8 +160,8 @@
   fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
 
   fun lookup_assm assms_net ct =
-    Z3_Proof_Tools.net_instance' burrow_snd_option assms_net ct
-    |> Option.map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
+    Z3_Proof_Tools.net_instances assms_net ct
+    |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
 in
 
 fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
@@ -183,7 +183,18 @@
         val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
       in (Thm.implies_elim thm thm', ctxt') end
 
-    fun add (idx, ct) ((is, thms), (ctxt, ptab)) =
+    fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) =
+      let
+        val (thm, ctxt') =
+          if exact then (Thm.implies_elim thm1 th, ctxt)
+          else assume thm1 ctxt
+        val thms' = if exact then thms else th :: thms
+      in 
+        ((insert (op =) i is, thms'),
+          (ctxt', Inttab.update (idx, Thm thm) ptab))
+      end
+
+    fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
       let
         val thm1 = 
           Thm.trivial ct
@@ -191,19 +202,10 @@
         val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
       in
         (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
-          NONE =>
+          [] =>
             let val (thm, ctxt') = assume thm1 ctxt
             in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
-        | SOME ((i, th), exact) =>
-            let
-              val (thm, ctxt') =
-                if exact then (Thm.implies_elim thm1 th, ctxt)
-                else assume thm1 ctxt
-              val thms' = if exact then thms else th :: thms
-            in 
-              ((insert (op =) i is, thms'),
-                (ctxt', Inttab.update (idx, Thm thm) ptab))
-            end)
+        | ithms => fold (add1 idx thm1) ithms cx)
       end
   in fold add asserted (([], []), (ctxt, Inttab.empty)) end
 
@@ -857,14 +859,15 @@
   fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
     @{thm reflexive}, Z3_Proof_Literals.true_thm]
 
-  fun discharge_tac rules =
-    Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac
-
+  fun discharge_assms_tac rules =
+    REPEAT (HEADGOAL (
+      Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
+    
   fun discharge_assms rules thm =
     if Thm.nprems_of thm = 0 then Goal.norm_result thm
     else
-      (case Seq.pull (discharge_tac rules 1 thm) of
-        SOME (thm', _) => discharge_assms rules thm'
+      (case Seq.pull (discharge_assms_tac rules thm) of
+        SOME (thm', _) => Goal.norm_result thm'
       | NONE => raise THM ("failed to discharge premise", 1, [thm]))
 
   fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 07 17:54:35 2011 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 07 17:54:38 2011 +0100
@@ -11,8 +11,7 @@
 
   (*theorem nets*)
   val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
-  val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
-    cterm -> 'a option
+  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
   val net_instance: thm Net.net -> cterm -> thm option
 
   (*proof combinators*)
@@ -68,16 +67,17 @@
     let
       val lookup = if match then Net.match_term else Net.unify_term
       val xthms = lookup net (Thm.term_of ct)
-      fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
-      fun first_of' f ct =
+      fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
+      fun select' ct =
         let val thm = Thm.trivial ct
-        in get_first (f (try (fn rule => rule COMP thm))) xthms end
-    in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
+        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
+    in (case select ct of [] => select' ct | xthms' => xthms') end
 in
 
-fun net_instance' f = instances_from_net false f
+val net_instances =
+  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
 
-val net_instance = instances_from_net true I
+val net_instance = try hd oo instances_from_net true I
 
 end