--- a/src/HOL/Integ/cooper_dec.ML Mon Dec 18 08:21:28 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Mon Dec 18 08:21:29 2006 +0100
@@ -74,34 +74,26 @@
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
-(*Transform a natural number to a term*)
-
-fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
- |mk_number 1 = Const("HOL.one",HOLogic.intT)
- |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n);
+(*Transform a natural (FIXME?) number to a term*)
+val mk_number = HOLogic.mk_number HOLogic.intT
-(*Transform an Term to an natural number*)
-
-fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
- |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
- |dest_number (Const ("Numeral.number_of",_) $ n) =
- HOLogic.dest_numeral n;
+(*Transform an Term to an natural (FIXME?) number*)
+fun dest_number t = let
+ val (T, n) = HOLogic.dest_number t
+ in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
+
(*Some terms often used for pattern matching*)
-
val zero = mk_number 0;
val one = mk_number 1;
-
+
(*Tests if a Term is representing a number*)
-
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t);
-
+val is_numeral = can dest_number;
+
(*maps a unary natural function on a term containing an natural number*)
-
-fun numeral1 f n = mk_number (f(dest_number n));
+fun numeral1 f n = mk_number (f (dest_number n));
(*maps a binary natural function on 2 term containing natural numbers*)
-
-fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n));
+fun numeral2 f m n = mk_number (f (dest_number m) (dest_number n));
(* ------------------------------------------------------------------------- *)
(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *)
--- a/src/HOL/Integ/int_arith1.ML Mon Dec 18 08:21:28 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML Mon Dec 18 08:21:29 2006 +0100
@@ -183,16 +183,8 @@
fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
-(*Decodes a binary INTEGER*)
-fun dest_number (Const("HOL.zero", _)) = 0
- | dest_number (Const("HOL.one", _)) = 1
- | dest_number (Const("Numeral.number_of", _) $ w) =
- (HOLogic.dest_numeral w
- handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_number:1", [w]))
- | dest_number t = raise TERM("Int_Numeral_Simprocs.dest_number:2", [t]);
-
fun find_first_numeral past (t::terms) =
- ((dest_number t, rev past @ terms)
+ ((snd (HOLogic.dest_number t), rev past @ terms)
handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
--- a/src/HOL/Integ/nat_simprocs.ML Mon Dec 18 08:21:28 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Mon Dec 18 08:21:29 2006 +0100
@@ -24,14 +24,7 @@
(*Utilities*)
fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
-
-(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
-fun dest_number (Const ("HOL.zero", _)) = 0
- | dest_number (Const ("Suc", _) $ t) = 1 + dest_number t
- | dest_number (Const("Numeral.number_of", _) $ w) =
- (IntInf.max (0, HOLogic.dest_numeral w)
- handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_number:1", [w]))
- | dest_number t = raise TERM("Nat_Numeral_Simprocs.dest_number:2", [t]);
+fun dest_number t = IntInf.max (0, snd (HOLogic.dest_number t));
fun find_first_numeral past (t::terms) =
((dest_number t, t, rev past @ terms)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Mon Dec 18 08:21:28 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Mon Dec 18 08:21:29 2006 +0100
@@ -74,34 +74,26 @@
(*Function is_arith_rel returns true if and only if the term is an operation of the
form [int,int]---> int*)
-(*Transform a natural number to a term*)
-
-fun mk_number 0 = Const("HOL.zero",HOLogic.intT)
- |mk_number 1 = Const("HOL.one",HOLogic.intT)
- |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n);
+(*Transform a natural (FIXME?) number to a term*)
+val mk_number = HOLogic.mk_number HOLogic.intT
-(*Transform an Term to an natural number*)
-
-fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0
- |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1
- |dest_number (Const ("Numeral.number_of",_) $ n) =
- HOLogic.dest_numeral n;
+(*Transform an Term to an natural (FIXME?) number*)
+fun dest_number t = let
+ val (T, n) = HOLogic.dest_number t
+ in if T = HOLogic.intT then n else error ("bad typ: " ^ Display.raw_string_of_typ T) end;
+
(*Some terms often used for pattern matching*)
-
val zero = mk_number 0;
val one = mk_number 1;
-
+
(*Tests if a Term is representing a number*)
-
-fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t);
-
+val is_numeral = can dest_number;
+
(*maps a unary natural function on a term containing an natural number*)
-
-fun numeral1 f n = mk_number (f(dest_number n));
+fun numeral1 f n = mk_number (f (dest_number n));
(*maps a binary natural function on 2 term containing natural numbers*)
-
-fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n));
+fun numeral2 f m n = mk_number (f (dest_number m) (dest_number n));
(* ------------------------------------------------------------------------- *)
(* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *)