# HG changeset patch
# User berghofe
# Date 1052592738 -7200
# Node ID 3d53dcd7787731a0b0f231155db2005625886fd5
# Parent  a994b92ab1eac014caa84b97fd19004e5629a9bd
- Added split_min and split_max to preprocessor
- Moved eta_long to Pure/pattern.ML

diff -r a994b92ab1ea -r 3d53dcd77877 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Fri May 09 18:00:30 2003 +0200
+++ b/src/HOL/Integ/presburger.ML	Sat May 10 20:52:18 2003 +0200
@@ -63,19 +63,6 @@
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* put a term into eta long beta normal form *)
-fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
-  | eta_long Ts t = (case strip_comb t of
-      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-    | (u, ts) => 
-      let
-        val Us = binder_types (fastype_of1 (Ts, t));
-        val i = length Us
-      in list_abs (map (pair "x") Us,
-        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
-      end);
-
 (* Some Types*)
 val bT = HOLogic.boolT;
 val iT = HOLogic.intT;
@@ -107,6 +94,8 @@
    ("op *", iT --> iT --> iT), 
    ("HOL.abs", iT --> iT),
    ("uminus", iT --> iT),
+   ("HOL.max", iT --> iT --> iT),
+   ("HOL.min", iT --> iT --> iT),
 
    ("op <=", nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
@@ -118,6 +107,8 @@
    ("op -", nT --> nT --> nT),
    ("op *", nT --> nT --> nT), 
    ("Suc", nT --> nT),
+   ("HOL.max", nT --> nT --> nT),
+   ("HOL.min", nT --> nT --> nT),
 
    ("Numeral.bin.Bit", binT --> bT --> binT),
    ("Numeral.bin.Pls", binT),
@@ -177,7 +168,7 @@
 
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
-      addsplits [split_zdiv, split_zmod, split_div']
+      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss
       addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
@@ -208,7 +199,7 @@
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
           (trace_msg ("calling procedure with term:\n" ^
              Sign.string_of_term sg t1);
-           ((mproof_of_int_qelim sg (eta_long [] t1) RS iffD2) RS pre_thm,
+           ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
diff -r a994b92ab1ea -r 3d53dcd77877 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Fri May 09 18:00:30 2003 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat May 10 20:52:18 2003 +0200
@@ -63,19 +63,6 @@
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* put a term into eta long beta normal form *)
-fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
-  | eta_long Ts t = (case strip_comb t of
-      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-    | (u, ts) => 
-      let
-        val Us = binder_types (fastype_of1 (Ts, t));
-        val i = length Us
-      in list_abs (map (pair "x") Us,
-        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
-      end);
-
 (* Some Types*)
 val bT = HOLogic.boolT;
 val iT = HOLogic.intT;
@@ -107,6 +94,8 @@
    ("op *", iT --> iT --> iT), 
    ("HOL.abs", iT --> iT),
    ("uminus", iT --> iT),
+   ("HOL.max", iT --> iT --> iT),
+   ("HOL.min", iT --> iT --> iT),
 
    ("op <=", nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
@@ -118,6 +107,8 @@
    ("op -", nT --> nT --> nT),
    ("op *", nT --> nT --> nT), 
    ("Suc", nT --> nT),
+   ("HOL.max", nT --> nT --> nT),
+   ("HOL.min", nT --> nT --> nT),
 
    ("Numeral.bin.Bit", binT --> bT --> binT),
    ("Numeral.bin.Pls", binT),
@@ -177,7 +168,7 @@
 
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
-      addsplits [split_zdiv, split_zmod, split_div']
+      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss
       addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
@@ -208,7 +199,7 @@
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
           (trace_msg ("calling procedure with term:\n" ^
              Sign.string_of_term sg t1);
-           ((mproof_of_int_qelim sg (eta_long [] t1) RS iffD2) RS pre_thm,
+           ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st