- deleted unneeded function eta_long (now in Pure/pattern.ML
authorberghofe
Fri May 21 21:49:45 2004 +0200 (2004-05-21)
changeset 148012d27b5ebc447
parent 14800 50581f2b2c0e
child 14802 e05116289ff9
- 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
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Integ/presburger.ML	Fri May 21 21:48:35 2004 +0200
     1.2 +++ b/src/HOL/Integ/presburger.ML	Fri May 21 21:49:45 2004 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4  (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
     1.5  (*-----------------------------------------------------------------*)
     1.6  
     1.7 +val presburger_ss = simpset_of (theory "Presburger");
     1.8 +
     1.9  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    1.10    let val (xn1,p1) = variant_abs (xn,xT,p)
    1.11    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    1.12 @@ -65,19 +67,6 @@
    1.13  
    1.14  fun term_typed_consts t = add_term_typed_consts(t,[]);
    1.15  
    1.16 -(* put a term into eta long beta normal form *)
    1.17 -fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
    1.18 -  | eta_long Ts t = (case strip_comb t of
    1.19 -      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
    1.20 -    | (u, ts) => 
    1.21 -      let
    1.22 -        val Us = binder_types (fastype_of1 (Ts, t));
    1.23 -        val i = length Us
    1.24 -      in list_abs (map (pair "x") Us,
    1.25 -        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
    1.26 -          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
    1.27 -      end);
    1.28 -
    1.29  (* Some Types*)
    1.30  val bT = HOLogic.boolT;
    1.31  val iT = HOLogic.intT;
    1.32 @@ -109,6 +98,8 @@
    1.33     ("op *", iT --> iT --> iT), 
    1.34     ("HOL.abs", iT --> iT),
    1.35     ("uminus", iT --> iT),
    1.36 +   ("HOL.max", iT --> iT --> iT),
    1.37 +   ("HOL.min", iT --> iT --> iT),
    1.38  
    1.39     ("op <=", nT --> nT --> bT),
    1.40     ("op =", nT --> nT --> bT),
    1.41 @@ -120,6 +111,8 @@
    1.42     ("op -", nT --> nT --> nT),
    1.43     ("op *", nT --> nT --> nT), 
    1.44     ("Suc", nT --> nT),
    1.45 +   ("HOL.max", nT --> nT --> nT),
    1.46 +   ("HOL.min", nT --> nT --> nT),
    1.47  
    1.48     ("Numeral.bin.Bit", binT --> bT --> binT),
    1.49     ("Numeral.bin.Pls", binT),
    1.50 @@ -268,7 +261,7 @@
    1.51      val pre_thm = Seq.hd (EVERY
    1.52        [simp_tac simpset0 1,
    1.53         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    1.54 -       TRY (simp_tac simpset3 1)]
    1.55 +       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
    1.56        (trivial ct))
    1.57      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    1.58      (* The result of the quantifier elimination *)
     2.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Fri May 21 21:48:35 2004 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Fri May 21 21:49:45 2004 +0200
     2.3 @@ -28,6 +28,8 @@
     2.4  (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
     2.5  (*-----------------------------------------------------------------*)
     2.6  
     2.7 +val presburger_ss = simpset_of (theory "Presburger");
     2.8 +
     2.9  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    2.10    let val (xn1,p1) = variant_abs (xn,xT,p)
    2.11    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    2.12 @@ -65,19 +67,6 @@
    2.13  
    2.14  fun term_typed_consts t = add_term_typed_consts(t,[]);
    2.15  
    2.16 -(* put a term into eta long beta normal form *)
    2.17 -fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
    2.18 -  | eta_long Ts t = (case strip_comb t of
    2.19 -      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
    2.20 -    | (u, ts) => 
    2.21 -      let
    2.22 -        val Us = binder_types (fastype_of1 (Ts, t));
    2.23 -        val i = length Us
    2.24 -      in list_abs (map (pair "x") Us,
    2.25 -        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
    2.26 -          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
    2.27 -      end);
    2.28 -
    2.29  (* Some Types*)
    2.30  val bT = HOLogic.boolT;
    2.31  val iT = HOLogic.intT;
    2.32 @@ -109,6 +98,8 @@
    2.33     ("op *", iT --> iT --> iT), 
    2.34     ("HOL.abs", iT --> iT),
    2.35     ("uminus", iT --> iT),
    2.36 +   ("HOL.max", iT --> iT --> iT),
    2.37 +   ("HOL.min", iT --> iT --> iT),
    2.38  
    2.39     ("op <=", nT --> nT --> bT),
    2.40     ("op =", nT --> nT --> bT),
    2.41 @@ -120,6 +111,8 @@
    2.42     ("op -", nT --> nT --> nT),
    2.43     ("op *", nT --> nT --> nT), 
    2.44     ("Suc", nT --> nT),
    2.45 +   ("HOL.max", nT --> nT --> nT),
    2.46 +   ("HOL.min", nT --> nT --> nT),
    2.47  
    2.48     ("Numeral.bin.Bit", binT --> bT --> binT),
    2.49     ("Numeral.bin.Pls", binT),
    2.50 @@ -268,7 +261,7 @@
    2.51      val pre_thm = Seq.hd (EVERY
    2.52        [simp_tac simpset0 1,
    2.53         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    2.54 -       TRY (simp_tac simpset3 1)]
    2.55 +       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
    2.56        (trivial ct))
    2.57      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    2.58      (* The result of the quantifier elimination *)