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