# HG changeset patch
# User boehmes
# Date 1292404368 -3600
# Node ID 130771a48c70fae7d778e4b4b76c69ada4ae2d35
# Parent  b88cfc0f745628cd0e9d47c0ed671beb55a24c3e
adapted the Z3 proof parser to recent changes in Z3's proof format;
keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)

diff -r b88cfc0f7456 -r 130771a48c70 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 10:12:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -66,7 +66,7 @@
 
 fun z3_options ctxt =
   ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
-    "MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
+    "MODEL=true", "-smt"]
   |> not (Config.get ctxt SMT_Config.oracle) ?
        append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
 
diff -r b88cfc0f7456 -r 130771a48c70 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 10:12:48 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -7,23 +7,24 @@
 signature Z3_PROOF_PARSER =
 sig
   (*proof rules*)
-  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 of string list
+  datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
+    Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
+    Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
+    Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
+    Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution |
+    Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
+    Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
+    Modus_Ponens_Oeq | Th_Lemma of string list
   val string_of_rule: rule -> string
 
   (*proof parser*)
   datatype proof_step = Proof_Step of {
     rule: rule,
+    args: cterm list,
     prems: int list,
     prop: cterm }
   val parse: Proof.context -> typ Symtab.table -> term Symtab.table ->
-    string list ->
-    int * (proof_step Inttab.table * string list * Proof.context)
+    string list -> (int * proof_step) list * string list * Proof.context
 end
 
 structure Z3_Proof_Parser: Z3_PROOF_PARSER =
@@ -33,58 +34,58 @@
 structure I = Z3_Interface
 
 
-
 (* proof rules *)
 
-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 of string list
+datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
+  Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
+  Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
+  Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res |
+  Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
+  Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos |
+  Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq |
+  Th_Lemma of string list
 
 val rule_names = Symtab.make [
-  ("true-axiom", TrueAxiom),
+  ("true-axiom", True_Axiom),
   ("asserted", Asserted),
   ("goal", Goal),
-  ("mp", ModusPonens),
+  ("mp", Modus_Ponens),
   ("refl", Reflexivity),
   ("symm", Symmetry),
   ("trans", Transitivity),
-  ("trans*", TransitivityStar),
+  ("trans*", Transitivity_Star),
   ("monotonicity", Monotonicity),
-  ("quant-intro", QuantIntro),
+  ("quant-intro", Quant_Intro),
   ("distributivity", Distributivity),
-  ("and-elim", AndElim),
-  ("not-or-elim", NotOrElim),
+  ("and-elim", And_Elim),
+  ("not-or-elim", Not_Or_Elim),
   ("rewrite", Rewrite),
-  ("rewrite*", RewriteStar),
-  ("pull-quant", PullQuant),
-  ("pull-quant*", PullQuantStar),
-  ("push-quant", PushQuant),
-  ("elim-unused", ElimUnusedVars),
-  ("der", DestEqRes),
-  ("quant-inst", QuantInst),
+  ("rewrite*", Rewrite_Star),
+  ("pull-quant", Pull_Quant),
+  ("pull-quant*", Pull_Quant_Star),
+  ("push-quant", Push_Quant),
+  ("elim-unused", Elim_Unused_Vars),
+  ("der", Dest_Eq_Res),
+  ("quant-inst", Quant_Inst),
   ("hypothesis", Hypothesis),
   ("lemma", Lemma),
-  ("unit-resolution", UnitResolution),
-  ("iff-true", IffTrue),
-  ("iff-false", IffFalse),
+  ("unit-resolution", Unit_Resolution),
+  ("iff-true", Iff_True),
+  ("iff-false", Iff_False),
   ("commutativity", Commutativity),
-  ("def-axiom", DefAxiom),
-  ("intro-def", IntroDef),
-  ("apply-def", ApplyDef),
-  ("iff~", IffOeq),
-  ("nnf-pos", NnfPos),
-  ("nnf-neg", NnfNeg),
-  ("nnf*", NnfStar),
-  ("cnf*", CnfStar),
+  ("def-axiom", Def_Axiom),
+  ("intro-def", Intro_Def),
+  ("apply-def", Apply_Def),
+  ("iff~", Iff_Oeq),
+  ("nnf-pos", Nnf_Pos),
+  ("nnf-neg", Nnf_Neg),
+  ("nnf*", Nnf_Star),
+  ("cnf*", Cnf_Star),
   ("sk", Skolemize),
-  ("mp~", ModusPonensOeq),
-  ("th-lemma", ThLemma [])]
+  ("mp~", Modus_Ponens_Oeq),
+  ("th-lemma", Th_Lemma [])]
 
-fun string_of_rule (ThLemma args) = space_implode " " ("th-lemma" :: args)
+fun string_of_rule (Th_Lemma args) = space_implode " " ("th-lemma" :: args)
   | string_of_rule r =
       let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
       in the (Symtab.get_first eq_rule rule_names) end
@@ -94,14 +95,16 @@
 (* certified terms and variables *)
 
 val (var_prefix, decl_prefix) = ("v", "sk")
-(* "decl_prefix" is for skolem constants (represented by free variables)
-   "var_prefix" is for pseudo-schematic variables (schematic with respect
-     to the Z3 proof, but represented by free variables)
+(*
+  "decl_prefix" is for skolem constants (represented by free variables),
+  "var_prefix" is for pseudo-schematic variables (schematic with respect
+  to the Z3 proof, but represented by free variables).
 
-     Both prefixes must be distinct to avoid name interferences.
-   More precisely, the naming of pseudo-schematic variables must be
-   context-independent modulo the current proof context to be able to
-   use fast inference kernel rules during proof reconstruction. *)
+  Both prefixes must be distinct to avoid name interferences.
+  More precisely, the naming of pseudo-schematic variables must be
+  context-independent modulo the current proof context to be able to
+  use fast inference kernel rules during proof reconstruction.
+*)
 
 val maxidx_of = #maxidx o Thm.rep_cterm
 
@@ -116,20 +119,20 @@
   let
     val inst = mk_inst ctxt vars
     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
-  in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
+  in (Thm.instantiate_cterm ([], inst) ct, names) end
 
 
-fun mk_bound thy (i, T) =
-  let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
+fun mk_bound ctxt (i, T) =
+  let val ct = U.certify ctxt (Var ((Name.uu, 0), T))
   in (ct, [(i, ct)]) end
 
 local
-  fun mk_quant thy q T (ct, vars) =
+  fun mk_quant1 ctxt q T (ct, vars) =
     let
       val cv =
         (case AList.lookup (op =) vars 0 of
           SOME cv => cv
-        | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
+        | _ => U.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
     in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
 
@@ -137,11 +140,12 @@
   val forall = quant @{const_name All}
   val exists = quant @{const_name Ex}
 in
-fun mk_forall thy = fold_rev (mk_quant thy forall)
-fun mk_exists thy = fold_rev (mk_quant thy exists)
+
+fun mk_quant is_forall ctxt =
+  fold_rev (mk_quant1 ctxt (if is_forall then forall else exists))
+
 end
 
-
 local
   fun equal_var cv (_, cu) = (cv aconvc cu)
 
@@ -175,6 +179,7 @@
 
 datatype proof_step = Proof_Step of {
   rule: rule,
+  args: cterm list,
   prems: int list,
   prop: cterm }
 
@@ -193,13 +198,13 @@
     fun cert @{const True} = not_false
       | cert t = U.certify ctxt' t
 
-  in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
+  in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
 
 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
   let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
   in (n', (typs, terms, exprs, steps, vars, ctxt')) end
 
-fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
+fun context_of (_, _, _, _, _, ctxt) = ctxt
 
 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
   (case Symtab.lookup terms n of
@@ -229,15 +234,28 @@
 
 fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
 
-fun add_proof_step k ((r, prems), prop) cx =
+fun add_proof_step k ((r, args), prop) cx =
   let
     val (typs, terms, exprs, steps, vars, ctxt) = cx
     val (ct, vs) = close ctxt prop
-    val step = Proof_Step {rule=r, prems=prems, prop=ct}
-    val vars' = union (op =) vs vars
-  in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end
+    fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps)
+      | part (NONE, i) (cts, ps) = (cts, i :: ps)
+    val (args', prems) = fold (part o `(lookup_expr cx)) args ([], [])
+    val (cts, vss) = split_list args'
+    val step =
+      Proof_Step {rule=r, args=rev cts, prems=rev prems, prop=U.mk_cprop ct}
+    val vars' = fold (union (op =)) (vs :: vss) vars
+  in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end
 
-fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt)
+fun finish (_, _, _, steps, vars, ctxt) =
+  let
+    fun add_prems (p as (k, Proof_Step {prems, ...})) (ps, ids) =
+      if Inttab.defined ids k then
+        (p :: ps, fold (Inttab.update o rpair ()) prems ids)
+      else (ps, ids)
+
+    val (steps', _) = fold add_prems steps ([], Inttab.make [(~1, ())])
+  in (steps', vars, ctxt) end
 
 
 (** core parser **)
@@ -249,7 +267,7 @@
 
 fun with_info f cx =
   (case f ((NONE, 1), cx) of
-    ((SOME root, _), cx') => (root, cx')
+    ((SOME _, _), cx') => cx'
   | ((_, line_no), _) => parse_exn line_no "bad proof")
 
 fun parse_line _ _ (st as ((SOME _, _), _)) = st
@@ -291,13 +309,16 @@
   "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
 
 fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
+
 fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
   fold (fn d => fn i => i * 10 + d) ds 0)) st
+
 fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
   (fn sign => nat_num >> sign)) st
 
 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
   member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
+
 fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
 
 fun sym st =
@@ -316,7 +337,7 @@
   | NONE => scan_exn ("unknown sort: " ^ quote n)))] st
 
 fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
-  lookup_context (mk_bound o theory_of)) st
+  lookup_context (mk_bound o context_of)) st
 
 fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
     SOME n' => Scan.succeed n'
@@ -364,8 +385,8 @@
   (the o mk_fun (K (SOME ctrue)))) st
 
 fun quant_kind st = st |> (
-  this "forall" >> K (mk_forall o theory_of) ||
-  this "exists" >> K (mk_exists o theory_of))
+  this "forall" >> K (mk_quant true o context_of) ||
+  this "exists" >> K (mk_quant false o context_of))
 
 fun quantifier st =
   (par (quant_kind -- sep variables --| pats -- sep arg) :|--
@@ -375,13 +396,13 @@
   Scan.first [bound, quantifier, pattern, application, number, constant] :|--
   with_context (pair NONE oo add_expr k)
 
-fun th_lemma_arg st =
-  Scan.lift (Scan.many1 (not o (is_blank orf equal rbra)) >> implode) st
+val rule_arg = id
+  (* if this is modified, then 'th_lemma_arg' needs reviewing *)
+
+val th_lemma_arg = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name)
 
 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
-    (SOME (ThLemma _), _) =>
-      let fun stop st = (sep id >> K "" || $$ rbra) st
-      in Scan.repeat (Scan.unless stop (sep th_lemma_arg)) >> ThLemma end
+    (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma
   | (SOME r, _) => Scan.succeed r
   | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
 
@@ -415,6 +436,6 @@
 fun parse ctxt typs terms proof_text =
   make_context ctxt typs terms
   |> with_info (fold (parse_line node) proof_text)
-  ||> finish
+  |> finish
 
 end
diff -r b88cfc0f7456 -r 130771a48c70 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 10:12:48 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -25,7 +25,7 @@
 
 
 
-(** net of schematic rules **)
+(* net of schematic rules *)
 
 val z3_ruleN = "z3_rule"
 
@@ -64,7 +64,7 @@
 
 
 
-(** proof tools **)
+(* proof tools *)
 
 fun named ctxt name prover ct =
   let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
@@ -107,9 +107,9 @@
 
 
 
-(** theorems and proofs **)
+(* theorems and proofs *)
 
-(* theorem incarnations *)
+(** theorem incarnations **)
 
 datatype theorem =
   Thm of thm | (* theorem without special features *)
@@ -128,16 +128,10 @@
   | literals_of p = L.make_littab [thm_of p]
 
 
-(* proof representation *)
-
-datatype proof = Unproved of P.proof_step | Proved of theorem
-
-
 
 (** core proof rules **)
 
 (* assumption *)
-
 local
   val remove_trigger = @{lemma "trigger t p == p"
     by (rule eq_reflection, rule trigger_def)}
@@ -178,7 +172,6 @@
 end
 
 
-
 (* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
 local
   val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
@@ -196,7 +189,6 @@
 end
 
 
-
 (* and_elim:     P1 & ... & Pn ==> Pi *)
 (* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
 local
@@ -208,8 +200,7 @@
       val ls = L.explode conj false false [t] lit
       val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
 
-      fun upd (Proved thm) = Proved (Literals (thm_of thm, lits'))
-        | upd p = p
+      fun upd thm = Literals (thm_of thm, lits')
     in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
 
   fun lit_elim conj (p, idx) ct ptab =
@@ -225,7 +216,6 @@
 end
 
 
-
 (* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
 local
   fun step lit thm =
@@ -244,7 +234,6 @@
 end
 
 
-
 (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
 local
   val explode_disj = L.explode false true false
@@ -264,7 +253,6 @@
 end
 
 
-
 (* P ==> P == True   or   P ==> P == False *)
 local
   val iff1 = @{lemma "P ==> P == (~ False)" by simp}
@@ -275,16 +263,13 @@
 end
 
 
-
 (* distributivity of | over & *)
 fun distributivity ctxt = Thm o try_apply ctxt [] [
   named ctxt "fast" (T.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}
@@ -334,7 +319,6 @@
 end
 
 
-
 (* local definitions *)
 local
   val intro_rules = [
@@ -363,9 +347,7 @@
 end
 
 
-
 (* negation normal form *)
-
 local
   val quant_rules1 = ([
     @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
@@ -416,7 +398,6 @@
 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}
@@ -426,7 +407,6 @@
 end
 
 
-
 (* s = t ==> t = u ==> s = u *)
 local
   val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
@@ -440,7 +420,6 @@
 end
 
 
-
 (* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
    (reflexive antecendents are droppped) *)
 local
@@ -496,7 +475,6 @@
 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)}
@@ -524,21 +502,18 @@
 end
 
 
-
 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
 fun pull_quant ctxt = Thm o try_apply ctxt [] [
   named ctxt "fast" (T.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" (T.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}
@@ -557,14 +532,12 @@
 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" (T.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}
@@ -575,7 +548,6 @@
 end
 
 
-
 (* c = SOME x. P x |- (EX x. P x) = P c
    c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
 local
@@ -645,11 +617,9 @@
 end
 
 
-
 (** theory proof rules **)
 
 (* theory lemmas: linear arithmetic, arrays *)
-
 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
   T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
     NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
@@ -657,7 +627,6 @@
       Arith_Data.arith_tac ctxt')))]
 
 
-
 (* rewriting: prove equalities:
      * ACI of conjunction/disjunction
      * contradiction, excluded middle
@@ -719,22 +688,16 @@
 
 
 
-(** proof reconstruction **)
+(* proof reconstruction *)
 
-(* tracing and checking *)
+(** tracing and checking **)
 
-local
-  fun count_rules ptab =
-    let
-      fun count (_, Unproved _) (solved, total) = (solved, total + 1)
-        | count (_, Proved _) (solved, total) = (solved + 1, total + 1)
-    in Inttab.fold count ptab (0, 0) end
+fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
+  "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r)
 
-  fun header idx r (solved, total) = 
-    "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r ^ " (goal " ^
-    string_of_int (solved + 1) ^ " of " ^ string_of_int total ^ ")"
-
-  fun check ctxt idx r ps ct p =
+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 ()
@@ -744,46 +707,37 @@
            [Pretty.block [Pretty.str "expected: ",
             Syntax.pretty_term ctxt (Thm.term_of ct)]])))
     end
-in
-fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
-  let
-    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
-    val result as (p, (ctxt', _)) = prove r ps ct cxp
-    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
-      else check ctxt' idx r ps ct p
-  in result end
-end
 
 
-(* overall reconstruction procedure *)
+(** overall reconstruction procedure **)
 
 local
   fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
     quote (P.string_of_rule r))
 
-  fun step assms simpset vars r ps ct (cxp as (cx, ptab)) =
+  fun prove_step assms simpset vars r ps ct (cxp as (cx, ptab)) =
     (case (r, ps) of
       (* core rules *)
-      (P.TrueAxiom, _) => (Thm L.true_thm, cxp)
+      (P.True_Axiom, _) => (Thm L.true_thm, cxp)
     | (P.Asserted, _) => (asserted cx assms ct, cxp)
     | (P.Goal, _) => (asserted cx assms ct, cxp)
-    | (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
-    | (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
-    | (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
-    | (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
+    | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
+    | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
+    | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
+    | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
     | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
     | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
-    | (P.UnitResolution, (p, _) :: ps) =>
+    | (P.Unit_Resolution, (p, _) :: ps) =>
         (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
-    | (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp)
-    | (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp)
+    | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
+    | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
     | (P.Distributivity, _) => (distributivity cx ct, cxp)
-    | (P.DefAxiom, _) => (def_axiom cx ct, cxp)
-    | (P.IntroDef, _) => intro_def ct cx ||> rpair ptab
-    | (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp)
-    | (P.IffOeq, [(p, _)]) => (p, cxp)
-    | (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp)
-    | (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp)
+    | (P.Def_Axiom, _) => (def_axiom cx ct, cxp)
+    | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab
+    | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
+    | (P.Iff_Oeq, [(p, _)]) => (p, cxp)
+    | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
+    | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
 
       (* equality rules *)
     | (P.Reflexivity, _) => (refl ct, cxp)
@@ -793,49 +747,43 @@
     | (P.Commutativity, _) => (commutativity ct, cxp)
 
       (* quantifier rules *)
-    | (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp)
-    | (P.PullQuant, _) => (pull_quant cx ct, cxp)
-    | (P.PushQuant, _) => (push_quant cx ct, cxp)
-    | (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp)
-    | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp)
-    | (P.QuantInst, _) => (quant_inst ct, cxp)
+    | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
+    | (P.Pull_Quant, _) => (pull_quant cx ct, cxp)
+    | (P.Push_Quant, _) => (push_quant cx ct, cxp)
+    | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
+    | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
+    | (P.Quant_Inst, _) => (quant_inst ct, cxp)
     | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
 
       (* theory rules *)
-    | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
+    | (P.Th_Lemma _, _) =>  (* FIXME: use arguments *)
         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
     | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
-    | (P.RewriteStar, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
+    | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
 
-    | (P.NnfStar, _) => not_supported r
-    | (P.CnfStar, _) => not_supported r
-    | (P.TransitivityStar, _) => not_supported r
-    | (P.PullQuantStar, _) => not_supported r
+    | (P.Nnf_Star, _) => not_supported r
+    | (P.Cnf_Star, _) => not_supported r
+    | (P.Transitivity_Star, _) => not_supported r
+    | (P.Pull_Quant_Star, _) => not_supported r
 
     | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
        " has an unexpected number of arguments."))
 
-  fun prove ctxt assms vars =
+  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 assms simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
     let
-      val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
- 
-      fun conclude idx rule prop (ps, cxp) =
-        trace_rule idx (step assms simpset vars) rule ps prop cxp
-        |-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p)
- 
-      fun lookup idx (cxp as (_, ptab)) =
-        (case Inttab.lookup ptab idx of
-          SOME (Unproved (P.Proof_Step {rule, prems, prop})) =>
-            fold_map lookup prems cxp
-            |>> map2 rpair prems
-            |> conclude idx rule prop
-        | SOME (Proved p) => (p, cxp)
-        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
- 
-      fun result (p, (cx, _)) = (thm_of p, cx)
-    in
-      (fn idx => result o lookup idx o pair ctxt o Inttab.map (K Unproved))
-    end
+      val P.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 assms simpset vars r ps prop
+        |> tap (check_after idx r ps prop)
+    in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
 
   val disch_rules = map (pair false)
     [@{thm allI}, @{thm refl}, @{thm reflexive}]
@@ -847,38 +795,33 @@
         SOME (thm', _) => disch_assm thm'
       | NONE => raise THM ("failed to discharge premise", 1, [thm]))
 
-  fun discharge outer_ctxt (thm, inner_ctxt) =
-    thm
+  fun discharge outer_ctxt (p, (inner_ctxt, _)) =
+    thm_of p
     |> singleton (ProofContext.export inner_ctxt outer_ctxt)
-    |> tap (tracing o prefix "final goal: " o PolyML.makestring)
     |> disch_assm    
 
-  fun filter_assms ctxt assms ptab =
+  fun filter_assms ctxt assms =
     let
-      fun step r ct =
+      fun add_assm r ct =
         (case r of
           P.Asserted => insert (op =) (find_assm ctxt assms ct)
         | P.Goal => insert (op =) (find_assm ctxt assms ct)
         | _ => I)
-
-      fun lookup idx =
-        (case Inttab.lookup ptab idx of
-          SOME (P.Proof_Step {rule, prems, prop}) =>
-            fold lookup prems #> step rule prop
-        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
-    in lookup end
+    in fold (fn (_, P.Proof_Step {rule, prop, ...}) => add_assm rule prop) end
 in
 
 fun reconstruct outer_ctxt recon output =
   let
     val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
-    val (idx, (ptab, vars, ctxt')) = P.parse ctxt typs terms output
+    val (steps, vars, ctxt') = P.parse ctxt typs terms output
     val assms' = prepare_assms ctxt' rewrite_rules assms
+    val simpset = T.make_simpset ctxt' (Z3_Simps.get ctxt')
   in
     if Config.get ctxt' SMT_Config.filter_only_facts then
-      (filter_assms ctxt' assms' ptab idx [], @{thm TrueI})
+      (filter_assms ctxt' assms' steps [], @{thm TrueI})
     else
-      prove ctxt' assms' vars idx ptab
+      (Thm @{thm TrueI}, (ctxt', Inttab.empty))
+      |> fold (prove assms' simpset vars) steps 
       |> discharge outer_ctxt
       |> pair []
   end