# HG changeset patch
# User haftmann
# Date 1166426489 -3600
# Node ID 62d2416728f55d4c0fc28ca83be12f4d4f775944
# Parent  75ba582dd6e9a6ea47d8c7a2c2d8e825731dc46d
introduced abstract view on number expressions in hologic.ML

diff -r 75ba582dd6e9 -r 62d2416728f5 src/HOL/Integ/cooper_dec.ML
--- 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          *) 
diff -r 75ba582dd6e9 -r 62d2416728f5 src/HOL/Integ/int_arith1.ML
--- 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", []);
 
diff -r 75ba582dd6e9 -r 62d2416728f5 src/HOL/Integ/nat_simprocs.ML
--- 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)
diff -r 75ba582dd6e9 -r 62d2416728f5 src/HOL/Tools/Presburger/cooper_dec.ML
--- 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          *)