--- a/src/HOL/Tools/SMT2/z3_new_proof.ML Thu Aug 28 00:40:38 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,303 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof.ML
- Author: Sascha Boehme, TU Muenchen
-
-Z3 proofs: parsing and abstract syntax tree.
-*)
-
-signature Z3_NEW_PROOF =
-sig
- (*proof rules*)
- datatype z3_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
-
- val is_assumption: z3_rule -> bool
- val string_of_rule: z3_rule -> string
-
- (*proofs*)
- datatype z3_step = Z3_Step of {
- id: int,
- rule: z3_rule,
- prems: int list,
- concl: term,
- fixes: string list,
- is_fix_step: bool}
-
- (*proof parser*)
- val parse: typ Symtab.table -> term Symtab.table -> string list ->
- Proof.context -> z3_step list * Proof.context
-end;
-
-structure Z3_New_Proof: Z3_NEW_PROOF =
-struct
-
-open SMTLIB2_Proof
-
-
-(* proof rules *)
-
-datatype z3_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
- (* some proof rules include further information that is currently dropped by the parser *)
-
-val rule_names = Symtab.make [
- ("true-axiom", True_Axiom),
- ("asserted", Asserted),
- ("goal", Goal),
- ("mp", Modus_Ponens),
- ("refl", Reflexivity),
- ("symm", Symmetry),
- ("trans", Transitivity),
- ("trans*", Transitivity_Star),
- ("monotonicity", Monotonicity),
- ("quant-intro", Quant_Intro),
- ("distributivity", Distributivity),
- ("and-elim", And_Elim),
- ("not-or-elim", Not_Or_Elim),
- ("rewrite", Rewrite),
- ("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", Unit_Resolution),
- ("iff-true", Iff_True),
- ("iff-false", Iff_False),
- ("commutativity", Commutativity),
- ("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~", Modus_Ponens_Oeq)]
-
-fun is_assumption Asserted = true
- | is_assumption Goal = true
- | is_assumption Hypothesis = true
- | is_assumption Intro_Def = true
- | is_assumption Skolemize = true
- | is_assumption _ = false
-
-fun rule_of_string name =
- (case Symtab.lookup rule_names name of
- SOME rule => rule
- | NONE => error ("unknown Z3 proof rule " ^ quote name))
-
-fun string_of_rule (Th_Lemma kind) = "th-lemma" ^ (if kind = "" then "" else " " ^ kind)
- | 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
-
-
-(* proofs *)
-
-datatype z3_node = Z3_Node of {
- id: int,
- rule: z3_rule,
- prems: z3_node list,
- concl: term,
- bounds: string list}
-
-fun mk_node id rule prems concl bounds =
- Z3_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
-
-datatype z3_step = Z3_Step of {
- id: int,
- rule: z3_rule,
- prems: int list,
- concl: term,
- fixes: string list,
- is_fix_step: bool}
-
-fun mk_step id rule prems concl fixes is_fix_step =
- Z3_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes,
- is_fix_step = is_fix_step}
-
-
-(* proof parser *)
-
-fun rule_of (SMTLIB2.Sym name) = rule_of_string name
- | rule_of (SMTLIB2.S (SMTLIB2.Sym "_" :: SMTLIB2.Sym name :: args)) =
- (case (name, args) of
- ("th-lemma", SMTLIB2.Sym kind :: _) => Th_Lemma kind
- | _ => rule_of_string name)
- | rule_of r = raise SMTLIB2_PARSE ("bad Z3 proof rule format", r)
-
-fun node_of p cx =
- (case p of
- SMTLIB2.Sym name =>
- (case lookup_binding cx name of
- Proof node => (node, cx)
- | Tree p' =>
- cx
- |> node_of p'
- |-> (fn node => pair node o update_binding (name, Proof node))
- | _ => raise SMTLIB2_PARSE ("bad Z3 proof format", p))
- | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, p] =>
- with_bindings (map dest_binding bindings) (node_of p) cx
- | SMTLIB2.S (name :: parts) =>
- let
- val (ps, p) = split_last parts
- val r = rule_of name
- in
- cx
- |> fold_map node_of ps
- ||>> `(with_fresh_names (term_of p))
- ||>> next_id
- |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns)
- end
- | _ => raise SMTLIB2_PARSE ("bad Z3 proof format", p))
-
-fun dest_name (SMTLIB2.Sym name) = name
- | dest_name t = raise SMTLIB2_PARSE ("bad name", t)
-
-fun dest_seq (SMTLIB2.S ts) = ts
- | dest_seq t = raise SMTLIB2_PARSE ("bad Z3 proof format", t)
-
-fun parse' (SMTLIB2.S (SMTLIB2.Sym "set-logic" :: _) :: ts) cx = parse' ts cx
- | parse' (SMTLIB2.S [SMTLIB2.Sym "declare-fun", n, tys, ty] :: ts) cx =
- let
- val name = dest_name n
- val Ts = map (type_of cx) (dest_seq tys)
- val T = type_of cx ty
- in parse' ts (declare_fun name (Ts ---> T) cx) end
- | parse' (SMTLIB2.S [SMTLIB2.Sym "proof", p] :: _) cx = node_of p cx
- | parse' ts _ = raise SMTLIB2_PARSE ("bad Z3 proof declarations", SMTLIB2.S ts)
-
-fun parse_proof typs funs lines ctxt =
- let
- val ts = dest_seq (SMTLIB2.parse lines)
- val (node, cx) = parse' ts (empty_context ctxt typs funs)
- in (node, ctxt_of cx) end
- handle SMTLIB2.PARSE (l, msg) => error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg)
- | SMTLIB2_PARSE (msg, t) => error (msg ^ ": " ^ SMTLIB2.str_of t)
-
-
-(* handling of bound variables *)
-
-fun subst_of tyenv =
- let fun add (ix, (S, T)) = cons (TVar (ix, S), T)
- in Vartab.fold add tyenv [] end
-
-fun substTs_same subst =
- let val applyT = Same.function (AList.lookup (op =) subst)
- in Term_Subst.map_atypsT_same applyT end
-
-fun subst_types ctxt env bounds t =
- let
- val match = Sign.typ_match (Proof_Context.theory_of ctxt)
-
- val t' = singleton (Variable.polymorphic ctxt) t
- val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
- val objTs = map (the o Symtab.lookup env) bounds
- val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
- in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
-
-fun eq_quant (@{const_name HOL.All}, _) (@{const_name HOL.All}, _) = true
- | eq_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.Ex}, _) = true
- | eq_quant _ _ = false
-
-fun opp_quant (@{const_name HOL.All}, _) (@{const_name HOL.Ex}, _) = true
- | opp_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.All}, _) = true
- | opp_quant _ _ = false
-
-fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) =
- if pred q1 q2 andalso T1 = T2 then
- let val t = Var (("", i), T1)
- in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end
- else NONE
- | with_quant _ _ _ = NONE
-
-fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) =
- Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2))
- | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2)
-
-fun dest_quant i t =
- (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of
- SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2))
- | NONE => raise TERM ("lift_quant", [t]))
-
-fun match_types ctxt pat obj =
- (Vartab.empty, Vartab.empty)
- |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj)
-
-fun strip_match ctxt pat i obj =
- (case try (match_types ctxt pat) obj of
- SOME (tyenv, _) => subst_of tyenv
- | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
-
-fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
- dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
- | dest_all i t = (i, t)
-
-fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t
-
-fun match_rule ctxt env (Z3_Node {bounds = bs', concl = t', ...}) bs t =
- let
- val t'' = singleton (Variable.polymorphic ctxt) t'
- val (i, obj) = dest_alls (subst_types ctxt env bs t)
- in
- (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of
- NONE => NONE
- | SOME subst =>
- let
- val applyT = Same.commit (substTs_same subst)
- val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
- in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
- end
-
-
-(* linearizing proofs and resolving types of bound variables *)
-
-fun has_step (tab, _) = Inttab.defined tab
-
-fun add_step id rule bounds concl is_fix_step ids (tab, sts) =
- let val step = mk_step id rule ids concl bounds is_fix_step
- in (id, (Inttab.update (id, ()) tab, step :: sts)) end
-
-fun is_fix_rule rule prems =
- member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1
-
-fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps =
- if has_step steps id then (id, steps)
- else
- let
- val t = subst_types ctxt env bounds concl
- val add = add_step id rule bounds t
- fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b
- in
- if is_fix_rule rule prems then
- (case match_rule ctxt env (hd prems) bounds t of
- NONE => rec_apply env false steps
- | SOME env' => rec_apply env' true steps)
- else rec_apply env false steps
- end
-
-fun linearize ctxt node =
- rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
-
-
-(* overall proof parser *)
-
-fun parse typs funs lines ctxt =
- let val (node, ctxt') = parse_proof typs funs lines ctxt
- in (linearize ctxt' node, ctxt') end
-
-end;