avoid ML structure aliases (especially single-letter abbreviations)
authorboehmes
Mon Dec 20 22:02:57 2010 +0100 (2010-12-20)
changeset 413286792a5c92a58
parent 41327 49feace87649
child 41329 b6242168e7fa
avoid ML structure aliases (especially single-letter abbreviations)
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_model.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Dec 20 21:04:45 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Dec 20 22:02:57 2010 +0100
     1.3 @@ -17,13 +17,13 @@
     1.4    ("Tools/SMT/smt_translate.ML")
     1.5    ("Tools/SMT/smt_solver.ML")
     1.6    ("Tools/SMT/smtlib_interface.ML")
     1.7 +  ("Tools/SMT/z3_interface.ML")
     1.8    ("Tools/SMT/z3_proof_parser.ML")
     1.9    ("Tools/SMT/z3_proof_tools.ML")
    1.10    ("Tools/SMT/z3_proof_literals.ML")
    1.11    ("Tools/SMT/z3_proof_methods.ML")
    1.12    ("Tools/SMT/z3_proof_reconstruction.ML")
    1.13    ("Tools/SMT/z3_model.ML")
    1.14 -  ("Tools/SMT/z3_interface.ML")
    1.15    ("Tools/SMT/smt_setup_solvers.ML")
    1.16  begin
    1.17  
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Dec 20 21:04:45 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Mon Dec 20 22:02:57 2010 +0100
     2.3 @@ -47,15 +47,12 @@
     2.4  structure SMT_Builtin: SMT_BUILTIN =
     2.5  struct
     2.6  
     2.7 -structure U = SMT_Utils
     2.8 -structure C = SMT_Config
     2.9 -
    2.10  
    2.11  (* built-in tables *)
    2.12  
    2.13  datatype ('a, 'b) kind = Ext of 'a | Int of 'b
    2.14  
    2.15 -type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict 
    2.16 +type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Utils.dict 
    2.17  
    2.18  fun typ_ord ((T, _), (U, _)) =
    2.19    let
    2.20 @@ -68,16 +65,17 @@
    2.21    in tord (T, U) end
    2.22  
    2.23  fun insert_ttab cs T f =
    2.24 -  U.dict_map_default (cs, [])
    2.25 +  SMT_Utils.dict_map_default (cs, [])
    2.26      (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
    2.27  
    2.28  fun merge_ttab ttabp =
    2.29 -  U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
    2.30 +  SMT_Utils.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
    2.31  
    2.32  fun lookup_ttab ctxt ttab T =
    2.33    let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
    2.34    in
    2.35 -    get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt))
    2.36 +    get_first (find_first match)
    2.37 +      (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt))
    2.38    end
    2.39  
    2.40  type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
    2.41 @@ -108,7 +106,7 @@
    2.42    Builtin_Types.map (insert_ttab cs T (Int (f, g)))
    2.43  
    2.44  fun add_builtin_typ_ext (T, f) =
    2.45 -  Builtin_Types.map (insert_ttab U.basicC T (Ext f))
    2.46 +  Builtin_Types.map (insert_ttab SMT_Utils.basicC T (Ext f))
    2.47  
    2.48  fun lookup_builtin_typ ctxt =
    2.49    lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
    2.50 @@ -168,7 +166,7 @@
    2.51    in add_builtin_fun cs (c, bfun) end
    2.52  
    2.53  fun add_builtin_fun_ext ((n, T), f) =
    2.54 -  Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
    2.55 +  Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f))
    2.56  
    2.57  fun add_builtin_fun_ext' c =
    2.58    add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
     3.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 21:04:45 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 22:02:57 2010 +0100
     3.3 @@ -18,16 +18,14 @@
     3.4  structure SMT_Normalize: SMT_NORMALIZE =
     3.5  struct
     3.6  
     3.7 -structure U = SMT_Utils
     3.8 -structure B = SMT_Builtin
     3.9 -
    3.10  
    3.11  (* general theorem normalizations *)
    3.12  
    3.13  (** instantiate elimination rules **)
    3.14   
    3.15  local
    3.16 -  val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
    3.17 +  val (cpfalse, cfalse) =
    3.18 +    `SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
    3.19  
    3.20    fun inst f ct thm =
    3.21      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    3.22 @@ -70,8 +68,8 @@
    3.23    | _ => Conv.all_conv) ct
    3.24  
    3.25  val setup_atomize =
    3.26 -  fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    3.27 -    @{const_name all}, @{const_name Trueprop}]
    3.28 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    3.29 +    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    3.30  
    3.31  
    3.32  (** unfold special quantifiers **)
    3.33 @@ -100,10 +98,11 @@
    3.34  in
    3.35  
    3.36  fun unfold_special_quants_conv ctxt =
    3.37 -  U.if_exists_conv (is_some o special_quant)
    3.38 +  SMT_Utils.if_exists_conv (is_some o special_quant)
    3.39      (Conv.top_conv special_quant_conv ctxt)
    3.40  
    3.41 -val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants
    3.42 +val setup_unfolded_quants =
    3.43 +  fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants
    3.44  
    3.45  end
    3.46  
    3.47 @@ -141,7 +140,8 @@
    3.48        "must have the same kind: " ^ Syntax.string_of_term ctxt t)
    3.49  
    3.50    fun check_trigger_conv ctxt ct =
    3.51 -    if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
    3.52 +    if proper_quant false proper_trigger (SMT_Utils.term_of ct) then
    3.53 +      Conv.all_conv ct
    3.54      else check_trigger_error ctxt (Thm.term_of ct)
    3.55  
    3.56  
    3.57 @@ -169,7 +169,7 @@
    3.58    fun is_simp_lhs ctxt t =
    3.59      (case Term.strip_comb t of
    3.60        (Const c, ts as _ :: _) =>
    3.61 -        not (B.is_builtin_fun_ext ctxt c ts) andalso
    3.62 +        not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
    3.63          forall (is_constr_pat (ProofContext.theory_of ctxt)) ts
    3.64      | _ => false)
    3.65  
    3.66 @@ -194,8 +194,9 @@
    3.67              Pattern.matches thy (t', u) andalso not (t aconv u))
    3.68          in not (Term.exists_subterm some_match u) end
    3.69  
    3.70 -  val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1
    3.71 -  fun mk_pat ct = Thm.capply (U.instT' ct pat) ct
    3.72 +  val pat =
    3.73 +    SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
    3.74 +  fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
    3.75  
    3.76    fun mk_clist T = pairself (Thm.cterm_of @{theory})
    3.77      (HOLogic.cons_const T, HOLogic.nil_const T)
    3.78 @@ -231,20 +232,24 @@
    3.79      | has_trigger _ = false
    3.80  
    3.81    fun try_trigger_conv cv ct =
    3.82 -    if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
    3.83 +    if SMT_Utils.under_quant has_trigger (SMT_Utils.term_of ct) then
    3.84 +      Conv.all_conv ct
    3.85      else Conv.try_conv cv ct
    3.86  
    3.87    fun infer_trigger_conv ctxt =
    3.88      if Config.get ctxt SMT_Config.infer_triggers then
    3.89 -      try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    3.90 +      try_trigger_conv
    3.91 +        (SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    3.92      else Conv.all_conv
    3.93  in
    3.94  
    3.95  fun trigger_conv ctxt =
    3.96 -  U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    3.97 +  SMT_Utils.prop_conv
    3.98 +    (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    3.99  
   3.100 -val setup_trigger = fold B.add_builtin_fun_ext''
   3.101 -  [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   3.102 +val setup_trigger =
   3.103 +  fold SMT_Builtin.add_builtin_fun_ext''
   3.104 +    [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   3.105  
   3.106  end
   3.107  
   3.108 @@ -272,7 +277,8 @@
   3.109        Syntax.string_of_term ctxt t)
   3.110  
   3.111    fun check_weight_conv ctxt ct =
   3.112 -    if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
   3.113 +    if SMT_Utils.under_quant proper_trigger (SMT_Utils.term_of ct) then
   3.114 +      Conv.all_conv ct
   3.115      else check_weight_error ctxt (Thm.term_of ct)
   3.116  
   3.117  
   3.118 @@ -294,13 +300,14 @@
   3.119    fun add_weight_conv NONE _ = Conv.all_conv
   3.120      | add_weight_conv (SOME weight) ctxt =
   3.121          let val cv = Conv.rewr_conv (mk_weight_eq weight)
   3.122 -        in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   3.123 +        in SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   3.124  in
   3.125  
   3.126  fun weight_conv weight ctxt = 
   3.127 -  U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   3.128 +  SMT_Utils.prop_conv
   3.129 +    (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   3.130  
   3.131 -val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight}
   3.132 +val setup_weight = SMT_Builtin.add_builtin_fun_ext'' @{const_name SMT.weight}
   3.133  
   3.134  end
   3.135  
   3.136 @@ -355,11 +362,12 @@
   3.137      "distinct [x, y] = (x ~= y)"
   3.138      by simp_all}
   3.139    fun distinct_conv _ =
   3.140 -    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
   3.141 +    SMT_Utils.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
   3.142  in
   3.143  
   3.144 -fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct
   3.145 -  (Conv.top_conv distinct_conv ctxt)
   3.146 +fun trivial_distinct_conv ctxt =
   3.147 +  SMT_Utils.if_exists_conv is_trivial_distinct
   3.148 +    (Conv.top_conv distinct_conv ctxt)
   3.149  
   3.150  end
   3.151  
   3.152 @@ -373,13 +381,14 @@
   3.153    val thm = mk_meta_eq @{lemma
   3.154      "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
   3.155  
   3.156 -  fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
   3.157 +  fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
   3.158  in
   3.159  
   3.160 -fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case
   3.161 -  (Conv.top_conv unfold_conv ctxt)
   3.162 +fun rewrite_bool_case_conv ctxt =
   3.163 +  SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
   3.164  
   3.165 -val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   3.166 +val setup_bool_case =
   3.167 +  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   3.168  
   3.169  end
   3.170  
   3.171 @@ -400,7 +409,8 @@
   3.172    val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   3.173      (@{const_name abs}, abs_def)]
   3.174  
   3.175 -  fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T)
   3.176 +  fun is_builtinT ctxt T =
   3.177 +    SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
   3.178  
   3.179    fun abs_min_max ctxt (Const (n, T)) =
   3.180          (case AList.lookup (op =) defs n of
   3.181 @@ -415,10 +425,10 @@
   3.182  in
   3.183  
   3.184  fun unfold_abs_min_max_conv ctxt =
   3.185 -  U.if_exists_conv (is_some o abs_min_max ctxt)
   3.186 +  SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt)
   3.187      (Conv.top_conv unfold_amm_conv ctxt)
   3.188    
   3.189 -val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs
   3.190 +val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) defs
   3.191  
   3.192  end
   3.193  
   3.194 @@ -482,7 +492,7 @@
   3.195  
   3.196    fun mk_number_eq ctxt i lhs =
   3.197      let
   3.198 -      val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   3.199 +      val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   3.200        val ss = HOL_ss
   3.201          addsimps [@{thm Nat_Numeral.int_nat_number_of}]
   3.202          addsimps @{thms neg_simps}
   3.203 @@ -508,11 +518,11 @@
   3.204    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
   3.205  
   3.206    and expand_conv ctxt =
   3.207 -    U.if_conv (is_nat_const o Term.head_of)
   3.208 +    SMT_Utils.if_conv (is_nat_const o Term.head_of)
   3.209        (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
   3.210        (int_conv ctxt)
   3.211  
   3.212 -  and nat_conv ctxt = U.if_exists_conv is_nat_const'
   3.213 +  and nat_conv ctxt = SMT_Utils.if_exists_conv is_nat_const'
   3.214      (Conv.top_sweep_conv expand_conv ctxt)
   3.215  
   3.216    val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
   3.217 @@ -525,8 +535,8 @@
   3.218    else (thms, [])
   3.219  
   3.220  val setup_nat_as_int =
   3.221 -  B.add_builtin_typ_ext (@{typ nat}, K true) #>
   3.222 -  fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
   3.223 +  SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
   3.224 +  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
   3.225  
   3.226  end
   3.227  
   3.228 @@ -542,7 +552,7 @@
   3.229  
   3.230    fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
   3.231          (case try HOLogic.dest_number t of
   3.232 -          SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2
   3.233 +          SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
   3.234          | NONE => false)
   3.235      | is_strange_number _ _ = false
   3.236  
   3.237 @@ -558,12 +568,14 @@
   3.238        "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
   3.239        by simp_all (simp add: pred_def)}
   3.240  
   3.241 -  fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt)
   3.242 -    (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   3.243 +  fun norm_num_conv ctxt =
   3.244 +    SMT_Utils.if_conv (is_strange_number ctxt)
   3.245 +      (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   3.246  in
   3.247  
   3.248 -fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt)
   3.249 -  (Conv.top_sweep_conv norm_num_conv ctxt)
   3.250 +fun normalize_numerals_conv ctxt =
   3.251 +  SMT_Utils.if_exists_conv (is_strange_number ctxt)
   3.252 +    (Conv.top_sweep_conv norm_num_conv ctxt)
   3.253  
   3.254  end
   3.255  
   3.256 @@ -599,18 +611,19 @@
   3.257  
   3.258  structure Extra_Norms = Generic_Data
   3.259  (
   3.260 -  type T = extra_norm U.dict
   3.261 +  type T = extra_norm SMT_Utils.dict
   3.262    val empty = []
   3.263    val extend = I
   3.264 -  fun merge data = U.dict_merge fst data
   3.265 +  fun merge data = SMT_Utils.dict_merge fst data
   3.266  )
   3.267  
   3.268 -fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
   3.269 +fun add_extra_norm (cs, norm) =
   3.270 +  Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
   3.271  
   3.272  fun apply_extra_norms ithms ctxt =
   3.273    let
   3.274      val cs = SMT_Config.solver_class_of ctxt
   3.275 -    val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   3.276 +    val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   3.277    in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
   3.278  
   3.279  fun normalize iwthms ctxt =
     4.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 20 21:04:45 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 20 22:02:57 2010 +0100
     4.3 @@ -51,8 +51,6 @@
     4.4  structure SMT_Solver: SMT_SOLVER =
     4.5  struct
     4.6  
     4.7 -structure C = SMT_Config
     4.8 -
     4.9  
    4.10  (* configuration *)
    4.11  
    4.12 @@ -109,13 +107,13 @@
    4.13    [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
    4.14  
    4.15  fun run ctxt cmd args input =
    4.16 -  (case C.certificates_of ctxt of
    4.17 +  (case SMT_Config.certificates_of ctxt of
    4.18      NONE =>
    4.19 -      if Config.get ctxt C.debug_files = "" then
    4.20 +      if Config.get ctxt SMT_Config.debug_files = "" then
    4.21          Cache_IO.run (make_cmd (choose cmd) args) input
    4.22        else
    4.23          let
    4.24 -          val base_path = Path.explode (Config.get ctxt C.debug_files)
    4.25 +          val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
    4.26            val in_path = Path.ext "smt_in" base_path
    4.27            val out_path = Path.ext "smt_out" base_path
    4.28          in
    4.29 @@ -124,7 +122,7 @@
    4.30    | SOME certs =>
    4.31        (case Cache_IO.lookup certs input of
    4.32          (NONE, key) =>
    4.33 -          if Config.get ctxt C.fixed then
    4.34 +          if Config.get ctxt SMT_Config.fixed then
    4.35              error ("Bad certificates cache: missing certificate")
    4.36            else
    4.37              Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
    4.38 @@ -140,14 +138,14 @@
    4.39      fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
    4.40        (map Pretty.str ls))
    4.41  
    4.42 -    val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
    4.43 +    val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
    4.44  
    4.45      val {redirected_output=res, output=err, return_code} =
    4.46 -      C.with_timeout ctxt (run ctxt cmd args) input
    4.47 -    val _ = C.trace_msg ctxt (pretty "Solver:") err
    4.48 +      SMT_Config.with_timeout ctxt (run ctxt cmd args) input
    4.49 +    val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
    4.50  
    4.51      val ls = rev (snd (chop_while (equal "") (rev res)))
    4.52 -    val _ = C.trace_msg ctxt (pretty "Result:") ls
    4.53 +    val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
    4.54  
    4.55      val _ = null ls andalso return_code <> 0 andalso
    4.56        raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
    4.57 @@ -155,8 +153,9 @@
    4.58  
    4.59  end
    4.60  
    4.61 -fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
    4.62 -  Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
    4.63 +fun trace_assms ctxt =
    4.64 +  SMT_Config.trace_msg ctxt (Pretty.string_of o
    4.65 +    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
    4.66  
    4.67  fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) =
    4.68    let
    4.69 @@ -164,7 +163,7 @@
    4.70      fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
    4.71      fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
    4.72    in
    4.73 -    C.trace_msg ctxt (fn () =>
    4.74 +    SMT_Config.trace_msg ctxt (fn () =>
    4.75        Pretty.string_of (Pretty.big_list "Names:" [
    4.76          Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
    4.77          Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
    4.78 @@ -172,10 +171,11 @@
    4.79  
    4.80  fun invoke name cmd options ithms ctxt =
    4.81    let
    4.82 -    val args = C.solver_options_of ctxt @ options ctxt
    4.83 +    val args = SMT_Config.solver_options_of ctxt @ options ctxt
    4.84      val comments = ("solver: " ^ name) ::
    4.85 -      ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
    4.86 -      ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
    4.87 +      ("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) ::
    4.88 +      ("random seed: " ^
    4.89 +        string_of_int (Config.get ctxt SMT_Config.random_seed)) ::
    4.90        "arguments:" :: args
    4.91  
    4.92      val (str, recon as {context=ctxt', ...}) =
    4.93 @@ -192,7 +192,7 @@
    4.94        |> filter (fn i => i >= 0)
    4.95        |> map_filter (AList.lookup (op =) iwthms)
    4.96    in
    4.97 -    if Config.get ctxt C.trace_used_facts andalso length wthms > 0
    4.98 +    if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0
    4.99      then
   4.100        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   4.101          (map (Display.pretty_thm ctxt o snd) wthms)))
   4.102 @@ -243,7 +243,7 @@
   4.103        (output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) =
   4.104      (case outcome output of
   4.105        (Unsat, ls) =>
   4.106 -        if not (Config.get ctxt C.oracle) andalso is_some reconstruct
   4.107 +        if not (Config.get ctxt SMT_Config.oracle) andalso is_some reconstruct
   4.108          then the reconstruct outer_ctxt recon ls
   4.109          else ([], ocl ())
   4.110      | (result, ls) =>
   4.111 @@ -273,7 +273,7 @@
   4.112    in
   4.113      Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
   4.114      Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
   4.115 -    Context.theory_map (C.add_solver (name, class))
   4.116 +    Context.theory_map (SMT_Config.add_solver (name, class))
   4.117    end
   4.118  
   4.119  end
   4.120 @@ -282,7 +282,7 @@
   4.121    the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
   4.122  
   4.123  fun name_and_solver_of ctxt =
   4.124 -  let val name = C.solver_of ctxt
   4.125 +  let val name = SMT_Config.solver_of ctxt
   4.126    in (name, get_info ctxt name) end
   4.127  
   4.128  val solver_name_of = fst o name_and_solver_of
   4.129 @@ -326,9 +326,9 @@
   4.130    let
   4.131      val ctxt =
   4.132        Proof.context_of st
   4.133 -      |> Config.put C.oracle false
   4.134 -      |> Config.put C.drop_bad_facts true
   4.135 -      |> Config.put C.filter_only_facts true
   4.136 +      |> Config.put SMT_Config.oracle false
   4.137 +      |> Config.put SMT_Config.drop_bad_facts true
   4.138 +      |> Config.put SMT_Config.filter_only_facts true
   4.139  
   4.140      val {facts, goal, ...} = Proof.goal st
   4.141      val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
   4.142 @@ -348,7 +348,7 @@
   4.143  fun smt_filter_tail time_limit run_remote
   4.144      ((xs, wthms), ((iwthms', ctxt), iwthms)) =
   4.145    let
   4.146 -    val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit)
   4.147 +    val ctxt = ctxt |> Config.put SMT_Config.timeout (Time.toReal time_limit)
   4.148      val xrules = xs ~~ map snd wthms
   4.149    in
   4.150      ((iwthms', ctxt), iwthms)
   4.151 @@ -369,15 +369,16 @@
   4.152    THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
   4.153      let
   4.154        val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort
   4.155 -      val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
   4.156 +      val tag = "Solver " ^ SMT_Config.solver_of ctxt' ^ ": "
   4.157        val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
   4.158        fun safe_solve iwthms =
   4.159          if pass_exns then SOME (solve iwthms)
   4.160          else (SOME (solve iwthms)
   4.161            handle
   4.162              SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
   4.163 -              (C.verbose_msg ctxt' str_of fail; NONE)
   4.164 -          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
   4.165 +              (SMT_Config.verbose_msg ctxt' str_of fail; NONE)
   4.166 +          | SMT_Failure.SMT fail =>
   4.167 +              (SMT_Config.trace_msg ctxt' str_of fail; NONE))
   4.168      in
   4.169        safe_solve (map (pair ~1 o pair NONE) (rules @ prems))
   4.170        |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
     5.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 20 21:04:45 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Dec 20 22:02:57 2010 +0100
     5.3 @@ -45,9 +45,6 @@
     5.4  structure SMT_Translate: SMT_TRANSLATE =
     5.5  struct
     5.6  
     5.7 -structure U = SMT_Utils
     5.8 -structure B = SMT_Builtin
     5.9 -
    5.10  
    5.11  (* intermediate term structure *)
    5.12  
    5.13 @@ -169,7 +166,7 @@
    5.14      in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
    5.15  
    5.16    fun expf k i T t =
    5.17 -    let val Ts = drop i (fst (U.dest_funT k T))
    5.18 +    let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
    5.19      in
    5.20        Term.incr_boundvars (length Ts) t
    5.21        |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
    5.22 @@ -195,7 +192,7 @@
    5.23        | expand t =
    5.24            (case Term.strip_comb t of
    5.25              (u as Const (c as (_, T)), ts) =>
    5.26 -              (case B.dest_builtin ctxt c ts of
    5.27 +              (case SMT_Builtin.dest_builtin ctxt c ts of
    5.28                  SOME (_, k, us, mk) =>
    5.29                    if k = length us then mk (map expand us)
    5.30                    else expf k (length ts) T (mk (map expand us))
    5.31 @@ -302,8 +299,10 @@
    5.32      (Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T)
    5.33  
    5.34    fun apply i t T ts =
    5.35 -    let val (ts1, ts2) = chop i ts
    5.36 -    in fst (fold app ts2 (Term.list_comb (t, ts1), snd (U.dest_funT i T))) end
    5.37 +    let
    5.38 +      val (ts1, ts2) = chop i ts
    5.39 +      val (_, U) = SMT_Utils.dest_funT i T
    5.40 +    in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
    5.41  in
    5.42  
    5.43  fun intro_explicit_application ts =
    5.44 @@ -351,14 +350,14 @@
    5.45      @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
    5.46  
    5.47    fun is_builtin_conn_or_pred ctxt c ts =
    5.48 -    is_some (B.dest_builtin_conn ctxt c ts) orelse
    5.49 -    is_some (B.dest_builtin_pred ctxt c ts)
    5.50 +    is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
    5.51 +    is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
    5.52  
    5.53    fun builtin b ctxt c ts =
    5.54      (case (Const c, ts) of
    5.55        (@{const HOL.eq (bool)}, [t, u]) =>
    5.56          if t = @{const SMT.term_true} orelse u = @{const SMT.term_true} then
    5.57 -          B.dest_builtin_eq ctxt t u
    5.58 +          SMT_Builtin.dest_builtin_eq ctxt t u
    5.59          else b ctxt c ts
    5.60      | _ => b ctxt c ts)
    5.61  in
    5.62 @@ -400,16 +399,16 @@
    5.63              q $ Abs (n, T, in_trigger u)
    5.64            else as_term (in_term t)
    5.65        | (Const c, ts) =>
    5.66 -          (case B.dest_builtin_conn ctxt c ts of
    5.67 +          (case SMT_Builtin.dest_builtin_conn ctxt c ts of
    5.68              SOME (_, _, us, mk) => mk (map in_form us)
    5.69            | NONE =>
    5.70 -              (case B.dest_builtin_pred ctxt c ts of
    5.71 +              (case SMT_Builtin.dest_builtin_pred ctxt c ts of
    5.72                  SOME (_, _, us, mk) => mk (map in_term us)
    5.73                | NONE => as_term (in_term t)))
    5.74        | _ => as_term (in_term t))
    5.75    in
    5.76      map (reduce_let #> in_form) #>
    5.77 -    cons (U.prop_of term_bool) #>
    5.78 +    cons (SMT_Utils.prop_of term_bool) #>
    5.79      pair (fol_rules, [term_bool], builtin)
    5.80    end
    5.81  
    5.82 @@ -466,7 +465,7 @@
    5.83      fun transT (T as TFree _) = add_typ T true
    5.84        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
    5.85        | transT (T as Type _) =
    5.86 -          (case B.dest_builtin_typ ctxt T of
    5.87 +          (case SMT_Builtin.dest_builtin_typ ctxt T of
    5.88              SOME n => pair n
    5.89            | NONE => add_typ T true)
    5.90  
    5.91 @@ -492,7 +491,7 @@
    5.92        | _ => raise TERM ("bad SMT term", [t]))
    5.93   
    5.94      and transs t T ts =
    5.95 -      let val (Us, U) = U.dest_funT (length ts) T
    5.96 +      let val (Us, U) = SMT_Utils.dest_funT (length ts) T
    5.97        in
    5.98          fold_map transT Us ##>> transT U #-> (fn Up =>
    5.99          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
   5.100 @@ -507,21 +506,21 @@
   5.101  
   5.102  structure Configs = Generic_Data
   5.103  (
   5.104 -  type T = (Proof.context -> config) U.dict
   5.105 +  type T = (Proof.context -> config) SMT_Utils.dict
   5.106    val empty = []
   5.107    val extend = I
   5.108 -  fun merge data = U.dict_merge fst data
   5.109 +  fun merge data = SMT_Utils.dict_merge fst data
   5.110  )
   5.111  
   5.112 -fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
   5.113 +fun add_config (cs, cfg) = Configs.map (SMT_Utils.dict_update (cs, cfg))
   5.114  
   5.115  fun get_config ctxt = 
   5.116    let val cs = SMT_Config.solver_class_of ctxt
   5.117    in
   5.118 -    (case U.dict_get (Configs.get (Context.Proof ctxt)) cs of
   5.119 +    (case SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of
   5.120        SOME cfg => cfg ctxt
   5.121      | NONE => error ("SMT: no translation configuration found " ^
   5.122 -        "for solver class " ^ quote (U.string_of_class cs)))
   5.123 +        "for solver class " ^ quote (SMT_Utils.string_of_class cs)))
   5.124    end
   5.125  
   5.126  fun translate ctxt comments ithms =
   5.127 @@ -533,7 +532,7 @@
   5.128  
   5.129      fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
   5.130  
   5.131 -    val ts1 = map (Envir.beta_eta_contract o U.prop_of o snd) ithms
   5.132 +    val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms
   5.133  
   5.134      val ((dtyps, tr_context, ctxt1), ts2) =
   5.135        ((make_tr_context prefixes, ctxt), ts1)
   5.136 @@ -551,7 +550,7 @@
   5.137      val rewrite_rules' = fun_app_eq :: rewrite_rules
   5.138    in
   5.139      (ts4, tr_context)
   5.140 -    |-> intermediate header dtyps (builtin B.dest_builtin) ctxt2
   5.141 +    |-> intermediate header dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
   5.142      |>> uncurry (serialize comments)
   5.143      ||> recon_of ctxt2 rewrite_rules' extra_thms ithms
   5.144    end
     6.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 20 21:04:45 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Dec 20 22:02:57 2010 +0100
     6.3 @@ -16,10 +16,6 @@
     6.4  structure SMTLIB_Interface: SMTLIB_INTERFACE =
     6.5  struct
     6.6  
     6.7 -structure U = SMT_Utils
     6.8 -structure B = SMT_Builtin
     6.9 -structure N = SMT_Normalize
    6.10 -structure T = SMT_Translate
    6.11  
    6.12  val smtlibC = ["smtlib"]
    6.13  
    6.14 @@ -29,8 +25,8 @@
    6.15  local
    6.16    fun int_num _ i = SOME (string_of_int i)
    6.17  
    6.18 -  fun is_linear [t] = U.is_number t
    6.19 -    | is_linear [t, u] = U.is_number t orelse U.is_number u
    6.20 +  fun is_linear [t] = SMT_Utils.is_number t
    6.21 +    | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u
    6.22      | is_linear _ = false
    6.23  
    6.24    fun times _ _ ts =
    6.25 @@ -49,8 +45,8 @@
    6.26  in
    6.27  
    6.28  val setup_builtins =
    6.29 -  B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
    6.30 -  fold (B.add_builtin_fun' smtlibC) [
    6.31 +  SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
    6.32 +  fold (SMT_Builtin.add_builtin_fun' smtlibC) [
    6.33      (@{const True}, "true"),
    6.34      (@{const False}, "false"),
    6.35      (@{const Not}, "not"),
    6.36 @@ -66,8 +62,10 @@
    6.37      (@{const uminus (int)}, "~"),
    6.38      (@{const plus (int)}, "+"),
    6.39      (@{const minus (int)}, "-") ] #>
    6.40 -  B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #>
    6.41 -  B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
    6.42 +  SMT_Builtin.add_builtin_fun smtlibC
    6.43 +    (Term.dest_Const @{const times (int)}, times) #>
    6.44 +  SMT_Builtin.add_builtin_fun smtlibC
    6.45 +    (Term.dest_Const @{const distinct ('a)}, distinct)
    6.46  
    6.47  end
    6.48  
    6.49 @@ -106,18 +104,20 @@
    6.50  
    6.51  fun var i = add "?v" #> add (string_of_int i)
    6.52  
    6.53 -fun sterm l (T.SVar i) = sep (var (l - i - 1))
    6.54 -  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
    6.55 -  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
    6.56 -  | sterm l (T.SQua (q, ss, ps, w, t)) =
    6.57 +fun sterm l (SMT_Translate.SVar i) = sep (var (l - i - 1))
    6.58 +  | sterm l (SMT_Translate.SApp (n, ts)) = app n (sterm l) ts
    6.59 +  | sterm _ (SMT_Translate.SLet _) =
    6.60 +      raise Fail "SMT-LIB: unsupported let expression"
    6.61 +  | sterm l (SMT_Translate.SQua (q, ss, ps, w, t)) =
    6.62        let
    6.63 -        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
    6.64 +        fun quant SMT_Translate.SForall = add "forall"
    6.65 +          | quant SMT_Translate.SExists = add "exists"
    6.66          val vs = map_index (apfst (Integer.add l)) ss
    6.67          fun var_decl (i, s) = par (var i #> sep (add s))
    6.68          val sub = sterm (l + length ss)
    6.69          fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
    6.70 -        fun pats (T.SPat ts) = pat ":pat" ts
    6.71 -          | pats (T.SNoPat ts) = pat ":nopat" ts
    6.72 +        fun pats (SMT_Translate.SPat ts) = pat ":pat" ts
    6.73 +          | pats (SMT_Translate.SNoPat ts) = pat ":nopat" ts
    6.74          fun weight NONE = I
    6.75            | weight (SOME i) =
    6.76                sep (add ":weight { " #> add (string_of_int i) #> add " }")
    6.77 @@ -168,6 +168,6 @@
    6.78  
    6.79  val setup = Context.theory_map (
    6.80    setup_builtins #>
    6.81 -  T.add_config (smtlibC, translate_config))
    6.82 +  SMT_Translate.add_config (smtlibC, translate_config))
    6.83  
    6.84  end
     7.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Mon Dec 20 21:04:45 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Dec 20 22:02:57 2010 +0100
     7.3 @@ -13,8 +13,6 @@
     7.4  structure Z3_Model: Z3_MODEL =
     7.5  struct
     7.6  
     7.7 -structure U = SMT_Utils
     7.8 -
     7.9  
    7.10  (* counterexample expressions *)
    7.11  
    7.12 @@ -125,7 +123,7 @@
    7.13    | trans_expr T (Value i) = pair (Var (("value", i), T))
    7.14    | trans_expr T (Array a) = trans_array T a
    7.15    | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
    7.16 -      let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
    7.17 +      let val Ts = fst (SMT_Utils.dest_funT (length es') (Term.fastype_of t))
    7.18        in
    7.19          fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
    7.20        end)
    7.21 @@ -167,7 +165,7 @@
    7.22  fun translate ((t, k), (e, cs)) =
    7.23    let
    7.24      val T = Term.fastype_of t
    7.25 -    val (Us, U) = U.dest_funT k (Term.fastype_of t)
    7.26 +    val (Us, U) = SMT_Utils.dest_funT k (Term.fastype_of t)
    7.27  
    7.28      fun mk_full_def u' pats =
    7.29        pats
     8.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Mon Dec 20 21:04:45 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Mon Dec 20 22:02:57 2010 +0100
     8.3 @@ -33,19 +33,17 @@
     8.4  structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
     8.5  struct
     8.6  
     8.7 -structure U = SMT_Utils
     8.8 -structure T = Z3_Proof_Tools
     8.9 -
    8.10  
    8.11  
    8.12  (* literal table *)
    8.13  
    8.14  type littab = thm Termtab.table
    8.15  
    8.16 -fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
    8.17 +fun make_littab thms =
    8.18 +  fold (Termtab.update o `SMT_Utils.prop_of) thms Termtab.empty
    8.19  
    8.20 -fun insert_lit thm = Termtab.update (`U.prop_of thm)
    8.21 -fun delete_lit thm = Termtab.delete (U.prop_of thm)
    8.22 +fun insert_lit thm = Termtab.update (`SMT_Utils.prop_of thm)
    8.23 +fun delete_lit thm = Termtab.delete (SMT_Utils.prop_of thm)
    8.24  fun lookup_lit lits = Termtab.lookup lits
    8.25  fun get_first_lit f =
    8.26    Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
    8.27 @@ -93,18 +91,20 @@
    8.28  (** explosion of conjunctions and disjunctions **)
    8.29  
    8.30  local
    8.31 +  val precomp = Z3_Proof_Tools.precompose2
    8.32 +
    8.33    fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
    8.34 -  val dest_conj1 = T.precompose2 destc @{thm conjunct1}
    8.35 -  val dest_conj2 = T.precompose2 destc @{thm conjunct2}
    8.36 +  val dest_conj1 = precomp destc @{thm conjunct1}
    8.37 +  val dest_conj2 = precomp destc @{thm conjunct2}
    8.38    fun dest_conj_rules t =
    8.39      dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
    8.40      
    8.41    fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
    8.42    val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
    8.43 -  val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
    8.44 -  val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
    8.45 -  val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
    8.46 -  val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
    8.47 +  val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
    8.48 +  val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
    8.49 +  val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
    8.50 +  val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
    8.51  
    8.52    fun dest_disj_rules t =
    8.53      (case dest_disj_term' is_neg t of
    8.54 @@ -115,7 +115,7 @@
    8.55      | NONE => NONE)
    8.56  
    8.57    fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
    8.58 -  val dneg_rule = T.precompose destn @{thm notnotD}
    8.59 +  val dneg_rule = Z3_Proof_Tools.precompose destn @{thm notnotD}
    8.60  in
    8.61  
    8.62  (*
    8.63 @@ -150,7 +150,7 @@
    8.64  (*
    8.65    extract a literal by applying previously collected rules
    8.66  *)
    8.67 -fun extract_lit thm rules = fold T.compose rules thm
    8.68 +fun extract_lit thm rules = fold Z3_Proof_Tools.compose rules thm
    8.69  
    8.70  
    8.71  (*
    8.72 @@ -162,9 +162,9 @@
    8.73      val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
    8.74  
    8.75      fun explode1 thm =
    8.76 -      if Termtab.defined tab (U.prop_of thm) then cons thm
    8.77 +      if Termtab.defined tab (SMT_Utils.prop_of thm) then cons thm
    8.78        else
    8.79 -        (case dest_rules (U.prop_of thm) of
    8.80 +        (case dest_rules (SMT_Utils.prop_of thm) of
    8.81            SOME (rule1, rule2) =>
    8.82              explode2 rule1 thm #>
    8.83              explode2 rule2 thm #>
    8.84 @@ -172,13 +172,14 @@
    8.85          | NONE => cons thm)
    8.86  
    8.87      and explode2 dest_rule thm =
    8.88 -      if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm)
    8.89 -      then explode1 (T.compose dest_rule thm)
    8.90 -      else cons (T.compose dest_rule thm)
    8.91 +      if full orelse
    8.92 +        exists_lit is_conj (Termtab.defined tab) (SMT_Utils.prop_of thm)
    8.93 +      then explode1 (Z3_Proof_Tools.compose dest_rule thm)
    8.94 +      else cons (Z3_Proof_Tools.compose dest_rule thm)
    8.95  
    8.96      fun explode0 thm =
    8.97 -      if not is_conj andalso is_dneg (U.prop_of thm)
    8.98 -      then [T.compose dneg_rule thm]
    8.99 +      if not is_conj andalso is_dneg (SMT_Utils.prop_of thm)
   8.100 +      then [Z3_Proof_Tools.compose dneg_rule thm]
   8.101        else explode1 thm []
   8.102  
   8.103    in explode0 end
   8.104 @@ -195,7 +196,7 @@
   8.105    fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
   8.106    fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
   8.107      Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
   8.108 -    |> T.discharge thm1 |> T.discharge thm2
   8.109 +    |> Z3_Proof_Tools.discharge thm1 |> Z3_Proof_Tools.discharge thm2
   8.110  
   8.111    fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
   8.112  
   8.113 @@ -219,13 +220,15 @@
   8.114    fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
   8.115      | dest_disj t = raise TERM ("dest_disj", [t])
   8.116  
   8.117 -  val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
   8.118 -  val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
   8.119 +  val precomp = Z3_Proof_Tools.precompose
   8.120 +  val dnegE = precomp (single o d2 o d1) @{thm notnotD}
   8.121 +  val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
   8.122    fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
   8.123  
   8.124 +  val precomp2 = Z3_Proof_Tools.precompose2
   8.125    fun dni f = apsnd f o Thm.dest_binop o f o d1
   8.126 -  val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
   8.127 -  val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
   8.128 +  val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
   8.129 +  val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
   8.130    val iff_const = @{const HOL.eq (bool)}
   8.131    fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
   8.132          f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
   8.133 @@ -241,16 +244,17 @@
   8.134  
   8.135      fun lookup_rule t =
   8.136        (case t of
   8.137 -        @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
   8.138 +        @{const Not} $ (@{const Not} $ t) =>
   8.139 +          (Z3_Proof_Tools.compose dnegI, lookup t)
   8.140        | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
   8.141 -            (T.compose negIffI, lookup (iff_const $ u $ t))
   8.142 +          (Z3_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t))
   8.143        | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
   8.144            let fun rewr lit = lit COMP @{thm not_sym}
   8.145            in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
   8.146        | _ =>
   8.147            (case as_dneg lookup t of
   8.148 -            NONE => (T.compose negIffE, as_negIff lookup t)
   8.149 -          | x => (T.compose dnegE, x)))
   8.150 +            NONE => (Z3_Proof_Tools.compose negIffE, as_negIff lookup t)
   8.151 +          | x => (Z3_Proof_Tools.compose dnegE, x)))
   8.152  
   8.153      fun join1 (s, t) =
   8.154        (case lookup t of
   8.155 @@ -285,7 +289,7 @@
   8.156    val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
   8.157    fun contra_left conj thm =
   8.158      let
   8.159 -      val rules = explode_term conj (U.prop_of thm)
   8.160 +      val rules = explode_term conj (SMT_Utils.prop_of thm)
   8.161        fun contra_lits (t, rs) =
   8.162          (case t of
   8.163            @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
   8.164 @@ -303,7 +307,8 @@
   8.165    fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
   8.166  in
   8.167  fun contradict conj ct =
   8.168 -  iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct)
   8.169 +  iff_intro (Z3_Proof_Tools.under_assumption (contra_left conj) ct)
   8.170 +    (contra_right ct)
   8.171  end
   8.172  
   8.173  
   8.174 @@ -314,8 +319,8 @@
   8.175        fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
   8.176        fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
   8.177  
   8.178 -      val thm1 = T.under_assumption (prove r cr o make_tab l) cl
   8.179 -      val thm2 = T.under_assumption (prove l cl o make_tab r) cr
   8.180 +      val thm1 = Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
   8.181 +      val thm2 = Z3_Proof_Tools.under_assumption (prove l cl o make_tab r) cr
   8.182      in iff_intro thm1 thm2 end
   8.183  
   8.184    datatype conj_disj = CONJ | DISJ | NCON | NDIS
     9.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Dec 20 21:04:45 2010 +0100
     9.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Dec 20 22:02:57 2010 +0100
     9.3 @@ -12,9 +12,6 @@
     9.4  structure Z3_Proof_Methods: Z3_PROOF_METHODS =
     9.5  struct
     9.6  
     9.7 -structure U = SMT_Utils
     9.8 -structure T = Z3_Proof_Tools
     9.9 -
    9.10  
    9.11  fun apply tac st =
    9.12    (case Seq.pull (tac 1 st) of
    9.13 @@ -36,24 +33,24 @@
    9.14  
    9.15  fun mk_inv_of ctxt ct =
    9.16    let
    9.17 -    val (dT, rT) = Term.dest_funT (U.typ_of ct)
    9.18 -    val inv = U.certify ctxt (mk_inv_into dT rT)
    9.19 -    val univ = U.certify ctxt (mk_univ dT)
    9.20 +    val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
    9.21 +    val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT)
    9.22 +    val univ = SMT_Utils.certify ctxt (mk_univ dT)
    9.23    in Thm.mk_binop inv univ ct end
    9.24  
    9.25  fun mk_inj_prop ctxt ct =
    9.26    let
    9.27 -    val (dT, rT) = Term.dest_funT (U.typ_of ct)
    9.28 -    val inj = U.certify ctxt (mk_inj_on dT rT)
    9.29 -    val univ = U.certify ctxt (mk_univ dT)
    9.30 -  in U.mk_cprop (Thm.mk_binop inj ct univ) end
    9.31 +    val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
    9.32 +    val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT)
    9.33 +    val univ = SMT_Utils.certify ctxt (mk_univ dT)
    9.34 +  in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
    9.35  
    9.36  
    9.37  val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
    9.38  
    9.39  fun prove_inj_prop ctxt def lhs =
    9.40    let
    9.41 -    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
    9.42 +    val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
    9.43      val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
    9.44    in
    9.45      Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
    9.46 @@ -64,7 +61,7 @@
    9.47    end
    9.48  
    9.49  fun prove_rhs ctxt def lhs =
    9.50 -  T.by_tac (
    9.51 +  Z3_Proof_Tools.by_tac (
    9.52      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    9.53      THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
    9.54      THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
    9.55 @@ -82,24 +79,27 @@
    9.56  fun prove_lhs ctxt rhs =
    9.57    let
    9.58      val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
    9.59 +    val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
    9.60    in
    9.61 -    T.by_tac (
    9.62 -      CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
    9.63 +    Z3_Proof_Tools.by_tac (
    9.64 +      CONVERSION (SMT_Utils.prop_conv conv)
    9.65        THEN' Simplifier.simp_tac HOL_ss)
    9.66    end
    9.67  
    9.68  
    9.69  fun mk_inv_def ctxt rhs =
    9.70    let
    9.71 -    val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
    9.72 +    val (ct, ctxt') =
    9.73 +      SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
    9.74      val (cl, cv) = Thm.dest_binop ct
    9.75      val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
    9.76      val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
    9.77 -  in Thm.assume (U.mk_cequals cg cu) end
    9.78 +  in Thm.assume (SMT_Utils.mk_cequals cg cu) end
    9.79  
    9.80  fun prove_inj_eq ctxt ct =
    9.81    let
    9.82 -    val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
    9.83 +    val (lhs, rhs) =
    9.84 +      pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct))
    9.85      val lhs_thm = prove_lhs ctxt rhs lhs
    9.86      val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
    9.87    in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
    9.88 @@ -109,22 +109,22 @@
    9.89  val swap_disj_thm = mk_meta_eq @{thm disj_commute}
    9.90  
    9.91  fun swap_conv dest eq =
    9.92 -  U.if_true_conv ((op <) o pairself Term.size_of_term o dest)
    9.93 +  SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
    9.94      (Conv.rewr_conv eq)
    9.95  
    9.96  val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
    9.97 -val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm
    9.98 +val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm
    9.99  
   9.100  fun norm_conv ctxt =
   9.101    swap_eq_conv then_conv
   9.102 -  Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv
   9.103 -  Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt)
   9.104 +  Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv
   9.105 +  Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt)
   9.106  
   9.107  in
   9.108  
   9.109  fun prove_injectivity ctxt =
   9.110 -  T.by_tac (
   9.111 -    CONVERSION (U.prop_conv (norm_conv ctxt))
   9.112 +  Z3_Proof_Tools.by_tac (
   9.113 +    CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
   9.114      THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
   9.115  
   9.116  end
    10.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Dec 20 21:04:45 2010 +0100
    10.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Dec 20 22:02:57 2010 +0100
    10.3 @@ -31,9 +31,6 @@
    10.4  structure Z3_Proof_Parser: Z3_PROOF_PARSER =
    10.5  struct
    10.6  
    10.7 -structure U = SMT_Utils
    10.8 -structure I = Z3_Interface
    10.9 -
   10.10  
   10.11  (* proof rules *)
   10.12  
   10.13 @@ -113,7 +110,8 @@
   10.14    let
   10.15      val max = fold (Integer.max o fst) vars 0
   10.16      val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
   10.17 -    fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   10.18 +    fun mk (i, v) =
   10.19 +      (v, SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   10.20    in map mk vars end
   10.21  
   10.22  fun close ctxt (ct, vars) =
   10.23 @@ -124,7 +122,7 @@
   10.24  
   10.25  
   10.26  fun mk_bound ctxt (i, T) =
   10.27 -  let val ct = U.certify ctxt (Var ((Name.uu, 0), T))
   10.28 +  let val ct = SMT_Utils.certify ctxt (Var ((Name.uu, 0), T))
   10.29    in (ct, [(i, ct)]) end
   10.30  
   10.31  local
   10.32 @@ -133,11 +131,13 @@
   10.33        val cv =
   10.34          (case AList.lookup (op =) vars 0 of
   10.35            SOME cv => cv
   10.36 -        | _ => U.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
   10.37 +        | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
   10.38        fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
   10.39 -    in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
   10.40 +      val vars' = map_filter dec vars
   10.41 +    in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
   10.42  
   10.43 -  fun quant name = U.mk_const_pat @{theory} name (U.destT1 o U.destT1)
   10.44 +  fun quant name =
   10.45 +    SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
   10.46    val forall = quant @{const_name All}
   10.47    val exists = quant @{const_name Ex}
   10.48  in
   10.49 @@ -197,7 +197,7 @@
   10.50        |> Symtab.fold (Variable.declare_term o snd) terms
   10.51  
   10.52      fun cert @{const True} = not_false
   10.53 -      | cert t = U.certify ctxt' t
   10.54 +      | cert t = SMT_Utils.certify ctxt' t
   10.55  
   10.56    in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
   10.57  
   10.58 @@ -212,20 +212,21 @@
   10.59      SOME _ => cx
   10.60    | NONE => cx |> fresh_name (decl_prefix ^ n)
   10.61        |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
   10.62 -           let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
   10.63 +           let
   10.64 +             val upd = Symtab.update (n, SMT_Utils.certify ctxt (Free (m, T)))
   10.65             in (typs, upd terms, exprs, steps, vars, ctxt) end))
   10.66  
   10.67 -fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 
   10.68 -  (case I.mk_builtin_typ ctxt s of
   10.69 +fun mk_typ (typs, _, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _)) = 
   10.70 +  (case Z3_Interface.mk_builtin_typ ctxt s of
   10.71      SOME T => SOME T
   10.72    | NONE => Symtab.lookup typs n)
   10.73  
   10.74  fun mk_num (_, _, _, _, _, ctxt) (i, T) =
   10.75 -  mk_fun (K (I.mk_builtin_num ctxt i T)) []
   10.76 +  mk_fun (K (Z3_Interface.mk_builtin_num ctxt i T)) []
   10.77  
   10.78 -fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) =
   10.79 +fun mk_app (_, terms, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _), es) =
   10.80    mk_fun (fn cts =>
   10.81 -    (case I.mk_builtin_fun ctxt s cts of
   10.82 +    (case Z3_Interface.mk_builtin_fun ctxt s cts of
   10.83        SOME ct => SOME ct
   10.84      | NONE =>
   10.85          Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
   10.86 @@ -243,8 +244,8 @@
   10.87        | part (NONE, i) (cts, ps) = (cts, i :: ps)
   10.88      val (args', prems) = fold (part o `(lookup_expr cx)) args ([], [])
   10.89      val (cts, vss) = split_list args'
   10.90 -    val step =
   10.91 -      Proof_Step {rule=r, args=rev cts, prems=rev prems, prop=U.mk_cprop ct}
   10.92 +    val step = Proof_Step {rule=r, args=rev cts, prems=rev prems,
   10.93 +      prop = SMT_Utils.mk_cprop ct}
   10.94      val vars' = fold (union (op =)) (vs :: vss) vars
   10.95    in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end
   10.96  
   10.97 @@ -326,8 +327,8 @@
   10.98  
   10.99  fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
  10.100  
  10.101 -fun sym st =
  10.102 -  (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st
  10.103 +fun sym st = (name --
  10.104 +  Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Z3_Interface.Sym) st
  10.105  
  10.106  fun id st = ($$ "#" |-- nat_num) st
  10.107  
  10.108 @@ -337,7 +338,7 @@
  10.109  fun sort st = Scan.first [
  10.110    this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
  10.111    par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
  10.112 -  sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn
  10.113 +  sym :|-- (fn s as Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn
  10.114      SOME T => Scan.succeed T
  10.115    | NONE => scan_exn ("unknown sort: " ^ quote n)))] st
  10.116  
  10.117 @@ -348,11 +349,13 @@
  10.118      SOME n' => Scan.succeed n'
  10.119    | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
  10.120  
  10.121 -fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn 
  10.122 -    SOME app' => Scan.succeed app'
  10.123 -  | NONE => scan_exn ("unknown function symbol: " ^ quote n))
  10.124 +fun appl (app as (Z3_Interface.Sym (n, _), _)) =
  10.125 +  lookup_context mk_app app :|-- (fn 
  10.126 +      SOME app' => Scan.succeed app'
  10.127 +    | NONE => scan_exn ("unknown function symbol: " ^ quote n))
  10.128  
  10.129 -fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st
  10.130 +fun bv_size st = (digits >> (fn sz =>
  10.131 +  Z3_Interface.Sym ("bv", [Z3_Interface.Sym (sz, [])]))) st
  10.132  
  10.133  fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
  10.134      SOME cT => Scan.succeed cT
  10.135 @@ -364,7 +367,7 @@
  10.136  fun frac_number st = (
  10.137    int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
  10.138      numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
  10.139 -      appl (I.Sym ("/", []), [n, m])))) st
  10.140 +      appl (Z3_Interface.Sym ("/", []), [n, m])))) st
  10.141  
  10.142  fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
  10.143  
    11.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Dec 20 21:04:45 2010 +0100
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Dec 20 22:02:57 2010 +0100
    11.3 @@ -15,11 +15,6 @@
    11.4  structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
    11.5  struct
    11.6  
    11.7 -structure U = SMT_Utils
    11.8 -structure P = Z3_Proof_Parser
    11.9 -structure T = Z3_Proof_Tools
   11.10 -structure L = Z3_Proof_Literals
   11.11 -structure M = Z3_Proof_Methods
   11.12  
   11.13  fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   11.14    ("Z3 proof reconstruction: " ^ msg))
   11.15 @@ -43,7 +38,8 @@
   11.16      val merge = Net.merge eq
   11.17    )
   11.18  
   11.19 -  val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true]
   11.20 +  val prep =
   11.21 +    `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
   11.22  
   11.23    fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
   11.24    fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
   11.25 @@ -55,7 +51,7 @@
   11.26  val add_z3_rule = Z3_Rules.map o ins
   11.27  
   11.28  fun by_schematic_rule ctxt ct =
   11.29 -  the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
   11.30 +  the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
   11.31  
   11.32  val z3_rules_setup =
   11.33    Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
   11.34 @@ -115,7 +111,7 @@
   11.35  datatype theorem =
   11.36    Thm of thm | (* theorem without special features *)
   11.37    MetaEq of thm | (* meta equality "t == s" *)
   11.38 -  Literals of thm * L.littab
   11.39 +  Literals of thm * Z3_Proof_Literals.littab
   11.40      (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
   11.41  
   11.42  fun thm_of (Thm thm) = thm
   11.43 @@ -126,7 +122,7 @@
   11.44    | meta_eq_of p = mk_meta_eq (thm_of p)
   11.45  
   11.46  fun literals_of (Literals (_, lits)) = lits
   11.47 -  | literals_of p = L.make_littab [thm_of p]
   11.48 +  | literals_of p = Z3_Proof_Literals.make_littab [thm_of p]
   11.49  
   11.50  
   11.51  
   11.52 @@ -143,27 +139,27 @@
   11.53      (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
   11.54  
   11.55    val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
   11.56 -    remove_fun_app, L.rewrite_true]
   11.57 +    remove_fun_app, Z3_Proof_Literals.rewrite_true]
   11.58  
   11.59    fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
   11.60  
   11.61    fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
   11.62  
   11.63    fun lookup_assm assms_net ct =
   11.64 -    T.net_instance' burrow_snd_option assms_net ct
   11.65 +    Z3_Proof_Tools.net_instance' burrow_snd_option assms_net ct
   11.66      |> Option.map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
   11.67  in
   11.68  
   11.69  fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
   11.70    let
   11.71 -    val eqs = map (rewrite ctxt [L.rewrite_true]) rewrite_rules
   11.72 +    val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules
   11.73      val eqs' = union Thm.eq_thm eqs prep_rules
   11.74  
   11.75      val assms_net =
   11.76        assms
   11.77        |> map (apsnd (rewrite ctxt eqs'))
   11.78        |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
   11.79 -      |> T.thm_net_of snd 
   11.80 +      |> Z3_Proof_Tools.thm_net_of snd 
   11.81  
   11.82      fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
   11.83  
   11.84 @@ -202,17 +198,20 @@
   11.85  
   11.86  (* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
   11.87  local
   11.88 -  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
   11.89 -  val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
   11.90 +  val precomp = Z3_Proof_Tools.precompose2
   11.91 +  val comp = Z3_Proof_Tools.compose
   11.92  
   11.93 -  val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
   11.94 -  val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
   11.95 +  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
   11.96 +  val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
   11.97 +
   11.98 +  val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
   11.99 +  val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
  11.100  in
  11.101 -fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
  11.102 +fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
  11.103    | mp p_q p = 
  11.104        let
  11.105          val pq = thm_of p_q
  11.106 -        val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
  11.107 +        val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
  11.108        in Thm (Thm.implies_elim thm p) end
  11.109  end
  11.110  
  11.111 @@ -220,23 +219,25 @@
  11.112  (* and_elim:     P1 & ... & Pn ==> Pi *)
  11.113  (* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
  11.114  local
  11.115 -  fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
  11.116 +  fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
  11.117  
  11.118    fun derive conj t lits idx ptab =
  11.119      let
  11.120 -      val lit = the (L.get_first_lit (is_sublit conj t) lits)
  11.121 -      val ls = L.explode conj false false [t] lit
  11.122 -      val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
  11.123 +      val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
  11.124 +      val ls = Z3_Proof_Literals.explode conj false false [t] lit
  11.125 +      val lits' = fold Z3_Proof_Literals.insert_lit ls
  11.126 +        (Z3_Proof_Literals.delete_lit lit lits)
  11.127  
  11.128        fun upd thm = Literals (thm_of thm, lits')
  11.129 -    in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
  11.130 +      val ptab' = Inttab.map_entry idx upd ptab
  11.131 +    in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end
  11.132  
  11.133    fun lit_elim conj (p, idx) ct ptab =
  11.134      let val lits = literals_of p
  11.135      in
  11.136 -      (case L.lookup_lit lits (U.term_of ct) of
  11.137 +      (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
  11.138          SOME lit => (Thm lit, ptab)
  11.139 -      | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
  11.140 +      | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
  11.141      end
  11.142  in
  11.143  val and_elim = lit_elim true
  11.144 @@ -248,36 +249,42 @@
  11.145  local
  11.146    fun step lit thm =
  11.147      Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
  11.148 -  val explode_disj = L.explode false false false
  11.149 +  val explode_disj = Z3_Proof_Literals.explode false false false
  11.150    fun intro hyps thm th = fold step (explode_disj hyps th) thm
  11.151  
  11.152    fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
  11.153 -  val ccontr = T.precompose dest_ccontr @{thm ccontr}
  11.154 +  val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
  11.155  in
  11.156  fun lemma thm ct =
  11.157    let
  11.158 -    val cu = L.negate (Thm.dest_arg ct)
  11.159 +    val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
  11.160      val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
  11.161 -  in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
  11.162 +    val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
  11.163 +  in Thm (Z3_Proof_Tools.compose ccontr th) end
  11.164  end
  11.165  
  11.166  
  11.167  (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
  11.168  local
  11.169 -  val explode_disj = L.explode false true false
  11.170 -  val join_disj = L.join false
  11.171 +  val explode_disj = Z3_Proof_Literals.explode false true false
  11.172 +  val join_disj = Z3_Proof_Literals.join false
  11.173    fun unit thm thms th =
  11.174 -    let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
  11.175 -    in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
  11.176 +    let
  11.177 +      val t = @{const Not} $ SMT_Utils.prop_of thm
  11.178 +      val ts = map SMT_Utils.prop_of thms
  11.179 +    in
  11.180 +      join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
  11.181 +    end
  11.182  
  11.183    fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
  11.184    fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
  11.185 -  val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
  11.186 +  val contrapos =
  11.187 +    Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
  11.188  in
  11.189  fun unit_resolution thm thms ct =
  11.190 -  L.negate (Thm.dest_arg ct)
  11.191 -  |> T.under_assumption (unit thm thms)
  11.192 -  |> Thm o T.discharge thm o T.compose contrapos
  11.193 +  Z3_Proof_Literals.negate (Thm.dest_arg ct)
  11.194 +  |> Z3_Proof_Tools.under_assumption (unit thm thms)
  11.195 +  |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
  11.196  end
  11.197  
  11.198  
  11.199 @@ -293,7 +300,7 @@
  11.200  
  11.201  (* distributivity of | over & *)
  11.202  fun distributivity ctxt = Thm o try_apply ctxt [] [
  11.203 -  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
  11.204 +  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
  11.205      (* FIXME: not very well tested *)
  11.206  
  11.207  
  11.208 @@ -305,11 +312,15 @@
  11.209    val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
  11.210  
  11.211    fun prove' conj1 conj2 ct2 thm =
  11.212 -    let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
  11.213 -    in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
  11.214 +    let
  11.215 +      val littab =
  11.216 +        Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
  11.217 +        |> cons Z3_Proof_Literals.true_thm
  11.218 +        |> Z3_Proof_Literals.make_littab
  11.219 +    in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
  11.220  
  11.221    fun prove rule (ct1, conj1) (ct2, conj2) =
  11.222 -    T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
  11.223 +    Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
  11.224  
  11.225    fun prove_def_axiom ct =
  11.226      let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
  11.227 @@ -318,32 +329,34 @@
  11.228          @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
  11.229            prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
  11.230        | @{const HOL.conj} $ _ $ _ =>
  11.231 -          prove disjI3 (L.negate ct2, false) (ct1, true)
  11.232 +          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
  11.233        | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
  11.234 -          prove disjI3 (L.negate ct2, false) (ct1, false)
  11.235 +          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
  11.236        | @{const HOL.disj} $ _ $ _ =>
  11.237 -          prove disjI2 (L.negate ct1, false) (ct2, true)
  11.238 +          prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
  11.239        | Const (@{const_name distinct}, _) $ _ =>
  11.240            let
  11.241              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
  11.242 +            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
  11.243              fun prv cu =
  11.244                let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
  11.245                in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
  11.246 -          in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
  11.247 +          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
  11.248        | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
  11.249            let
  11.250              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
  11.251 +            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
  11.252              fun prv cu =
  11.253                let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
  11.254                in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
  11.255 -          in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
  11.256 +          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
  11.257        | _ => raise CTERM ("prove_def_axiom", [ct]))
  11.258      end
  11.259  in
  11.260  fun def_axiom ctxt = Thm o try_apply ctxt [] [
  11.261    named ctxt "conj/disj/distinct" prove_def_axiom,
  11.262 -  T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
  11.263 -    named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
  11.264 +  Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
  11.265 +    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
  11.266  end
  11.267  
  11.268  
  11.269 @@ -360,14 +373,14 @@
  11.270      @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
  11.271        by (atomize(full)) fastsimp} ]
  11.272  
  11.273 -  val inst_rule = T.match_instantiate Thm.dest_arg
  11.274 +  val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
  11.275  
  11.276    fun apply_rule ct =
  11.277      (case get_first (try (inst_rule ct)) intro_rules of
  11.278        SOME thm => thm
  11.279      | NONE => raise CTERM ("intro_def", [ct]))
  11.280  in
  11.281 -fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm
  11.282 +fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
  11.283  
  11.284  fun apply_def thm =
  11.285    get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
  11.286 @@ -394,17 +407,20 @@
  11.287      (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
  11.288      (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
  11.289  
  11.290 +  fun nnf_quant_tac_varified vars eq =
  11.291 +    nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
  11.292 +
  11.293    fun nnf_quant vars qs p ct =
  11.294 -    T.as_meta_eq ct
  11.295 -    |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
  11.296 +    Z3_Proof_Tools.as_meta_eq ct
  11.297 +    |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
  11.298  
  11.299    fun prove_nnf ctxt = try_apply ctxt [] [
  11.300 -    named ctxt "conj/disj" L.prove_conj_disj_eq,
  11.301 -    T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
  11.302 -      named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
  11.303 +    named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
  11.304 +    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
  11.305 +      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
  11.306  in
  11.307  fun nnf ctxt vars ps ct =
  11.308 -  (case U.term_of ct of
  11.309 +  (case SMT_Utils.term_of ct of
  11.310      _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
  11.311        if l aconv r
  11.312        then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
  11.313 @@ -414,8 +430,9 @@
  11.314    | _ =>
  11.315        let
  11.316          val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
  11.317 -          (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
  11.318 -      in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
  11.319 +          (Z3_Proof_Tools.unfold_eqs ctxt
  11.320 +            (map (Thm.symmetric o meta_eq_of) ps)))
  11.321 +      in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
  11.322  end
  11.323  
  11.324  
  11.325 @@ -483,15 +500,15 @@
  11.326        SOME eq => eq
  11.327      | NONE => if exn then raise MONO else prove_refl cp)
  11.328    
  11.329 -  val prove_eq_exn = prove_eq true
  11.330 -  and prove_eq_safe = prove_eq false
  11.331 +  val prove_exn = prove_eq true
  11.332 +  and prove_safe = prove_eq false
  11.333  
  11.334    fun mono f (cp as (cl, _)) =
  11.335      (case Term.head_of (Thm.term_of cl) of
  11.336 -      @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
  11.337 -    | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
  11.338 -    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
  11.339 -    | _ => prove (prove_eq_safe f)) cp
  11.340 +      @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
  11.341 +    | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
  11.342 +    | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
  11.343 +    | _ => prove (prove_safe f)) cp
  11.344  in
  11.345  fun monotonicity eqs ct =
  11.346    let
  11.347 @@ -499,7 +516,7 @@
  11.348      val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
  11.349      val lookup = AList.lookup (op aconv) teqs
  11.350      val cp = Thm.dest_binop (Thm.dest_arg ct)
  11.351 -  in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
  11.352 +  in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
  11.353  end
  11.354  
  11.355  
  11.356 @@ -507,7 +524,9 @@
  11.357  local
  11.358    val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
  11.359  in
  11.360 -fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
  11.361 +fun commutativity ct =
  11.362 +  MetaEq (Z3_Proof_Tools.match_instantiate I
  11.363 +    (Z3_Proof_Tools.as_meta_eq ct) rule)
  11.364  end
  11.365  
  11.366  
  11.367 @@ -524,21 +543,22 @@
  11.368  fun quant_intro vars p ct =
  11.369    let
  11.370      val thm = meta_eq_of p
  11.371 -    val rules' = T.varify vars thm :: rules
  11.372 -    val cu = T.as_meta_eq ct
  11.373 -  in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
  11.374 +    val rules' = Z3_Proof_Tools.varify vars thm :: rules
  11.375 +    val cu = Z3_Proof_Tools.as_meta_eq ct
  11.376 +    val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
  11.377 +  in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
  11.378  end
  11.379  
  11.380  
  11.381  (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
  11.382  fun pull_quant ctxt = Thm o try_apply ctxt [] [
  11.383 -  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
  11.384 +  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
  11.385      (* FIXME: not very well tested *)
  11.386  
  11.387  
  11.388  (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
  11.389  fun push_quant ctxt = Thm o try_apply ctxt [] [
  11.390 -  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
  11.391 +  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
  11.392      (* FIXME: not very well tested *)
  11.393  
  11.394  
  11.395 @@ -556,13 +576,13 @@
  11.396        Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
  11.397        ORELSE' CONVERSION (elim_unused_conv ctxt))
  11.398  in
  11.399 -fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
  11.400 +fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
  11.401  end
  11.402  
  11.403  
  11.404  (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
  11.405  fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
  11.406 -  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
  11.407 +  named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
  11.408      (* FIXME: not very well tested *)
  11.409  
  11.410  
  11.411 @@ -570,7 +590,7 @@
  11.412  local
  11.413    val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
  11.414  in
  11.415 -val quant_inst = Thm o T.by_tac (
  11.416 +val quant_inst = Thm o Z3_Proof_Tools.by_tac (
  11.417    REPEAT_ALL_NEW (Tactic.match_tac [rule])
  11.418    THEN' Tactic.rtac @{thm excluded_middle})
  11.419  end
  11.420 @@ -599,7 +619,7 @@
  11.421  
  11.422    fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
  11.423      | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
  11.424 -        (sk_all_rule, Thm.dest_arg, L.negate)
  11.425 +        (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate)
  11.426      | kind t = raise TERM ("skolemize", [t])
  11.427  
  11.428    fun dest_abs_type (Abs (_, T, _)) = T
  11.429 @@ -628,7 +648,8 @@
  11.430      (case mct of
  11.431        SOME ct =>
  11.432          ctxt
  11.433 -        |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
  11.434 +        |> Z3_Proof_Tools.make_hyp_def
  11.435 +             (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
  11.436          |>> pair ((cv, ct) :: is) o Thm.transitive thm
  11.437      | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
  11.438  in
  11.439 @@ -649,10 +670,12 @@
  11.440  
  11.441  (* theory lemmas: linear arithmetic, arrays *)
  11.442  fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
  11.443 -  T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
  11.444 -    NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
  11.445 -    ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
  11.446 -      Arith_Data.arith_tac ctxt')))]
  11.447 +  Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' =>
  11.448 +    Z3_Proof_Tools.by_tac (
  11.449 +      NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
  11.450 +      ORELSE' NAMED ctxt' "simp+arith" (
  11.451 +        Simplifier.simp_tac simpset
  11.452 +        THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
  11.453  
  11.454  
  11.455  (* rewriting: prove equalities:
  11.456 @@ -680,14 +703,18 @@
  11.457      | prep (Literals (thm, _)) = spec_meta_eq_of thm
  11.458  
  11.459    fun unfold_conv ctxt ths =
  11.460 -    Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
  11.461 +    Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
  11.462 +      (map prep ths)))
  11.463  
  11.464    fun with_conv _ [] prv = prv
  11.465 -    | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
  11.466 +    | with_conv ctxt ths prv =
  11.467 +        Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
  11.468  
  11.469    val unfold_conv =
  11.470 -    Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
  11.471 -  val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
  11.472 +    Conv.arg_conv (Conv.binop_conv
  11.473 +      (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
  11.474 +  val prove_conj_disj_eq =
  11.475 +    Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
  11.476  
  11.477    fun assume_prems ctxt thm =
  11.478      Assumption.add_assumes (Drule.cprems_of thm) ctxt
  11.479 @@ -697,20 +724,23 @@
  11.480  fun rewrite simpset ths ct ctxt =
  11.481    apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
  11.482      named ctxt "conj/disj/distinct" prove_conj_disj_eq,
  11.483 -    T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
  11.484 -      NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
  11.485 -      THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
  11.486 -    T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
  11.487 -      NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
  11.488 -      THEN_ALL_NEW (
  11.489 -        NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
  11.490 -        ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
  11.491 -    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
  11.492 -      NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
  11.493 -      THEN_ALL_NEW (
  11.494 -        NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
  11.495 -        ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
  11.496 -    named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
  11.497 +    Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
  11.498 +      Z3_Proof_Tools.by_tac (
  11.499 +        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
  11.500 +        THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
  11.501 +    Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
  11.502 +      Z3_Proof_Tools.by_tac (
  11.503 +        NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
  11.504 +        THEN_ALL_NEW (
  11.505 +          NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
  11.506 +          ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
  11.507 +    Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
  11.508 +      Z3_Proof_Tools.by_tac (
  11.509 +        NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
  11.510 +        THEN_ALL_NEW (
  11.511 +          NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
  11.512 +          ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
  11.513 +    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
  11.514  
  11.515  end
  11.516  
  11.517 @@ -721,7 +751,7 @@
  11.518  (** tracing and checking **)
  11.519  
  11.520  fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
  11.521 -  "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r)
  11.522 +  "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)
  11.523  
  11.524  fun check_after idx r ps ct (p, (ctxt, _)) =
  11.525    if not (Config.get ctxt SMT_Config.trace) then ()
  11.526 @@ -729,11 +759,13 @@
  11.527      let val thm = thm_of p |> tap (Thm.join_proofs o single)
  11.528      in
  11.529        if (Thm.cprop_of thm) aconvc ct then ()
  11.530 -      else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
  11.531 -        quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
  11.532 +      else
  11.533 +        z3_exn (Pretty.string_of (Pretty.big_list
  11.534 +          ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
  11.535 +            " (#" ^ string_of_int idx ^ ")")
  11.536            (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
  11.537 -           [Pretty.block [Pretty.str "expected: ",
  11.538 -            Syntax.pretty_term ctxt (Thm.term_of ct)]])))
  11.539 +            [Pretty.block [Pretty.str "expected: ",
  11.540 +              Syntax.pretty_term ctxt (Thm.term_of ct)]])))
  11.541      end
  11.542  
  11.543  
  11.544 @@ -741,61 +773,67 @@
  11.545  
  11.546  local
  11.547    fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
  11.548 -    quote (P.string_of_rule r))
  11.549 +    quote (Z3_Proof_Parser.string_of_rule r))
  11.550  
  11.551    fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
  11.552      (case (r, ps) of
  11.553        (* core rules *)
  11.554 -      (P.True_Axiom, _) => (Thm L.true_thm, cxp)
  11.555 -    | (P.Asserted, _) => raise Fail "bad assertion"
  11.556 -    | (P.Goal, _) => raise Fail "bad assertion"
  11.557 -    | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
  11.558 -    | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
  11.559 -    | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
  11.560 -    | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
  11.561 -    | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
  11.562 -    | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
  11.563 -    | (P.Unit_Resolution, (p, _) :: ps) =>
  11.564 +      (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
  11.565 +    | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
  11.566 +    | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
  11.567 +    | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
  11.568 +        (mp q (thm_of p), cxp)
  11.569 +    | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
  11.570 +        (mp q (thm_of p), cxp)
  11.571 +    | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
  11.572 +        and_elim (p, i) ct ptab ||> pair cx
  11.573 +    | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
  11.574 +        not_or_elim (p, i) ct ptab ||> pair cx
  11.575 +    | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
  11.576 +    | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
  11.577 +    | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
  11.578          (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
  11.579 -    | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
  11.580 -    | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
  11.581 -    | (P.Distributivity, _) => (distributivity cx ct, cxp)
  11.582 -    | (P.Def_Axiom, _) => (def_axiom cx ct, cxp)
  11.583 -    | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab
  11.584 -    | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
  11.585 -    | (P.Iff_Oeq, [(p, _)]) => (p, cxp)
  11.586 -    | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
  11.587 -    | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
  11.588 +    | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
  11.589 +    | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
  11.590 +    | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
  11.591 +    | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
  11.592 +    | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
  11.593 +    | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
  11.594 +    | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
  11.595 +    | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
  11.596 +    | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
  11.597  
  11.598        (* equality rules *)
  11.599 -    | (P.Reflexivity, _) => (refl ct, cxp)
  11.600 -    | (P.Symmetry, [(p, _)]) => (symm p, cxp)
  11.601 -    | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
  11.602 -    | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
  11.603 -    | (P.Commutativity, _) => (commutativity ct, cxp)
  11.604 +    | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
  11.605 +    | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
  11.606 +    | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
  11.607 +    | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
  11.608 +    | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
  11.609  
  11.610        (* quantifier rules *)
  11.611 -    | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
  11.612 -    | (P.Pull_Quant, _) => (pull_quant cx ct, cxp)
  11.613 -    | (P.Push_Quant, _) => (push_quant cx ct, cxp)
  11.614 -    | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
  11.615 -    | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
  11.616 -    | (P.Quant_Inst, _) => (quant_inst ct, cxp)
  11.617 -    | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
  11.618 +    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
  11.619 +    | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
  11.620 +    | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
  11.621 +    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
  11.622 +    | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
  11.623 +    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
  11.624 +    | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab
  11.625  
  11.626        (* theory rules *)
  11.627 -    | (P.Th_Lemma _, _) =>  (* FIXME: use arguments *)
  11.628 +    | (Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
  11.629          (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
  11.630 -    | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
  11.631 -    | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
  11.632 +    | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
  11.633 +    | (Z3_Proof_Parser.Rewrite_Star, ps) =>
  11.634 +        rewrite simpset (map fst ps) ct cx ||> rpair ptab
  11.635  
  11.636 -    | (P.Nnf_Star, _) => not_supported r
  11.637 -    | (P.Cnf_Star, _) => not_supported r
  11.638 -    | (P.Transitivity_Star, _) => not_supported r
  11.639 -    | (P.Pull_Quant_Star, _) => not_supported r
  11.640 +    | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
  11.641 +    | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
  11.642 +    | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
  11.643 +    | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
  11.644  
  11.645 -    | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
  11.646 -       " has an unexpected number of arguments."))
  11.647 +    | _ => raise Fail ("Z3: proof rule " ^
  11.648 +        quote (Z3_Proof_Parser.string_of_rule r) ^
  11.649 +        " has an unexpected number of arguments."))
  11.650  
  11.651    fun lookup_proof ptab idx =
  11.652      (case Inttab.lookup ptab idx of
  11.653 @@ -804,7 +842,7 @@
  11.654  
  11.655    fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
  11.656      let
  11.657 -      val P.Proof_Step {rule=r, prems, prop, ...} = step
  11.658 +      val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
  11.659        val ps = map (lookup_proof ptab) prems
  11.660        val _ = trace_before ctxt idx r
  11.661        val (thm, (ctxt', ptab')) =
  11.662 @@ -832,9 +870,10 @@
  11.663  fun reconstruct outer_ctxt recon output =
  11.664    let
  11.665      val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
  11.666 -    val (asserted, steps, vars, ctxt1) = P.parse ctxt typs terms output
  11.667 +    val (asserted, steps, vars, ctxt1) =
  11.668 +      Z3_Proof_Parser.parse ctxt typs terms output
  11.669  
  11.670 -    val simpset = T.make_simpset ctxt1 (Z3_Simps.get ctxt1)
  11.671 +    val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
  11.672  
  11.673      val ((is, rules), cxp as (ctxt2, _)) =
  11.674        add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
    12.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Dec 20 21:04:45 2010 +0100
    12.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Dec 20 22:02:57 2010 +0100
    12.3 @@ -44,14 +44,12 @@
    12.4  structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
    12.5  struct
    12.6  
    12.7 -structure U = SMT_Utils
    12.8 -structure I = Z3_Interface
    12.9 -
   12.10  
   12.11  
   12.12  (* modifying terms *)
   12.13  
   12.14 -fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
   12.15 +fun as_meta_eq ct =
   12.16 +  uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct))
   12.17  
   12.18  
   12.19  
   12.20 @@ -80,7 +78,7 @@
   12.21  (* proof combinators *)
   12.22  
   12.23  fun under_assumption f ct =
   12.24 -  let val ct' = U.mk_cprop ct
   12.25 +  let val ct' = SMT_Utils.mk_cprop ct
   12.26    in Thm.implies_intr ct' (f (Thm.assume ct')) end
   12.27  
   12.28  fun with_conv conv prove ct =
   12.29 @@ -109,7 +107,7 @@
   12.30    let
   12.31      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
   12.32      val (cf, cvs) = Drule.strip_comb lhs
   12.33 -    val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
   12.34 +    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
   12.35      fun apply cv th =
   12.36        Thm.combination th (Thm.reflexive cv)
   12.37        |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
   12.38 @@ -149,8 +147,8 @@
   12.39      | NONE =>
   12.40          let
   12.41            val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
   12.42 -          val cv = U.certify ctxt'
   12.43 -            (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
   12.44 +          val cv = SMT_Utils.certify ctxt'
   12.45 +            (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
   12.46            val cu = Drule.list_comb (cv, cvs')
   12.47            val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
   12.48            val beta_norm' = beta_norm orelse not (null cvs')
   12.49 @@ -211,7 +209,7 @@
   12.50        | t => (fn cx =>
   12.51            if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
   12.52            else if with_theories andalso
   12.53 -            I.is_builtin_theory_term (context_of cx) t
   12.54 +            Z3_Interface.is_builtin_theory_term (context_of cx) t
   12.55            then abs_args abstr cvs ct cx
   12.56            else fresh_abstraction cvs ct cx))
   12.57    in abstr [] end