(*  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)

    fun schematic_label full = "schematic rules" |> full ? suffix " (full)"

    fun schematic ctxt full ct =

      ct

      |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms

      |> named ctxt (schematic_label full) (by_schematic_rule ctxt)

      |> fold Thm.elim_implies thms

  in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end

local

  val rewr_if =

    @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}

in

fun HOL_fast_tac ctxt =

  Classical.fast_tac (put_claset HOL_cs ctxt)

fun simp_fast_tac ctxt =

  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])

  THEN_ALL_NEW HOL_fast_tac ctxt

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 (HOL_fast_tac ctxt))]

    (* 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 0 (true, false) ctxt [] (fn ctxt' =>

    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]

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 0 (true, false) ctxt [] (fn ctxt' =>

      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]

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 (HOL_fast_tac ctxt))]

    (* 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 (HOL_fast_tac ctxt))]

    (* FIXME: not very well tested *)

(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)

local

  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}

  val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}

  fun elim_unused_tac i st = (

    Tactic.match_tac [@{thm refl}]

    ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)

    ORELSE' (

      Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]

      THEN' elim_unused_tac)) i st

in

val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac

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 (HOL_fast_tac ctxt))]

    (* 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

(* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)

local

  val forall =

    SMT_Utils.mk_const_pat @{theory} @{const_name all}

      (SMT_Utils.destT1 o SMT_Utils.destT1)

  fun mk_forall cv ct =

    Thm.capply (SMT_Utils.instT' cv forall) (Thm.cabs cv ct)

  fun get_vars f mk pred ctxt t =

    Term.fold_aterms f t []

    |> map_filter (fn v =>

         if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE)

  fun close vars f ct ctxt =

    let

      val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)

      val vs = frees_of ctxt (Thm.term_of ct)

      val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt

      val vars_of = get_vars Term.add_vars Var (K true) ctxt'

    in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end

  val sk_rules = @{lemma

    "(EX x. P x) = P (SOME x. P x)"   "(~(ALL x. P x)) = (~P (SOME x. ~P x))"

    by (metis someI_ex)+}

in

fun skolemize vars =

  apfst Thm oo close vars (yield_singleton Assumption.add_assumes)

fun discharge_sk_tac i st = (

  Tactic.rtac @{thm trans}

  THEN' Tactic.resolve_tac sk_rules

  THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st

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 0 (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 declare_hyps ctxt thm =

    (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))

in

val abstraction_depth = 3

  (*

    This value was chosen large enough to potentially catch exceptions,

    yet small enough to not cause too much harm.  The value might be

    increased in the future, if reconstructing 'rewrite' fails on problems

    that get too much abstracted to be reconstructable.

  *)

fun rewrite simpset ths ct ctxt =

  apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [

    named ctxt "conj/disj/distinct" prove_conj_disj_eq,

    Z3_Proof_Tools.by_abstraction 0 (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)" (fast_tac ctxt'))),

    Z3_Proof_Tools.by_abstraction 0 (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)" (HOL_fast_tac ctxt')

          ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),

    Z3_Proof_Tools.by_abstraction 0 (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)" (HOL_fast_tac ctxt')

          ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),

    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),

    Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []

      (fn ctxt' =>

        Z3_Proof_Tools.by_tac (

          NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)

          THEN_ALL_NEW (

            NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')

            ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac

              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 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 vars 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

  fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},

    @{thm reflexive}, Z3_Proof_Literals.true_thm]

  fun discharge_tac rules =

    Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac

  fun discharge_assms rules thm =

    if Thm.nprems_of thm = 0 then Goal.norm_result thm

    else

      (case Seq.pull (discharge_tac rules 1 thm) of

        SOME (thm', _) => discharge_assms rules thm'

      | NONE => raise THM ("failed to discharge premise", 1, [thm]))

  fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =

    thm_of p

    |> singleton (Proof_Context.export inner_ctxt outer_ctxt)

    |> discharge_assms (make_discharge_rules 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 rules outer_ctxt

      |> pair []

  end

end

val setup = z3_rules_setup #> Z3_Simps.setup

end