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