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