# HG changeset patch # User boehmes # Date 1320684878 -3600 # Node ID 13ab80eafd71ec4d6421a97bad77d8926d24c2af # Parent 828e08541cee4b43cd470d72316c50b7d322ba5a try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways diff -r 828e08541cee -r 13ab80eafd71 src/HOL/SMT_Examples/SMT_Examples.certs --- 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 diff -r 828e08541cee -r 13ab80eafd71 src/HOL/SMT_Examples/SMT_Examples.thy --- 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 } \ Sup { b | i::bool . True }" + and "Sup { b | i::bool . True } \ Sup { a | i::bool . True }" + shows "Sup { a | i::bool . True } \ Sup { a | i::bool . True }" + using assms by (smt order_trans) + +end + + + section {* Monomorphization examples *} definition Pred :: "'a \ bool" where "Pred x = True" diff -r 828e08541cee -r 13ab80eafd71 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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, _)) = diff -r 828e08541cee -r 13ab80eafd71 src/HOL/Tools/SMT/z3_proof_tools.ML --- 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