src/HOL/Tools/SMT/z3_proof_reconstruction.ML

clarified example settings for Proof General;

(*  Title:      HOL/Tools/SMT/z3_proof_reconstruction.ML
    Author:     Sascha Boehme, TU Muenchen

Proof reconstruction for proofs found by Z3.
*)

signature Z3_PROOF_RECONSTRUCTION =
sig
  val add_z3_rule: thm -> Context.generic -> Context.generic
  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
    int list * thm
  val setup: theory -> theory
end

structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
struct


fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
  ("Z3 proof reconstruction: " ^ msg))



(* net of schematic rules *)

val z3_ruleN = "z3_rule"

local
  val description = "declaration of Z3 proof rules"

  val eq = Thm.eq_thm

  structure Z3_Rules = Generic_Data
  (
    type T = thm Net.net
    val empty = Net.empty
    val extend = I
    val merge = Net.merge eq
  )

  val prep =
    `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]

  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net

  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
  val del = Thm.declaration_attribute (Z3_Rules.map o del)
in

val add_z3_rule = Z3_Rules.map o ins

fun by_schematic_rule ctxt ct =
  the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)

val z3_rules_setup =
  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)

end



(* proof tools *)

fun named ctxt name prover ct =
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
  in prover ct end

fun NAMED ctxt name tac i st =
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
  in tac i st end

fun pretty_goal ctxt thms t =
  [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
  |> not (null thms) ? cons (Pretty.big_list "assumptions:"
       (map (Display.pretty_thm ctxt) thms))

fun try_apply ctxt thms =
  let
    fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
      Pretty.big_list ("Z3 found a proof," ^
        " but proof reconstruction failed at the following subgoal:")
        (pretty_goal ctxt thms (Thm.term_of ct)),
      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
        " might solve this problem.")])

    fun apply [] ct = error (try_apply_err ct)
      | apply (prover :: provers) ct =
          (case try prover ct of
            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
          | NONE => apply provers ct)

  in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end

local
  val rewr_if =
    @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
in
val simp_fast_tac =
  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
  THEN_ALL_NEW Classical.fast_tac HOL_cs
end



(* theorems and proofs *)

(** theorem incarnations **)

datatype theorem =
  Thm of thm | (* theorem without special features *)
  MetaEq of thm | (* meta equality "t == s" *)
  Literals of thm * Z3_Proof_Literals.littab
    (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)

fun thm_of (Thm thm) = thm
  | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
  | thm_of (Literals (thm, _)) = thm

fun meta_eq_of (MetaEq thm) = thm
  | meta_eq_of p = mk_meta_eq (thm_of p)

fun literals_of (Literals (_, lits)) = lits
  | literals_of p = Z3_Proof_Literals.make_littab [thm_of p]



(** core proof rules **)

(* assumption *)

local
  val remove_trigger = mk_meta_eq @{thm SMT.trigger_def}
  val remove_weight = mk_meta_eq @{thm SMT.weight_def}
  val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}

  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)

  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
    remove_fun_app, Z3_Proof_Literals.rewrite_true]

  fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)

  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)

  fun lookup_assm assms_net ct =
    Z3_Proof_Tools.net_instance' burrow_snd_option assms_net ct
    |> Option.map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
in

fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
  let
    val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules
    val eqs' = union Thm.eq_thm eqs prep_rules

    val assms_net =
      assms
      |> map (apsnd (rewrite ctxt eqs'))
      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
      |> Z3_Proof_Tools.thm_net_of snd 

    fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion

    fun assume thm ctxt =
      let
        val ct = Thm.cprem_of thm 1
        val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
      in (Thm.implies_elim thm thm', ctxt') end

    fun add (idx, ct) ((is, thms), (ctxt, ptab)) =
      let
        val thm1 = 
          Thm.trivial ct
          |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
        val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
      in
        (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
          NONE =>
            let val (thm, ctxt') = assume thm1 ctxt
            in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
        | SOME ((i, th), exact) =>
            let
              val (thm, ctxt') =
                if exact then (Thm.implies_elim thm1 th, ctxt)
                else assume thm1 ctxt
              val thms' = if exact then thms else th :: thms
            in 
              ((insert (op =) i is, thms'),
                (ctxt', Inttab.update (idx, Thm thm) ptab))
            end)
      end
  in fold add asserted (([], []), (ctxt, Inttab.empty)) end

end


(* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
local
  val precomp = Z3_Proof_Tools.precompose2
  val comp = Z3_Proof_Tools.compose

  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
  val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1

  val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
  val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
in
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
  | mp p_q p = 
      let
        val pq = thm_of p_q
        val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
      in Thm (Thm.implies_elim thm p) end
end


(* and_elim:     P1 & ... & Pn ==> Pi *)
(* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
local
  fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)

  fun derive conj t lits idx ptab =
    let
      val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
      val ls = Z3_Proof_Literals.explode conj false false [t] lit
      val lits' = fold Z3_Proof_Literals.insert_lit ls
        (Z3_Proof_Literals.delete_lit lit lits)

      fun upd thm = Literals (thm_of thm, lits')
      val ptab' = Inttab.map_entry idx upd ptab
    in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end

  fun lit_elim conj (p, idx) ct ptab =
    let val lits = literals_of p
    in
      (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
        SOME lit => (Thm lit, ptab)
      | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
    end
in
val and_elim = lit_elim true
val not_or_elim = lit_elim false
end


(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
local
  fun step lit thm =
    Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
  val explode_disj = Z3_Proof_Literals.explode false false false
  fun intro hyps thm th = fold step (explode_disj hyps th) thm

  fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
  val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
in
fun lemma thm ct =
  let
    val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
    val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
  in Thm (Z3_Proof_Tools.compose ccontr th) end
end


(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
local
  val explode_disj = Z3_Proof_Literals.explode false true false
  val join_disj = Z3_Proof_Literals.join false
  fun unit thm thms th =
    let
      val t = @{const Not} $ SMT_Utils.prop_of thm
      val ts = map SMT_Utils.prop_of thms
    in
      join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
    end

  fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
  val contrapos =
    Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
in
fun unit_resolution thm thms ct =
  Z3_Proof_Literals.negate (Thm.dest_arg ct)
  |> Z3_Proof_Tools.under_assumption (unit thm thms)
  |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
end


(* P ==> P == True   or   P ==> P == False *)
local
  val iff1 = @{lemma "P ==> P == (~ False)" by simp}
  val iff2 = @{lemma "~P ==> P == False" by simp}
in
fun iff_true thm = MetaEq (thm COMP iff1)
fun iff_false thm = MetaEq (thm COMP iff2)
end


(* distributivity of | over & *)
fun distributivity ctxt = Thm o try_apply ctxt [] [
  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
    (* FIXME: not very well tested *)


(* Tseitin-like axioms *)
local
  val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
  val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
  val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
  val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}

  fun prove' conj1 conj2 ct2 thm =
    let
      val littab =
        Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
        |> cons Z3_Proof_Literals.true_thm
        |> Z3_Proof_Literals.make_littab
    in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end

  fun prove rule (ct1, conj1) (ct2, conj2) =
    Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule

  fun prove_def_axiom ct =
    let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
    in
      (case Thm.term_of ct1 of
        @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
          prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
      | @{const HOL.conj} $ _ $ _ =>
          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
      | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
      | @{const HOL.disj} $ _ $ _ =>
          prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
      | Const (@{const_name distinct}, _) $ _ =>
          let
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
            fun prv cu =
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
              in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
      | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
          let
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
            fun prv cu =
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
              in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
      | _ => raise CTERM ("prove_def_axiom", [ct]))
    end
in
fun def_axiom ctxt = Thm o try_apply ctxt [] [
  named ctxt "conj/disj/distinct" prove_def_axiom,
  Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
end


(* local definitions *)
local
  val intro_rules = [
    @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
    @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
      by simp},
    @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]

  val apply_rules = [
    @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
    @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
      by (atomize(full)) fastsimp} ]

  val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg

  fun apply_rule ct =
    (case get_first (try (inst_rule ct)) intro_rules of
      SOME thm => thm
    | NONE => raise CTERM ("intro_def", [ct]))
in
fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm

fun apply_def thm =
  get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
  |> the_default (Thm thm)
end


(* negation normal form *)
local
  val quant_rules1 = ([
    @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
    @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
    @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
    @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])

  val quant_rules2 = ([
    @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
    @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
    @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
    @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])

  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
    Tactic.rtac thm ORELSE'
    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st

  fun nnf_quant_tac_varified vars eq =
    nnf_quant_tac (Z3_Proof_Tools.varify vars eq)

  fun nnf_quant vars qs p ct =
    Z3_Proof_Tools.as_meta_eq ct
    |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)

  fun prove_nnf ctxt = try_apply ctxt [] [
    named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
in
fun nnf ctxt vars ps ct =
  (case SMT_Utils.term_of ct of
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
      if l aconv r
      then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
      else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
  | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
  | _ =>
      let
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
          (Z3_Proof_Tools.unfold_eqs ctxt
            (map (Thm.symmetric o meta_eq_of) ps)))
      in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
end



(** equality proof rules **)

(* |- t = t *)
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))


(* s = t ==> t = s *)
local
  val symm_rule = @{lemma "s = t ==> t == s" by simp}
in
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
  | symm p = MetaEq (thm_of p COMP symm_rule)
end


(* s = t ==> t = u ==> s = u *)
local
  val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
  val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
  val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
in
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
  | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
  | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
end


(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
   (reflexive antecendents are droppped) *)
local
  exception MONO

  fun prove_refl (ct, _) = Thm.reflexive ct
  fun prove_comb f g cp =
    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
    in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
  fun prove_arg f = prove_comb prove_refl f

  fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp

  fun prove_nary is_comb f =
    let
      fun prove (cp as (ct, _)) = f cp handle MONO =>
        if is_comb (Thm.term_of ct)
        then prove_comb (prove_arg prove) prove cp
        else prove_refl cp
    in prove end

  fun prove_list f n cp =
    if n = 0 then prove_refl cp
    else prove_comb (prove_arg f) (prove_list f (n-1)) cp

  fun with_length f (cp as (cl, _)) =
    f (length (HOLogic.dest_list (Thm.term_of cl))) cp

  fun prove_distinct f = prove_arg (with_length (prove_list f))

  fun prove_eq exn lookup cp =
    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
      SOME eq => eq
    | NONE => if exn then raise MONO else prove_refl cp)
  
  val prove_exn = prove_eq true
  and prove_safe = prove_eq false

  fun mono f (cp as (cl, _)) =
    (case Term.head_of (Thm.term_of cl) of
      @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
    | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
    | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
    | _ => prove (prove_safe f)) cp
in
fun monotonicity eqs ct =
  let
    fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
    val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
    val lookup = AList.lookup (op aconv) teqs
    val cp = Thm.dest_binop (Thm.dest_arg ct)
  in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
end


(* |- f a b = f b a (where f is equality) *)
local
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
in
fun commutativity ct =
  MetaEq (Z3_Proof_Tools.match_instantiate I
    (Z3_Proof_Tools.as_meta_eq ct) rule)
end



(** quantifier proof rules **)

(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
   P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
local
  val rules = [
    @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
    @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
in
fun quant_intro vars p ct =
  let
    val thm = meta_eq_of p
    val rules' = Z3_Proof_Tools.varify vars thm :: rules
    val cu = Z3_Proof_Tools.as_meta_eq ct
    val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
  in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
end


(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
fun pull_quant ctxt = Thm o try_apply ctxt [] [
  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
    (* FIXME: not very well tested *)


(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
fun push_quant ctxt = Thm o try_apply ctxt [] [
  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
    (* FIXME: not very well tested *)


(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
local
  val elim_all = @{lemma "(ALL x. P) == P" by simp}
  val elim_ex = @{lemma "(EX x. P) == P" by simp}

  fun elim_unused_conv ctxt =
    Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt

  fun elim_unused_tac ctxt =
    REPEAT_ALL_NEW (
      Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
      ORELSE' CONVERSION (elim_unused_conv ctxt))
in
fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
end


(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
    (* FIXME: not very well tested *)


(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
local
  val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
in
val quant_inst = Thm o Z3_Proof_Tools.by_tac (
  REPEAT_ALL_NEW (Tactic.match_tac [rule])
  THEN' Tactic.rtac @{thm excluded_middle})
end


(* c = SOME x. P x |- (EX x. P x) = P c
   c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
local
  val elim_ex = @{lemma "EX x. P == P" by simp}
  val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
  val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
    by simp (intro eq_reflection some_eq_ex[symmetric])}
  val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
    by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
  val sk_ex_rule = ((sk_ex, I), elim_ex)
  and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)

  fun dest f sk_rule = 
    Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
  fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
  fun pair2 (a, b) (c, d) = [(a, c), (b, d)]
  fun inst_sk (sk_rule, f) p c =
    Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
    |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk')
    |> Conv.fconv_rule (Thm.beta_conversion true)

  fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
    | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
        (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate)
    | kind t = raise TERM ("skolemize", [t])

  fun dest_abs_type (Abs (_, T, _)) = T
    | dest_abs_type t = raise TERM ("dest_abs_type", [t])

  fun bodies_of thy lhs rhs =
    let
      val (rule, dest, make) = kind (Thm.term_of lhs)

      fun dest_body idx cbs ct =
        let
          val cb = Thm.dest_arg (dest ct)
          val T = dest_abs_type (Thm.term_of cb)
          val cv = Thm.cterm_of thy (Var (("x", idx), T))
          val cu = make (Drule.beta_conv cb cv)
          val cbs' = (cv, cb) :: cbs
        in
          (snd (Thm.first_order_match (cu, rhs)), rev cbs')
          handle Pattern.MATCH => dest_body (idx+1) cbs' cu
        end
    in (rule, dest_body 1 [] lhs) end

  fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))

  fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) =
    (case mct of
      SOME ct =>
        ctxt
        |> Z3_Proof_Tools.make_hyp_def
             (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
        |>> pair ((cv, ct) :: is) o Thm.transitive thm
    | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
in
fun skolemize ct ctxt =
  let
    val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct)
    val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs
    fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
  in
    (([], Thm.reflexive lhs), ctxt)
    |> fold (sk_step rule) (map lookup_var cbs)
    |>> MetaEq o snd
  end
end


(** theory proof rules **)

(* theory lemmas: linear arithmetic, arrays *)
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
  Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' =>
    Z3_Proof_Tools.by_tac (
      NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
      ORELSE' NAMED ctxt' "simp+arith" (
        Simplifier.simp_tac simpset
        THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]


(* rewriting: prove equalities:
     * ACI of conjunction/disjunction
     * contradiction, excluded middle
     * logical rewriting rules (for negation, implication, equivalence,
         distinct)
     * normal forms for polynoms (integer/real arithmetic)
     * quantifier elimination over linear arithmetic
     * ... ? **)
structure Z3_Simps = Named_Thms
(
  val name = "z3_simp"
  val description = "simplification rules for Z3 proof reconstruction"
)

local
  fun spec_meta_eq_of thm =
    (case try (fn th => th RS @{thm spec}) thm of
      SOME thm' => spec_meta_eq_of thm'
    | NONE => mk_meta_eq thm)

  fun prep (Thm thm) = spec_meta_eq_of thm
    | prep (MetaEq thm) = thm
    | prep (Literals (thm, _)) = spec_meta_eq_of thm

  fun unfold_conv ctxt ths =
    Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
      (map prep ths)))

  fun with_conv _ [] prv = prv
    | with_conv ctxt ths prv =
        Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv

  val unfold_conv =
    Conv.arg_conv (Conv.binop_conv
      (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
  val prove_conj_disj_eq =
    Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq

  fun assume_prems ctxt thm =
    Assumption.add_assumes (Drule.cprems_of thm) ctxt
    |>> (fn thms => fold Thm.elim_implies thms thm)
in

fun rewrite simpset ths ct ctxt =
  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
      Z3_Proof_Tools.by_tac (
        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
        THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
    Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
      Z3_Proof_Tools.by_tac (
        NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
        THEN_ALL_NEW (
          NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
          ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
      Z3_Proof_Tools.by_tac (
        NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
        THEN_ALL_NEW (
          NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
          ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))

end



(* proof reconstruction *)

(** tracing and checking **)

fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
  "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)

fun check_after idx r ps ct (p, (ctxt, _)) =
  if not (Config.get ctxt SMT_Config.trace) then ()
  else
    let val thm = thm_of p |> tap (Thm.join_proofs o single)
    in
      if (Thm.cprop_of thm) aconvc ct then ()
      else
        z3_exn (Pretty.string_of (Pretty.big_list
          ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
            " (#" ^ string_of_int idx ^ ")")
          (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
            [Pretty.block [Pretty.str "expected: ",
              Syntax.pretty_term ctxt (Thm.term_of ct)]])))
    end


(** overall reconstruction procedure **)

local
  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
    quote (Z3_Proof_Parser.string_of_rule r))

  fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
    (case (r, ps) of
      (* core rules *)
      (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
    | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
    | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
    | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
        (mp q (thm_of p), cxp)
    | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
        (mp q (thm_of p), cxp)
    | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
        and_elim (p, i) ct ptab ||> pair cx
    | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
        not_or_elim (p, i) ct ptab ||> pair cx
    | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
    | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
    | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
    | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
    | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
    | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
    | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
    | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
    | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
    | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
    | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
    | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)

      (* equality rules *)
    | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
    | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
    | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
    | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
    | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)

      (* quantifier rules *)
    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
    | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
    | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
    | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
    | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab

      (* theory rules *)
    | (Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
    | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
    | (Z3_Proof_Parser.Rewrite_Star, ps) =>
        rewrite simpset (map fst ps) ct cx ||> rpair ptab

    | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
    | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
    | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
    | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r

    | _ => raise Fail ("Z3: proof rule " ^
        quote (Z3_Proof_Parser.string_of_rule r) ^
        " has an unexpected number of arguments."))

  fun lookup_proof ptab idx =
    (case Inttab.lookup ptab idx of
      SOME p => (p, idx)
    | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))

  fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
    let
      val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
      val ps = map (lookup_proof ptab) prems
      val _ = trace_before ctxt idx r
      val (thm, (ctxt', ptab')) =
        cxp
        |> prove_step simpset vars r ps prop
        |> tap (check_after idx r ps prop)
    in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end

  val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive},
    Z3_Proof_Literals.true_thm]
  fun all_disch_rules rules = map (pair false) (disch_rules @ rules)

  fun disch_assm rules thm =
    if Thm.nprems_of thm = 0 then Drule.flexflex_unique thm
    else
      (case Seq.pull (Thm.biresolution false rules 1 thm) of
        SOME (thm', _) => disch_assm rules thm'
      | NONE => raise THM ("failed to discharge premise", 1, [thm]))

  fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
    thm_of p
    |> singleton (ProofContext.export inner_ctxt outer_ctxt)
    |> disch_assm rules
in

fun reconstruct outer_ctxt recon output =
  let
    val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
    val (asserted, steps, vars, ctxt1) =
      Z3_Proof_Parser.parse ctxt typs terms output

    val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)

    val ((is, rules), cxp as (ctxt2, _)) =
      add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
  in
    if Config.get ctxt2 SMT_Config.filter_only_facts then (is, @{thm TrueI})
    else
      (Thm @{thm TrueI}, cxp)
      |> fold (prove simpset vars) steps 
      |> discharge (all_disch_rules rules) outer_ctxt
      |> pair []
  end

end

val setup = z3_rules_setup #> Z3_Simps.setup

end