# HG changeset patch
# User boehmes
# Date 1270665642 -7200
# Node ID 3176ec2244adac58ec69ffb23aa71372fda3a6d6
# Parent  59f843c3f17f4c00abb41e1dc48378b8c65b8cc6
always unfold definitions of specific constants (including special binders)

diff -r 59f843c3f17f -r 3176ec2244ad src/HOL/SMT/SMT.thy
--- 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
diff -r 59f843c3f17f -r 3176ec2244ad src/HOL/SMT/SMT_Base.thy
--- 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
diff -r 59f843c3f17f -r 3176ec2244ad src/HOL/SMT/Tools/smt_normalize.ML
--- 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
diff -r 59f843c3f17f -r 3176ec2244ad src/HOL/SMT/Tools/smtlib_interface.ML
--- 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 = {