src/HOL/Tools/SMT2/z3_new_proof.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 56122 40f7b45b2472
child 56811 b66639331db5
permissions -rw-r--r--
more qualified names;
     1 (*  Title:      HOL/Tools/SMT2/z3_new_proof.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Z3 proofs: parsing and abstract syntax tree.
     5 *)
     6 
     7 signature Z3_NEW_PROOF =
     8 sig
     9   (*proof rules*)
    10   datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
    11     Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
    12     Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
    13     Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars |
    14     Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution |
    15     Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def |
    16     Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize |
    17     Modus_Ponens_Oeq | Th_Lemma of string
    18   val string_of_rule: z3_rule -> string
    19 
    20   (*proofs*)
    21   datatype z3_step = Z3_Step of {
    22     id: int,
    23     rule: z3_rule,
    24     prems: int list,
    25     concl: term,
    26     fixes: string list,
    27     is_fix_step: bool}
    28 
    29   (*type and term parsers*)
    30   type type_parser = SMTLIB2.tree * typ list -> typ option
    31   type term_parser = SMTLIB2.tree * term list -> term option
    32   val add_type_parser: type_parser -> Context.generic -> Context.generic
    33   val add_term_parser: term_parser -> Context.generic -> Context.generic
    34 
    35   (*proof parser*)
    36   val parse: typ Symtab.table -> term Symtab.table -> string list ->
    37     Proof.context -> z3_step list * Proof.context
    38 end
    39 
    40 structure Z3_New_Proof: Z3_NEW_PROOF =
    41 struct
    42 
    43 (* proof rules *)
    44 
    45 datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity |
    46   Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro |
    47   Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star |
    48   Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res |
    49   Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False |
    50   Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos |
    51   Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq |
    52   Th_Lemma of string
    53   (* TODO: some proof rules come with further information
    54      that is currently dropped by the parser *)
    55 
    56 val rule_names = Symtab.make [
    57   ("true-axiom", True_Axiom),
    58   ("asserted", Asserted),
    59   ("goal", Goal),
    60   ("mp", Modus_Ponens),
    61   ("refl", Reflexivity),
    62   ("symm", Symmetry),
    63   ("trans", Transitivity),
    64   ("trans*", Transitivity_Star),
    65   ("monotonicity", Monotonicity),
    66   ("quant-intro", Quant_Intro),
    67   ("distributivity", Distributivity),
    68   ("and-elim", And_Elim),
    69   ("not-or-elim", Not_Or_Elim),
    70   ("rewrite", Rewrite),
    71   ("rewrite*", Rewrite_Star),
    72   ("pull-quant", Pull_Quant),
    73   ("pull-quant*", Pull_Quant_Star),
    74   ("push-quant", Push_Quant),
    75   ("elim-unused", Elim_Unused_Vars),
    76   ("der", Dest_Eq_Res),
    77   ("quant-inst", Quant_Inst),
    78   ("hypothesis", Hypothesis),
    79   ("lemma", Lemma),
    80   ("unit-resolution", Unit_Resolution),
    81   ("iff-true", Iff_True),
    82   ("iff-false", Iff_False),
    83   ("commutativity", Commutativity),
    84   ("def-axiom", Def_Axiom),
    85   ("intro-def", Intro_Def),
    86   ("apply-def", Apply_Def),
    87   ("iff~", Iff_Oeq),
    88   ("nnf-pos", Nnf_Pos),
    89   ("nnf-neg", Nnf_Neg),
    90   ("nnf*", Nnf_Star),
    91   ("cnf*", Cnf_Star),
    92   ("sk", Skolemize),
    93   ("mp~", Modus_Ponens_Oeq)]
    94 
    95 fun rule_of_string name =
    96   (case Symtab.lookup rule_names name of
    97     SOME rule => rule
    98   | NONE => error ("unknown Z3 proof rule " ^ quote name))
    99 
   100 fun string_of_rule (Th_Lemma kind) = "th-lemma " ^ kind
   101   | string_of_rule r =
   102       let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
   103       in the (Symtab.get_first eq_rule rule_names) end
   104 
   105 
   106 
   107 (* proofs *)
   108 
   109 datatype z3_node = Z3_Node of {
   110   id: int,
   111   rule: z3_rule,
   112   prems: z3_node list,
   113   concl: term,
   114   bounds: string list}
   115 
   116 fun mk_node id rule prems concl bounds =
   117   Z3_Node {id=id, rule=rule, prems=prems, concl=concl, bounds=bounds}
   118 
   119 datatype z3_step = Z3_Step of {
   120   id: int,
   121   rule: z3_rule,
   122   prems: int list,
   123   concl: term,
   124   fixes: string list,
   125   is_fix_step: bool}
   126 
   127 fun mk_step id rule prems concl fixes is_fix_step =
   128   Z3_Step {id=id, rule=rule, prems=prems, concl=concl, fixes=fixes,
   129     is_fix_step=is_fix_step}
   130 
   131 
   132 
   133 (* core type and term parser *)
   134 
   135 fun core_type_parser (SMTLIB2.Sym "Bool", []) = SOME @{typ HOL.bool}
   136   | core_type_parser (SMTLIB2.Sym "Int", []) = SOME @{typ Int.int}
   137   | core_type_parser _ = NONE
   138 
   139 fun mk_unary n t =
   140   let val T = fastype_of t
   141   in Const (n, T --> T) $ t end
   142 
   143 fun mk_binary' n T U t1 t2 = Const (n, [T, T] ---> U) $ t1 $ t2
   144 
   145 fun mk_binary n t1 t2 =
   146   let val T = fastype_of t1
   147   in mk_binary' n T T t1 t2 end
   148 
   149 fun mk_rassoc f t ts =
   150   let val us = rev (t :: ts)
   151   in fold f (tl us) (hd us) end
   152 
   153 fun mk_lassoc f t ts = fold (fn u1 => fn u2 => f u2 u1) ts t
   154 
   155 fun mk_lassoc' n = mk_lassoc (mk_binary n)
   156 
   157 fun mk_binary_pred n S t1 t2 =
   158   let
   159     val T1 = fastype_of t1
   160     val T2 = fastype_of t2
   161     val T =
   162       if T1 <> Term.dummyT then T1
   163       else if T2 <> Term.dummyT then T2
   164       else TVar (("?a", serial ()), S)
   165   in mk_binary' n T @{typ HOL.bool} t1 t2 end
   166 
   167 fun mk_less t1 t2 = mk_binary_pred @{const_name ord_class.less} @{sort linorder} t1 t2
   168 fun mk_less_eq t1 t2 = mk_binary_pred @{const_name ord_class.less_eq} @{sort linorder} t1 t2
   169 
   170 fun core_term_parser (SMTLIB2.Sym "true", _) = SOME @{const HOL.True}
   171   | core_term_parser (SMTLIB2.Sym "false", _) = SOME @{const HOL.False}
   172   | core_term_parser (SMTLIB2.Sym "not", [t]) = SOME (HOLogic.mk_not t)
   173   | core_term_parser (SMTLIB2.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
   174   | core_term_parser (SMTLIB2.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)
   175   | core_term_parser (SMTLIB2.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2))
   176   | core_term_parser (SMTLIB2.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2))
   177   | core_term_parser (SMTLIB2.Sym "=", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2))
   178   | core_term_parser (SMTLIB2.Sym "~", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2))
   179   | core_term_parser (SMTLIB2.Sym "ite", [t1, t2, t3]) =
   180       let
   181         val T = fastype_of t2
   182         val c = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T)
   183       in SOME (c $ t1 $ t2 $ t3) end
   184   | core_term_parser (SMTLIB2.Num i, []) = SOME (HOLogic.mk_number @{typ Int.int} i)
   185   | core_term_parser (SMTLIB2.Sym "-", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t)
   186   | core_term_parser (SMTLIB2.Sym "~", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t)
   187   | core_term_parser (SMTLIB2.Sym "+", t :: ts) =
   188       SOME (mk_lassoc' @{const_name plus_class.plus} t ts)
   189   | core_term_parser (SMTLIB2.Sym "-", t :: ts) =
   190       SOME (mk_lassoc' @{const_name minus_class.minus} t ts)
   191   | core_term_parser (SMTLIB2.Sym "*", t :: ts) =
   192       SOME (mk_lassoc' @{const_name times_class.times} t ts)
   193   | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3div} t1 t2)
   194   | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3mod} t1 t2)
   195   | core_term_parser (SMTLIB2.Sym "<", [t1, t2]) = SOME (mk_less t1 t2)
   196   | core_term_parser (SMTLIB2.Sym ">", [t1, t2]) = SOME (mk_less t2 t1)
   197   | core_term_parser (SMTLIB2.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2)
   198   | core_term_parser (SMTLIB2.Sym ">=", [t1, t2]) = SOME (mk_less_eq t2 t1)
   199   | core_term_parser _ = NONE
   200 
   201 
   202 
   203 (* type and term parsers *)
   204 
   205 type type_parser = SMTLIB2.tree * typ list -> typ option
   206 
   207 type term_parser = SMTLIB2.tree * term list -> term option
   208 
   209 fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
   210 
   211 structure Parsers = Generic_Data
   212 (
   213   type T = (int * type_parser) list * (int * term_parser) list
   214   val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
   215   val extend = I
   216   fun merge ((tys1, ts1), (tys2, ts2)) =
   217     (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2))
   218 )
   219 
   220 fun add_type_parser type_parser =
   221   Parsers.map (apfst (Ord_List.insert id_ord (serial (), type_parser)))
   222 
   223 fun add_term_parser term_parser =
   224   Parsers.map (apsnd (Ord_List.insert id_ord (serial (), term_parser)))
   225 
   226 fun get_type_parsers ctxt = map snd (fst (Parsers.get (Context.Proof ctxt)))
   227 fun get_term_parsers ctxt = map snd (snd (Parsers.get (Context.Proof ctxt)))
   228 
   229 fun apply_parsers parsers x =
   230   let
   231     fun apply [] = NONE
   232       | apply (parser :: parsers) =
   233           (case parser x of
   234             SOME y => SOME y
   235           | NONE => apply parsers)
   236   in apply parsers end
   237 
   238 
   239 
   240 (* proof parser context *)
   241 
   242 datatype shared = Tree of SMTLIB2.tree | Term of term | Proof of z3_node | None
   243 
   244 type 'a context = {
   245   ctxt: Proof.context,
   246   id: int,
   247   syms: shared Symtab.table,
   248   typs: typ Symtab.table,
   249   funs: term Symtab.table,
   250   extra: 'a}
   251 
   252 fun mk_context ctxt id syms typs funs extra: 'a context =
   253   {ctxt=ctxt, id=id, syms=syms, typs=typs, funs=funs, extra=extra}
   254 
   255 fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs []
   256 
   257 fun ctxt_of ({ctxt, ...}: 'a context) = ctxt
   258 
   259 fun next_id ({ctxt, id, syms, typs, funs, extra}: 'a context) =
   260   (id, mk_context ctxt (id + 1) syms typs funs extra)
   261 
   262 fun lookup_binding ({syms, ...}: 'a context) =
   263   the_default None o Symtab.lookup syms
   264 
   265 fun map_syms f ({ctxt, id, syms, typs, funs, extra}: 'a context) =
   266   mk_context ctxt id (f syms) typs funs extra
   267 
   268 fun update_binding b = map_syms (Symtab.update b)
   269 
   270 fun with_bindings bs f cx =
   271   let val bs' = map (lookup_binding cx o fst) bs
   272   in
   273     cx
   274     |> fold update_binding bs
   275     |> f
   276     ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
   277   end
   278 
   279 fun lookup_typ ({typs, ...}: 'a context) = Symtab.lookup typs
   280 fun lookup_fun ({funs, ...}: 'a context) = Symtab.lookup funs
   281 
   282 fun fresh_fun add name n T ({ctxt, id, syms, typs, funs, extra}: 'a context) =
   283   let
   284     val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
   285     val t = Free (n', T)
   286     val funs' = Symtab.update (name, t) funs
   287   in (t, mk_context ctxt' id syms typs funs' (add (n', T) extra)) end
   288 
   289 fun declare_fun name n T = snd o fresh_fun cons name n T
   290 fun declare_free name n T = fresh_fun (cons o pair name) name n T
   291 
   292 fun with_fresh_names f ({ctxt, id, syms, typs, funs, extra}: 'a context) =
   293   let
   294     fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t
   295 
   296     val needs_inferT = equal Term.dummyT orf Term.is_TVar
   297     val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT)
   298     fun infer_types ctxt =
   299       singleton (Type_Infer_Context.infer_types ctxt) #>
   300       singleton (Proof_Context.standard_term_check_finish ctxt)
   301     fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
   302 
   303     type bindings = (string * (string * typ)) list
   304     val (t, {ctxt=ctxt', extra=names, ...}: bindings context) =
   305       f (mk_context ctxt id syms typs funs [])
   306     val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t))
   307    
   308   in ((t', map fst names), mk_context ctxt id syms typs funs extra) end
   309 
   310 
   311 
   312 (* proof parser *)
   313 
   314 exception Z3_PARSE of string * SMTLIB2.tree
   315 
   316 val desymbolize = Name.desymbolize false o perhaps (try (unprefix "?"))
   317 
   318 fun parse_type cx ty Ts =
   319   (case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of
   320     SOME T => T
   321   | NONE =>
   322       (case ty of
   323         SMTLIB2.Sym name =>
   324           (case lookup_typ cx name of
   325             SOME T => T
   326           | NONE => raise Z3_PARSE ("unknown Z3 type", ty))
   327       | _ => raise Z3_PARSE ("bad Z3 type format", ty)))
   328 
   329 fun parse_term t ts cx =
   330   (case apply_parsers (get_term_parsers (ctxt_of cx)) (t, ts) of
   331     SOME u => (u, cx)
   332   | NONE =>
   333       (case t of
   334         SMTLIB2.Sym name =>
   335           (case lookup_fun cx name of
   336             SOME u => (Term.list_comb (u, ts), cx)
   337           | NONE =>
   338               if null ts then declare_free name (desymbolize name) Term.dummyT cx
   339               else raise Z3_PARSE ("bad Z3 term", t))
   340       | _ => raise Z3_PARSE ("bad Z3 term format", t)))
   341 
   342 fun type_of cx ty =
   343   (case try (parse_type cx ty) [] of
   344     SOME T => T
   345   | NONE =>
   346       (case ty of
   347         SMTLIB2.S (ty' :: tys) => parse_type cx ty' (map (type_of cx) tys)
   348       | _ => raise Z3_PARSE ("bad Z3 type", ty)))
   349 
   350 fun dest_var cx (SMTLIB2.S [SMTLIB2.Sym name, ty]) = (name, (desymbolize name, type_of cx ty))
   351   | dest_var _ v = raise Z3_PARSE ("bad Z3 quantifier variable format", v)
   352 
   353 fun dest_body (SMTLIB2.S (SMTLIB2.Sym "!" :: body :: _)) = dest_body body
   354   | dest_body body = body
   355 
   356 fun dest_binding (SMTLIB2.S [SMTLIB2.Sym name, t]) = (name, Tree t)
   357   | dest_binding b = raise Z3_PARSE ("bad Z3 let binding format", b)
   358 
   359 fun term_of t cx =
   360   (case t of
   361     SMTLIB2.S [SMTLIB2.Sym "forall", SMTLIB2.S vars, body] =>
   362       quant HOLogic.mk_all vars body cx
   363   | SMTLIB2.S [SMTLIB2.Sym "exists", SMTLIB2.S vars, body] =>
   364       quant HOLogic.mk_exists vars body cx
   365   | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, body] =>
   366       with_bindings (map dest_binding bindings) (term_of body) cx
   367   | SMTLIB2.S (SMTLIB2.Sym "!" :: t :: _) => term_of t cx
   368   | SMTLIB2.S (f :: args) =>
   369       cx
   370       |> fold_map term_of args
   371       |-> parse_term f
   372   | SMTLIB2.Sym name =>
   373       (case lookup_binding cx name of
   374         Tree u =>
   375           cx
   376           |> term_of u
   377           |-> (fn u' => pair u' o update_binding (name, Term u'))
   378       | Term u => (u, cx)
   379       | None => parse_term t [] cx
   380       | _ => raise Z3_PARSE ("bad Z3 term format", t))
   381   | _ => parse_term t [] cx)
   382 
   383 and quant q vars body cx =
   384   let val vs = map (dest_var cx) vars
   385   in
   386     cx
   387     |> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body))
   388     |>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs
   389   end
   390 
   391 fun rule_of (SMTLIB2.Sym name) = rule_of_string name
   392   | rule_of (SMTLIB2.S (SMTLIB2.Sym "_" :: SMTLIB2.Sym name :: args)) =
   393       (case (name, args) of
   394         ("th-lemma", SMTLIB2.Sym kind :: _) => Th_Lemma kind
   395       | _ => rule_of_string name)
   396   | rule_of r = raise Z3_PARSE ("bad Z3 proof rule format", r)
   397 
   398 fun node_of p cx =
   399   (case p of
   400     SMTLIB2.Sym name =>
   401       (case lookup_binding cx name of
   402         Proof node => (node, cx)
   403       | Tree p' =>
   404           cx
   405           |> node_of p'
   406           |-> (fn node => pair node o update_binding (name, Proof node))
   407       | _ => raise Z3_PARSE ("bad Z3 proof format", p))
   408   | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, p] =>
   409       with_bindings (map dest_binding bindings) (node_of p) cx
   410   | SMTLIB2.S (name :: parts) =>
   411       let
   412         val (ps, p) = split_last parts
   413         val r = rule_of name
   414       in
   415         cx
   416         |> fold_map node_of ps
   417         ||>> with_fresh_names (term_of p)
   418         ||>> next_id
   419         |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns)
   420       end
   421   | _ => raise Z3_PARSE ("bad Z3 proof format", p))
   422 
   423 fun dest_name (SMTLIB2.Sym name) = name
   424   | dest_name t = raise Z3_PARSE ("bad name", t)
   425 
   426 fun dest_seq (SMTLIB2.S ts) = ts
   427   | dest_seq t = raise Z3_PARSE ("bad Z3 proof format", t)
   428 
   429 fun parse' (SMTLIB2.S (SMTLIB2.Sym "set-logic" :: _) :: ts) cx = parse' ts cx
   430   | parse' (SMTLIB2.S [SMTLIB2.Sym "declare-fun", n, tys, ty] :: ts) cx =
   431       let
   432         val name = dest_name n
   433         val Ts = map (type_of cx) (dest_seq tys)
   434         val T = type_of cx ty
   435       in parse' ts (declare_fun name (desymbolize name) (Ts ---> T) cx) end
   436   | parse' (SMTLIB2.S [SMTLIB2.Sym "proof", p] :: _) cx = node_of p cx
   437   | parse' ts _ = raise Z3_PARSE ("bad Z3 proof declarations", SMTLIB2.S ts)
   438 
   439 fun parse_proof typs funs lines ctxt =
   440   let
   441     val ts = dest_seq (SMTLIB2.parse lines)
   442     val (node, cx) = parse' ts (empty_context ctxt typs funs)
   443   in (node, ctxt_of cx) end
   444   handle SMTLIB2.PARSE (l, msg) =>
   445            error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg)
   446        | Z3_PARSE (msg, t) =>
   447            error (msg ^ ": " ^ SMTLIB2.str_of t)
   448 
   449 
   450 
   451 (* handling of bound variables *)
   452 
   453 fun subst_of tyenv =
   454   let fun add (ix, (S, T)) = cons (TVar (ix, S), T)
   455   in Vartab.fold add tyenv [] end
   456 
   457 fun substTs_same subst = 
   458   let val applyT = Same.function (AList.lookup (op =) subst)
   459   in Term_Subst.map_atypsT_same applyT end
   460 
   461 fun subst_types ctxt env bounds t =
   462   let
   463     val match = Sign.typ_match (Proof_Context.theory_of ctxt)
   464 
   465     val t' = singleton (Variable.polymorphic ctxt) t
   466     val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
   467     val objTs = map (the o Symtab.lookup env) bounds
   468     val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   469   in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
   470 
   471 fun eq_quant (@{const_name HOL.All}, _) (@{const_name HOL.All}, _) = true
   472   | eq_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.Ex}, _) = true
   473   | eq_quant _ _ = false
   474 
   475 fun opp_quant (@{const_name HOL.All}, _) (@{const_name HOL.Ex}, _) = true
   476   | opp_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.All}, _) = true
   477   | opp_quant _ _ = false
   478 
   479 fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) =
   480       if pred q1 q2 andalso T1 = T2 then
   481         let val t = Var (("", i), T1)
   482         in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end
   483       else NONE
   484   | with_quant _ _ _ = NONE
   485 
   486 fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) =
   487       Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2))
   488   | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2)
   489 
   490 fun dest_quant i t =
   491   (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of
   492     SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2))
   493   | NONE => raise TERM ("lift_quant", [t]))
   494 
   495 fun match_types ctxt pat obj =
   496   (Vartab.empty, Vartab.empty)
   497   |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj)
   498 
   499 fun strip_match ctxt pat i obj =
   500   (case try (match_types ctxt pat) obj of
   501     SOME (tyenv, _) => subst_of tyenv
   502   | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
   503 
   504 fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
   505       dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
   506   | dest_all i t = (i, t)
   507 
   508 fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t
   509 
   510 fun match_rule ctxt env (Z3_Node {bounds=bs', concl=t', ...}) bs t =
   511   let
   512     val t'' = singleton (Variable.polymorphic ctxt) t'
   513     val (i, obj) = dest_alls (subst_types ctxt env bs t)
   514   in
   515     (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of
   516       NONE => NONE
   517     | SOME subst =>
   518         let
   519           val applyT = Same.commit (substTs_same subst)
   520           val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
   521         in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
   522   end
   523 
   524 
   525 
   526 (* linearizing proofs and resolving types of bound variables *)
   527 
   528 fun has_step (tab, _) = Inttab.defined tab
   529 
   530 fun add_step id rule bounds concl is_fix_step ids (tab, sts) =
   531   let val step = mk_step id rule ids concl bounds is_fix_step
   532   in (id, (Inttab.update (id, ()) tab, step :: sts)) end
   533 
   534 fun is_fix_rule rule prems =
   535   member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1
   536 
   537 fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps =
   538   if has_step steps id then (id, steps)
   539   else
   540     let
   541       val t = subst_types ctxt env bounds concl
   542       val add = add_step id rule bounds t
   543       fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b
   544     in
   545       if is_fix_rule rule prems then
   546         (case match_rule ctxt env (hd prems) bounds t of
   547           NONE => rec_apply env false steps
   548         | SOME env' => rec_apply env' true steps)
   549       else rec_apply env false steps
   550     end
   551 
   552 fun linearize ctxt node =
   553   rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
   554 
   555 
   556 
   557 (* overall proof parser *)
   558 
   559 fun parse typs funs lines ctxt =
   560   let val (node, ctxt') = parse_proof typs funs lines ctxt
   561   in (linearize ctxt' node, ctxt') end
   562 
   563 end