# 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