src/HOL/SMT/Tools/z3_proof_rules.ML

slightly more general simproc (avoids errors of linarith)

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

Z3 proof rules and their reconstruction.
*)

signature Z3_PROOF_RULES =
sig
  (*proof rule names*)
  type rule  
  val rule_of_string: string -> rule option
  val string_of_rule: rule -> string

  (*proof reconstruction*)
  type proof
  val make_proof: rule -> int list -> cterm * cterm list -> proof
  val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
    thm

  (*setup*)
  val trace_assms: bool Config.T
  val setup: theory -> theory
end

structure Z3_Proof_Rules: Z3_PROOF_RULES =
struct

structure T = Z3_Proof_Terms

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


(* proof rule names *)

datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
  Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
  Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
  PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
  Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
  DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
  CnfStar | Skolemize | ModusPonensOeq | ThLemma

val rule_names = Symtab.make [
  ("true-axiom", TrueAxiom),
  ("asserted", Asserted),
  ("goal", Goal),
  ("mp", ModusPonens),
  ("refl", Reflexivity),
  ("symm", Symmetry),
  ("trans", Transitivity),
  ("trans*", TransitivityStar),
  ("monotonicity", Monotonicity),
  ("quant-intro", QuantIntro),
  ("distributivity", Distributivity),
  ("and-elim", AndElim),
  ("not-or-elim", NotOrElim),
  ("rewrite", Rewrite),
  ("rewrite*", RewriteStar),
  ("pull-quant", PullQuant),
  ("pull-quant*", PullQuantStar),
  ("push-quant", PushQuant),
  ("elim-unused", ElimUnusedVars),
  ("der", DestEqRes),
  ("quant-inst", QuantInst),
  ("hypothesis", Hypothesis),
  ("lemma", Lemma),
  ("unit-resolution", UnitResolution),
  ("iff-true", IffTrue),
  ("iff-false", IffFalse),
  ("commutativity", Commutativity),
  ("def-axiom", DefAxiom),
  ("intro-def", IntroDef),
  ("apply-def", ApplyDef),
  ("iff~", IffOeq),
  ("nnf-pos", NnfPos),
  ("nnf-neg", NnfNeg),
  ("nnf*", NnfStar),
  ("cnf*", CnfStar),
  ("sk", Skolemize),
  ("mp~", ModusPonensOeq),
  ("th-lemma", ThLemma)]

val rule_of_string = Symtab.lookup rule_names
fun string_of_rule r =
  let fun fit (s, r') = if r = r' then SOME s else NONE 
  in the (Symtab.get_first fit rule_names) end


(* proof representation *)

datatype theorem =
  Thm of thm |
  MetaEq of thm |
  Literals of thm * thm Termtab.table

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)

datatype proof =
  Unproved of {
    rule: rule,
    subs: int list,
    prop: cterm,
    vars: cterm list } |
  Sequent of {
    hyps: cterm list,
    vars: cterm list,
    thm: theorem }

fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs}


(* proof reconstruction utilities *)

fun try_apply ctxt name nfs ct =
  let
    val trace = SMT_Solver.trace_msg ctxt I

    fun first [] = z3_exn (name ^ " failed")
      | first ((n, f) :: nfs) =
          (case try f ct of
            SOME thm => (trace (n ^ " succeeded"); thm)
          | NONE => (trace (n ^ " failed"); first nfs))
  in first nfs end

fun prop_of thm = (case Thm.prop_of thm of @{term Trueprop} $ t => t | t => t)

fun as_meta_eq ct = uncurry T.mk_meta_eq (Thm.dest_binop ct)

fun by_tac' tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
fun by_tac tac ct = by_tac' tac (T.mk_prop ct)

fun match_instantiate' f ct thm =
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
val match_instantiate = match_instantiate' I

local
  fun maybe_instantiate ct thm =
    try Thm.first_order_match (Thm.cprop_of thm, ct)
    |> Option.map (fn inst => Thm.instantiate inst thm)
in
fun thm_net_of thms =
  let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
  in fold insert thms Net.empty end

fun first_of thms ct = get_first (maybe_instantiate ct) thms
fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
end

fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
fun certify_var ctxt idx T = certify ctxt (Var (("x", idx), T))
fun certify_free ctxt idx T = certify ctxt (Free ("x" ^ string_of_int idx, T))

fun varify ctxt =
  let
    fun varify1 cv thm =
      let
        val T = Thm.typ_of (Thm.ctyp_of_term cv)
        val v = certify_var ctxt (Thm.maxidx_of thm + 1) T
       in SMT_Normalize.instantiate_free (cv, v) thm end
  in fold varify1 end

fun under_assumption f ct =
  let val ct' = T.mk_prop ct
  in Thm.implies_intr ct' (f (Thm.assume ct')) end

fun with_conv conv prove ct =
  let val eq = Thm.symmetric (conv ct)
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end

fun list2 (x, y) = [x, y]

fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)

fun discharge p pq = Thm.implies_elim pq p

fun compose (cvs, f, rule) thm =
  let fun inst thm = Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm))
  in discharge thm (inst thm rule) end

fun make_hyp_def thm = (* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
  let
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
    val (cf, cvs) = Drule.strip_comb lhs
    val eq = T.mk_meta_eq cf (fold_rev Thm.cabs cvs rhs)
    fun apply cv th =
      Thm.combination th (Thm.reflexive cv)
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
  in ([eq], Thm.implies_elim thm (fold apply cvs (Thm.assume eq))) end

val true_thm = @{lemma "~False" by simp}

val is_neg = (fn @{term Not} $ _ => true | _ => false)
fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)

(** explosion of conjunctions and disjunctions **)

local
  val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)

  val negate_term = (fn @{term Not} $ t => t | t => @{term Not} $ t)
  fun dest_disj_term' f = (fn
      @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
    | _ => NONE)
  val dest_disj_term = dest_disj_term' negate_term

  fun destc ct = list2 (Thm.dest_binop (Thm.dest_arg ct))
  val dest_conj1 = precompose destc @{thm conjunct1}
  val dest_conj2 = precompose destc @{thm conjunct2}
  fun dest_conj_rules t =
    dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
    
  fun destd f ct = list2 (f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct))))
  val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
  val dest_disj1 = precompose (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
  and dest_disj2 = precompose (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
  and dest_disj3 = precompose (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
  and dest_disj4 = precompose (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}

  fun dest_disj_rules t =
    (case dest_disj_term' is_neg t of
      SOME (true, true) => SOME (dest_disj2, dest_disj4)
    | SOME (true, false) => SOME (dest_disj2, dest_disj3)
    | SOME (false, true) => SOME (dest_disj1, dest_disj4)
    | SOME (false, false) => SOME (dest_disj1, dest_disj3)
    | NONE => NONE)

  val is_dneg = is_neg' is_neg
  fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
  val dneg_rule = precompose destn @{thm notnotD}
in
fun exists_lit is_conj P =
  let
    val dest = if is_conj then dest_conj_term else dest_disj_term
    fun exists t = P t orelse
      (case dest t of
        SOME (t1, t2) => exists t1 orelse exists t2
      | NONE => false)
  in exists end

fun explode_term is_conj keep_intermediate =
  let
    val dest = if is_conj then dest_conj_term else dest_disj_term
    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
    fun explode1 rules t =
      (case dest t of
        SOME (t1, t2) =>
          let val (rule1, rule2) = the (dest_rules t)
          in
            explode1 (rule1 :: rules) t1 #>
            explode1 (rule2 :: rules) t2 #>
            keep_intermediate ? cons (t, rev rules)
          end
      | NONE => cons (t, rev rules))
    fun explode0 (@{term Not} $ (@{term Not} $ t)) = [(t, [dneg_rule])]
      | explode0 t = explode1 [] t []
  in explode0 end

fun extract_lit thm rules = fold compose rules thm

fun explode_thm is_conj full keep_intermediate stop_lits =
  let
    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
    val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty

    fun explode1 thm =
      if Termtab.defined tab (prop_of thm) then cons thm
      else
        (case dest_rules (prop_of thm) of
          SOME (rule1, rule2) => explode2 rule1 thm #> explode2 rule2 thm #>
            keep_intermediate ? cons thm
        | NONE => cons thm)
    and explode2 dest_rule thm =
      if full orelse exists_lit is_conj (Termtab.defined tab) (prop_of thm)
      then explode1 (compose dest_rule thm)
      else cons (compose dest_rule thm)
    fun explode0 thm =
      if not is_conj andalso is_dneg (prop_of thm) then [compose dneg_rule thm]
      else explode1 thm []
  in explode0 end
end

(** joining of literals to conjunctions or disjunctions **)

local
  fun precomp2 f g thm =
    (f (Thm.cprem_of thm 1), g (Thm.cprem_of thm 2), f, g, thm)
  fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
    let val inst = [(cv1, f (Thm.cprop_of thm1)), (cv2, g (Thm.cprop_of thm2))]
    in Thm.instantiate ([], inst) rule |> discharge thm1 |> discharge thm2 end

  fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)

  val conj_rule = precomp2 d1 d1 @{thm conjI}
  fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2

  val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
  val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
  val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
  val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}

  fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
    | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
    | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
    | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2

  fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
    | dest_conj t = raise TERM ("dest_conj", [t])

  val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
  fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
    | dest_disj t = raise TERM ("dest_disj", [t])

  val dnegE = precompose (single o d2 o d1) @{thm notnotD}
  val dnegI = precompose (single o d1) @{lemma "P ==> ~~P" by fast}
  fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))

  fun dni f = list2 o apsnd f o Thm.dest_binop o f o d1
  val negIffE = precompose (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
  val negIffI = precompose (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
  val iff_const = @{term "op = :: bool => _"}
  fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
        f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
    | as_negIff _ _ = NONE
in
fun make_lit_tab thms = fold (Termtab.update o ` prop_of) thms Termtab.empty

fun join is_conj tab t =
  let
    val comp = if is_conj then comp_conj else comp_disj
    val dest = if is_conj then dest_conj else dest_disj

    val lookup_lit = Termtab.lookup tab
    fun lookup_lit' t =
      (case t of
        @{term Not} $ (@{term Not} $ t) => (compose dnegI, lookup_lit t)
      | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
          (compose negIffI, lookup_lit (iff_const $ u $ t))
      | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
          let fun rewr lit = lit COMP @{thm not_sym}
          in (rewr, lookup_lit (@{term Not} $ (eq $ u $ t))) end
      | _ =>
          (case as_dneg lookup_lit t of
            NONE => (compose negIffE, as_negIff lookup_lit t)
          | x => (compose dnegE, x)))
    fun join1 (s, t) =
      (case lookup_lit t of
        SOME lit => (s, lit)
      | NONE => 
          (case lookup_lit' t of
            (rewrite, SOME lit) => (s, rewrite lit)
          | (_, NONE) => (s, comp (pairself join1 (dest t)))))
  in snd (join1 (if is_conj then (false, t) else (true, t))) end
end

(** proving equality of conjunctions or disjunctions **)

fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})

local
  val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
  val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
  val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
  val neg = Thm.capply @{cterm Not}
in
fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
end

local
  fun prove_eq l r (cl, cr) =
    let
      fun explode is_conj = explode_thm is_conj true (l <> r) []
      fun make_tab is_conj thm = make_lit_tab (true_thm :: explode is_conj thm)
      fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)

      val thm1 = under_assumption (prove r cr o make_tab l) cl
      val thm2 = under_assumption (prove l cl o make_tab r) cr
    in iff_intro thm1 thm2 end

  datatype conj_disj = CONJ | DISJ | NCON | NDIS
  fun kind_of t =
    if is_conj t then SOME CONJ
    else if is_disj t then SOME DISJ
    else if is_neg' is_conj t then SOME NCON
    else if is_neg' is_disj t then SOME NDIS
    else NONE
in
fun prove_conj_disj_eq ct =
  let val cp = Thm.dest_binop ct
  in
    (case pairself (kind_of o Thm.term_of) cp of
      (SOME CONJ, SOME CONJ) => prove_eq true true cp
    | (SOME CONJ, SOME NDIS) => prove_eq true false cp
    | (SOME CONJ, NONE) => prove_eq true true cp
    | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
    | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
    | (SOME DISJ, NONE) => contrapos1 (prove_eq false false) cp
    | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
    | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
    | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
    | (SOME NDIS, SOME NDIS) => prove_eq false false cp
    | (SOME NDIS, SOME CONJ) => prove_eq false true cp
    | (SOME NDIS, NONE) => prove_eq false true cp
    | _ => raise CTERM ("prove_conj_disj_eq", [ct]))
  end
end

(** unfolding of distinct **)

local
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
  val set2 = @{lemma "x ~: set [x] == False" by simp}
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
  val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}

  fun set_conv ct =
    (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct

  val dist1 = @{lemma "distinct [] == ~False" by simp}
  val dist2 = @{lemma "distinct [x] == ~False" by simp}
  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
    by simp}

  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
fun unfold_distinct_conv ct =
  (More_Conv.rewrs_conv [dist1, dist2] else_conv
  (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
end

(** proving abstractions **)

fun fold_map_op f ct =
  let val (cf, cu) = Thm.dest_comb ct
  in f cu #>> Thm.capply cf end

fun fold_map_binop f1 f2 ct =
  let val ((cf, cu1), cu2) = apfst Thm.dest_comb (Thm.dest_comb ct)
  in f1 cu1 ##>> f2 cu2 #>> uncurry (Thm.mk_binop cf) end

fun abstraction_context ctxt = (ctxt, certify_var, 1, false, Ctermtab.empty)
fun abstraction_context' ctxt = (ctxt, certify_free, 1, true, Ctermtab.empty)

fun fresh_abstraction ct (cx as (ctxt, mk_var, idx, gen, tab)) =
  (case Ctermtab.lookup tab ct of
    SOME cv => (cv, cx)
  | NONE =>
      let val cv = mk_var ctxt idx (#T (Thm.rep_cterm ct))
      in (cv, (ctxt, mk_var, idx + 1, gen, Ctermtab.update (ct, cv) tab)) end)

fun prove_abstraction tac ct (_, _, _, gen, tab) =
  let
    val insts = map swap (Ctermtab.dest tab)
    val thm = Goal.prove_internal [] ct (fn _ => tac 1)
  in
    if gen
    then fold SMT_Normalize.instantiate_free insts thm
    else Thm.instantiate ([], insts) thm
  end


(* core proof rules *)

datatype assms = Some of thm list | Many of thm Net.net

val true_false = @{lemma "True == ~ False" by simp}

val (trace_assms, trace_assms_setup) =
  Attrib.config_bool "z3_trace_assms" false

local
  val TT_eq = @{lemma "(P = (~False)) == P" by simp}
  val remove_trigger = @{lemma "trigger t p == p"
    by (rule eq_reflection, rule trigger_def)}
  val remove_iff = @{lemma "p iff q == p = q"
    by (rule eq_reflection, rule iff_def)}

  fun with_context simpset ctxt = Simplifier.context ctxt simpset

  val prep_ss = with_context (Simplifier.empty_ss addsimps
    [@{thm Let_def}, remove_trigger, remove_iff, true_false, TT_eq])

  val TT_eq_conv = Conv.rewr_conv TT_eq
  val norm_conv = More_Conv.bottom_conv (K (Conv.try_conv TT_eq_conv))

  val threshold = 10
  
  fun trace ctxt thm =
    if Config.get ctxt trace_assms
    then tracing (Display.string_of_thm ctxt thm)
    else ()

  val lookup = (fn Some thms => first_of thms | Many net => net_instance net)
  fun lookup_assm ctxt assms ct =
    (case lookup assms ct of
      SOME thm => (trace ctxt thm; thm)
    | _ => z3_exn ("not asserted: " ^
        quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
in
fun prepare_assms ctxt assms =
  let
    val rewrite = Conv.fconv_rule (Simplifier.rewrite (prep_ss ctxt))
    val thms = map rewrite assms
  in if length assms < threshold then Some thms else Many (thm_net_of thms) end

fun asserted _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
  | asserted ctxt (SOME assms) ct =
      Thm (with_conv (norm_conv ctxt) (lookup_assm ctxt assms) (T.mk_prop ct))
end


(** P ==> P = Q ==> Q   or   P ==> P --> Q ==> Q **)
local
  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
  val meta_iffD1_c = precompose (list2 o Thm.dest_binop) meta_iffD1

  val iffD1_c = precompose (list2 o Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
  val mp_c = precompose (list2 o Thm.dest_binop o Thm.dest_arg) @{thm mp}
in
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (compose meta_iffD1_c thm) p)
  | mp p_q p = 
      let
        val pq = thm_of p_q
        val thm = compose iffD1_c pq handle THM _ => compose 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 get_lit conj t (l, thm) =
    let val is_sublit_of = exists_lit conj (fn u => u aconv t)
    in if is_sublit_of (prop_of thm) then SOME (l, thm) else NONE end

  fun derive conj t lits idx ptab =
    let
      val (l, lit) = the (Termtab.get_first (get_lit conj t) lits)
      val ls = explode_thm conj false false [t] lit
      val lits' = fold (Termtab.update o ` prop_of) ls (Termtab.delete l lits)
      fun upd (Sequent {hyps, vars, thm}) =
            Sequent {hyps=hyps, vars=vars, thm = Literals (thm_of thm, lits')}
        | upd p = p
    in (the (Termtab.lookup lits' t), Inttab.map_entry idx upd ptab) end

  val mk_tab = make_lit_tab o single
  val literals_of = (fn Literals (_, lits) => lits | p => mk_tab (thm_of p))
  fun lit_elim conj (p, idx) ct ptab =
    let val lits = literals_of p
    in
      (case Termtab.lookup lits (Thm.term_of ct) of
        SOME lit => (Thm lit, ptab)
      | NONE => apfst Thm (derive conj (Thm.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 = explode_thm 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 = precompose dest_ccontr @{thm ccontr}
in
fun lemma thm ct =
  let
    val cu = Thm.capply @{cterm Not} ct
    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
  in Thm (compose ccontr (under_assumption (intro hyps thm) cu)) end
end


(** \/{P1, ..., Pn, Q1, ..., Qn} & ~P1 & ... & ~Pn ==> \/{Q1, ..., Qn} **)
local
  val explode_disj = explode_thm false true false and join_disj = join false
  fun unit thm thms th =
    let val t = @{term Not} $ prop_of thm and ts = map prop_of thms
    in join_disj (make_lit_tab (thms @ explode_disj ts th)) t end

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


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 & **)
val distributivity = Thm o by_tac (Classical.fast_tac HOL_cs)


(** 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 tab =
      make_lit_tab (true_thm :: explode_thm conj1 true (conj1 <> conj2) [] thm)
    in join conj2 tab (Thm.term_of ct2) end

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

  fun prove_def_axiom ct =
    let val (ct1, ct2) = Thm.dest_binop ct
    in
      (case Thm.term_of ct1 of
        @{term Not} $ (@{term "op &"} $ _ $ _) =>
          prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
      | @{term "op &"} $ _ $ _ =>
          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
      | @{term Not} $ (@{term "op |"} $ _ $ _) =>
          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
      | @{term "op |"} $ _ $ _ =>
          prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
      | Const (@{const_name distinct}, _) $ _ =>
          let
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
            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 with_conv (dis_conv unfold_distinct_conv) prv (T.mk_prop ct) end
      | @{term Not} $ (Const (@{const_name distinct}, _) $ _) =>
          let
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
            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 with_conv (dis_conv unfold_distinct_conv) prv (T.mk_prop ct) end
      | _ => raise CTERM ("prove_def_axiom", [ct]))
    end

  val ifI = @{lemma "(P ==> Q1) ==> (~P ==> Q2) ==> if P then Q1 else Q2"
    by simp}
  val ifE = @{lemma
    "(if P then Q1 else Q2) ==> (P --> Q1 ==> ~P --> Q2 ==> R) ==> R" by simp}
  val claset = HOL_cs addIs [ifI] addEs [ifE]
in
fun def_axiom ctxt ct =
  Thm (try_apply ctxt "def_axiom" [
    ("conj/disj", prove_def_axiom),
    ("simp", by_tac (Simplifier.simp_tac HOL_ss)),
    ("fast", by_tac (Classical.fast_tac claset)),
    ("simp+fast", by_tac (Simplifier.simp_tac HOL_ss THEN_ALL_NEW
      Classical.fast_tac claset))] ct)
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 = match_instantiate' Thm.dest_arg

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

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


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 ctxt qs (p, (vars, _)) ct =
    as_meta_eq ct
    |> by_tac' (nnf_quant_tac (varify ctxt vars (meta_eq_of p)) qs)

  val nnf_rules = thm_net_of [@{thm not_not}]

  fun abstract ct =
    (case Thm.term_of ct of
      @{term False} => pair
    | @{term Not} $ _ => fold_map_op abstract
    | @{term "op &"} $ _ $ _ => fold_map_binop abstract abstract
    | @{term "op |"} $ _ $ _ => fold_map_binop abstract abstract
    | @{term "op -->"} $ _ $ _ => fold_map_binop abstract abstract
    | @{term "op = :: bool => _"} $ _ $ _ => fold_map_binop abstract abstract
    | _ => fresh_abstraction) ct

  fun abstracted ctxt ct =
    abstraction_context' ctxt
    |> abstract (Thm.dest_arg ct)
    |>> T.mk_prop
    |-> prove_abstraction (Classical.best_tac HOL_cs)

  fun prove_nnf ctxt =
    try_apply ctxt "nnf" [
      ("conj/disj", prove_conj_disj_eq o Thm.dest_arg),
      ("rule", the o net_instance nnf_rules),
      ("abstract", abstracted ctxt),
      ("tactic", by_tac' (Classical.best_tac HOL_cs))]
in
fun nnf ctxt ps ct =
  (case Thm.term_of ct of
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
      if l aconv r then MetaEq (Thm.reflexive (Thm.dest_arg ct))
      else MetaEq (nnf_quant ctxt quant_rules1 (hd ps) ct)
  | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
      MetaEq (nnf_quant ctxt quant_rules2 (hd ps) ct)
  | _ =>
      let
        val eqs = map (Thm.symmetric o meta_eq_of o fst) ps
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
          (More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt))
      in Thm (with_conv nnf_rewr_conv (prove_nnf ctxt) (T.mk_prop ct)) end)
end


(* equality proof rules *)

(** t = t **)
fun refl ct = MetaEq (Thm.reflexive (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 trans_rule = @{lemma "s = t ==> t = u ==> s == u" by simp}
in
fun trans (MetaEq thm) q = MetaEq (Thm.transitive thm (meta_eq_of q))
  | trans p (MetaEq thm) = MetaEq (Thm.transitive (meta_eq_of p) thm)
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans_rule))
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_eq_exn = prove_eq true and prove_eq_safe = prove_eq false

  fun mono f (cp as (cl, _)) =
    (case Term.head_of (Thm.term_of cl) of
      @{term "op &"} => prove_nary is_conj (prove_eq_exn f)
    | @{term "op |"} => prove_nary is_disj (prove_eq_exn f)
    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
    | _ => prove (prove_eq_safe f)) cp
in
fun monotonicity eqs ct =
  let
    val tab = map (` Thm.prop_of o meta_eq_of) eqs
    val lookup = AList.lookup (op aconv) tab
    val cp = Thm.dest_binop ct
  in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
end


(** f a b = f b a **)
local
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
in
fun commutativity ct = MetaEq (match_instantiate (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) ==> (EX x. P x) == (EX x. Q x)" by simp},
    @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}]
in
fun quant_intro ctxt (p, (vars, _)) ct =
  let
    val rules' = varify ctxt vars (meta_eq_of p) :: rules
    val cu = as_meta_eq ct
  in MetaEq (by_tac' (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
end


(** |- ((ALL x. P x) | Q) = (ALL x. P x | Q) **)
val pull_quant =
  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)


(** |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) **)
val push_quant =
  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)


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

  val rule = (fn @{const_name All} => elim_all | _ => elim_ex)

  fun collect xs tp =
    if (op aconv) tp then rev xs
    else
      (case tp of
        (Const (q, _) $ Abs (_, _, l), r' as Const _ $ Abs (_, _, r)) =>
          if l aconv r then rev xs
          else if Term.loose_bvar1 (l, 0) then collect (NONE :: xs) (l, r)
          else collect (SOME (rule q) :: xs) (Term.incr_bv (~1, 0, l), r')
      | (Const (q, _) $ Abs (_, _, l), r) =>
          collect (SOME (rule q) :: xs) (Term.incr_bv (~1, 0, l), r)
      | (l, r) => raise TERM ("elim_unused", [l, r]))

  fun elim _ [] ct = Conv.all_conv ct
    | elim ctxt (x::xs) ct =
        (case x of
          SOME rule => Conv.rewr_conv rule then_conv elim ctxt xs
        | _ => Conv.arg_conv (Conv.abs_conv (fn (_,cx) => elim cx xs) ctxt)) ct
in
fun elim_unused_vars ctxt ct =
  let val (lhs, rhs) = Thm.dest_binop ct
  in MetaEq (elim ctxt (collect [] (Thm.term_of lhs, Thm.term_of rhs)) lhs) end
end


(** 
  |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn
**)
val dest_eq_res = Thm o by_tac (Simplifier.simp_tac HOL_ss)


(** |- ~(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 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 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 ([], (list2 (dest f sk') ~~ [p, c])) sk')
    |> Conv.fconv_rule (Thm.beta_conversion true)

  fun kind (Const (q as @{const_name Ex}, _) $ _) = (sk_ex_rule, q, I, I)
    | kind (@{term Not} $ (Const (q as @{const_name All}, _) $ _)) =
        (sk_all_rule, q, Thm.dest_arg, Thm.capply @{cterm Not})
    | kind _ = z3_exn "skolemize: no quantifier"

  fun bodies_of ctxt ct =
    let
      val (rule, q, dest, make) = kind (Thm.term_of ct)

      fun inst_abs idx T cbs ct =
        let
          val cv = certify_var ctxt idx T
          val cu = Drule.beta_conv (Thm.dest_arg ct) cv
        in dest_body (idx + 1) ((cv, Thm.dest_arg ct) :: cbs) cu end
      and dest_body idx cbs ct =
        (case Thm.term_of ct of
          Const (qname, _) $ Abs (_, T, _) =>
            if q = qname then inst_abs idx T cbs ct else (make ct, rev cbs)
        | _ => (make ct, rev cbs))
    in (rule, dest_body (#maxidx (Thm.rep_cterm ct) + 1) [] (dest ct)) end

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

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


(* theory proof rules *)

(** prove linear arithmetic problems via generalization **)
local
  val is_numeral = can HOLogic.dest_number
  fun is_number (Const (@{const_name uminus}, _) $ t) = is_numeral t
    | is_number t = is_numeral t

  local
    val int_distrib = @{lemma "n * (x + y) == n * x + n * (y::int)"
      by (simp add: int_distrib)}
    val real_distrib = @{lemma "n * (x + y) == n * x + n * (y::real)"
      by (simp add: mult.add_right)}
    val int_assoc = @{lemma "n * (m * x) == (n * m) * (x::int)" by linarith}
    val real_assoc = @{lemma "n * (m * x) == (n * m) * (x::real)" by linarith}

    val number_of_cong = @{lemma 
      "number_of x * number_of y == (number_of (x * y) :: int)"
      "number_of x * number_of y == (number_of (x * y) :: real)"
      by simp_all}
    val reduce_ss = HOL_ss addsimps @{thms mult_bin_simps}
      addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
      addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
      addsimps number_of_cong
    val reduce_conv = Simplifier.rewrite reduce_ss

    fun apply_conv distrib assoc u ct =
     ((case u of
        Const (@{const_name times}, _) $ n $ _ =>
          if is_number n
          then Conv.rewr_conv assoc then_conv Conv.arg1_conv reduce_conv 
          else Conv.rewr_conv distrib
      | _ => Conv.rewr_conv distrib)
      then_conv Conv.binop_conv (Conv.try_conv distrib_conv)) ct

    and distrib_conv ct = 
      (case Thm.term_of ct of
        @{term "op * :: int => _"} $ n $ u =>
          if is_number n then apply_conv int_distrib int_assoc u
          else Conv.no_conv
      | @{term "op * :: real => _"} $ n $ u =>
          if is_number n then apply_conv real_distrib real_assoc u
          else Conv.no_conv
      | _ => Conv.no_conv) ct
  in
  val all_distrib_conv = More_Conv.top_sweep_conv (K distrib_conv)
  end

  local
    fun fresh ct = fresh_abstraction ct

    fun mult f1 f2 ct t u =
      if is_number t 
      then if is_number u then pair ct else fold_map_binop f1 f2 ct
      else fresh ct

    fun poly ct =
      (case Thm.term_of ct of
        Const (@{const_name plus}, _) $ _ $ _ => fold_map_binop poly poly ct
      | Const (@{const_name minus}, _) $ _ $ _ => fold_map_binop poly poly ct
      | Const (@{const_name times}, _) $ t $ u => mult pair fresh ct t u
      | Const (@{const_name div}, _) $ t $ u => mult fresh pair ct t u
      | Const (@{const_name mod}, _) $ t $ u => mult fresh pair ct t u
      | t => if is_number t then pair ct else fresh ct)

    val ineq_ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"},
      @{term "op <= :: int => _"}, @{term "op = :: real => _"},
      @{term "op < :: real => _"}, @{term "op <= :: real => _"}]
    fun ineq ct =
      (case Thm.term_of ct of
        t $ _ $ _ =>
          if member (op =) ineq_ops t then fold_map_binop poly poly ct
          else raise CTERM ("arith_lemma", [ct])
      | @{term Not} $ (t $ _ $ _) =>
          if member (op =) ineq_ops t
          then fold_map_op (fold_map_binop poly poly) ct
          else raise CTERM ("arith_lemma", [ct])
      | _ => raise CTERM ("arith_lemma", [ct]))

    fun conj ct =
      (case Thm.term_of ct of
        @{term "op &"} $ _ $ _ => fold_map_binop conj conj ct
      | @{term "~False"} => pair ct
      | _ => ineq ct)

    fun disj ct =
      (case Thm.term_of ct of
        @{term "op |"} $ _ $ _ => fold_map_binop disj disj ct
      | @{term False} => pair ct
      | _ => conj ct)
  in
  fun prove_arith ctxt thms ct =
    abstraction_context ctxt
    |> fold_map (fold_map_op ineq o Thm.cprop_of) thms
    ||>> fold_map_op disj ct
    |>> uncurry (fold_rev (Thm.mk_binop @{cterm "op ==>"}))
    |-> prove_abstraction (Arith_Data.arith_tac ctxt)
    |> fold (fn th1 => fn th2 => Thm.implies_elim th2 th1) thms
  end
in
fun arith_lemma ctxt thms ct =
  let val thms' = map (Conv.fconv_rule (all_distrib_conv ctxt)) thms
  in with_conv (all_distrib_conv ctxt) (prove_arith ctxt thms') ct end
end

(** theory simpset **)
local
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}

  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
    | dest_binop t = raise TERM ("dest_binop", [t])

  fun prove_antisym_le ss t =
    let
      val (le, r, s) = dest_binop t
      val less = Const (@{const_name less}, Term.fastype_of le)
      val prems = Simplifier.prems_of_ss ss
    in
      (case find_first (eq_prop (le $ s $ r)) prems of
        NONE =>
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
          |> Option.map (fn thm => thm RS antisym_less1)
      | SOME thm => SOME (thm RS antisym_le1))
    end
    handle THM _ => NONE

  fun prove_antisym_less ss t =
    let
      val (less, r, s) = dest_binop (HOLogic.dest_not t)
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
      val prems = prems_of_ss ss
    in
      (case find_first (eq_prop (le $ r $ s)) prems of
        NONE =>
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
          |> Option.map (fn thm => thm RS antisym_less2)
      | SOME thm => SOME (thm RS antisym_le2))
  end
  handle THM _ => NONE
in
val z3_simpset = HOL_ss addsimps @{thms array_rules}
  addsimps @{thms ring_distribs} addsimps @{thms field_eq_simps}
  addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
  addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
  addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
  addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
  addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
  addsimps [@{thm mult_1_left}]
  addsimprocs [
    Simplifier.simproc @{theory} "fast_int_arith" [
      "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
    Simplifier.simproc @{theory} "fast_real_arith" [
      "(m::real) < n", "(m::real) <= n", "(m::real) = n"]
      (K Lin_Arith.simproc),
    Simplifier.simproc @{theory} "antisym le" ["(x::'a::order) <= y"]
      (K prove_antisym_le),
    Simplifier.simproc @{theory} "antisym less" ["~ (x::'a::linorder) < y"]
      (K prove_antisym_less)]
end

(** theory lemmas: linear arithmetic, arrays **)
local
  val array_ss = HOL_ss addsimps @{thms array_rules}
  val array_pre_ss = HOL_ss addsimps @{thms apply_def array_ext_def}
  fun array_tac thms =
    Tactic.cut_facts_tac thms
    THEN' (Simplifier.asm_full_simp_tac array_pre_ss)
    THEN' (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
      Tactic.rtac @{thm someI2_ex}
      THEN_ALL_NEW (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
        Classical.fast_tac HOL_cs))

  fun full_arith_tac ctxt thms =
    Tactic.cut_facts_tac thms
    THEN' Arith_Data.arith_tac ctxt

  fun simp_arith_tac ctxt thms =
    Tactic.cut_facts_tac thms
    THEN' Simplifier.asm_full_simp_tac z3_simpset
    THEN' Arith_Data.arith_tac ctxt
in
fun th_lemma ctxt thms ct =
  Thm (try_apply ctxt "th-lemma" [
    ("abstract arith", arith_lemma ctxt thms),
    ("array", by_tac' (array_tac thms)),
    ("full arith", by_tac' (full_arith_tac ctxt thms)),
    ("simp arith", by_tac' (simp_arith_tac ctxt thms))] (T.mk_prop ct))
end

(** 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_Rewrite_Rules =
struct
  val name = "z3_rewrite"
  val descr = "Z3 rewrite rules used in proof reconstruction"

  structure Data = Generic_Data
  (
    type T = thm Net.net
    val empty = Net.empty
    val extend = I
    val merge = Net.merge Thm.eq_thm_prop
  )
  val get = Data.get o Context.Proof

  val entry = ` Thm.prop_of o Simplifier.rewrite_rule [true_false]
  val eq = Thm.eq_thm_prop
  val ins = Net.insert_term eq o entry and del = Net.delete_term eq o entry
  fun insert thm net = ins thm net handle Net.INSERT => net
  fun delete thm net = del thm net handle Net.DELETE => net

  val add = Thm.declaration_attribute (Data.map o insert)
  val del = Thm.declaration_attribute (Data.map o delete)
  val setup = Attrib.setup (Binding.name name) (Attrib.add_del add del) descr
end

local
  val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
  fun contra_left conj thm =
    let
      fun make_tab xs = fold Termtab.update xs Termtab.empty
      val tab = make_tab (explode_term conj true (prop_of thm))
      fun pnlits (t, nrs) =
        (case t of
          @{term Not} $ u => Termtab.lookup tab u |> Option.map (pair nrs)
        | _ => NONE)
    in
      (case Termtab.lookup tab @{term False} of
        SOME rs => extract_lit thm rs
      | NONE =>
          pairself (extract_lit thm) (the (Termtab.get_first pnlits tab))
          |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
    end
  val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
  fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
  fun contradiction conj ct =
    iff_intro (under_assumption (contra_left conj) ct) (contra_right ct)

  fun conj_disj ct =
    let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
    in
      (case Thm.term_of cr of
        @{term False} => contradiction true cl
      | @{term "~False"} => contrapos2 (contradiction false o fst) cp
      | _ => prove_conj_disj_eq (Thm.dest_arg ct))
    end

  val distinct =
    let val try_unfold = Conv.try_conv unfold_distinct_conv
    in with_conv (Conv.arg_conv (Conv.binop_conv try_unfold)) conj_disj end

  val nnf_neg_rule = @{lemma "~~P == P" by fastsimp}
  val nnf_cd_rules = @{lemma "~(P | Q) == ~P & ~Q" "~(P & Q) == ~P | ~Q"
    by fastsimp+}

  fun nnf_conv ct = Conv.try_conv (
    (Conv.rewr_conv nnf_neg_rule then_conv nnf_conv) else_conv
    (More_Conv.rewrs_conv nnf_cd_rules then_conv Conv.binop_conv nnf_conv)) ct
  val iffI_rule = @{lemma "~P | Q ==> ~Q | P ==> P = Q" by fast}
  fun arith_tac ctxt = CSUBGOAL (fn (goal, i) =>
    let val prep_then = with_conv (Conv.arg_conv (Conv.binop_conv nnf_conv))
    in Tactic.rtac (prep_then (arith_lemma ctxt []) goal) i end)
  fun arith_eq_tac ctxt =
    Tactic.rtac iffI_rule THEN_ALL_NEW arith_tac ctxt
    ORELSE' arith_tac ctxt

  fun simp_tac thms = CHANGED o Simplifier.simp_tac (z3_simpset addsimps thms)
    ORELSE' Classical.best_tac HOL_cs
  fun simp_arith_tac ctxt thms = Simplifier.simp_tac (z3_simpset addsimps thms)
    THEN_ALL_NEW Arith_Data.arith_tac ctxt
in
fun rewrite ctxt thms ct =
  let val rules_net = Z3_Rewrite_Rules.get ctxt
  in
    Thm (try_apply ctxt "rewrite" [
      ("schematic rule", the o net_instance rules_net),
      ("conj/disj", conj_disj),
      ("distinct", distinct),
      ("arith", by_tac' (arith_eq_tac ctxt)),
      ("classical", by_tac' (Classical.best_tac HOL_cs)),
      ("simp", by_tac' (simp_tac thms)),
      ("simp+arith", by_tac' (simp_arith_tac ctxt thms)),
      ("full arith", by_tac' (Arith_Data.arith_tac ctxt))] (T.mk_prop ct))
  end
end


(* tracing and debugging *)

fun check idx r ct ((_, p), _) =
  let val thm = thm_of p |> tap (Thm.join_proofs o single)
  in
    if (Thm.cprop_of thm) aconvc (T.mk_prop ct) then ()
    else z3_exn ("proof step failed: " ^ quote (string_of_rule r) ^
      " (#" ^ string_of_int idx ^ ")")
  end

local
  fun trace_before ctxt idx (r, ps, ct) =
    Pretty.string_of (
      Pretty.big_list ("#" ^ string_of_int idx ^ ": " ^ string_of_rule r) [
        Pretty.big_list "assumptions:"
          (map (Display.pretty_thm ctxt o thm_of o fst) ps),
        Pretty.block [Pretty.str "goal: ",
          Syntax.pretty_term ctxt (Thm.term_of ct)]])

  fun trace_after ctxt ((_, p), _) = Pretty.string_of (Pretty.block
    [Pretty.str "result: ", Display.pretty_thm ctxt (thm_of p)])
in
fun trace_rule ctxt idx prove r ps ct ptab =
  let
    val _ = SMT_Solver.trace_msg ctxt (trace_before ctxt idx) (r, ps, ct)
    val result = prove r ps ct ptab
    val _ = SMT_Solver.trace_msg ctxt (trace_after ctxt) result
  in result end
end


(* overall reconstruction procedure *)

fun not_supported r =
  z3_exn ("proof rule not implemented: " ^ quote (string_of_rule r))

fun prove ctxt assms =
  let
    val prems = Option.map (prepare_assms ctxt) assms

    fun step r ps ct ptab =
      (case (r, ps) of
        (* core rules *)
        (TrueAxiom, _) => (([], Thm true_thm), ptab)
      | (Asserted, _) => (([], asserted ctxt prems ct), ptab)
      | (Goal, _) => (([], asserted ctxt prems ct), ptab)
      | (ModusPonens, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
      | (ModusPonensOeq, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
      | (AndElim, [(p, (_, i))]) => apfst (pair []) (and_elim (p, i) ct ptab)
      | (NotOrElim, [(p, (_, i))]) =>
          apfst (pair []) (not_or_elim (p, i) ct ptab)
      | (Hypothesis, _) => (([], Thm (Thm.assume (T.mk_prop ct))), ptab)
      | (Lemma, [(p, _)]) => (([], lemma (thm_of p) ct), ptab)
      | (UnitResolution, (p, _) :: ps) =>
          (([], unit_resolution (thm_of p) (map (thm_of o fst) ps) ct), ptab)
      | (IffTrue, [(p, _)]) => (([], iff_true (thm_of p)), ptab)
      | (IffFalse, [(p, _)]) => (([], iff_false (thm_of p)), ptab)
      | (Distributivity, _) => (([], distributivity ct), ptab)
      | (DefAxiom, _) => (([], def_axiom ctxt ct), ptab)
      | (IntroDef, _) => (intro_def ct, ptab)
      | (ApplyDef, [(p, _)]) => (([], apply_def (thm_of p)), ptab)
      | (IffOeq, [(p, _)]) => (([], p), ptab)
      | (NnfPos, _) => (([], nnf ctxt ps ct), ptab)
      | (NnfNeg, _) => (([], nnf ctxt ps ct), ptab)

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

        (* quantifier rules *)
      | (QuantIntro, [p]) => (([], quant_intro ctxt p ct), ptab)
      | (PullQuant, _) => (([], pull_quant ct), ptab)
      | (PushQuant, _) => (([], push_quant ct), ptab)
      | (ElimUnusedVars, _) => (([], elim_unused_vars ctxt ct), ptab)
      | (DestEqRes, _) => (([], dest_eq_res ct), ptab)
      | (QuantInst, _) => (([], quant_inst ct), ptab)
      | (Skolemize, _) => (skolemize ctxt ct, ptab)

        (* theory rules *)
      | (ThLemma, _) => (([], th_lemma ctxt (map (thm_of o fst) ps) ct), ptab)
      | (Rewrite, _) => (([], rewrite ctxt [] ct), ptab)
      | (RewriteStar, ps) =>
          (([], rewrite ctxt (map (thm_of o fst) ps) ct), ptab)

      | (NnfStar, _) => not_supported r
      | (CnfStar, _) => not_supported r
      | (TransitivityStar, _) => not_supported r
      | (PullQuantStar, _) => not_supported r

      | _ => z3_exn ("Proof rule " ^ quote (string_of_rule r) ^
         " has an unexpected number of arguments."))

    fun eq_hyp (ct, cu) = Thm.dest_arg1 ct aconvc Thm.dest_arg1 cu

    fun conclude idx rule prop ((hypss, ps), ptab) =
      trace_rule ctxt idx step rule ps prop ptab
      |> Config.get ctxt SMT_Solver.trace ? tap (check idx rule prop)
      |>> apfst (distinct eq_hyp o fold append hypss)

    fun add_sequent idx vars (hyps, thm) ptab =
      let val s = Sequent {hyps=hyps, vars=vars, thm=thm}
      in ((hyps, (thm, vars)), Inttab.update (idx, s) ptab) end

    fun lookup idx ptab =
      (case Inttab.lookup ptab idx of
        SOME (Unproved {rule, subs, vars, prop}) =>
          fold_map lookup subs ptab
          |>> split_list
          |>> apsnd (map2 (fn idx => fn (p, vs) => (p, (vs, idx))) subs)
          |> conclude idx rule prop
          |-> add_sequent idx vars
      | SOME (Sequent {hyps, vars, thm}) => ((hyps, (thm, vars)), ptab)
      | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))

    fun result (hyps, (thm, _)) =
      fold SMT_Normalize.discharge_definition hyps (thm_of thm)

  in (fn ptab => fn idx => result (fst (lookup idx ptab))) end

val setup = trace_assms_setup #> Z3_Rewrite_Rules.setup

end