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 precomp = Z3_Proof_Tools.precompose2
11.89 + val comp = Z3_Proof_Tools.compose
11.90 +
11.91 val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
11.92 - val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
11.93 + val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
11.94
11.95 - val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
11.96 - val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
11.97 + val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
11.98 + val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
11.99 in
11.100 -fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
11.101 +fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
11.102 | mp p_q p =
11.103 let
11.104 val pq = thm_of p_q
11.105 - val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
11.106 + val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
11.107 in Thm (Thm.implies_elim thm p) end
11.108 end
11.109
11.110 @@ -220,23 +219,25 @@
11.111 (* and_elim: P1 & ... & Pn ==> Pi *)
11.112 (* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *)
11.113 local
11.114 - fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
11.115 + fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
11.116
11.117 fun derive conj t lits idx ptab =
11.118 let
11.119 - val lit = the (L.get_first_lit (is_sublit conj t) lits)
11.120 - val ls = L.explode conj false false [t] lit
11.121 - val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
11.122 + val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
11.123 + val ls = Z3_Proof_Literals.explode conj false false [t] lit
11.124 + val lits' = fold Z3_Proof_Literals.insert_lit ls
11.125 + (Z3_Proof_Literals.delete_lit lit lits)
11.126
11.127 fun upd thm = Literals (thm_of thm, lits')
11.128 - in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
11.129 + val ptab' = Inttab.map_entry idx upd ptab
11.130 + in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end
11.131
11.132 fun lit_elim conj (p, idx) ct ptab =
11.133 let val lits = literals_of p
11.134 in
11.135 - (case L.lookup_lit lits (U.term_of ct) of
11.136 + (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
11.137 SOME lit => (Thm lit, ptab)
11.138 - | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
11.139 + | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
11.140 end
11.141 in
11.142 val and_elim = lit_elim true
11.143 @@ -248,36 +249,42 @@
11.144 local
11.145 fun step lit thm =
11.146 Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
11.147 - val explode_disj = L.explode false false false
11.148 + val explode_disj = Z3_Proof_Literals.explode false false false
11.149 fun intro hyps thm th = fold step (explode_disj hyps th) thm
11.150
11.151 fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
11.152 - val ccontr = T.precompose dest_ccontr @{thm ccontr}
11.153 + val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
11.154 in
11.155 fun lemma thm ct =
11.156 let
11.157 - val cu = L.negate (Thm.dest_arg ct)
11.158 + val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
11.159 val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
11.160 - in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
11.161 + val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
11.162 + in Thm (Z3_Proof_Tools.compose ccontr th) end
11.163 end
11.164
11.165
11.166 (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
11.167 local
11.168 - val explode_disj = L.explode false true false
11.169 - val join_disj = L.join false
11.170 + val explode_disj = Z3_Proof_Literals.explode false true false
11.171 + val join_disj = Z3_Proof_Literals.join false
11.172 fun unit thm thms th =
11.173 - let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
11.174 - in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
11.175 + let
11.176 + val t = @{const Not} $ SMT_Utils.prop_of thm
11.177 + val ts = map SMT_Utils.prop_of thms
11.178 + in
11.179 + join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
11.180 + end
11.181
11.182 fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
11.183 fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
11.184 - val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
11.185 + val contrapos =
11.186 + Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
11.187 in
11.188 fun unit_resolution thm thms ct =
11.189 - L.negate (Thm.dest_arg ct)
11.190 - |> T.under_assumption (unit thm thms)
11.191 - |> Thm o T.discharge thm o T.compose contrapos
11.192 + Z3_Proof_Literals.negate (Thm.dest_arg ct)
11.193 + |> Z3_Proof_Tools.under_assumption (unit thm thms)
11.194 + |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
11.195 end
11.196
11.197
11.198 @@ -293,7 +300,7 @@
11.199
11.200 (* distributivity of | over & *)
11.201 fun distributivity ctxt = Thm o try_apply ctxt [] [
11.202 - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
11.203 + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
11.204 (* FIXME: not very well tested *)
11.205
11.206
11.207 @@ -305,11 +312,15 @@
11.208 val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
11.209
11.210 fun prove' conj1 conj2 ct2 thm =
11.211 - let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
11.212 - in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
11.213 + let
11.214 + val littab =
11.215 + Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
11.216 + |> cons Z3_Proof_Literals.true_thm
11.217 + |> Z3_Proof_Literals.make_littab
11.218 + in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
11.219
11.220 fun prove rule (ct1, conj1) (ct2, conj2) =
11.221 - T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
11.222 + Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
11.223
11.224 fun prove_def_axiom ct =
11.225 let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
11.226 @@ -318,32 +329,34 @@
11.227 @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
11.228 prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
11.229 | @{const HOL.conj} $ _ $ _ =>
11.230 - prove disjI3 (L.negate ct2, false) (ct1, true)
11.231 + prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
11.232 | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
11.233 - prove disjI3 (L.negate ct2, false) (ct1, false)
11.234 + prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
11.235 | @{const HOL.disj} $ _ $ _ =>
11.236 - prove disjI2 (L.negate ct1, false) (ct2, true)
11.237 + prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
11.238 | Const (@{const_name distinct}, _) $ _ =>
11.239 let
11.240 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
11.241 + val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
11.242 fun prv cu =
11.243 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
11.244 in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
11.245 - in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
11.246 + in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
11.247 | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
11.248 let
11.249 fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
11.250 + val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
11.251 fun prv cu =
11.252 let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
11.253 in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
11.254 - in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
11.255 + in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
11.256 | _ => raise CTERM ("prove_def_axiom", [ct]))
11.257 end
11.258 in
11.259 fun def_axiom ctxt = Thm o try_apply ctxt [] [
11.260 named ctxt "conj/disj/distinct" prove_def_axiom,
11.261 - T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
11.262 - named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
11.263 + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
11.264 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
11.265 end
11.266
11.267
11.268 @@ -360,14 +373,14 @@
11.269 @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
11.270 by (atomize(full)) fastsimp} ]
11.271
11.272 - val inst_rule = T.match_instantiate Thm.dest_arg
11.273 + val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
11.274
11.275 fun apply_rule ct =
11.276 (case get_first (try (inst_rule ct)) intro_rules of
11.277 SOME thm => thm
11.278 | NONE => raise CTERM ("intro_def", [ct]))
11.279 in
11.280 -fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm
11.281 +fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
11.282
11.283 fun apply_def thm =
11.284 get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
11.285 @@ -394,17 +407,20 @@
11.286 (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
11.287 (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
11.288
11.289 + fun nnf_quant_tac_varified vars eq =
11.290 + nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
11.291 +
11.292 fun nnf_quant vars qs p ct =
11.293 - T.as_meta_eq ct
11.294 - |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
11.295 + Z3_Proof_Tools.as_meta_eq ct
11.296 + |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
11.297
11.298 fun prove_nnf ctxt = try_apply ctxt [] [
11.299 - named ctxt "conj/disj" L.prove_conj_disj_eq,
11.300 - T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
11.301 - named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
11.302 + named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
11.303 + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
11.304 + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
11.305 in
11.306 fun nnf ctxt vars ps ct =
11.307 - (case U.term_of ct of
11.308 + (case SMT_Utils.term_of ct of
11.309 _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
11.310 if l aconv r
11.311 then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
11.312 @@ -414,8 +430,9 @@
11.313 | _ =>
11.314 let
11.315 val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
11.316 - (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
11.317 - in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
11.318 + (Z3_Proof_Tools.unfold_eqs ctxt
11.319 + (map (Thm.symmetric o meta_eq_of) ps)))
11.320 + in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
11.321 end
11.322
11.323
11.324 @@ -483,15 +500,15 @@
11.325 SOME eq => eq
11.326 | NONE => if exn then raise MONO else prove_refl cp)
11.327
11.328 - val prove_eq_exn = prove_eq true
11.329 - and prove_eq_safe = prove_eq false
11.330 + val prove_exn = prove_eq true
11.331 + and prove_safe = prove_eq false
11.332
11.333 fun mono f (cp as (cl, _)) =
11.334 (case Term.head_of (Thm.term_of cl) of
11.335 - @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
11.336 - | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
11.337 - | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
11.338 - | _ => prove (prove_eq_safe f)) cp
11.339 + @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
11.340 + | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
11.341 + | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
11.342 + | _ => prove (prove_safe f)) cp
11.343 in
11.344 fun monotonicity eqs ct =
11.345 let
11.346 @@ -499,7 +516,7 @@
11.347 val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
11.348 val lookup = AList.lookup (op aconv) teqs
11.349 val cp = Thm.dest_binop (Thm.dest_arg ct)
11.350 - in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
11.351 + in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
11.352 end
11.353
11.354
11.355 @@ -507,7 +524,9 @@
11.356 local
11.357 val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
11.358 in
11.359 -fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
11.360 +fun commutativity ct =
11.361 + MetaEq (Z3_Proof_Tools.match_instantiate I
11.362 + (Z3_Proof_Tools.as_meta_eq ct) rule)
11.363 end
11.364
11.365
11.366 @@ -524,21 +543,22 @@
11.367 fun quant_intro vars p ct =
11.368 let
11.369 val thm = meta_eq_of p
11.370 - val rules' = T.varify vars thm :: rules
11.371 - val cu = T.as_meta_eq ct
11.372 - in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
11.373 + val rules' = Z3_Proof_Tools.varify vars thm :: rules
11.374 + val cu = Z3_Proof_Tools.as_meta_eq ct
11.375 + val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
11.376 + in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
11.377 end
11.378
11.379
11.380 (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
11.381 fun pull_quant ctxt = Thm o try_apply ctxt [] [
11.382 - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
11.383 + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
11.384 (* FIXME: not very well tested *)
11.385
11.386
11.387 (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
11.388 fun push_quant ctxt = Thm o try_apply ctxt [] [
11.389 - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
11.390 + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
11.391 (* FIXME: not very well tested *)
11.392
11.393
11.394 @@ -556,13 +576,13 @@
11.395 Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
11.396 ORELSE' CONVERSION (elim_unused_conv ctxt))
11.397 in
11.398 -fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
11.399 +fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
11.400 end
11.401
11.402
11.403 (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
11.404 fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
11.405 - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
11.406 + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
11.407 (* FIXME: not very well tested *)
11.408
11.409
11.410 @@ -570,7 +590,7 @@
11.411 local
11.412 val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
11.413 in
11.414 -val quant_inst = Thm o T.by_tac (
11.415 +val quant_inst = Thm o Z3_Proof_Tools.by_tac (
11.416 REPEAT_ALL_NEW (Tactic.match_tac [rule])
11.417 THEN' Tactic.rtac @{thm excluded_middle})
11.418 end
11.419 @@ -599,7 +619,7 @@
11.420
11.421 fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
11.422 | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
11.423 - (sk_all_rule, Thm.dest_arg, L.negate)
11.424 + (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate)
11.425 | kind t = raise TERM ("skolemize", [t])
11.426
11.427 fun dest_abs_type (Abs (_, T, _)) = T
11.428 @@ -628,7 +648,8 @@
11.429 (case mct of
11.430 SOME ct =>
11.431 ctxt
11.432 - |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
11.433 + |> Z3_Proof_Tools.make_hyp_def
11.434 + (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
11.435 |>> pair ((cv, ct) :: is) o Thm.transitive thm
11.436 | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
11.437 in
11.438 @@ -649,10 +670,12 @@
11.439
11.440 (* theory lemmas: linear arithmetic, arrays *)
11.441 fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
11.442 - T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
11.443 - NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
11.444 - ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
11.445 - Arith_Data.arith_tac ctxt')))]
11.446 + Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' =>
11.447 + Z3_Proof_Tools.by_tac (
11.448 + NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
11.449 + ORELSE' NAMED ctxt' "simp+arith" (
11.450 + Simplifier.simp_tac simpset
11.451 + THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
11.452
11.453
11.454 (* rewriting: prove equalities:
11.455 @@ -680,14 +703,18 @@
11.456 | prep (Literals (thm, _)) = spec_meta_eq_of thm
11.457
11.458 fun unfold_conv ctxt ths =
11.459 - Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
11.460 + Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
11.461 + (map prep ths)))
11.462
11.463 fun with_conv _ [] prv = prv
11.464 - | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
11.465 + | with_conv ctxt ths prv =
11.466 + Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
11.467
11.468 val unfold_conv =
11.469 - Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
11.470 - val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
11.471 + Conv.arg_conv (Conv.binop_conv
11.472 + (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
11.473 + val prove_conj_disj_eq =
11.474 + Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
11.475
11.476 fun assume_prems ctxt thm =
11.477 Assumption.add_assumes (Drule.cprems_of thm) ctxt
11.478 @@ -697,20 +724,23 @@
11.479 fun rewrite simpset ths ct ctxt =
11.480 apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
11.481 named ctxt "conj/disj/distinct" prove_conj_disj_eq,
11.482 - T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
11.483 - NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
11.484 - THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
11.485 - T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
11.486 - NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
11.487 - THEN_ALL_NEW (
11.488 - NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
11.489 - ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
11.490 - T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
11.491 - NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
11.492 - THEN_ALL_NEW (
11.493 - NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
11.494 - ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
11.495 - named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
11.496 + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
11.497 + Z3_Proof_Tools.by_tac (
11.498 + NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
11.499 + THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
11.500 + Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
11.501 + Z3_Proof_Tools.by_tac (
11.502 + NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
11.503 + THEN_ALL_NEW (
11.504 + NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
11.505 + ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
11.506 + Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
11.507 + Z3_Proof_Tools.by_tac (
11.508 + NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
11.509 + THEN_ALL_NEW (
11.510 + NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
11.511 + ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
11.512 + named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
11.513
11.514 end
11.515
11.516 @@ -721,7 +751,7 @@
11.517 (** tracing and checking **)
11.518
11.519 fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
11.520 - "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r)
11.521 + "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)
11.522
11.523 fun check_after idx r ps ct (p, (ctxt, _)) =
11.524 if not (Config.get ctxt SMT_Config.trace) then ()
11.525 @@ -729,11 +759,13 @@
11.526 let val thm = thm_of p |> tap (Thm.join_proofs o single)
11.527 in
11.528 if (Thm.cprop_of thm) aconvc ct then ()
11.529 - else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
11.530 - quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
11.531 + else
11.532 + z3_exn (Pretty.string_of (Pretty.big_list
11.533 + ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
11.534 + " (#" ^ string_of_int idx ^ ")")
11.535 (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
11.536 - [Pretty.block [Pretty.str "expected: ",
11.537 - Syntax.pretty_term ctxt (Thm.term_of ct)]])))
11.538 + [Pretty.block [Pretty.str "expected: ",
11.539 + Syntax.pretty_term ctxt (Thm.term_of ct)]])))
11.540 end
11.541
11.542
11.543 @@ -741,61 +773,67 @@
11.544
11.545 local
11.546 fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
11.547 - quote (P.string_of_rule r))
11.548 + quote (Z3_Proof_Parser.string_of_rule r))
11.549
11.550 fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
11.551 (case (r, ps) of
11.552 (* core rules *)
11.553 - (P.True_Axiom, _) => (Thm L.true_thm, cxp)
11.554 - | (P.Asserted, _) => raise Fail "bad assertion"
11.555 - | (P.Goal, _) => raise Fail "bad assertion"
11.556 - | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
11.557 - | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
11.558 - | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
11.559 - | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
11.560 - | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
11.561 - | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
11.562 - | (P.Unit_Resolution, (p, _) :: ps) =>
11.563 + (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
11.564 + | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
11.565 + | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
11.566 + | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
11.567 + (mp q (thm_of p), cxp)
11.568 + | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
11.569 + (mp q (thm_of p), cxp)
11.570 + | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
11.571 + and_elim (p, i) ct ptab ||> pair cx
11.572 + | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
11.573 + not_or_elim (p, i) ct ptab ||> pair cx
11.574 + | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
11.575 + | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
11.576 + | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
11.577 (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
11.578 - | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
11.579 - | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
11.580 - | (P.Distributivity, _) => (distributivity cx ct, cxp)
11.581 - | (P.Def_Axiom, _) => (def_axiom cx ct, cxp)
11.582 - | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab
11.583 - | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
11.584 - | (P.Iff_Oeq, [(p, _)]) => (p, cxp)
11.585 - | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
11.586 - | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
11.587 + | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
11.588 + | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
11.589 + | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
11.590 + | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
11.591 + | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
11.592 + | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
11.593 + | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
11.594 + | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
11.595 + | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
11.596
11.597 (* equality rules *)
11.598 - | (P.Reflexivity, _) => (refl ct, cxp)
11.599 - | (P.Symmetry, [(p, _)]) => (symm p, cxp)
11.600 - | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
11.601 - | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
11.602 - | (P.Commutativity, _) => (commutativity ct, cxp)
11.603 + | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
11.604 + | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
11.605 + | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
11.606 + | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
11.607 + | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
11.608
11.609 (* quantifier rules *)
11.610 - | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
11.611 - | (P.Pull_Quant, _) => (pull_quant cx ct, cxp)
11.612 - | (P.Push_Quant, _) => (push_quant cx ct, cxp)
11.613 - | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
11.614 - | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
11.615 - | (P.Quant_Inst, _) => (quant_inst ct, cxp)
11.616 - | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
11.617 + | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
11.618 + | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
11.619 + | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
11.620 + | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
11.621 + | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
11.622 + | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
11.623 + | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab
11.624
11.625 (* theory rules *)
11.626 - | (P.Th_Lemma _, _) => (* FIXME: use arguments *)
11.627 + | (Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *)
11.628 (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
11.629 - | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
11.630 - | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
11.631 + | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
11.632 + | (Z3_Proof_Parser.Rewrite_Star, ps) =>
11.633 + rewrite simpset (map fst ps) ct cx ||> rpair ptab
11.634
11.635 - | (P.Nnf_Star, _) => not_supported r
11.636 - | (P.Cnf_Star, _) => not_supported r
11.637 - | (P.Transitivity_Star, _) => not_supported r
11.638 - | (P.Pull_Quant_Star, _) => not_supported r
11.639 + | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
11.640 + | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
11.641 + | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
11.642 + | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
11.643
11.644 - | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
11.645 - " has an unexpected number of arguments."))
11.646 + | _ => raise Fail ("Z3: proof rule " ^
11.647 + quote (Z3_Proof_Parser.string_of_rule r) ^
11.648 + " has an unexpected number of arguments."))
11.649
11.650 fun lookup_proof ptab idx =
11.651 (case Inttab.lookup ptab idx of
11.652 @@ -804,7 +842,7 @@
11.653
11.654 fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
11.655 let
11.656 - val P.Proof_Step {rule=r, prems, prop, ...} = step
11.657 + val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
11.658 val ps = map (lookup_proof ptab) prems
11.659 val _ = trace_before ctxt idx r
11.660 val (thm, (ctxt', ptab')) =
11.661 @@ -832,9 +870,10 @@
11.662 fun reconstruct outer_ctxt recon output =
11.663 let
11.664 val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
11.665 - val (asserted, steps, vars, ctxt1) = P.parse ctxt typs terms output
11.666 + val (asserted, steps, vars, ctxt1) =
11.667 + Z3_Proof_Parser.parse ctxt typs terms output
11.668
11.669 - val simpset = T.make_simpset ctxt1 (Z3_Simps.get ctxt1)
11.670 + val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
11.671
11.672 val ((is, rules), cxp as (ctxt2, _)) =
11.673 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