--- a/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
@@ -76,8 +76,4 @@
declare [[ smt_trace = false ]]
-text {* Unfold (some) definitions passed to the SMT solver: *}
-
-declare [[ smt_unfold_defs = true ]]
-
end
--- a/src/HOL/SMT/SMT_Base.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy Wed Apr 07 20:40:42 2010 +0200
@@ -138,6 +138,6 @@
use "Tools/smt_solver.ML"
use "Tools/smtlib_interface.ML"
-setup {* SMT_Normalize.setup #> SMT_Solver.setup *}
+setup {* SMT_Solver.setup *}
end
--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 20:40:42 2010 +0200
@@ -20,23 +20,18 @@
val trivial_let: Proof.context -> thm list -> thm list
val positive_numerals: Proof.context -> thm list -> thm list
val nat_as_int: Proof.context -> thm list -> thm list
- val unfold_defs: bool Config.T
val add_pair_rules: Proof.context -> thm list -> thm list
val add_fun_upd_rules: Proof.context -> thm list -> thm list
- val add_abs_min_max_rules: Proof.context -> thm list -> thm list
datatype config =
RewriteTrivialLets |
RewriteNegativeNumerals |
RewriteNaturalNumbers |
AddPairRules |
- AddFunUpdRules |
- AddAbsMinMaxRules
+ AddFunUpdRules
val normalize: config list -> Proof.context -> thm list ->
cterm list * thm list
-
- val setup: theory -> theory
end
structure SMT_Normalize: SMT_NORMALIZE =
@@ -137,7 +132,6 @@
fun normalize_rule ctxt =
Conv.fconv_rule (
- unfold_quants_conv ctxt then_conv
Thm.beta_conversion true then_conv
Thm.eta_conversion then_conv
norm_binder_conv ctxt) #>
@@ -283,9 +277,6 @@
(* include additional rules *)
-val (unfold_defs, unfold_defs_setup) =
- Attrib.config_bool "smt_unfold_defs" (K true)
-
local
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
@@ -304,36 +295,42 @@
end
+(* unfold definitions of specific constants *)
+
local
- fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
+ fun mk_entry (t as Const (n, _)) thm = ((n, t), thm)
+ | mk_entry t _ = raise TERM ("mk_entry", [t])
fun prepare_def thm =
- (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
- Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
+ (case Thm.prop_of thm of
+ Const (@{const_name "=="}, _) $ t $ _ => mk_entry (Term.head_of t) thm
| t => raise TERM ("prepare_def", [t]))
val defs = map prepare_def [
- @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
- @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
- @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
+ @{thm abs_if[where 'a = int, THEN eq_reflection]},
+ @{thm abs_if[where 'a = real, THEN eq_reflection]},
+ @{thm min_def[where 'a = int, THEN eq_reflection]},
+ @{thm min_def[where 'a = real, THEN eq_reflection]},
+ @{thm max_def[where 'a = int, THEN eq_reflection]},
+ @{thm max_def[where 'a = real, THEN eq_reflection]},
+ @{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
- fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
- fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
+ fun matches thy ((t as Const (n, _)), (m, p)) =
+ n = m andalso Pattern.matches thy (p, t)
+ | matches _ _ = false
- fun unfold_def_conv ds ct =
- (case AList.lookup (op =) ds (Term.head_of (Thm.term_of ct)) of
- SOME (_, eq) => Conv.rewr_conv eq
+ fun lookup_def thy = AList.lookup (matches thy) defs
+ fun lookup_def_head thy = lookup_def thy o Term.head_of
+
+ fun occurs_def thy = Term.exists_subterm (is_some o lookup_def thy)
+
+ fun unfold_def_conv ctxt ct =
+ (case lookup_def_head (ProofContext.theory_of ctxt) (Thm.term_of ct) of
+ SOME thm => Conv.rewr_conv thm
| NONE => Conv.all_conv) ct
-
- fun unfold_conv ctxt thm =
- (case filter (member (op =) (add_syms [thm]) o fst) defs of
- [] => thm
- | ds => thm |> Conv.fconv_rule
- (More_Conv.bottom_conv (K (unfold_def_conv ds)) ctxt))
in
-fun add_abs_min_max_rules ctxt thms =
- if Config.get ctxt unfold_defs
- then map (unfold_conv ctxt) thms
- else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
+fun unfold_defs ctxt =
+ (occurs_def (ProofContext.theory_of ctxt) o Thm.prop_of) ??
+ Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt)
end
@@ -493,8 +490,7 @@
RewriteNegativeNumerals |
RewriteNaturalNumbers |
AddPairRules |
- AddFunUpdRules |
- AddAbsMinMaxRules
+ AddFunUpdRules
fun normalize config ctxt thms =
let fun if_enabled c f = member (op =) config c ? f ctxt
@@ -505,12 +501,9 @@
|> if_enabled RewriteNaturalNumbers nat_as_int
|> if_enabled AddPairRules add_pair_rules
|> if_enabled AddFunUpdRules add_fun_upd_rules
- |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
- |> map (normalize_rule ctxt)
+ |> map (unfold_defs ctxt #> normalize_rule ctxt)
|> lift_lambdas ctxt
|> apsnd (explicit_application ctxt)
end
-val setup = unfold_defs_setup
-
end
--- a/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200
@@ -158,7 +158,6 @@
SMT_Normalize.RewriteTrivialLets,
SMT_Normalize.RewriteNegativeNumerals,
SMT_Normalize.RewriteNaturalNumbers,
- SMT_Normalize.AddAbsMinMaxRules,
SMT_Normalize.AddPairRules,
SMT_Normalize.AddFunUpdRules ],
translate = {