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