# HG changeset patch
# User berghofe
# Date 1085168985 -7200
# Node ID 2d27b5ebc4471d0258ee267aa9f5699769b196ba
# Parent  50581f2b2c0ef74ca87d130b8582f7a3e73fabcc
- deleted unneeded function eta_long (now in Pure/pattern.ML
- added HOL.min / HOL.max to allowed consts again
- added final simplification step with presburger_ss to
  preprocessor again

diff -r 50581f2b2c0e -r 2d27b5ebc447 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Fri May 21 21:48:35 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Fri May 21 21:49:45 2004 +0200
@@ -28,6 +28,8 @@
 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
 (*-----------------------------------------------------------------*)
 
+val presburger_ss = simpset_of (theory "Presburger");
+
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
   let val (xn1,p1) = variant_abs (xn,xT,p)
   in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
@@ -65,19 +67,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;
@@ -109,6 +98,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),
@@ -120,6 +111,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),
@@ -268,7 +261,7 @@
     val pre_thm = Seq.hd (EVERY
       [simp_tac simpset0 1,
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
-       TRY (simp_tac simpset3 1)]
+       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
       (trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
diff -r 50581f2b2c0e -r 2d27b5ebc447 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Fri May 21 21:48:35 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri May 21 21:49:45 2004 +0200
@@ -28,6 +28,8 @@
 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
 (*-----------------------------------------------------------------*)
 
+val presburger_ss = simpset_of (theory "Presburger");
+
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
   let val (xn1,p1) = variant_abs (xn,xT,p)
   in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
@@ -65,19 +67,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;
@@ -109,6 +98,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),
@@ -120,6 +111,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),
@@ -268,7 +261,7 @@
     val pre_thm = Seq.hd (EVERY
       [simp_tac simpset0 1,
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
-       TRY (simp_tac simpset3 1)]
+       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
       (trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)