--- a/src/HOL/SMT.thy Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/SMT.thy Mon Dec 20 22:02:57 2010 +0100
@@ -17,13 +17,13 @@
("Tools/SMT/smt_translate.ML")
("Tools/SMT/smt_solver.ML")
("Tools/SMT/smtlib_interface.ML")
+ ("Tools/SMT/z3_interface.ML")
("Tools/SMT/z3_proof_parser.ML")
("Tools/SMT/z3_proof_tools.ML")
("Tools/SMT/z3_proof_literals.ML")
("Tools/SMT/z3_proof_methods.ML")
("Tools/SMT/z3_proof_reconstruction.ML")
("Tools/SMT/z3_model.ML")
- ("Tools/SMT/z3_interface.ML")
("Tools/SMT/smt_setup_solvers.ML")
begin
--- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 20 22:02:57 2010 +0100
@@ -47,15 +47,12 @@
structure SMT_Builtin: SMT_BUILTIN =
struct
-structure U = SMT_Utils
-structure C = SMT_Config
-
(* built-in tables *)
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
-type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Utils.dict
fun typ_ord ((T, _), (U, _)) =
let
@@ -68,16 +65,17 @@
in tord (T, U) end
fun insert_ttab cs T f =
- U.dict_map_default (cs, [])
+ SMT_Utils.dict_map_default (cs, [])
(Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
fun merge_ttab ttabp =
- U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
+ SMT_Utils.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp
fun lookup_ttab ctxt ttab T =
let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
in
- get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt))
+ get_first (find_first match)
+ (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt))
end
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
@@ -108,7 +106,7 @@
Builtin_Types.map (insert_ttab cs T (Int (f, g)))
fun add_builtin_typ_ext (T, f) =
- Builtin_Types.map (insert_ttab U.basicC T (Ext f))
+ Builtin_Types.map (insert_ttab SMT_Utils.basicC T (Ext f))
fun lookup_builtin_typ ctxt =
lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
@@ -168,7 +166,7 @@
in add_builtin_fun cs (c, bfun) end
fun add_builtin_fun_ext ((n, T), f) =
- Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
+ Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f))
fun add_builtin_fun_ext' c =
add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 20 22:02:57 2010 +0100
@@ -18,16 +18,14 @@
structure SMT_Normalize: SMT_NORMALIZE =
struct
-structure U = SMT_Utils
-structure B = SMT_Builtin
-
(* general theorem normalizations *)
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
+ val (cpfalse, cfalse) =
+ `SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -70,8 +68,8 @@
| _ => Conv.all_conv) ct
val setup_atomize =
- fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
- @{const_name all}, @{const_name Trueprop}]
+ fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
+ @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
(** unfold special quantifiers **)
@@ -100,10 +98,11 @@
in
fun unfold_special_quants_conv ctxt =
- U.if_exists_conv (is_some o special_quant)
+ SMT_Utils.if_exists_conv (is_some o special_quant)
(Conv.top_conv special_quant_conv ctxt)
-val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants
+val setup_unfolded_quants =
+ fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants
end
@@ -141,7 +140,8 @@
"must have the same kind: " ^ Syntax.string_of_term ctxt t)
fun check_trigger_conv ctxt ct =
- if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
+ if proper_quant false proper_trigger (SMT_Utils.term_of ct) then
+ Conv.all_conv ct
else check_trigger_error ctxt (Thm.term_of ct)
@@ -169,7 +169,7 @@
fun is_simp_lhs ctxt t =
(case Term.strip_comb t of
(Const c, ts as _ :: _) =>
- not (B.is_builtin_fun_ext ctxt c ts) andalso
+ not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
forall (is_constr_pat (ProofContext.theory_of ctxt)) ts
| _ => false)
@@ -194,8 +194,9 @@
Pattern.matches thy (t', u) andalso not (t aconv u))
in not (Term.exists_subterm some_match u) end
- val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1
- fun mk_pat ct = Thm.capply (U.instT' ct pat) ct
+ val pat =
+ SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
+ fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
fun mk_clist T = pairself (Thm.cterm_of @{theory})
(HOLogic.cons_const T, HOLogic.nil_const T)
@@ -231,20 +232,24 @@
| has_trigger _ = false
fun try_trigger_conv cv ct =
- if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
+ if SMT_Utils.under_quant has_trigger (SMT_Utils.term_of ct) then
+ Conv.all_conv ct
else Conv.try_conv cv ct
fun infer_trigger_conv ctxt =
if Config.get ctxt SMT_Config.infer_triggers then
- try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
+ try_trigger_conv
+ (SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
else Conv.all_conv
in
fun trigger_conv ctxt =
- U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
+ SMT_Utils.prop_conv
+ (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
-val setup_trigger = fold B.add_builtin_fun_ext''
- [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
+val setup_trigger =
+ fold SMT_Builtin.add_builtin_fun_ext''
+ [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
end
@@ -272,7 +277,8 @@
Syntax.string_of_term ctxt t)
fun check_weight_conv ctxt ct =
- if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
+ if SMT_Utils.under_quant proper_trigger (SMT_Utils.term_of ct) then
+ Conv.all_conv ct
else check_weight_error ctxt (Thm.term_of ct)
@@ -294,13 +300,14 @@
fun add_weight_conv NONE _ = Conv.all_conv
| add_weight_conv (SOME weight) ctxt =
let val cv = Conv.rewr_conv (mk_weight_eq weight)
- in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end
+ in SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
in
fun weight_conv weight ctxt =
- U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
+ SMT_Utils.prop_conv
+ (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
-val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight}
+val setup_weight = SMT_Builtin.add_builtin_fun_ext'' @{const_name SMT.weight}
end
@@ -355,11 +362,12 @@
"distinct [x, y] = (x ~= y)"
by simp_all}
fun distinct_conv _ =
- U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
+ SMT_Utils.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
in
-fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct
- (Conv.top_conv distinct_conv ctxt)
+fun trivial_distinct_conv ctxt =
+ SMT_Utils.if_exists_conv is_trivial_distinct
+ (Conv.top_conv distinct_conv ctxt)
end
@@ -373,13 +381,14 @@
val thm = mk_meta_eq @{lemma
"bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
- fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
+ fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
in
-fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case
- (Conv.top_conv unfold_conv ctxt)
+fun rewrite_bool_case_conv ctxt =
+ SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
-val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
+val setup_bool_case =
+ SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
end
@@ -400,7 +409,8 @@
val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
(@{const_name abs}, abs_def)]
- fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T)
+ fun is_builtinT ctxt T =
+ SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
fun abs_min_max ctxt (Const (n, T)) =
(case AList.lookup (op =) defs n of
@@ -415,10 +425,10 @@
in
fun unfold_abs_min_max_conv ctxt =
- U.if_exists_conv (is_some o abs_min_max ctxt)
+ SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt)
(Conv.top_conv unfold_amm_conv ctxt)
-val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs
+val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) defs
end
@@ -482,7 +492,7 @@
fun mk_number_eq ctxt i lhs =
let
- val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
+ val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
val ss = HOL_ss
addsimps [@{thm Nat_Numeral.int_nat_number_of}]
addsimps @{thms neg_simps}
@@ -508,11 +518,11 @@
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
and expand_conv ctxt =
- U.if_conv (is_nat_const o Term.head_of)
+ SMT_Utils.if_conv (is_nat_const o Term.head_of)
(expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
(int_conv ctxt)
- and nat_conv ctxt = U.if_exists_conv is_nat_const'
+ and nat_conv ctxt = SMT_Utils.if_exists_conv is_nat_const'
(Conv.top_sweep_conv expand_conv ctxt)
val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
@@ -525,8 +535,8 @@
else (thms, [])
val setup_nat_as_int =
- B.add_builtin_typ_ext (@{typ nat}, K true) #>
- fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
+ SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
+ fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
end
@@ -542,7 +552,7 @@
fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
(case try HOLogic.dest_number t of
- SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2
+ SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
| NONE => false)
| is_strange_number _ _ = false
@@ -558,12 +568,14 @@
"Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
by simp_all (simp add: pred_def)}
- fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt)
- (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
+ fun norm_num_conv ctxt =
+ SMT_Utils.if_conv (is_strange_number ctxt)
+ (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
in
-fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt)
- (Conv.top_sweep_conv norm_num_conv ctxt)
+fun normalize_numerals_conv ctxt =
+ SMT_Utils.if_exists_conv (is_strange_number ctxt)
+ (Conv.top_sweep_conv norm_num_conv ctxt)
end
@@ -599,18 +611,19 @@
structure Extra_Norms = Generic_Data
(
- type T = extra_norm U.dict
+ type T = extra_norm SMT_Utils.dict
val empty = []
val extend = I
- fun merge data = U.dict_merge fst data
+ fun merge data = SMT_Utils.dict_merge fst data
)
-fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
+fun add_extra_norm (cs, norm) =
+ Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
fun apply_extra_norms ithms ctxt =
let
val cs = SMT_Config.solver_class_of ctxt
- val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
+ val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
fun normalize iwthms ctxt =
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 20 22:02:57 2010 +0100
@@ -51,8 +51,6 @@
structure SMT_Solver: SMT_SOLVER =
struct
-structure C = SMT_Config
-
(* configuration *)
@@ -109,13 +107,13 @@
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
fun run ctxt cmd args input =
- (case C.certificates_of ctxt of
+ (case SMT_Config.certificates_of ctxt of
NONE =>
- if Config.get ctxt C.debug_files = "" then
+ if Config.get ctxt SMT_Config.debug_files = "" then
Cache_IO.run (make_cmd (choose cmd) args) input
else
let
- val base_path = Path.explode (Config.get ctxt C.debug_files)
+ val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
val in_path = Path.ext "smt_in" base_path
val out_path = Path.ext "smt_out" base_path
in
@@ -124,7 +122,7 @@
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
- if Config.get ctxt C.fixed then
+ if Config.get ctxt SMT_Config.fixed then
error ("Bad certificates cache: missing certificate")
else
Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
@@ -140,14 +138,14 @@
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
(map Pretty.str ls))
- val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
+ val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
val {redirected_output=res, output=err, return_code} =
- C.with_timeout ctxt (run ctxt cmd args) input
- val _ = C.trace_msg ctxt (pretty "Solver:") err
+ SMT_Config.with_timeout ctxt (run ctxt cmd args) input
+ val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
val ls = rev (snd (chop_while (equal "") (rev res)))
- val _ = C.trace_msg ctxt (pretty "Result:") ls
+ val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls
val _ = null ls andalso return_code <> 0 andalso
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
@@ -155,8 +153,9 @@
end
-fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+fun trace_assms ctxt =
+ SMT_Config.trace_msg ctxt (Pretty.string_of o
+ Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) =
let
@@ -164,7 +163,7 @@
fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t)
in
- C.trace_msg ctxt (fn () =>
+ SMT_Config.trace_msg ctxt (fn () =>
Pretty.string_of (Pretty.big_list "Names:" [
Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)),
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
@@ -172,10 +171,11 @@
fun invoke name cmd options ithms ctxt =
let
- val args = C.solver_options_of ctxt @ options ctxt
+ val args = SMT_Config.solver_options_of ctxt @ options ctxt
val comments = ("solver: " ^ name) ::
- ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
- ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
+ ("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) ::
+ ("random seed: " ^
+ string_of_int (Config.get ctxt SMT_Config.random_seed)) ::
"arguments:" :: args
val (str, recon as {context=ctxt', ...}) =
@@ -192,7 +192,7 @@
|> filter (fn i => i >= 0)
|> map_filter (AList.lookup (op =) iwthms)
in
- if Config.get ctxt C.trace_used_facts andalso length wthms > 0
+ if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0
then
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
(map (Display.pretty_thm ctxt o snd) wthms)))
@@ -243,7 +243,7 @@
(output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) =
(case outcome output of
(Unsat, ls) =>
- if not (Config.get ctxt C.oracle) andalso is_some reconstruct
+ if not (Config.get ctxt SMT_Config.oracle) andalso is_some reconstruct
then the reconstruct outer_ctxt recon ls
else ([], ocl ())
| (result, ls) =>
@@ -273,7 +273,7 @@
in
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
- Context.theory_map (C.add_solver (name, class))
+ Context.theory_map (SMT_Config.add_solver (name, class))
end
end
@@ -282,7 +282,7 @@
the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
fun name_and_solver_of ctxt =
- let val name = C.solver_of ctxt
+ let val name = SMT_Config.solver_of ctxt
in (name, get_info ctxt name) end
val solver_name_of = fst o name_and_solver_of
@@ -326,9 +326,9 @@
let
val ctxt =
Proof.context_of st
- |> Config.put C.oracle false
- |> Config.put C.drop_bad_facts true
- |> Config.put C.filter_only_facts true
+ |> Config.put SMT_Config.oracle false
+ |> Config.put SMT_Config.drop_bad_facts true
+ |> Config.put SMT_Config.filter_only_facts true
val {facts, goal, ...} = Proof.goal st
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
@@ -348,7 +348,7 @@
fun smt_filter_tail time_limit run_remote
((xs, wthms), ((iwthms', ctxt), iwthms)) =
let
- val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit)
+ val ctxt = ctxt |> Config.put SMT_Config.timeout (Time.toReal time_limit)
val xrules = xs ~~ map snd wthms
in
((iwthms', ctxt), iwthms)
@@ -369,15 +369,16 @@
THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
let
val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort
- val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
+ val tag = "Solver " ^ SMT_Config.solver_of ctxt' ^ ": "
val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
fun safe_solve iwthms =
if pass_exns then SOME (solve iwthms)
else (SOME (solve iwthms)
handle
SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
- (C.verbose_msg ctxt' str_of fail; NONE)
- | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
+ (SMT_Config.verbose_msg ctxt' str_of fail; NONE)
+ | SMT_Failure.SMT fail =>
+ (SMT_Config.trace_msg ctxt' str_of fail; NONE))
in
safe_solve (map (pair ~1 o pair NONE) (rules @ prems))
|> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 20 22:02:57 2010 +0100
@@ -45,9 +45,6 @@
structure SMT_Translate: SMT_TRANSLATE =
struct
-structure U = SMT_Utils
-structure B = SMT_Builtin
-
(* intermediate term structure *)
@@ -169,7 +166,7 @@
in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
fun expf k i T t =
- let val Ts = drop i (fst (U.dest_funT k T))
+ let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
in
Term.incr_boundvars (length Ts) t
|> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
@@ -195,7 +192,7 @@
| expand t =
(case Term.strip_comb t of
(u as Const (c as (_, T)), ts) =>
- (case B.dest_builtin ctxt c ts of
+ (case SMT_Builtin.dest_builtin ctxt c ts of
SOME (_, k, us, mk) =>
if k = length us then mk (map expand us)
else expf k (length ts) T (mk (map expand us))
@@ -302,8 +299,10 @@
(Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T)
fun apply i t T ts =
- let val (ts1, ts2) = chop i ts
- in fst (fold app ts2 (Term.list_comb (t, ts1), snd (U.dest_funT i T))) end
+ let
+ val (ts1, ts2) = chop i ts
+ val (_, U) = SMT_Utils.dest_funT i T
+ in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
in
fun intro_explicit_application ts =
@@ -351,14 +350,14 @@
@{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
fun is_builtin_conn_or_pred ctxt c ts =
- is_some (B.dest_builtin_conn ctxt c ts) orelse
- is_some (B.dest_builtin_pred ctxt c ts)
+ is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
+ is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
fun builtin b ctxt c ts =
(case (Const c, ts) of
(@{const HOL.eq (bool)}, [t, u]) =>
if t = @{const SMT.term_true} orelse u = @{const SMT.term_true} then
- B.dest_builtin_eq ctxt t u
+ SMT_Builtin.dest_builtin_eq ctxt t u
else b ctxt c ts
| _ => b ctxt c ts)
in
@@ -400,16 +399,16 @@
q $ Abs (n, T, in_trigger u)
else as_term (in_term t)
| (Const c, ts) =>
- (case B.dest_builtin_conn ctxt c ts of
+ (case SMT_Builtin.dest_builtin_conn ctxt c ts of
SOME (_, _, us, mk) => mk (map in_form us)
| NONE =>
- (case B.dest_builtin_pred ctxt c ts of
+ (case SMT_Builtin.dest_builtin_pred ctxt c ts of
SOME (_, _, us, mk) => mk (map in_term us)
| NONE => as_term (in_term t)))
| _ => as_term (in_term t))
in
map (reduce_let #> in_form) #>
- cons (U.prop_of term_bool) #>
+ cons (SMT_Utils.prop_of term_bool) #>
pair (fol_rules, [term_bool], builtin)
end
@@ -466,7 +465,7 @@
fun transT (T as TFree _) = add_typ T true
| transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
| transT (T as Type _) =
- (case B.dest_builtin_typ ctxt T of
+ (case SMT_Builtin.dest_builtin_typ ctxt T of
SOME n => pair n
| NONE => add_typ T true)
@@ -492,7 +491,7 @@
| _ => raise TERM ("bad SMT term", [t]))
and transs t T ts =
- let val (Us, U) = U.dest_funT (length ts) T
+ let val (Us, U) = SMT_Utils.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
@@ -507,21 +506,21 @@
structure Configs = Generic_Data
(
- type T = (Proof.context -> config) U.dict
+ type T = (Proof.context -> config) SMT_Utils.dict
val empty = []
val extend = I
- fun merge data = U.dict_merge fst data
+ fun merge data = SMT_Utils.dict_merge fst data
)
-fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
+fun add_config (cs, cfg) = Configs.map (SMT_Utils.dict_update (cs, cfg))
fun get_config ctxt =
let val cs = SMT_Config.solver_class_of ctxt
in
- (case U.dict_get (Configs.get (Context.Proof ctxt)) cs of
+ (case SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of
SOME cfg => cfg ctxt
| NONE => error ("SMT: no translation configuration found " ^
- "for solver class " ^ quote (U.string_of_class cs)))
+ "for solver class " ^ quote (SMT_Utils.string_of_class cs)))
end
fun translate ctxt comments ithms =
@@ -533,7 +532,7 @@
fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
- val ts1 = map (Envir.beta_eta_contract o U.prop_of o snd) ithms
+ val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms
val ((dtyps, tr_context, ctxt1), ts2) =
((make_tr_context prefixes, ctxt), ts1)
@@ -551,7 +550,7 @@
val rewrite_rules' = fun_app_eq :: rewrite_rules
in
(ts4, tr_context)
- |-> intermediate header dtyps (builtin B.dest_builtin) ctxt2
+ |-> intermediate header dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
|>> uncurry (serialize comments)
||> recon_of ctxt2 rewrite_rules' extra_thms ithms
end
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 20 22:02:57 2010 +0100
@@ -16,10 +16,6 @@
structure SMTLIB_Interface: SMTLIB_INTERFACE =
struct
-structure U = SMT_Utils
-structure B = SMT_Builtin
-structure N = SMT_Normalize
-structure T = SMT_Translate
val smtlibC = ["smtlib"]
@@ -29,8 +25,8 @@
local
fun int_num _ i = SOME (string_of_int i)
- fun is_linear [t] = U.is_number t
- | is_linear [t, u] = U.is_number t orelse U.is_number u
+ fun is_linear [t] = SMT_Utils.is_number t
+ | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u
| is_linear _ = false
fun times _ _ ts =
@@ -49,8 +45,8 @@
in
val setup_builtins =
- B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
- fold (B.add_builtin_fun' smtlibC) [
+ SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
+ fold (SMT_Builtin.add_builtin_fun' smtlibC) [
(@{const True}, "true"),
(@{const False}, "false"),
(@{const Not}, "not"),
@@ -66,8 +62,10 @@
(@{const uminus (int)}, "~"),
(@{const plus (int)}, "+"),
(@{const minus (int)}, "-") ] #>
- B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #>
- B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
+ SMT_Builtin.add_builtin_fun smtlibC
+ (Term.dest_Const @{const times (int)}, times) #>
+ SMT_Builtin.add_builtin_fun smtlibC
+ (Term.dest_Const @{const distinct ('a)}, distinct)
end
@@ -106,18 +104,20 @@
fun var i = add "?v" #> add (string_of_int i)
-fun sterm l (T.SVar i) = sep (var (l - i - 1))
- | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
- | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
- | sterm l (T.SQua (q, ss, ps, w, t)) =
+fun sterm l (SMT_Translate.SVar i) = sep (var (l - i - 1))
+ | sterm l (SMT_Translate.SApp (n, ts)) = app n (sterm l) ts
+ | sterm _ (SMT_Translate.SLet _) =
+ raise Fail "SMT-LIB: unsupported let expression"
+ | sterm l (SMT_Translate.SQua (q, ss, ps, w, t)) =
let
- val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
+ fun quant SMT_Translate.SForall = add "forall"
+ | quant SMT_Translate.SExists = add "exists"
val vs = map_index (apfst (Integer.add l)) ss
fun var_decl (i, s) = par (var i #> sep (add s))
val sub = sterm (l + length ss)
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
- fun pats (T.SPat ts) = pat ":pat" ts
- | pats (T.SNoPat ts) = pat ":nopat" ts
+ fun pats (SMT_Translate.SPat ts) = pat ":pat" ts
+ | pats (SMT_Translate.SNoPat ts) = pat ":nopat" ts
fun weight NONE = I
| weight (SOME i) =
sep (add ":weight { " #> add (string_of_int i) #> add " }")
@@ -168,6 +168,6 @@
val setup = Context.theory_map (
setup_builtins #>
- T.add_config (smtlibC, translate_config))
+ SMT_Translate.add_config (smtlibC, translate_config))
end
--- a/src/HOL/Tools/SMT/z3_model.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Mon Dec 20 22:02:57 2010 +0100
@@ -13,8 +13,6 @@
structure Z3_Model: Z3_MODEL =
struct
-structure U = SMT_Utils
-
(* counterexample expressions *)
@@ -125,7 +123,7 @@
| trans_expr T (Value i) = pair (Var (("value", i), T))
| trans_expr T (Array a) = trans_array T a
| trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
- let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
+ let val Ts = fst (SMT_Utils.dest_funT (length es') (Term.fastype_of t))
in
fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
end)
@@ -167,7 +165,7 @@
fun translate ((t, k), (e, cs)) =
let
val T = Term.fastype_of t
- val (Us, U) = U.dest_funT k (Term.fastype_of t)
+ val (Us, U) = SMT_Utils.dest_funT k (Term.fastype_of t)
fun mk_full_def u' pats =
pats
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Dec 20 22:02:57 2010 +0100
@@ -33,19 +33,17 @@
structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
struct
-structure U = SMT_Utils
-structure T = Z3_Proof_Tools
-
(* literal table *)
type littab = thm Termtab.table
-fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
+fun make_littab thms =
+ fold (Termtab.update o `SMT_Utils.prop_of) thms Termtab.empty
-fun insert_lit thm = Termtab.update (`U.prop_of thm)
-fun delete_lit thm = Termtab.delete (U.prop_of thm)
+fun insert_lit thm = Termtab.update (`SMT_Utils.prop_of thm)
+fun delete_lit thm = Termtab.delete (SMT_Utils.prop_of thm)
fun lookup_lit lits = Termtab.lookup lits
fun get_first_lit f =
Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
@@ -93,18 +91,20 @@
(** explosion of conjunctions and disjunctions **)
local
+ val precomp = Z3_Proof_Tools.precompose2
+
fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
- val dest_conj1 = T.precompose2 destc @{thm conjunct1}
- val dest_conj2 = T.precompose2 destc @{thm conjunct2}
+ val dest_conj1 = precomp destc @{thm conjunct1}
+ val dest_conj2 = precomp destc @{thm conjunct2}
fun dest_conj_rules t =
dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
- val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
- val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
- val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
- val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
+ val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
+ val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
+ val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
+ val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
fun dest_disj_rules t =
(case dest_disj_term' is_neg t of
@@ -115,7 +115,7 @@
| NONE => NONE)
fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
- val dneg_rule = T.precompose destn @{thm notnotD}
+ val dneg_rule = Z3_Proof_Tools.precompose destn @{thm notnotD}
in
(*
@@ -150,7 +150,7 @@
(*
extract a literal by applying previously collected rules
*)
-fun extract_lit thm rules = fold T.compose rules thm
+fun extract_lit thm rules = fold Z3_Proof_Tools.compose rules thm
(*
@@ -162,9 +162,9 @@
val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
fun explode1 thm =
- if Termtab.defined tab (U.prop_of thm) then cons thm
+ if Termtab.defined tab (SMT_Utils.prop_of thm) then cons thm
else
- (case dest_rules (U.prop_of thm) of
+ (case dest_rules (SMT_Utils.prop_of thm) of
SOME (rule1, rule2) =>
explode2 rule1 thm #>
explode2 rule2 thm #>
@@ -172,13 +172,14 @@
| NONE => cons thm)
and explode2 dest_rule thm =
- if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm)
- then explode1 (T.compose dest_rule thm)
- else cons (T.compose dest_rule thm)
+ if full orelse
+ exists_lit is_conj (Termtab.defined tab) (SMT_Utils.prop_of thm)
+ then explode1 (Z3_Proof_Tools.compose dest_rule thm)
+ else cons (Z3_Proof_Tools.compose dest_rule thm)
fun explode0 thm =
- if not is_conj andalso is_dneg (U.prop_of thm)
- then [T.compose dneg_rule thm]
+ if not is_conj andalso is_dneg (SMT_Utils.prop_of thm)
+ then [Z3_Proof_Tools.compose dneg_rule thm]
else explode1 thm []
in explode0 end
@@ -195,7 +196,7 @@
fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
- |> T.discharge thm1 |> T.discharge thm2
+ |> Z3_Proof_Tools.discharge thm1 |> Z3_Proof_Tools.discharge thm2
fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -219,13 +220,15 @@
fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
- val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
- val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
+ val precomp = Z3_Proof_Tools.precompose
+ val dnegE = precomp (single o d2 o d1) @{thm notnotD}
+ val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
+ val precomp2 = Z3_Proof_Tools.precompose2
fun dni f = apsnd f o Thm.dest_binop o f o d1
- val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
- val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
+ val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
+ val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
val iff_const = @{const HOL.eq (bool)}
fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
@@ -241,16 +244,17 @@
fun lookup_rule t =
(case t of
- @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+ @{const Not} $ (@{const Not} $ t) =>
+ (Z3_Proof_Tools.compose dnegI, lookup t)
| @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
- (T.compose negIffI, lookup (iff_const $ u $ t))
+ (Z3_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t))
| @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
| _ =>
(case as_dneg lookup t of
- NONE => (T.compose negIffE, as_negIff lookup t)
- | x => (T.compose dnegE, x)))
+ NONE => (Z3_Proof_Tools.compose negIffE, as_negIff lookup t)
+ | x => (Z3_Proof_Tools.compose dnegE, x)))
fun join1 (s, t) =
(case lookup t of
@@ -285,7 +289,7 @@
val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
fun contra_left conj thm =
let
- val rules = explode_term conj (U.prop_of thm)
+ val rules = explode_term conj (SMT_Utils.prop_of thm)
fun contra_lits (t, rs) =
(case t of
@{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
@@ -303,7 +307,8 @@
fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
in
fun contradict conj ct =
- iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct)
+ iff_intro (Z3_Proof_Tools.under_assumption (contra_left conj) ct)
+ (contra_right ct)
end
@@ -314,8 +319,8 @@
fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
- val thm1 = T.under_assumption (prove r cr o make_tab l) cl
- val thm2 = T.under_assumption (prove l cl o make_tab r) cr
+ val thm1 = Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
+ val thm2 = Z3_Proof_Tools.under_assumption (prove l cl o make_tab r) cr
in iff_intro thm1 thm2 end
datatype conj_disj = CONJ | DISJ | NCON | NDIS
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Dec 20 22:02:57 2010 +0100
@@ -12,9 +12,6 @@
structure Z3_Proof_Methods: Z3_PROOF_METHODS =
struct
-structure U = SMT_Utils
-structure T = Z3_Proof_Tools
-
fun apply tac st =
(case Seq.pull (tac 1 st) of
@@ -36,24 +33,24 @@
fun mk_inv_of ctxt ct =
let
- val (dT, rT) = Term.dest_funT (U.typ_of ct)
- val inv = U.certify ctxt (mk_inv_into dT rT)
- val univ = U.certify ctxt (mk_univ dT)
+ val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
+ val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT)
+ val univ = SMT_Utils.certify ctxt (mk_univ dT)
in Thm.mk_binop inv univ ct end
fun mk_inj_prop ctxt ct =
let
- val (dT, rT) = Term.dest_funT (U.typ_of ct)
- val inj = U.certify ctxt (mk_inj_on dT rT)
- val univ = U.certify ctxt (mk_univ dT)
- in U.mk_cprop (Thm.mk_binop inj ct univ) end
+ val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
+ val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT)
+ val univ = SMT_Utils.certify ctxt (mk_univ dT)
+ in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
fun prove_inj_prop ctxt def lhs =
let
- val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
+ val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
in
Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
@@ -64,7 +61,7 @@
end
fun prove_rhs ctxt def lhs =
- T.by_tac (
+ Z3_Proof_Tools.by_tac (
CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
@@ -82,24 +79,27 @@
fun prove_lhs ctxt rhs =
let
val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
+ val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
in
- T.by_tac (
- CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
+ Z3_Proof_Tools.by_tac (
+ CONVERSION (SMT_Utils.prop_conv conv)
THEN' Simplifier.simp_tac HOL_ss)
end
fun mk_inv_def ctxt rhs =
let
- val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
+ val (ct, ctxt') =
+ SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
val (cl, cv) = Thm.dest_binop ct
val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
- in Thm.assume (U.mk_cequals cg cu) end
+ in Thm.assume (SMT_Utils.mk_cequals cg cu) end
fun prove_inj_eq ctxt ct =
let
- val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
+ val (lhs, rhs) =
+ pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct))
val lhs_thm = prove_lhs ctxt rhs lhs
val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
@@ -109,22 +109,22 @@
val swap_disj_thm = mk_meta_eq @{thm disj_commute}
fun swap_conv dest eq =
- U.if_true_conv ((op <) o pairself Term.size_of_term o dest)
+ SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
(Conv.rewr_conv eq)
val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
-val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm
+val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm
fun norm_conv ctxt =
swap_eq_conv then_conv
- Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv
- Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt)
+ Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv
+ Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt)
in
fun prove_injectivity ctxt =
- T.by_tac (
- CONVERSION (U.prop_conv (norm_conv ctxt))
+ Z3_Proof_Tools.by_tac (
+ CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
end
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Dec 20 22:02:57 2010 +0100
@@ -31,9 +31,6 @@
structure Z3_Proof_Parser: Z3_PROOF_PARSER =
struct
-structure U = SMT_Utils
-structure I = Z3_Interface
-
(* proof rules *)
@@ -113,7 +110,8 @@
let
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
- fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+ fun mk (i, v) =
+ (v, SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
fun close ctxt (ct, vars) =
@@ -124,7 +122,7 @@
fun mk_bound ctxt (i, T) =
- let val ct = U.certify ctxt (Var ((Name.uu, 0), T))
+ let val ct = SMT_Utils.certify ctxt (Var ((Name.uu, 0), T))
in (ct, [(i, ct)]) end
local
@@ -133,11 +131,13 @@
val cv =
(case AList.lookup (op =) vars 0 of
SOME cv => cv
- | _ => U.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
+ | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
- in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
+ val vars' = map_filter dec vars
+ in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
- fun quant name = U.mk_const_pat @{theory} name (U.destT1 o U.destT1)
+ fun quant name =
+ SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
val forall = quant @{const_name All}
val exists = quant @{const_name Ex}
in
@@ -197,7 +197,7 @@
|> Symtab.fold (Variable.declare_term o snd) terms
fun cert @{const True} = not_false
- | cert t = U.certify ctxt' t
+ | cert t = SMT_Utils.certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
@@ -212,20 +212,21 @@
SOME _ => cx
| NONE => cx |> fresh_name (decl_prefix ^ n)
|> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
- let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
+ let
+ val upd = Symtab.update (n, SMT_Utils.certify ctxt (Free (m, T)))
in (typs, upd terms, exprs, steps, vars, ctxt) end))
-fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) =
- (case I.mk_builtin_typ ctxt s of
+fun mk_typ (typs, _, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _)) =
+ (case Z3_Interface.mk_builtin_typ ctxt s of
SOME T => SOME T
| NONE => Symtab.lookup typs n)
fun mk_num (_, _, _, _, _, ctxt) (i, T) =
- mk_fun (K (I.mk_builtin_num ctxt i T)) []
+ mk_fun (K (Z3_Interface.mk_builtin_num ctxt i T)) []
-fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) =
+fun mk_app (_, terms, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _), es) =
mk_fun (fn cts =>
- (case I.mk_builtin_fun ctxt s cts of
+ (case Z3_Interface.mk_builtin_fun ctxt s cts of
SOME ct => SOME ct
| NONE =>
Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es
@@ -243,8 +244,8 @@
| part (NONE, i) (cts, ps) = (cts, i :: ps)
val (args', prems) = fold (part o `(lookup_expr cx)) args ([], [])
val (cts, vss) = split_list args'
- val step =
- Proof_Step {rule=r, args=rev cts, prems=rev prems, prop=U.mk_cprop ct}
+ val step = Proof_Step {rule=r, args=rev cts, prems=rev prems,
+ prop = SMT_Utils.mk_cprop ct}
val vars' = fold (union (op =)) (vs :: vss) vars
in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end
@@ -326,8 +327,8 @@
fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
-fun sym st =
- (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st
+fun sym st = (name --
+ Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Z3_Interface.Sym) st
fun id st = ($$ "#" |-- nat_num) st
@@ -337,7 +338,7 @@
fun sort st = Scan.first [
this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
- sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn
+ sym :|-- (fn s as Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn
SOME T => Scan.succeed T
| NONE => scan_exn ("unknown sort: " ^ quote n)))] st
@@ -348,11 +349,13 @@
SOME n' => Scan.succeed n'
| NONE => scan_exn ("unknown number: " ^ quote (string_of_int i)))
-fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn
- SOME app' => Scan.succeed app'
- | NONE => scan_exn ("unknown function symbol: " ^ quote n))
+fun appl (app as (Z3_Interface.Sym (n, _), _)) =
+ lookup_context mk_app app :|-- (fn
+ SOME app' => Scan.succeed app'
+ | NONE => scan_exn ("unknown function symbol: " ^ quote n))
-fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st
+fun bv_size st = (digits >> (fn sz =>
+ Z3_Interface.Sym ("bv", [Z3_Interface.Sym (sz, [])]))) st
fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn
SOME cT => Scan.succeed cT
@@ -364,7 +367,7 @@
fun frac_number st = (
int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) =>
numb (i, T) -- numb (j, T) :|-- (fn (n, m) =>
- appl (I.Sym ("/", []), [n, m])))) st
+ appl (Z3_Interface.Sym ("/", []), [n, m])))) st
fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Dec 20 22:02:57 2010 +0100
@@ -15,11 +15,6 @@
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
struct
-structure U = SMT_Utils
-structure P = Z3_Proof_Parser
-structure T = Z3_Proof_Tools
-structure L = Z3_Proof_Literals
-structure M = Z3_Proof_Methods
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
("Z3 proof reconstruction: " ^ msg))
@@ -43,7 +38,8 @@
val merge = Net.merge eq
)
- val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true]
+ val prep =
+ `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
@@ -55,7 +51,7 @@
val add_z3_rule = Z3_Rules.map o ins
fun by_schematic_rule ctxt ct =
- the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
+ the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
val z3_rules_setup =
Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
@@ -115,7 +111,7 @@
datatype theorem =
Thm of thm | (* theorem without special features *)
MetaEq of thm | (* meta equality "t == s" *)
- Literals of thm * L.littab
+ Literals of thm * Z3_Proof_Literals.littab
(* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
fun thm_of (Thm thm) = thm
@@ -126,7 +122,7 @@
| meta_eq_of p = mk_meta_eq (thm_of p)
fun literals_of (Literals (_, lits)) = lits
- | literals_of p = L.make_littab [thm_of p]
+ | literals_of p = Z3_Proof_Literals.make_littab [thm_of p]
@@ -143,27 +139,27 @@
(Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
- remove_fun_app, L.rewrite_true]
+ remove_fun_app, Z3_Proof_Literals.rewrite_true]
fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
fun lookup_assm assms_net ct =
- T.net_instance' burrow_snd_option assms_net ct
+ Z3_Proof_Tools.net_instance' burrow_snd_option assms_net ct
|> Option.map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
in
fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
let
- val eqs = map (rewrite ctxt [L.rewrite_true]) rewrite_rules
+ val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules
val eqs' = union Thm.eq_thm eqs prep_rules
val assms_net =
assms
|> map (apsnd (rewrite ctxt eqs'))
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> T.thm_net_of snd
+ |> Z3_Proof_Tools.thm_net_of snd
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
@@ -202,17 +198,20 @@
(* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *)
local
- val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
- val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
+ val precomp = Z3_Proof_Tools.precompose2
+ val comp = Z3_Proof_Tools.compose
- val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
- val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
+ val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
+ val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
+
+ val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
+ val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
in
-fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
+fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
| mp p_q p =
let
val pq = thm_of p_q
- val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
+ val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
in Thm (Thm.implies_elim thm p) end
end
@@ -220,23 +219,25 @@
(* and_elim: P1 & ... & Pn ==> Pi *)
(* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *)
local
- fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
+ fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
fun derive conj t lits idx ptab =
let
- val lit = the (L.get_first_lit (is_sublit conj t) lits)
- val ls = L.explode conj false false [t] lit
- val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
+ val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
+ val ls = Z3_Proof_Literals.explode conj false false [t] lit
+ val lits' = fold Z3_Proof_Literals.insert_lit ls
+ (Z3_Proof_Literals.delete_lit lit lits)
fun upd thm = Literals (thm_of thm, lits')
- in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
+ val ptab' = Inttab.map_entry idx upd ptab
+ in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end
fun lit_elim conj (p, idx) ct ptab =
let val lits = literals_of p
in
- (case L.lookup_lit lits (U.term_of ct) of
+ (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
SOME lit => (Thm lit, ptab)
- | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
+ | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
end
in
val and_elim = lit_elim true
@@ -248,36 +249,42 @@
local
fun step lit thm =
Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
- val explode_disj = L.explode false false false
+ val explode_disj = Z3_Proof_Literals.explode false false false
fun intro hyps thm th = fold step (explode_disj hyps th) thm
fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
- val ccontr = T.precompose dest_ccontr @{thm ccontr}
+ val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
in
fun lemma thm ct =
let
- val cu = L.negate (Thm.dest_arg ct)
+ val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
- in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
+ val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
+ in Thm (Z3_Proof_Tools.compose ccontr th) end
end
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
local
- val explode_disj = L.explode false true false
- val join_disj = L.join false
+ val explode_disj = Z3_Proof_Literals.explode false true false
+ val join_disj = Z3_Proof_Literals.join false
fun unit thm thms th =
- let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
- in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
+ let
+ val t = @{const Not} $ SMT_Utils.prop_of thm
+ val ts = map SMT_Utils.prop_of thms
+ in
+ join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
+ end
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
- val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
+ val contrapos =
+ Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
in
fun unit_resolution thm thms ct =
- L.negate (Thm.dest_arg ct)
- |> T.under_assumption (unit thm thms)
- |> Thm o T.discharge thm o T.compose contrapos
+ Z3_Proof_Literals.negate (Thm.dest_arg ct)
+ |> Z3_Proof_Tools.under_assumption (unit thm thms)
+ |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
end
@@ -293,7 +300,7 @@
(* distributivity of | over & *)
fun distributivity ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
(* FIXME: not very well tested *)
@@ -305,11 +312,15 @@
val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
fun prove' conj1 conj2 ct2 thm =
- let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
- in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
+ let
+ val littab =
+ Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
+ |> cons Z3_Proof_Literals.true_thm
+ |> Z3_Proof_Literals.make_littab
+ in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
fun prove rule (ct1, conj1) (ct2, conj2) =
- T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
+ Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
fun prove_def_axiom ct =
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
@@ -318,32 +329,34 @@
@{const Not} $ (@{const HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
| @{const HOL.conj} $ _ $ _ =>
- prove disjI3 (L.negate ct2, false) (ct1, true)
+ prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
| @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
- prove disjI3 (L.negate ct2, false) (ct1, false)
+ prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
| @{const HOL.disj} $ _ $ _ =>
- prove disjI2 (L.negate ct1, false) (ct2, true)
+ prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
| Const (@{const_name distinct}, _) $ _ =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
+ val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
fun prv cu =
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
- in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
+ in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
| @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
+ val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
fun prv cu =
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
- in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
+ in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
| _ => raise CTERM ("prove_def_axiom", [ct]))
end
in
fun def_axiom ctxt = Thm o try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_def_axiom,
- T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
+ Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
end
@@ -360,14 +373,14 @@
@{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
by (atomize(full)) fastsimp} ]
- val inst_rule = T.match_instantiate Thm.dest_arg
+ val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
fun apply_rule ct =
(case get_first (try (inst_rule ct)) intro_rules of
SOME thm => thm
| NONE => raise CTERM ("intro_def", [ct]))
in
-fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm
+fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
fun apply_def thm =
get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
@@ -394,17 +407,20 @@
(Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
(Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+ fun nnf_quant_tac_varified vars eq =
+ nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
+
fun nnf_quant vars qs p ct =
- T.as_meta_eq ct
- |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
+ Z3_Proof_Tools.as_meta_eq ct
+ |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
fun prove_nnf ctxt = try_apply ctxt [] [
- named ctxt "conj/disj" L.prove_conj_disj_eq,
- T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
- named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
+ named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
+ Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+ named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))]
in
fun nnf ctxt vars ps ct =
- (case U.term_of ct of
+ (case SMT_Utils.term_of ct of
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
if l aconv r
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
@@ -414,8 +430,9 @@
| _ =>
let
val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
- (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
- in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
+ (Z3_Proof_Tools.unfold_eqs ctxt
+ (map (Thm.symmetric o meta_eq_of) ps)))
+ in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
end
@@ -483,15 +500,15 @@
SOME eq => eq
| NONE => if exn then raise MONO else prove_refl cp)
- val prove_eq_exn = prove_eq true
- and prove_eq_safe = prove_eq false
+ val prove_exn = prove_eq true
+ and prove_safe = prove_eq false
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
- | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
- | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
- | _ => prove (prove_eq_safe f)) cp
+ @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
+ | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
+ | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
+ | _ => prove (prove_safe f)) cp
in
fun monotonicity eqs ct =
let
@@ -499,7 +516,7 @@
val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
val lookup = AList.lookup (op aconv) teqs
val cp = Thm.dest_binop (Thm.dest_arg ct)
- in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
+ in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
end
@@ -507,7 +524,9 @@
local
val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
in
-fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
+fun commutativity ct =
+ MetaEq (Z3_Proof_Tools.match_instantiate I
+ (Z3_Proof_Tools.as_meta_eq ct) rule)
end
@@ -524,21 +543,22 @@
fun quant_intro vars p ct =
let
val thm = meta_eq_of p
- val rules' = T.varify vars thm :: rules
- val cu = T.as_meta_eq ct
- in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
+ val rules' = Z3_Proof_Tools.varify vars thm :: rules
+ val cu = Z3_Proof_Tools.as_meta_eq ct
+ val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
+ in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
end
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
fun pull_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
(* FIXME: not very well tested *)
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
fun push_quant ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
(* FIXME: not very well tested *)
@@ -556,13 +576,13 @@
Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
ORELSE' CONVERSION (elim_unused_conv ctxt))
in
-fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
+fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
end
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
- named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))]
(* FIXME: not very well tested *)
@@ -570,7 +590,7 @@
local
val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
in
-val quant_inst = Thm o T.by_tac (
+val quant_inst = Thm o Z3_Proof_Tools.by_tac (
REPEAT_ALL_NEW (Tactic.match_tac [rule])
THEN' Tactic.rtac @{thm excluded_middle})
end
@@ -599,7 +619,7 @@
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
| kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
- (sk_all_rule, Thm.dest_arg, L.negate)
+ (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate)
| kind t = raise TERM ("skolemize", [t])
fun dest_abs_type (Abs (_, T, _)) = T
@@ -628,7 +648,8 @@
(case mct of
SOME ct =>
ctxt
- |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
+ |> Z3_Proof_Tools.make_hyp_def
+ (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
|>> pair ((cv, ct) :: is) o Thm.transitive thm
| NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
in
@@ -649,10 +670,12 @@
(* theory lemmas: linear arithmetic, arrays *)
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
- T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
- NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
- ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
- Arith_Data.arith_tac ctxt')))]
+ Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' =>
+ Z3_Proof_Tools.by_tac (
+ NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
+ ORELSE' NAMED ctxt' "simp+arith" (
+ Simplifier.simp_tac simpset
+ THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
(* rewriting: prove equalities:
@@ -680,14 +703,18 @@
| prep (Literals (thm, _)) = spec_meta_eq_of thm
fun unfold_conv ctxt ths =
- Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
+ Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
+ (map prep ths)))
fun with_conv _ [] prv = prv
- | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
+ | with_conv ctxt ths prv =
+ Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
val unfold_conv =
- Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
- val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
+ Conv.arg_conv (Conv.binop_conv
+ (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
+ val prove_conj_disj_eq =
+ Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
fun assume_prems ctxt thm =
Assumption.add_assumes (Drule.cprems_of thm) ctxt
@@ -697,20 +724,23 @@
fun rewrite simpset ths ct ctxt =
apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
named ctxt "conj/disj/distinct" prove_conj_disj_eq,
- T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
- T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW (
- NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
- ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
- T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW (
- NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
- ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
- named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
+ Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' =>
+ Z3_Proof_Tools.by_tac (
+ NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+ Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' =>
+ Z3_Proof_Tools.by_tac (
+ NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW (
+ NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+ ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
+ Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' =>
+ Z3_Proof_Tools.by_tac (
+ NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW (
+ NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+ ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
+ named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct))
end
@@ -721,7 +751,7 @@
(** tracing and checking **)
fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
- "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r)
+ "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)
fun check_after idx r ps ct (p, (ctxt, _)) =
if not (Config.get ctxt SMT_Config.trace) then ()
@@ -729,11 +759,13 @@
let val thm = thm_of p |> tap (Thm.join_proofs o single)
in
if (Thm.cprop_of thm) aconvc ct then ()
- else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
- quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
+ else
+ z3_exn (Pretty.string_of (Pretty.big_list
+ ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
+ " (#" ^ string_of_int idx ^ ")")
(pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
- [Pretty.block [Pretty.str "expected: ",
- Syntax.pretty_term ctxt (Thm.term_of ct)]])))
+ [Pretty.block [Pretty.str "expected: ",
+ Syntax.pretty_term ctxt (Thm.term_of ct)]])))
end
@@ -741,61 +773,67 @@
local
fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
- quote (P.string_of_rule r))
+ quote (Z3_Proof_Parser.string_of_rule r))
fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
(case (r, ps) of
(* core rules *)
- (P.True_Axiom, _) => (Thm L.true_thm, cxp)
- | (P.Asserted, _) => raise Fail "bad assertion"
- | (P.Goal, _) => raise Fail "bad assertion"
- | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
- | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
- | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
- | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
- | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
- | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
- | (P.Unit_Resolution, (p, _) :: ps) =>
+ (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
+ | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
+ | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
+ | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
+ (mp q (thm_of p), cxp)
+ | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
+ (mp q (thm_of p), cxp)
+ | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
+ and_elim (p, i) ct ptab ||> pair cx
+ | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
+ not_or_elim (p, i) ct ptab ||> pair cx
+ | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
+ | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
+ | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
(unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
- | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
- | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
- | (P.Distributivity, _) => (distributivity cx ct, cxp)
- | (P.Def_Axiom, _) => (def_axiom cx ct, cxp)
- | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab
- | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
- | (P.Iff_Oeq, [(p, _)]) => (p, cxp)
- | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
- | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
+ | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
+ | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
+ | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
+ | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
+ | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
+ | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
+ | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
+ | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
+ | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
(* equality rules *)
- | (P.Reflexivity, _) => (refl ct, cxp)
- | (P.Symmetry, [(p, _)]) => (symm p, cxp)
- | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
- | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
- | (P.Commutativity, _) => (commutativity ct, cxp)
+ | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
+ | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
+ | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
+ | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
+ | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
(* quantifier rules *)
- | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
- | (P.Pull_Quant, _) => (pull_quant cx ct, cxp)
- | (P.Push_Quant, _) => (push_quant cx ct, cxp)
- | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
- | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
- | (P.Quant_Inst, _) => (quant_inst ct, cxp)
- | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
+ | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
+ | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
+ | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
+ | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
+ | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
+ | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
+ | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab
(* theory rules *)
- | (P.Th_Lemma _, _) => (* FIXME: use arguments *)
+ | (Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *)
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
- | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
- | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
+ | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
+ | (Z3_Proof_Parser.Rewrite_Star, ps) =>
+ rewrite simpset (map fst ps) ct cx ||> rpair ptab
- | (P.Nnf_Star, _) => not_supported r
- | (P.Cnf_Star, _) => not_supported r
- | (P.Transitivity_Star, _) => not_supported r
- | (P.Pull_Quant_Star, _) => not_supported r
+ | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
+ | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
+ | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
+ | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
- | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
- " has an unexpected number of arguments."))
+ | _ => raise Fail ("Z3: proof rule " ^
+ quote (Z3_Proof_Parser.string_of_rule r) ^
+ " has an unexpected number of arguments."))
fun lookup_proof ptab idx =
(case Inttab.lookup ptab idx of
@@ -804,7 +842,7 @@
fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
let
- val P.Proof_Step {rule=r, prems, prop, ...} = step
+ val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
val ps = map (lookup_proof ptab) prems
val _ = trace_before ctxt idx r
val (thm, (ctxt', ptab')) =
@@ -832,9 +870,10 @@
fun reconstruct outer_ctxt recon output =
let
val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
- val (asserted, steps, vars, ctxt1) = P.parse ctxt typs terms output
+ val (asserted, steps, vars, ctxt1) =
+ Z3_Proof_Parser.parse ctxt typs terms output
- val simpset = T.make_simpset ctxt1 (Z3_Simps.get ctxt1)
+ val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
val ((is, rules), cxp as (ctxt2, _)) =
add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Dec 20 21:04:45 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Dec 20 22:02:57 2010 +0100
@@ -44,14 +44,12 @@
structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
struct
-structure U = SMT_Utils
-structure I = Z3_Interface
-
(* modifying terms *)
-fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
+fun as_meta_eq ct =
+ uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct))
@@ -80,7 +78,7 @@
(* proof combinators *)
fun under_assumption f ct =
- let val ct' = U.mk_cprop ct
+ let val ct' = SMT_Utils.mk_cprop ct
in Thm.implies_intr ct' (f (Thm.assume ct')) end
fun with_conv conv prove ct =
@@ -109,7 +107,7 @@
let
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
val (cf, cvs) = Drule.strip_comb lhs
- val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
+ val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
fun apply cv th =
Thm.combination th (Thm.reflexive cv)
|> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
@@ -149,8 +147,8 @@
| NONE =>
let
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
- val cv = U.certify ctxt'
- (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
+ val cv = SMT_Utils.certify ctxt'
+ (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
val cu = Drule.list_comb (cv, cvs')
val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
val beta_norm' = beta_norm orelse not (null cvs')
@@ -211,7 +209,7 @@
| t => (fn cx =>
if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
else if with_theories andalso
- I.is_builtin_theory_term (context_of cx) t
+ Z3_Interface.is_builtin_theory_term (context_of cx) t
then abs_args abstr cvs ct cx
else fresh_abstraction cvs ct cx))
in abstr [] end