diff -r 8e55aa1306c5 -r bcd6fce5bf06 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed May 12 23:54:04 2010 +0200
@@ -29,6 +29,10 @@
 structure Z3_Proof_Parser: Z3_PROOF_PARSER =
 struct
 
+structure I = Z3_Interface
+
+
+
 (** proof rules **)
 
 datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
@@ -87,16 +91,15 @@
 
 (** certified terms and variables **)
 
-val (var_prefix, decl_prefix) = ("v", "sk")  (* must be distinct *)
+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)
 
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
-fun ctyp_of (ct, _) = Thm.ctyp_of_term ct
-fun instT' t = instT (ctyp_of t)
+     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. *)
 
 fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
 
@@ -128,12 +131,11 @@
         (case AList.lookup (op =) vars 0 of
           SOME cv => cv
         | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
-      val cq = instT (Thm.ctyp_of_term cv) q
       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
-    in (Thm.capply cq (Thm.cabs cv ct), map_filter dec vars) end
+    in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
 
-  val forall = mk_inst_pair (destT1 o destT1) @{cpat All}
-  val exists = mk_inst_pair (destT1 o destT1) @{cpat Ex}
+  val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All}
+  val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex}
 in
 fun mk_forall thy = fold_rev (mk_quant thy forall)
 fun mk_exists thy = fold_rev (mk_quant thy exists)
@@ -143,118 +145,29 @@
 local
   fun equal_var cv (_, cu) = (cv aconvc cu)
 
-  fun apply (ct2, vars2) (ct1, vars1) =
+  fun prep (ct, vars) (maxidx, all_vars) =
     let
-      val incr = Thm.incr_indexes_cterm (maxidx_of ct1 + maxidx_of ct2 + 2)
+      val maxidx' = maxidx_of ct + maxidx + 1
 
       fun part (v as (i, cv)) =
-        (case AList.lookup (op =) vars1 i of
+        (case AList.lookup (op =) all_vars i of
           SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
         | NONE =>
-            if not (exists (equal_var cv) vars1) then apsnd (cons v)
+            if not (exists (equal_var cv) all_vars) then apsnd (cons v)
             else
-              let val cv' = incr cv
+              let val cv' = Thm.incr_indexes_cterm maxidx' cv
               in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
 
-      val (ct2', vars2') =
-        if null vars1 then (ct2, vars2)
-        else fold part vars2 ([], [])
-          |>> (fn inst => Thm.instantiate_cterm ([], inst) ct2)
-
-    in (Thm.capply ct1 ct2', vars1 @ vars2') end
-in
-fun mk_fun ct ts = fold apply ts (ct, [])
-fun mk_binop f t u = mk_fun f [t, u]
-fun mk_nary _ e [] = e
-  | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es)
-end
-
-
-val mk_true = mk_fun @{cterm "~False"} []
-val mk_false = mk_fun @{cterm "False"} []
-fun mk_not t = mk_fun @{cterm Not} [t]
-val mk_imp = mk_binop @{cterm "op -->"}
-val mk_iff = mk_binop @{cterm "op = :: bool => _"}
-
-val eq = mk_inst_pair destT1 @{cpat "op ="}
-fun mk_eq t u = mk_binop (instT' t eq) t u
-
-val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
-fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u]
-
-val nil_term = mk_inst_pair destT1 @{cpat Nil}
-val cons_term = mk_inst_pair destT1 @{cpat Cons}
-fun mk_list cT es =
-  fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) [])
-
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
-fun mk_distinct [] = mk_true
-  | mk_distinct (es as (e :: _)) =
-      mk_fun (instT' e distinct) [mk_list (ctyp_of e) es]
-
-
-(* arithmetic *)
-
-fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
-fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []
-fun mk_real_frac_num (e, NONE) = mk_real_num e
-  | mk_real_frac_num (e, SOME d) =
-      mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d)
-
-fun has_int_type e = (Thm.typ_of (ctyp_of e) = @{typ int})
-fun choose e i r = if has_int_type e then i else r
+      val (inst, vars') =
+        if null vars then ([], vars)
+        else fold part vars ([], [])
 
-val uminus_i = @{cterm "uminus :: int => _"}
-val uminus_r = @{cterm "uminus :: real => _"}
-fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e]
-
-fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u
-
-val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"}
-val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"}
-val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"}
-val mk_int_div = mk_binop @{cterm "op div :: int => _"}
-val mk_real_div = mk_binop @{cterm "op / :: real => _"}
-val mk_mod = mk_binop @{cterm "op mod :: int => _"}
-val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"}
-val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"}
-
-
-(* arrays *)
-
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
-fun mk_access array index =
-  let val cTs = Thm.dest_ctyp (ctyp_of array)
-  in mk_fun (instTs cTs access) [array, index] end
-
-val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
-fun mk_update array index value =
-  let val cTs = Thm.dest_ctyp (ctyp_of array)
-  in mk_fun (instTs cTs update) [array, index, value] end
-
-
-(* bitvectors *)
-
-fun mk_binT size =
-  let
-    fun bitT i T =
-      if i = 0
-      then Type (@{type_name "Numeral_Type.bit0"}, [T])
-      else Type (@{type_name "Numeral_Type.bit1"}, [T])
-
-    fun binT i =
-      if i = 0 then @{typ "Numeral_Type.num0"}
-      else if i = 1 then @{typ "Numeral_Type.num1"}
-      else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end
-  in
-    if size >= 0 then binT size
-    else raise TYPE ("mk_binT: " ^ string_of_int size, [], [])
-  end
-
-fun mk_wordT size = Type (@{type_name "word"}, [mk_binT size])
-
-fun mk_bv_num thy (num, size) =
-  mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (mk_wordT size)) num) []
+    in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
+in
+fun mk_fun f ts =
+  let val (cts, (_, vars)) = fold_map prep ts (~1, [])
+  in f cts |> Option.map (rpair vars) end
+end
 
 
 
@@ -277,6 +190,7 @@
 
     fun cert @{term True} = @{cterm "~False"}
       | cert t = certify ctxt' t
+
   in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
 
 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
@@ -285,14 +199,6 @@
 
 fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
 
-fun typ_of_sort n (cx as (typs, _, _, _, _, _)) =
-  (case Symtab.lookup typs n of
-    SOME T => (T, cx)
-  | NONE => cx
-      |> fresh_name ("'" ^ n) |>> TFree o rpair @{sort type}
-      |> (fn (T, (typs, terms, exprs, steps, vars, ctxt)) =>
-           (T, (Symtab.update (n, T) typs, terms, exprs, steps, vars, ctxt))))
-
 fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
   (case Symtab.lookup terms n of
     SOME _ => cx
@@ -301,36 +207,20 @@
            let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
            in (typs, upd terms, exprs, steps, vars, ctxt) end))
 
-datatype sym = Sym of string * sym list
+fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 
+  (case I.mk_builtin_typ ctxt s of
+    SOME T => SOME T
+  | NONE => Symtab.lookup typs n)
 
-fun mk_app _ (Sym ("true", _), _) = SOME mk_true
-  | mk_app _ (Sym ("false", _), _) = SOME mk_false
-  | mk_app _ (Sym ("=", _), [t, u]) = SOME (mk_eq t u)
-  | mk_app _ (Sym ("distinct", _), ts) = SOME (mk_distinct ts)
-  | mk_app _ (Sym ("ite", _), [s, t, u]) = SOME (mk_if s t u)
-  | mk_app _ (Sym ("and", _), ts) = SOME (mk_nary @{cterm "op &"} mk_true ts)
-  | mk_app _ (Sym ("or", _), ts) = SOME (mk_nary @{cterm "op |"} mk_false ts)
-  | mk_app _ (Sym ("iff", _), [t, u]) = SOME (mk_iff t u)
-  | mk_app _ (Sym ("xor", _), [t, u]) = SOME (mk_not (mk_iff t u))
-  | mk_app _ (Sym ("not", _), [t]) = SOME (mk_not t)
-  | mk_app _ (Sym ("implies", _), [t, u]) = SOME (mk_imp t u)
-  | mk_app _ (Sym ("~", _), [t, u]) = SOME (mk_iff t u)
-  | mk_app _ (Sym ("<", _), [t, u]) = SOME (mk_lt t u)
-  | mk_app _ (Sym ("<=", _), [t, u]) = SOME (mk_le t u)
-  | mk_app _ (Sym (">", _), [t, u]) = SOME (mk_lt u t)
-  | mk_app _ (Sym (">=", _), [t, u]) = SOME (mk_le u t)
-  | mk_app _ (Sym ("+", _), [t, u]) = SOME (mk_add t u)
-  | mk_app _ (Sym ("-", _), [t, u]) = SOME (mk_sub t u)
-  | mk_app _ (Sym ("-", _), [t]) = SOME (mk_uminus t)
-  | mk_app _ (Sym ("*", _), [t, u]) = SOME (mk_mul t u)
-  | mk_app _ (Sym ("/", _), [t, u]) = SOME (mk_real_div t u)
-  | mk_app _ (Sym ("div", _), [t, u]) = SOME (mk_int_div t u)
-  | mk_app _ (Sym ("mod", _), [t, u]) = SOME (mk_mod t u)
-  | mk_app _ (Sym ("select", _), [m, k]) = SOME (mk_access m k)
-  | mk_app _ (Sym ("store", _), [m, k, v]) = SOME (mk_update m k v)
-  | mk_app _ (Sym ("pattern", _), _) = SOME mk_true
-  | mk_app (_, terms, _, _, _, _) (Sym (n, _), ts) =
-      Symtab.lookup terms n |> Option.map (fn ct => mk_fun ct ts)
+fun mk_num (_, _, _, _, _, ctxt) (i, T) =
+  mk_fun (K (I.mk_builtin_num ctxt i T)) []
+
+fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) =
+  mk_fun (fn cts =>
+    (case I.mk_builtin_fun ctxt s cts of
+      SOME ct => SOME ct
+    | NONE =>
+        Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
 
 fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
   (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
@@ -395,8 +285,9 @@
   "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
   "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
 
-fun mk_num ds = fold (fn d => fn i => i * 10 + d) ds 0
-val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> mk_num
+val digits = Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode
+val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
+  fold (fn d => fn i => i * 10 + d) ds 0)
 val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
   (fn sign => nat_num >> sign)
 
@@ -404,7 +295,8 @@
   member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
 val name = Scan.lift (Scan.many1 is_char) >> implode
 
-fun sym st = (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Sym) st
+fun sym st =
+  (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st
 
 fun id st = ($$ "#" |-- nat_num) st
 
@@ -412,29 +304,40 @@
 (* parsers for various parts of Z3 proofs *)
 
 fun sort st = Scan.first [
-  this "bool" >> K @{typ bool},
-  this "int" >> K @{typ int},
-  this "real" >> K @{typ real},
-  this "bv" |-- bra nat_num >> mk_wordT,
   this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
   par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
-  name :|-- with_context typ_of_sort] st
+  sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn
+    SOME T => Scan.succeed T
+  | 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
 
-fun number st = st |> (
-  int_num -- Scan.option ($$ "/" |-- int_num) --| this "::" :|--
-  (fn num as (n, _) =>
-    this "int" >> K (mk_int_num n) ||
-    this "real" >> K (mk_real_frac_num num)))
+fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn
+    SOME n' => Scan.succeed n'
+  | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
+
+fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn 
+    SOME app' => Scan.succeed app'
+  | NONE => scan_exn ("unknown function symbol: " ^ quote n))
+
+fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st
 
-fun bv_number st = (this "bv" |-- bra (nat_num --| $$ ":" -- nat_num) :|--
-  lookup_context (mk_bv_num o theory_of)) st
+fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
+    SOME cT => Scan.succeed cT
+  | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st
+
+fun bv_number st =
+  (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st
 
-fun appl (app as (Sym (n, _), _)) = lookup_context mk_app app :|-- (fn 
-    SOME app' => Scan.succeed app'
-  | NONE => scan_exn ("unknown function: " ^ quote n))
+fun frac_number st = (
+  int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
+    numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
+      appl (I.Sym ("/", []), [n, m])))) st
+
+fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
+
+fun number st = Scan.first [bv_number, frac_number, plain_number] st
 
 fun constant st = ((sym >> rpair []) :|-- appl) st
 
@@ -442,24 +345,27 @@
     SOME e => Scan.succeed e
   | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
 
-fun arg st = Scan.first [expr_id, number, bv_number, constant] st
+fun arg st = Scan.first [expr_id, number, constant] st
 
 fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
 
 fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
 
-fun patterns st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+
+fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
+  (the o mk_fun (K (SOME @{cterm True})))) st
 
 fun quant_kind st = st |> (
   this "forall" >> K (mk_forall o theory_of) ||
   this "exists" >> K (mk_exists o theory_of))
 
 fun quantifier st =
-  (par (quant_kind -- sep variables --| patterns -- sep arg) :|--
+  (par (quant_kind -- sep variables --| pats -- sep arg) :|--
      lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
 
 fun expr k =
-  Scan.first [bound, quantifier, application, number, bv_number, constant] :|--
+  Scan.first [bound, quantifier, pattern, application, number, constant] :|--
   with_context (pair NONE oo add_expr k)
 
 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn