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