author blanchet Thu, 13 Mar 2014 13:18:14 +0100 changeset 56100 0dc5f68a7802 parent 56099 bc036c1cf111 child 56101 6d9fe46429e6
tuning
```--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -49,8 +49,7 @@
(case Thm.prop_of thm of
@{const Trueprop} \$ (Const (@{const_name HOL.eq}, _) \$ _ \$ Abs _) =>
norm_def (thm RS @{thm fun_cong})
-  | Const (@{const_name "=="}, _) \$ _ \$ Abs _ =>
-      norm_def (thm RS @{thm meta_eq_to_obj_eq})
+  | Const (@{const_name "=="}, _) \$ _ \$ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
| _ => thm)

@@ -368,8 +367,7 @@
(** unfold abs, min and max **)

local
-  val abs_def = mk_meta_eq @{lemma
-    "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
+  val abs_def = mk_meta_eq @{lemma "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
by (rule ext) (rule abs_if)}

val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
@@ -381,13 +379,10 @@
val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
(@{const_name abs}, abs_def)]

-  fun is_builtinT ctxt T =
-    SMT2_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
-
-  fun abs_min_max ctxt (Const (n, T)) =
+  fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
(case AList.lookup (op =) defs n of
NONE => NONE
-        | SOME thm => if is_builtinT ctxt T then SOME thm else NONE)
+        | SOME thm => if SMT2_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
| abs_min_max _ _ = NONE

fun unfold_amm_conv ctxt ct =
@@ -498,8 +493,7 @@
val nat_as_int_conv = nat_conv