--- a/src/HOL/Tools/numeral_simprocs.ML Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Jan 28 11:48:49 2010 +0100
@@ -34,12 +34,12 @@
val long_mk_sum = Arith_Data.long_mk_sum;
val dest_sum = Arith_Data.dest_sum;
-val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
-val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
+val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus};
+val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
-val mk_times = HOLogic.mk_binop @{const_name HOL.times};
+val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
-fun one_of T = Const(@{const_name HOL.one},T);
+fun one_of T = Const(@{const_name Algebras.one}, T);
(* build product with trailing 1 rather than Numeral 1 in order to avoid the
unnecessary restriction to type class number_ring
@@ -56,7 +56,7 @@
fun long_mk_prod T [] = one_of T
| long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
-val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -72,7 +72,7 @@
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort TermOrd.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
@@ -96,7 +96,7 @@
Fractions are reduced later by the cancel_numeral_factor simproc.*)
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
-val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
(*Build term (p / q) * t*)
fun mk_fcoeff ((p, q), t) =
@@ -104,8 +104,8 @@
in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
(*Express t as a product of a fraction with other sorted terms*)
-fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
- | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
+fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
+ | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
let val (p, t') = dest_coeff sign t
val (q, u') = dest_coeff 1 u
in (mk_frac (p, q), mk_divide (t', u')) end
@@ -230,8 +230,8 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val bal_add1 = @{thm less_add_iff1} RS trans
val bal_add2 = @{thm less_add_iff2} RS trans
);
@@ -239,8 +239,8 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val bal_add1 = @{thm le_add_iff1} RS trans
val bal_add2 = @{thm le_add_iff2} RS trans
);
@@ -392,8 +392,8 @@
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
val cancel = @{thm mult_divide_mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -410,8 +410,8 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val cancel = @{thm mult_less_cancel_left} RS trans
val neg_exchanges = true
)
@@ -419,8 +419,8 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val cancel = @{thm mult_le_cancel_left} RS trans
val neg_exchanges = true
)
@@ -485,8 +485,8 @@
in
fun sign_conv pos_th neg_th ss t =
let val T = fastype_of t;
- val zero = Const(@{const_name HOL.zero}, T);
- val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+ val zero = Const(@{const_name Algebras.zero}, T);
+ val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
Option.map Eq_True_elim (Lin_Arith.simproc ss p)
@@ -525,8 +525,8 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
val simp_conv = sign_conv
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
);
@@ -535,8 +535,8 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
+ val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
val simp_conv = sign_conv
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
);
@@ -571,8 +571,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
- val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
- val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+ val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide}
+ val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);