--- a/src/HOL/Tools/SMT/smt_utils.ML Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Sun Dec 19 17:55:56 2010 +0100
@@ -28,6 +28,7 @@
val dest_conj: term -> term * term
val dest_disj: term -> term * term
val under_quant: (term -> 'a) -> term -> 'a
+ val is_number: term -> bool
(*patterns and instantiations*)
val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
@@ -132,6 +133,19 @@
| Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u
| _ => f t)
+val is_number =
+ let
+ fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) =
+ is_num env t andalso is_num env u
+ | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
+ is_num (t :: env) u
+ | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
+ | is_num env (Const (@{const_name divide}, _) $ t $ u) =
+ is_num env t andalso is_num env u
+ | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
+ | is_num _ t = can HOLogic.dest_number t
+ in is_num [] end
+
(* patterns and instantiations *)