1.1 --- a/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
1.2 +++ b/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
1.3 @@ -76,8 +76,4 @@
1.4
1.5 declare [[ smt_trace = false ]]
1.6
1.7 -text {* Unfold (some) definitions passed to the SMT solver: *}
1.8 -
1.9 -declare [[ smt_unfold_defs = true ]]
1.10 -
1.11 end
2.1 --- a/src/HOL/SMT/SMT_Base.thy Wed Apr 07 20:40:42 2010 +0200
2.2 +++ b/src/HOL/SMT/SMT_Base.thy Wed Apr 07 20:40:42 2010 +0200
2.3 @@ -138,6 +138,6 @@
2.4 use "Tools/smt_solver.ML"
2.5 use "Tools/smtlib_interface.ML"
2.6
2.7 -setup {* SMT_Normalize.setup #> SMT_Solver.setup *}
2.8 +setup {* SMT_Solver.setup *}
2.9
2.10 end
3.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 20:40:42 2010 +0200
3.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed Apr 07 20:40:42 2010 +0200
3.3 @@ -20,23 +20,18 @@
3.4 val trivial_let: Proof.context -> thm list -> thm list
3.5 val positive_numerals: Proof.context -> thm list -> thm list
3.6 val nat_as_int: Proof.context -> thm list -> thm list
3.7 - val unfold_defs: bool Config.T
3.8 val add_pair_rules: Proof.context -> thm list -> thm list
3.9 val add_fun_upd_rules: Proof.context -> thm list -> thm list
3.10 - val add_abs_min_max_rules: Proof.context -> thm list -> thm list
3.11
3.12 datatype config =
3.13 RewriteTrivialLets |
3.14 RewriteNegativeNumerals |
3.15 RewriteNaturalNumbers |
3.16 AddPairRules |
3.17 - AddFunUpdRules |
3.18 - AddAbsMinMaxRules
3.19 + AddFunUpdRules
3.20
3.21 val normalize: config list -> Proof.context -> thm list ->
3.22 cterm list * thm list
3.23 -
3.24 - val setup: theory -> theory
3.25 end
3.26
3.27 structure SMT_Normalize: SMT_NORMALIZE =
3.28 @@ -137,7 +132,6 @@
3.29
3.30 fun normalize_rule ctxt =
3.31 Conv.fconv_rule (
3.32 - unfold_quants_conv ctxt then_conv
3.33 Thm.beta_conversion true then_conv
3.34 Thm.eta_conversion then_conv
3.35 norm_binder_conv ctxt) #>
3.36 @@ -283,9 +277,6 @@
3.37
3.38 (* include additional rules *)
3.39
3.40 -val (unfold_defs, unfold_defs_setup) =
3.41 - Attrib.config_bool "smt_unfold_defs" (K true)
3.42 -
3.43 local
3.44 val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
3.45
3.46 @@ -304,36 +295,42 @@
3.47 end
3.48
3.49
3.50 +(* unfold definitions of specific constants *)
3.51 +
3.52 local
3.53 - fun mk_entry t thm = (Term.head_of t, (thm, thm RS @{thm eq_reflection}))
3.54 + fun mk_entry (t as Const (n, _)) thm = ((n, t), thm)
3.55 + | mk_entry t _ = raise TERM ("mk_entry", [t])
3.56 fun prepare_def thm =
3.57 - (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
3.58 - Const (@{const_name "op ="}, _) $ t $ _ => mk_entry t thm
3.59 + (case Thm.prop_of thm of
3.60 + Const (@{const_name "=="}, _) $ t $ _ => mk_entry (Term.head_of t) thm
3.61 | t => raise TERM ("prepare_def", [t]))
3.62
3.63 val defs = map prepare_def [
3.64 - @{thm abs_if[where 'a = int]}, @{thm abs_if[where 'a = real]},
3.65 - @{thm min_def[where 'a = int]}, @{thm min_def[where 'a = real]},
3.66 - @{thm max_def[where 'a = int]}, @{thm max_def[where 'a = real]}]
3.67 + @{thm abs_if[where 'a = int, THEN eq_reflection]},
3.68 + @{thm abs_if[where 'a = real, THEN eq_reflection]},
3.69 + @{thm min_def[where 'a = int, THEN eq_reflection]},
3.70 + @{thm min_def[where 'a = real, THEN eq_reflection]},
3.71 + @{thm max_def[where 'a = int, THEN eq_reflection]},
3.72 + @{thm max_def[where 'a = real, THEN eq_reflection]},
3.73 + @{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}]
3.74
3.75 - fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
3.76 - fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
3.77 + fun matches thy ((t as Const (n, _)), (m, p)) =
3.78 + n = m andalso Pattern.matches thy (p, t)
3.79 + | matches _ _ = false
3.80
3.81 - fun unfold_def_conv ds ct =
3.82 - (case AList.lookup (op =) ds (Term.head_of (Thm.term_of ct)) of
3.83 - SOME (_, eq) => Conv.rewr_conv eq
3.84 + fun lookup_def thy = AList.lookup (matches thy) defs
3.85 + fun lookup_def_head thy = lookup_def thy o Term.head_of
3.86 +
3.87 + fun occurs_def thy = Term.exists_subterm (is_some o lookup_def thy)
3.88 +
3.89 + fun unfold_def_conv ctxt ct =
3.90 + (case lookup_def_head (ProofContext.theory_of ctxt) (Thm.term_of ct) of
3.91 + SOME thm => Conv.rewr_conv thm
3.92 | NONE => Conv.all_conv) ct
3.93 -
3.94 - fun unfold_conv ctxt thm =
3.95 - (case filter (member (op =) (add_syms [thm]) o fst) defs of
3.96 - [] => thm
3.97 - | ds => thm |> Conv.fconv_rule
3.98 - (More_Conv.bottom_conv (K (unfold_def_conv ds)) ctxt))
3.99 in
3.100 -fun add_abs_min_max_rules ctxt thms =
3.101 - if Config.get ctxt unfold_defs
3.102 - then map (unfold_conv ctxt) thms
3.103 - else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
3.104 +fun unfold_defs ctxt =
3.105 + (occurs_def (ProofContext.theory_of ctxt) o Thm.prop_of) ??
3.106 + Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt)
3.107 end
3.108
3.109
3.110 @@ -493,8 +490,7 @@
3.111 RewriteNegativeNumerals |
3.112 RewriteNaturalNumbers |
3.113 AddPairRules |
3.114 - AddFunUpdRules |
3.115 - AddAbsMinMaxRules
3.116 + AddFunUpdRules
3.117
3.118 fun normalize config ctxt thms =
3.119 let fun if_enabled c f = member (op =) config c ? f ctxt
3.120 @@ -505,12 +501,9 @@
3.121 |> if_enabled RewriteNaturalNumbers nat_as_int
3.122 |> if_enabled AddPairRules add_pair_rules
3.123 |> if_enabled AddFunUpdRules add_fun_upd_rules
3.124 - |> if_enabled AddAbsMinMaxRules add_abs_min_max_rules
3.125 - |> map (normalize_rule ctxt)
3.126 + |> map (unfold_defs ctxt #> normalize_rule ctxt)
3.127 |> lift_lambdas ctxt
3.128 |> apsnd (explicit_application ctxt)
3.129 end
3.130
3.131 -val setup = unfold_defs_setup
3.132 -
3.133 end
4.1 --- a/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200
4.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML Wed Apr 07 20:40:42 2010 +0200
4.3 @@ -158,7 +158,6 @@
4.4 SMT_Normalize.RewriteTrivialLets,
4.5 SMT_Normalize.RewriteNegativeNumerals,
4.6 SMT_Normalize.RewriteNaturalNumbers,
4.7 - SMT_Normalize.AddAbsMinMaxRules,
4.8 SMT_Normalize.AddPairRules,
4.9 SMT_Normalize.AddFunUpdRules ],
4.10 translate = {