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)
--- 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"]
--- 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
--- 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