src/HOL/Tools/SMT/z3_proof_reconstruction.ML
author wenzelm
Thu Apr 18 17:07:01 2013 +0200 (2013-04-18)
changeset 51717 9e7d1c139569
parent 49980 34b0464d7eef
child 52230 1105b3b5aa77
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
     1 (*  Title:      HOL/Tools/SMT/z3_proof_reconstruction.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Proof reconstruction for proofs found by Z3.
     5 *)
     6 
     7 signature Z3_PROOF_RECONSTRUCTION =
     8 sig
     9   val add_z3_rule: thm -> Context.generic -> Context.generic
    10   val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
    11     int list * thm
    12   val setup: theory -> theory
    13 end
    14 
    15 structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
    16 struct
    17 
    18 
    19 fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
    20   ("Z3 proof reconstruction: " ^ msg))
    21 
    22 
    23 
    24 (* net of schematic rules *)
    25 
    26 val z3_ruleN = "z3_rule"
    27 
    28 local
    29   val description = "declaration of Z3 proof rules"
    30 
    31   val eq = Thm.eq_thm
    32 
    33   structure Z3_Rules = Generic_Data
    34   (
    35     type T = thm Net.net
    36     val empty = Net.empty
    37     val extend = I
    38     val merge = Net.merge eq
    39   )
    40 
    41   val prep =
    42     `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
    43 
    44   fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
    45   fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
    46 
    47   val add = Thm.declaration_attribute (Z3_Rules.map o ins)
    48   val del = Thm.declaration_attribute (Z3_Rules.map o del)
    49 in
    50 
    51 val add_z3_rule = Z3_Rules.map o ins
    52 
    53 fun by_schematic_rule ctxt ct =
    54   the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
    55 
    56 val z3_rules_setup =
    57   Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
    58   Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
    59 
    60 end
    61 
    62 
    63 
    64 (* proof tools *)
    65 
    66 fun named ctxt name prover ct =
    67   let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    68   in prover ct end
    69 
    70 fun NAMED ctxt name tac i st =
    71   let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
    72   in tac i st end
    73 
    74 fun pretty_goal ctxt thms t =
    75   [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
    76   |> not (null thms) ? cons (Pretty.big_list "assumptions:"
    77        (map (Display.pretty_thm ctxt) thms))
    78 
    79 fun try_apply ctxt thms =
    80   let
    81     fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
    82       Pretty.big_list ("Z3 found a proof," ^
    83         " but proof reconstruction failed at the following subgoal:")
    84         (pretty_goal ctxt thms (Thm.term_of ct)),
    85       Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
    86         " might solve this problem.")])
    87 
    88     fun apply [] ct = error (try_apply_err ct)
    89       | apply (prover :: provers) ct =
    90           (case try prover ct of
    91             SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
    92           | NONE => apply provers ct)
    93 
    94     fun schematic_label full = "schematic rules" |> full ? suffix " (full)"
    95     fun schematic ctxt full ct =
    96       ct
    97       |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms
    98       |> named ctxt (schematic_label full) (by_schematic_rule ctxt)
    99       |> fold Thm.elim_implies thms
   100 
   101   in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end
   102 
   103 local
   104   val rewr_if =
   105     @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
   106 in
   107 
   108 fun HOL_fast_tac ctxt =
   109   Classical.fast_tac (put_claset HOL_cs ctxt)
   110 
   111 fun simp_fast_tac ctxt =
   112   Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if])
   113   THEN_ALL_NEW HOL_fast_tac ctxt
   114 
   115 end
   116 
   117 
   118 
   119 (* theorems and proofs *)
   120 
   121 (** theorem incarnations **)
   122 
   123 datatype theorem =
   124   Thm of thm | (* theorem without special features *)
   125   MetaEq of thm | (* meta equality "t == s" *)
   126   Literals of thm * Z3_Proof_Literals.littab
   127     (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
   128 
   129 fun thm_of (Thm thm) = thm
   130   | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
   131   | thm_of (Literals (thm, _)) = thm
   132 
   133 fun meta_eq_of (MetaEq thm) = thm
   134   | meta_eq_of p = mk_meta_eq (thm_of p)
   135 
   136 fun literals_of (Literals (_, lits)) = lits
   137   | literals_of p = Z3_Proof_Literals.make_littab [thm_of p]
   138 
   139 
   140 
   141 (** core proof rules **)
   142 
   143 (* assumption *)
   144 
   145 local
   146   val remove_trigger = mk_meta_eq @{thm SMT.trigger_def}
   147   val remove_weight = mk_meta_eq @{thm SMT.weight_def}
   148   val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
   149 
   150   fun rewrite_conv _ [] = Conv.all_conv
   151     | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
   152 
   153   val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
   154     remove_fun_app, Z3_Proof_Literals.rewrite_true]
   155 
   156   fun rewrite _ [] = I
   157     | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
   158 
   159   fun lookup_assm assms_net ct =
   160     Z3_Proof_Tools.net_instances assms_net ct
   161     |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
   162 in
   163 
   164 fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
   165   let
   166     val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules
   167     val eqs' = union Thm.eq_thm eqs prep_rules
   168 
   169     val assms_net =
   170       assms
   171       |> map (apsnd (rewrite ctxt eqs'))
   172       |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
   173       |> Z3_Proof_Tools.thm_net_of snd 
   174 
   175     fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
   176 
   177     fun assume thm ctxt =
   178       let
   179         val ct = Thm.cprem_of thm 1
   180         val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
   181       in (Thm.implies_elim thm thm', ctxt') end
   182 
   183     fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) =
   184       let
   185         val (thm, ctxt') =
   186           if exact then (Thm.implies_elim thm1 th, ctxt)
   187           else assume thm1 ctxt
   188         val thms' = if exact then thms else th :: thms
   189       in 
   190         ((insert (op =) i is, thms'),
   191           (ctxt', Inttab.update (idx, Thm thm) ptab))
   192       end
   193 
   194     fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
   195       let
   196         val thm1 = 
   197           Thm.trivial ct
   198           |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
   199         val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
   200       in
   201         (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
   202           [] =>
   203             let val (thm, ctxt') = assume thm1 ctxt
   204             in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
   205         | ithms => fold (add1 idx thm1) ithms cx)
   206       end
   207   in fold add asserted (([], []), (ctxt, Inttab.empty)) end
   208 
   209 end
   210 
   211 
   212 (* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
   213 local
   214   val precomp = Z3_Proof_Tools.precompose2
   215   val comp = Z3_Proof_Tools.compose
   216 
   217   val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
   218   val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
   219 
   220   val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
   221   val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
   222 in
   223 fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
   224   | mp p_q p = 
   225       let
   226         val pq = thm_of p_q
   227         val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
   228       in Thm (Thm.implies_elim thm p) end
   229 end
   230 
   231 
   232 (* and_elim:     P1 & ... & Pn ==> Pi *)
   233 (* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
   234 local
   235   fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
   236 
   237   fun derive conj t lits idx ptab =
   238     let
   239       val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
   240       val ls = Z3_Proof_Literals.explode conj false false [t] lit
   241       val lits' = fold Z3_Proof_Literals.insert_lit ls
   242         (Z3_Proof_Literals.delete_lit lit lits)
   243 
   244       fun upd thm = Literals (thm_of thm, lits')
   245       val ptab' = Inttab.map_entry idx upd ptab
   246     in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end
   247 
   248   fun lit_elim conj (p, idx) ct ptab =
   249     let val lits = literals_of p
   250     in
   251       (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
   252         SOME lit => (Thm lit, ptab)
   253       | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
   254     end
   255 in
   256 val and_elim = lit_elim true
   257 val not_or_elim = lit_elim false
   258 end
   259 
   260 
   261 (* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
   262 local
   263   fun step lit thm =
   264     Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
   265   val explode_disj = Z3_Proof_Literals.explode false false false
   266   fun intro hyps thm th = fold step (explode_disj hyps th) thm
   267 
   268   fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
   269   val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
   270 in
   271 fun lemma thm ct =
   272   let
   273     val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
   274     val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
   275     val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
   276   in Thm (Z3_Proof_Tools.compose ccontr th) end
   277 end
   278 
   279 
   280 (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
   281 local
   282   val explode_disj = Z3_Proof_Literals.explode false true false
   283   val join_disj = Z3_Proof_Literals.join false
   284   fun unit thm thms th =
   285     let
   286       val t = @{const Not} $ SMT_Utils.prop_of thm
   287       val ts = map SMT_Utils.prop_of thms
   288     in
   289       join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
   290     end
   291 
   292   fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
   293   fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
   294   val contrapos =
   295     Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
   296 in
   297 fun unit_resolution thm thms ct =
   298   Z3_Proof_Literals.negate (Thm.dest_arg ct)
   299   |> Z3_Proof_Tools.under_assumption (unit thm thms)
   300   |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
   301 end
   302 
   303 
   304 (* P ==> P == True   or   P ==> P == False *)
   305 local
   306   val iff1 = @{lemma "P ==> P == (~ False)" by simp}
   307   val iff2 = @{lemma "~P ==> P == False" by simp}
   308 in
   309 fun iff_true thm = MetaEq (thm COMP iff1)
   310 fun iff_false thm = MetaEq (thm COMP iff2)
   311 end
   312 
   313 
   314 (* distributivity of | over & *)
   315 fun distributivity ctxt = Thm o try_apply ctxt [] [
   316   named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   317     (* FIXME: not very well tested *)
   318 
   319 
   320 (* Tseitin-like axioms *)
   321 local
   322   val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
   323   val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
   324   val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
   325   val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
   326 
   327   fun prove' conj1 conj2 ct2 thm =
   328     let
   329       val littab =
   330         Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
   331         |> cons Z3_Proof_Literals.true_thm
   332         |> Z3_Proof_Literals.make_littab
   333     in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
   334 
   335   fun prove rule (ct1, conj1) (ct2, conj2) =
   336     Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
   337 
   338   fun prove_def_axiom ct =
   339     let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
   340     in
   341       (case Thm.term_of ct1 of
   342         @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
   343           prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
   344       | @{const HOL.conj} $ _ $ _ =>
   345           prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
   346       | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
   347           prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
   348       | @{const HOL.disj} $ _ $ _ =>
   349           prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
   350       | Const (@{const_name distinct}, _) $ _ =>
   351           let
   352             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
   353             val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
   354             fun prv cu =
   355               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
   356               in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
   357           in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
   358       | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
   359           let
   360             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
   361             val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
   362             fun prv cu =
   363               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
   364               in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
   365           in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
   366       | _ => raise CTERM ("prove_def_axiom", [ct]))
   367     end
   368 in
   369 fun def_axiom ctxt = Thm o try_apply ctxt [] [
   370   named ctxt "conj/disj/distinct" prove_def_axiom,
   371   Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
   372     named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
   373 end
   374 
   375 
   376 (* local definitions *)
   377 local
   378   val intro_rules = [
   379     @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
   380     @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
   381       by simp},
   382     @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
   383 
   384   val apply_rules = [
   385     @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
   386     @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
   387       by (atomize(full)) fastforce} ]
   388 
   389   val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
   390 
   391   fun apply_rule ct =
   392     (case get_first (try (inst_rule ct)) intro_rules of
   393       SOME thm => thm
   394     | NONE => raise CTERM ("intro_def", [ct]))
   395 in
   396 fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
   397 
   398 fun apply_def thm =
   399   get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
   400   |> the_default (Thm thm)
   401 end
   402 
   403 
   404 (* negation normal form *)
   405 local
   406   val quant_rules1 = ([
   407     @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
   408     @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
   409     @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
   410     @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
   411 
   412   val quant_rules2 = ([
   413     @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
   414     @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
   415     @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
   416     @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
   417 
   418   fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
   419     Tactic.rtac thm ORELSE'
   420     (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
   421     (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
   422 
   423   fun nnf_quant_tac_varified vars eq =
   424     nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
   425 
   426   fun nnf_quant vars qs p ct =
   427     Z3_Proof_Tools.as_meta_eq ct
   428     |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
   429 
   430   fun prove_nnf ctxt = try_apply ctxt [] [
   431     named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
   432     Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
   433       named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
   434 in
   435 fun nnf ctxt vars ps ct =
   436   (case SMT_Utils.term_of ct of
   437     _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
   438       if l aconv r
   439       then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
   440       else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
   441   | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
   442       MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
   443   | _ =>
   444       let
   445         val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
   446           (Z3_Proof_Tools.unfold_eqs ctxt
   447             (map (Thm.symmetric o meta_eq_of) ps)))
   448       in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
   449 end
   450 
   451 
   452 
   453 (** equality proof rules **)
   454 
   455 (* |- t = t *)
   456 fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
   457 
   458 
   459 (* s = t ==> t = s *)
   460 local
   461   val symm_rule = @{lemma "s = t ==> t == s" by simp}
   462 in
   463 fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
   464   | symm p = MetaEq (thm_of p COMP symm_rule)
   465 end
   466 
   467 
   468 (* s = t ==> t = u ==> s = u *)
   469 local
   470   val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
   471   val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
   472   val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
   473 in
   474 fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
   475   | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
   476   | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
   477   | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
   478 end
   479 
   480 
   481 (* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
   482    (reflexive antecendents are droppped) *)
   483 local
   484   exception MONO
   485 
   486   fun prove_refl (ct, _) = Thm.reflexive ct
   487   fun prove_comb f g cp =
   488     let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
   489     in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
   490   fun prove_arg f = prove_comb prove_refl f
   491 
   492   fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
   493 
   494   fun prove_nary is_comb f =
   495     let
   496       fun prove (cp as (ct, _)) = f cp handle MONO =>
   497         if is_comb (Thm.term_of ct)
   498         then prove_comb (prove_arg prove) prove cp
   499         else prove_refl cp
   500     in prove end
   501 
   502   fun prove_list f n cp =
   503     if n = 0 then prove_refl cp
   504     else prove_comb (prove_arg f) (prove_list f (n-1)) cp
   505 
   506   fun with_length f (cp as (cl, _)) =
   507     f (length (HOLogic.dest_list (Thm.term_of cl))) cp
   508 
   509   fun prove_distinct f = prove_arg (with_length (prove_list f))
   510 
   511   fun prove_eq exn lookup cp =
   512     (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
   513       SOME eq => eq
   514     | NONE => if exn then raise MONO else prove_refl cp)
   515   
   516   val prove_exn = prove_eq true
   517   and prove_safe = prove_eq false
   518 
   519   fun mono f (cp as (cl, _)) =
   520     (case Term.head_of (Thm.term_of cl) of
   521       @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
   522     | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
   523     | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
   524     | _ => prove (prove_safe f)) cp
   525 in
   526 fun monotonicity eqs ct =
   527   let
   528     fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
   529     val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
   530     val lookup = AList.lookup (op aconv) teqs
   531     val cp = Thm.dest_binop (Thm.dest_arg ct)
   532   in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
   533 end
   534 
   535 
   536 (* |- f a b = f b a (where f is equality) *)
   537 local
   538   val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
   539 in
   540 fun commutativity ct =
   541   MetaEq (Z3_Proof_Tools.match_instantiate I
   542     (Z3_Proof_Tools.as_meta_eq ct) rule)
   543 end
   544 
   545 
   546 
   547 (** quantifier proof rules **)
   548 
   549 (* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
   550    P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
   551 local
   552   val rules = [
   553     @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
   554     @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
   555 in
   556 fun quant_intro vars p ct =
   557   let
   558     val thm = meta_eq_of p
   559     val rules' = Z3_Proof_Tools.varify vars thm :: rules
   560     val cu = Z3_Proof_Tools.as_meta_eq ct
   561     val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
   562   in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
   563 end
   564 
   565 
   566 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
   567 fun pull_quant ctxt = Thm o try_apply ctxt [] [
   568   named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   569     (* FIXME: not very well tested *)
   570 
   571 
   572 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
   573 fun push_quant ctxt = Thm o try_apply ctxt [] [
   574   named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   575     (* FIXME: not very well tested *)
   576 
   577 
   578 (* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
   579 local
   580   val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
   581   val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
   582 
   583   fun elim_unused_tac i st = (
   584     Tactic.match_tac [@{thm refl}]
   585     ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
   586     ORELSE' (
   587       Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
   588       THEN' elim_unused_tac)) i st
   589 in
   590 
   591 val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
   592 
   593 end
   594 
   595 
   596 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
   597 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
   598   named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
   599     (* FIXME: not very well tested *)
   600 
   601 
   602 (* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
   603 local
   604   val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
   605 in
   606 val quant_inst = Thm o Z3_Proof_Tools.by_tac (
   607   REPEAT_ALL_NEW (Tactic.match_tac [rule])
   608   THEN' Tactic.rtac @{thm excluded_middle})
   609 end
   610 
   611 
   612 (* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
   613 local
   614   val forall =
   615     SMT_Utils.mk_const_pat @{theory} @{const_name all}
   616       (SMT_Utils.destT1 o SMT_Utils.destT1)
   617   fun mk_forall cv ct =
   618     Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
   619 
   620   fun get_vars f mk pred ctxt t =
   621     Term.fold_aterms f t []
   622     |> map_filter (fn v =>
   623          if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE)
   624 
   625   fun close vars f ct ctxt =
   626     let
   627       val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)
   628       val vs = frees_of ctxt (Thm.term_of ct)
   629       val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
   630       val vars_of = get_vars Term.add_vars Var (K true) ctxt'
   631     in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
   632 
   633   val sk_rules = @{lemma
   634     "c = (SOME x. P x) ==> (EX x. P x) = P c"
   635     "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
   636     by (metis someI_ex)+}
   637 in
   638 
   639 fun skolemize vars =
   640   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
   641 
   642 fun discharge_sk_tac i st = (
   643   Tactic.rtac @{thm trans} i
   644   THEN Tactic.resolve_tac sk_rules i
   645   THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
   646   THEN Tactic.rtac @{thm refl} i) st
   647 
   648 end
   649 
   650 
   651 
   652 (** theory proof rules **)
   653 
   654 (* theory lemmas: linear arithmetic, arrays *)
   655 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
   656   Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
   657     Z3_Proof_Tools.by_tac (
   658       NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
   659       ORELSE' NAMED ctxt' "simp+arith" (
   660         Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
   661         THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
   662 
   663 
   664 (* rewriting: prove equalities:
   665      * ACI of conjunction/disjunction
   666      * contradiction, excluded middle
   667      * logical rewriting rules (for negation, implication, equivalence,
   668          distinct)
   669      * normal forms for polynoms (integer/real arithmetic)
   670      * quantifier elimination over linear arithmetic
   671      * ... ? **)
   672 structure Z3_Simps = Named_Thms
   673 (
   674   val name = @{binding z3_simp}
   675   val description = "simplification rules for Z3 proof reconstruction"
   676 )
   677 
   678 local
   679   fun spec_meta_eq_of thm =
   680     (case try (fn th => th RS @{thm spec}) thm of
   681       SOME thm' => spec_meta_eq_of thm'
   682     | NONE => mk_meta_eq thm)
   683 
   684   fun prep (Thm thm) = spec_meta_eq_of thm
   685     | prep (MetaEq thm) = thm
   686     | prep (Literals (thm, _)) = spec_meta_eq_of thm
   687 
   688   fun unfold_conv ctxt ths =
   689     Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
   690       (map prep ths)))
   691 
   692   fun with_conv _ [] prv = prv
   693     | with_conv ctxt ths prv =
   694         Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
   695 
   696   val unfold_conv =
   697     Conv.arg_conv (Conv.binop_conv
   698       (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
   699   val prove_conj_disj_eq =
   700     Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
   701 
   702   fun declare_hyps ctxt thm =
   703     (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
   704 in
   705 
   706 val abstraction_depth = 3
   707   (*
   708     This value was chosen large enough to potentially catch exceptions,
   709     yet small enough to not cause too much harm.  The value might be
   710     increased in the future, if reconstructing 'rewrite' fails on problems
   711     that get too much abstracted to be reconstructable.
   712   *)
   713 
   714 fun rewrite simpset ths ct ctxt =
   715   apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
   716     named ctxt "conj/disj/distinct" prove_conj_disj_eq,
   717     named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
   718     Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
   719       Z3_Proof_Tools.by_tac (
   720         NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   721         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
   722     Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
   723       Z3_Proof_Tools.by_tac (
   724         (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   725         THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   726         THEN_ALL_NEW (
   727           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
   728           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
   729     Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
   730       Z3_Proof_Tools.by_tac (
   731         (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   732         THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   733         THEN_ALL_NEW (
   734           NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
   735           ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
   736     named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),
   737     Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
   738       (fn ctxt' =>
   739         Z3_Proof_Tools.by_tac (
   740           (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
   741           THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
   742           THEN_ALL_NEW (
   743             NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
   744             ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
   745               ctxt'))))]) ct))
   746 
   747 end
   748 
   749 
   750 
   751 (* proof reconstruction *)
   752 
   753 (** tracing and checking **)
   754 
   755 fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
   756   "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)
   757 
   758 fun check_after idx r ps ct (p, (ctxt, _)) =
   759   if not (Config.get ctxt SMT_Config.trace) then ()
   760   else
   761     let val thm = thm_of p |> tap (Thm.join_proofs o single)
   762     in
   763       if (Thm.cprop_of thm) aconvc ct then ()
   764       else
   765         z3_exn (Pretty.string_of (Pretty.big_list
   766           ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
   767             " (#" ^ string_of_int idx ^ ")")
   768           (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
   769             [Pretty.block [Pretty.str "expected: ",
   770               Syntax.pretty_term ctxt (Thm.term_of ct)]])))
   771     end
   772 
   773 
   774 (** overall reconstruction procedure **)
   775 
   776 local
   777   fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
   778     quote (Z3_Proof_Parser.string_of_rule r))
   779 
   780   fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
   781     (case (r, ps) of
   782       (* core rules *)
   783       (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
   784     | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
   785     | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
   786     | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
   787         (mp q (thm_of p), cxp)
   788     | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
   789         (mp q (thm_of p), cxp)
   790     | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
   791         and_elim (p, i) ct ptab ||> pair cx
   792     | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
   793         not_or_elim (p, i) ct ptab ||> pair cx
   794     | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
   795     | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
   796     | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
   797         (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
   798     | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
   799     | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
   800     | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
   801     | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
   802     | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
   803     | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
   804     | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
   805     | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
   806     | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
   807 
   808       (* equality rules *)
   809     | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
   810     | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
   811     | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
   812     | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
   813     | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
   814 
   815       (* quantifier rules *)
   816     | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
   817     | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
   818     | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
   819     | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
   820     | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
   821     | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
   822     | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
   823 
   824       (* theory rules *)
   825     | (Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
   826         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
   827     | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
   828     | (Z3_Proof_Parser.Rewrite_Star, ps) =>
   829         rewrite simpset (map fst ps) ct cx ||> rpair ptab
   830 
   831     | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
   832     | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
   833     | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
   834     | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
   835 
   836     | _ => raise Fail ("Z3: proof rule " ^
   837         quote (Z3_Proof_Parser.string_of_rule r) ^
   838         " has an unexpected number of arguments."))
   839 
   840   fun lookup_proof ptab idx =
   841     (case Inttab.lookup ptab idx of
   842       SOME p => (p, idx)
   843     | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
   844 
   845   fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
   846     let
   847       val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
   848       val ps = map (lookup_proof ptab) prems
   849       val _ = trace_before ctxt idx r
   850       val (thm, (ctxt', ptab')) =
   851         cxp
   852         |> prove_step simpset vars r ps prop
   853         |> tap (check_after idx r ps prop)
   854     in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
   855 
   856   fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
   857     @{thm reflexive}, Z3_Proof_Literals.true_thm]
   858 
   859   fun discharge_assms_tac rules =
   860     REPEAT (HEADGOAL (
   861       Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
   862     
   863   fun discharge_assms rules thm =
   864     if Thm.nprems_of thm = 0 then Goal.norm_result thm
   865     else
   866       (case Seq.pull (discharge_assms_tac rules thm) of
   867         SOME (thm', _) => Goal.norm_result thm'
   868       | NONE => raise THM ("failed to discharge premise", 1, [thm]))
   869 
   870   fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
   871     thm_of p
   872     |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
   873     |> discharge_assms (make_discharge_rules rules)
   874 in
   875 
   876 fun reconstruct outer_ctxt recon output =
   877   let
   878     val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
   879     val (asserted, steps, vars, ctxt1) =
   880       Z3_Proof_Parser.parse ctxt typs terms output
   881 
   882     val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
   883 
   884     val ((is, rules), cxp as (ctxt2, _)) =
   885       add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
   886   in
   887     if Config.get ctxt2 SMT_Config.filter_only_facts then (is, @{thm TrueI})
   888     else
   889       (Thm @{thm TrueI}, cxp)
   890       |> fold (prove simpset vars) steps 
   891       |> discharge rules outer_ctxt
   892       |> pair []
   893   end
   894 
   895 end
   896 
   897 val setup = z3_rules_setup #> Z3_Simps.setup
   898 
   899 end