src/HOL/Tools/SMT/z3_proof.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66427 d14e7666d785
child 68057 7811d8828775
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/SMT/z3_proof.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Z3 proofs: parsing and abstract syntax tree.
     5 *)
     6 
     7 signature Z3_PROOF =
     8 sig
     9   (*proof rules*)
    10   datatype z3_rule =
    11     True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | Symmetry | Transitivity |
    12     Transitivity_Star | Monotonicity | Quant_Intro | Distributivity | And_Elim | Not_Or_Elim |
    13     Rewrite | Rewrite_Star | Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
    14     Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
    15     Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star |
    16     Cnf_Star | Skolemize | Modus_Ponens_Oeq | Th_Lemma of string
    17 
    18   val is_assumption: z3_rule -> bool
    19   val string_of_rule: z3_rule -> string
    20 
    21   (*proofs*)
    22   datatype z3_step = Z3_Step of {
    23     id: int,
    24     rule: z3_rule,
    25     prems: int list,
    26     concl: term,
    27     fixes: string list,
    28     is_fix_step: bool}
    29 
    30   (*proof parser*)
    31   val parse: typ Symtab.table -> term Symtab.table -> string list ->
    32     Proof.context -> z3_step list * Proof.context
    33 end;
    34 
    35 structure Z3_Proof: Z3_PROOF =
    36 struct
    37 
    38 open SMTLIB_Proof
    39 
    40 
    41 (* proof rules *)
    42 
    43 datatype z3_rule =
    44   True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | Symmetry | Transitivity |
    45   Transitivity_Star | Monotonicity | Quant_Intro | Distributivity | And_Elim | Not_Or_Elim |
    46   Rewrite | Rewrite_Star | Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
    47   Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
    48   Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star |
    49   Cnf_Star | Skolemize | Modus_Ponens_Oeq | Th_Lemma of string
    50   (* some proof rules include further information that is currently dropped by the parser *)
    51 
    52 val rule_names = Symtab.make [
    53   ("true-axiom", True_Axiom),
    54   ("asserted", Asserted),
    55   ("goal", Goal),
    56   ("mp", Modus_Ponens),
    57   ("refl", Reflexivity),
    58   ("symm", Symmetry),
    59   ("trans", Transitivity),
    60   ("trans*", Transitivity_Star),
    61   ("monotonicity", Monotonicity),
    62   ("quant-intro", Quant_Intro),
    63   ("distributivity", Distributivity),
    64   ("and-elim", And_Elim),
    65   ("not-or-elim", Not_Or_Elim),
    66   ("rewrite", Rewrite),
    67   ("rewrite*", Rewrite_Star),
    68   ("pull-quant", Pull_Quant),
    69   ("pull-quant*", Pull_Quant_Star),
    70   ("push-quant", Push_Quant),
    71   ("elim-unused", Elim_Unused_Vars),
    72   ("der", Dest_Eq_Res),
    73   ("quant-inst", Quant_Inst),
    74   ("hypothesis", Hypothesis),
    75   ("lemma", Lemma),
    76   ("unit-resolution", Unit_Resolution),
    77   ("iff-true", Iff_True),
    78   ("iff-false", Iff_False),
    79   ("commutativity", Commutativity),
    80   ("def-axiom", Def_Axiom),
    81   ("intro-def", Intro_Def),
    82   ("apply-def", Apply_Def),
    83   ("iff~", Iff_Oeq),
    84   ("nnf-pos", Nnf_Pos),
    85   ("nnf-neg", Nnf_Neg),
    86   ("nnf*", Nnf_Star),
    87   ("cnf*", Cnf_Star),
    88   ("sk", Skolemize),
    89   ("mp~", Modus_Ponens_Oeq)]
    90 
    91 fun is_assumption Asserted = true
    92   | is_assumption Goal = true
    93   | is_assumption Hypothesis = true
    94   | is_assumption Intro_Def = true
    95   | is_assumption Skolemize = true
    96   | is_assumption _ = false
    97 
    98 fun rule_of_string name =
    99   (case Symtab.lookup rule_names name of
   100     SOME rule => rule
   101   | NONE => error ("unknown Z3 proof rule " ^ quote name))
   102 
   103 fun string_of_rule (Th_Lemma kind) = "th-lemma" ^ (if kind = "" then "" else " " ^ kind)
   104   | string_of_rule r =
   105       let fun eq_rule (s, r') = if r = r' then SOME s else NONE
   106       in the (Symtab.get_first eq_rule rule_names) end
   107 
   108 
   109 (* proofs *)
   110 
   111 datatype z3_node = Z3_Node of {
   112   id: int,
   113   rule: z3_rule,
   114   prems: z3_node list,
   115   concl: term,
   116   bounds: string list}
   117 
   118 fun mk_node id rule prems concl bounds =
   119   Z3_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
   120 
   121 fun string_of_node ctxt =
   122   let
   123     fun str depth (Z3_Node {id, rule, prems, concl, bounds}) =
   124       replicate_string depth "  " ^
   125       enclose "{" "}" (commas
   126         [string_of_int id,
   127          string_of_rule rule,
   128          enclose "[" "]" (space_implode " " bounds),
   129          Syntax.string_of_term ctxt concl] ^
   130         cat_lines (map (prefix "\n" o str (depth + 1)) prems))
   131   in str 0 end
   132 
   133 datatype z3_step = Z3_Step of {
   134   id: int,
   135   rule: z3_rule,
   136   prems: int list,
   137   concl: term,
   138   fixes: string list,
   139   is_fix_step: bool}
   140 
   141 fun mk_step id rule prems concl fixes is_fix_step =
   142   Z3_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes,
   143     is_fix_step = is_fix_step}
   144 
   145 
   146 (* proof parser *)
   147 
   148 fun rule_of (SMTLIB.Sym name) = rule_of_string name
   149   | rule_of (SMTLIB.S (SMTLIB.Sym "_" :: SMTLIB.Sym name :: args)) =
   150       (case (name, args) of
   151         ("th-lemma", SMTLIB.Sym kind :: _) => Th_Lemma kind
   152       | _ => rule_of_string name)
   153   | rule_of r = raise SMTLIB_PARSE ("bad Z3 proof rule format", r)
   154 
   155 fun node_of p cx =
   156   (case p of
   157     SMTLIB.Sym name =>
   158       (case lookup_binding cx name of
   159         Proof node => (node, cx)
   160       | Tree p' =>
   161           cx
   162           |> node_of p'
   163           |-> (fn node => pair node o update_binding (name, Proof node))
   164       | _ => raise SMTLIB_PARSE ("bad Z3 proof format", p))
   165   | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, p] =>
   166       with_bindings (map dest_binding bindings) (node_of p) cx
   167   | SMTLIB.S (name :: parts) =>
   168       let
   169         val (ps, p) = split_last parts
   170         val r = rule_of name
   171       in
   172         cx
   173         |> fold_map node_of ps
   174         ||>> `(with_fresh_names (term_of p))
   175         ||>> next_id
   176         |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns)
   177       end
   178   | _ => raise SMTLIB_PARSE ("bad Z3 proof format", p))
   179 
   180 fun dest_name (SMTLIB.Sym name) = name
   181   | dest_name t = raise SMTLIB_PARSE ("bad name", t)
   182 
   183 fun dest_seq (SMTLIB.S ts) = ts
   184   | dest_seq t = raise SMTLIB_PARSE ("bad Z3 proof format", t)
   185 
   186 fun parse' (SMTLIB.S (SMTLIB.Sym "set-logic" :: _) :: ts) cx = parse' ts cx
   187   | parse' (SMTLIB.S [SMTLIB.Sym "declare-fun", n, tys, ty] :: ts) cx =
   188       let
   189         val name = dest_name n
   190         val Ts = map (type_of cx) (dest_seq tys)
   191         val T = type_of cx ty
   192       in parse' ts (declare_fun name (Ts ---> T) cx) end
   193   | parse' (SMTLIB.S [SMTLIB.Sym "proof", p] :: _) cx = node_of p cx
   194   | parse' ts _ = raise SMTLIB_PARSE ("bad Z3 proof declarations", SMTLIB.S ts)
   195 
   196 fun parse_proof typs funs lines ctxt =
   197   let
   198     val ts = dest_seq (SMTLIB.parse lines)
   199     val (node, cx) = parse' ts (empty_context ctxt typs funs)
   200   in (node, ctxt_of cx) end
   201   handle SMTLIB.PARSE (l, msg) => error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg)
   202        | SMTLIB_PARSE (msg, t) => error (msg ^ ": " ^ SMTLIB.str_of t)
   203 
   204 
   205 (* handling of bound variables *)
   206 
   207 fun subst_of tyenv =
   208   let fun add (ix, (S, T)) = cons (TVar (ix, S), T)
   209   in Vartab.fold add tyenv [] end
   210 
   211 fun substTs_same subst =
   212   let val applyT = Same.function (AList.lookup (op =) subst)
   213   in Term_Subst.map_atypsT_same applyT end
   214 
   215 fun subst_types ctxt env bounds t =
   216   let
   217     val match = Sign.typ_match (Proof_Context.theory_of ctxt)
   218 
   219     val t' = singleton (Variable.polymorphic ctxt) t
   220     val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
   221     val objTs = map (the o Symtab.lookup env) bounds
   222     val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   223   in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
   224 
   225 fun eq_quant (@{const_name HOL.All}, _) (@{const_name HOL.All}, _) = true
   226   | eq_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.Ex}, _) = true
   227   | eq_quant _ _ = false
   228 
   229 fun opp_quant (@{const_name HOL.All}, _) (@{const_name HOL.Ex}, _) = true
   230   | opp_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.All}, _) = true
   231   | opp_quant _ _ = false
   232 
   233 fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) =
   234       if pred q1 q2 andalso T1 = T2 then
   235         let val t = Var (("", i), T1)
   236         in SOME (apply2 Term.subst_bound ((t, t1), (t, t2))) end
   237       else NONE
   238   | with_quant _ _ _ = NONE
   239 
   240 fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) =
   241       Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2))
   242   | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2)
   243 
   244 fun dest_quant i t =
   245   (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of
   246     SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2))
   247   | NONE => raise TERM ("lift_quant", [t]))
   248 
   249 fun match_types ctxt pat obj =
   250   (Vartab.empty, Vartab.empty)
   251   |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj)
   252 
   253 fun strip_match ctxt pat i obj =
   254   (case try (match_types ctxt pat) obj of
   255     SOME (tyenv, _) => subst_of tyenv
   256   | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
   257 
   258 fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
   259       dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
   260   | dest_all i t = (i, t)
   261 
   262 fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t
   263 
   264 fun match_rule ctxt env (Z3_Node {bounds = bs', concl = t', ...}) bs t =
   265   let
   266     val t'' = singleton (Variable.polymorphic ctxt) t'
   267     val (i, obj) = dest_alls (subst_types ctxt env bs t)
   268   in
   269     (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of
   270       NONE => NONE
   271     | SOME subst =>
   272         let
   273           val applyT = Same.commit (substTs_same subst)
   274           val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
   275         in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
   276   end
   277 
   278 
   279 (* linearizing proofs and resolving types of bound variables *)
   280 
   281 fun has_step (tab, _) = Inttab.defined tab
   282 
   283 fun add_step id rule bounds concl is_fix_step ids (tab, sts) =
   284   let val step = mk_step id rule ids concl bounds is_fix_step
   285   in (id, (Inttab.update (id, ()) tab, step :: sts)) end
   286 
   287 fun is_fix_rule rule prems =
   288   member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1
   289 
   290 fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps =
   291   if has_step steps id then (id, steps)
   292   else
   293     let
   294       val t = subst_types ctxt env bounds concl
   295       val add = add_step id rule bounds t
   296       fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b
   297     in
   298       if is_fix_rule rule prems then
   299         (case match_rule ctxt env (hd prems) bounds t of
   300           NONE => rec_apply env false steps
   301         | SOME env' => rec_apply env' true steps)
   302       else rec_apply env false steps
   303     end
   304 
   305 fun linearize ctxt node =
   306   rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
   307 
   308 
   309 (* overall proof parser *)
   310 
   311 fun parse typs funs lines ctxt =
   312   let val (node, ctxt') = parse_proof typs funs lines ctxt
   313   in (linearize ctxt' node, ctxt') end
   314 
   315 end;