--- a/src/HOL/Hyperreal/IntFloor.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Hyperreal/IntFloor.ML Tue Feb 17 10:41:59 2004 +0100
@@ -4,8 +4,6 @@
Description: Floor and ceiling operations over reals
*)
-val real_number_of = thm"real_number_of";
-
Goal "((number_of n) < real (m::int)) = (number_of n < m)";
by Auto_tac;
by (rtac (real_of_int_less_iff RS iffD1) 1);
--- a/src/HOL/Integ/IntArith.thy Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/IntArith.thy Tue Feb 17 10:41:59 2004 +0100
@@ -429,6 +429,7 @@
val zle_add1_eq_le = thm "zle_add1_eq_le";
val nonneg_eq_int = thm "nonneg_eq_int";
val abs_minus_one = thm "abs_minus_one";
+val of_int_number_of_eq = thm"of_int_number_of_eq";
val nat_eq_iff = thm "nat_eq_iff";
val nat_eq_iff2 = thm "nat_eq_iff2";
val nat_less_iff = thm "nat_less_iff";
--- a/src/HOL/Integ/NatBin.thy Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy Tue Feb 17 10:41:59 2004 +0100
@@ -86,7 +86,7 @@
add: neg_nat nat_number_of_def not_neg_nat add_assoc)
-(** Successor **)
+subsubsection{*Successor *}
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
apply (rule sym)
@@ -108,7 +108,7 @@
done
-(** Addition **)
+subsubsection{*Addition *}
(*"neg" is used in rewrite rules for binary comparisons*)
lemma add_nat_number_of [simp]:
@@ -121,7 +121,7 @@
simp add: nat_number_of_def nat_add_distrib [symmetric])
-(** Subtraction **)
+subsubsection{*Subtraction *}
lemma diff_nat_eq_if:
"nat z - nat z' =
@@ -141,7 +141,7 @@
-(** Multiplication **)
+subsubsection{*Multiplication *}
lemma mult_nat_number_of [simp]:
"(number_of v :: nat) * number_of v' =
@@ -152,7 +152,7 @@
-(** Quotient **)
+subsubsection{*Quotient *}
lemma div_nat_number_of [simp]:
"(number_of v :: nat) div number_of v' =
@@ -167,7 +167,7 @@
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-(** Remainder **)
+subsubsection{*Remainder *}
lemma mod_nat_number_of [simp]:
"(number_of v :: nat) mod number_of v' =
@@ -210,16 +210,16 @@
*}
-(*** Comparisons ***)
+subsection{*Comparisons*}
-(** Equals (=) **)
+subsubsection{*Equals (=) *}
lemma eq_nat_nat_iff:
"[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
by (auto elim!: nonneg_eq_int)
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma eq_nat_number_of:
+lemma eq_nat_number_of [simp]:
"((number_of v :: nat) = number_of v') =
(if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))
else if neg (number_of v' :: int) then iszero (number_of v :: int)
@@ -231,21 +231,19 @@
apply (simp add: not_neg_eq_ge_0 [symmetric])
done
-declare eq_nat_number_of [simp]
-(** Less-than (<) **)
+subsubsection{*Less-than (<) *}
(*"neg" is used in rewrite rules for binary comparisons*)
-lemma less_nat_number_of:
+lemma less_nat_number_of [simp]:
"((number_of v :: nat) < number_of v') =
(if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)
else neg (number_of (bin_add v (bin_minus v')) :: int))"
-apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
+by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
- cong add: imp_cong, simp)
-done
+ cong add: imp_cong, simp)
-declare less_nat_number_of [simp]
+
(*Maps #n to n for n = 0, 1, 2*)
@@ -335,7 +333,7 @@
done
-(** Nat **)
+subsubsection{*Nat *}
lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
by (simp add: numerals)
@@ -344,7 +342,7 @@
NOT suitable for rewriting because n recurs in the condition.*)
lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
-(** Arith **)
+subsubsection{*Arith *}
lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
by (simp add: numerals)
@@ -372,33 +370,31 @@
declare diff_less' [of "number_of v", standard, simp]
-(*** Comparisons involving (0::nat) ***)
+subsection{*Comparisons involving (0::nat) *}
-lemma eq_number_of_0:
+text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
+
+lemma eq_number_of_0 [simp]:
"(number_of v = (0::nat)) =
(if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-apply (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
-done
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
-lemma eq_0_number_of:
+lemma eq_0_number_of [simp]:
"((0::nat) = number_of v) =
(if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-apply (rule trans [OF eq_sym_conv eq_number_of_0])
-done
+by (rule trans [OF eq_sym_conv eq_number_of_0])
-lemma less_0_number_of:
+lemma less_0_number_of [simp]:
"((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
-(*Simplification already handles n<0, n<=0 and 0<=n.*)
-declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
-(*** Comparisons involving Suc ***)
+subsection{*Comparisons involving Suc *}
lemma eq_number_of_Suc [simp]:
"(number_of v = Suc n) =
@@ -415,8 +411,7 @@
"(Suc n = number_of v) =
(let pv = number_of (bin_pred v) in
if neg pv then False else nat pv = n)"
-apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
-done
+by (rule trans [OF eq_sym_conv eq_number_of_Suc])
lemma less_number_of_Suc [simp]:
"(number_of v < Suc n) =
@@ -444,15 +439,13 @@
"(number_of v <= Suc n) =
(let pv = number_of (bin_pred v) in
if neg pv then True else nat pv <= n)"
-apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
-done
+by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
lemma le_Suc_number_of [simp]:
"(Suc n <= number_of v) =
(let pv = number_of (bin_pred v) in
if neg pv then False else n <= nat pv)"
-apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
-done
+by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
(* Push int(.) inwards: *)
@@ -500,7 +493,7 @@
-(*** Literal arithmetic involving powers, type nat ***)
+subsection{*Literal arithmetic involving powers*}
lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
apply (induct_tac "n")
@@ -518,7 +511,7 @@
-(*** Literal arithmetic involving powers, type int ***)
+text{*For the integers*}
lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
by (simp add: zpower_zpower mult_commute)
@@ -612,6 +605,40 @@
by (simp add: Let_def)
+subsection{*Literal arithmetic and @{term of_nat}*}
+
+lemma of_nat_double:
+ "0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)"
+by (simp only: mult_2 nat_add_distrib of_nat_add)
+
+lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
+by (simp only: nat_number_of_def, simp)
+
+lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
+by arith
+
+lemma of_nat_number_of_lemma:
+ "of_nat (number_of v :: nat) =
+ (if 0 \<le> (number_of v :: int)
+ then (number_of v :: 'a :: number_ring)
+ else 0)"
+apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
+apply (simp only: number_of nat_number_of_def)
+txt{*Generalize in order to eliminate the function @{term number_of} and
+its annoying simprules*}
+apply (erule rev_mp)
+apply (rule_tac x="number_of bin :: int" in spec)
+apply (rule_tac x="number_of bin :: 'a" in spec)
+apply (simp add: nat_add_distrib of_nat_double int_double_iff)
+done
+
+lemma of_nat_number_of_eq [simp]:
+ "of_nat (number_of v :: nat) =
+ (if neg (number_of v :: int) then 0
+ else (number_of v :: 'a :: number_ring))"
+by (simp only: of_nat_number_of_lemma neg_def, simp)
+
+
subsection {*Lemmas for the Combination and Cancellation Simprocs*}
lemma nat_number_of_add_left:
@@ -619,17 +646,16 @@
(if neg (number_of v :: int) then number_of v' + k
else if neg (number_of v' :: int) then number_of v + k
else number_of (bin_add v v') + k)"
-apply simp
-done
+by simp
-(** For combine_numerals **)
+subsubsection{*For @{text combine_numerals}*}
lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
by (simp add: add_mult_distrib)
-(** For cancel_numerals **)
+subsubsection{*For @{text cancel_numerals}*}
lemma nat_diff_add_eq1:
"j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
@@ -664,7 +690,7 @@
by (auto split add: nat_diff_split simp add: add_mult_distrib)
-(** For cancel_numeral_factors **)
+subsubsection{*For @{text cancel_numeral_factors} *}
lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
by auto
@@ -679,7 +705,7 @@
by auto
-(** For cancel_factor **)
+subsubsection{*For @{text cancel_factor} *}
lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
by auto
@@ -734,6 +760,7 @@
val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
+val of_nat_number_of_eq = thm"of_nat_number_of_eq";
val nat_power_eq = thm"nat_power_eq";
val power_nat_number_of = thm"power_nat_number_of";
val zpower_even = thm"zpower_even";
--- a/src/HOL/Integ/int_arith1.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/int_arith1.ML Tue Feb 17 10:41:59 2004 +0100
@@ -476,7 +476,7 @@
(* reduce contradictory <= to False *)
val add_rules =
simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
- [numeral_0_eq_0, numeral_1_eq_1,
+ [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
minus_zero, diff_minus, left_minus, right_minus,
mult_zero_left, mult_zero_right, mult_1, mult_1_right,
minus_mult_left RS sym, minus_mult_right RS sym,
--- a/src/HOL/Integ/int_factor_simprocs.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Tue Feb 17 10:41:59 2004 +0100
@@ -3,12 +3,25 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
-Factor cancellation simprocs for the integers.
+Factor cancellation simprocs for the integers (and for fields).
This file can't be combined with int_arith1 because it requires IntDiv.thy.
*)
-(** Factor cancellation theorems for "int" **)
+
+(*To quote from Provers/Arith/cancel_numeral_factor.ML:
+
+Cancels common coefficients in balanced expressions:
+
+ u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
+
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
+and d = gcd(m,m') and n=m/d and n'=m'/d.
+*)
+
+val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
+
+(** Factor cancellation theorems for integer division (div, not /) **)
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
by (stac zdiv_zmult_zmult1 1);
@@ -31,13 +44,18 @@
val dest_coeff = dest_coeff 1
val trans_tac = trans_tac
val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@mult_1s))
+ ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
- val simplify_meta_eq = simplify_meta_eq mult_1s
+ val numeral_simp_tac =
+ ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
+ val simplify_meta_eq =
+ Int_Numeral_Simprocs.simplify_meta_eq
+ [add_0, add_0_right,
+ mult_zero_left, mult_zero_right, mult_1, mult_1_right];
end
+(*Version for integer division*)
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
@@ -47,20 +65,41 @@
val neg_exchanges = false
)
+(*Version for fields*)
+structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+ val cancel = mult_divide_cancel_left RS trans
+ val neg_exchanges = false
+)
+
+(*Version for ordered rings: mult_cancel_left requires an ordering*)
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
+ val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
val cancel = mult_cancel_left RS trans
val neg_exchanges = false
)
+(*Version for (unordered) fields*)
+structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val cancel = field_mult_cancel_left RS trans
+ val neg_exchanges = false
+)
+
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
+ val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
val cancel = mult_less_cancel_left RS trans
val neg_exchanges = true
)
@@ -69,26 +108,46 @@
(open CancelNumeralFactorCommon
val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
+ val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
val cancel = mult_le_cancel_left RS trans
val neg_exchanges = true
)
-val int_cancel_numeral_factors =
+val ring_cancel_numeral_factors =
map Bin_Simprocs.prep_simproc
- [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
+ [("ring_eq_cancel_numeral_factor",
+ ["(l::'a::{ordered_ring,number_ring}) * m = n",
+ "(l::'a::{ordered_ring,number_ring}) = m * n"],
EqCancelNumeralFactor.proc),
- ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
+ ("ring_less_cancel_numeral_factor",
+ ["(l::'a::{ordered_ring,number_ring}) * m < n",
+ "(l::'a::{ordered_ring,number_ring}) < m * n"],
LessCancelNumeralFactor.proc),
- ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
+ ("ring_le_cancel_numeral_factor",
+ ["(l::'a::{ordered_ring,number_ring}) * m <= n",
+ "(l::'a::{ordered_ring,number_ring}) <= m * n"],
LeCancelNumeralFactor.proc),
- ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
+ ("int_div_cancel_numeral_factors",
+ ["((l::int) * m) div n", "(l::int) div (m * n)"],
DivCancelNumeralFactor.proc)];
+
+val field_cancel_numeral_factors =
+ map Bin_Simprocs.prep_simproc
+ [("field_eq_cancel_numeral_factor",
+ ["(l::'a::{field,number_ring}) * m = n",
+ "(l::'a::{field,number_ring}) = m * n"],
+ FieldEqCancelNumeralFactor.proc),
+ ("field_cancel_numeral_factor",
+ ["((l::'a::{field,number_ring}) * m) / n",
+ "(l::'a::{field,number_ring}) / (m * n)",
+ "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
+ FieldDivCancelNumeralFactor.proc)]
+
end;
-Addsimprocs int_cancel_numeral_factors;
-
+Addsimprocs ring_cancel_numeral_factors;
+Addsimprocs field_cancel_numeral_factors;
(*examples:
print_depth 22;
@@ -125,6 +184,38 @@
test "-x <= -23 * (y::int)";
*)
+(*And the same examples for fields such as rat or real:
+test "0 <= (y::rat) * -2";
+test "9*x = 12 * (y::rat)";
+test "(9*x) / (12 * (y::rat)) = z";
+test "9*x < 12 * (y::rat)";
+test "9*x <= 12 * (y::rat)";
+
+test "-99*x = 132 * (y::rat)";
+test "(-99*x) / (132 * (y::rat)) = z";
+test "-99*x < 132 * (y::rat)";
+test "-99*x <= 132 * (y::rat)";
+
+test "999*x = -396 * (y::rat)";
+test "(999*x) / (-396 * (y::rat)) = z";
+test "999*x < -396 * (y::rat)";
+test "999*x <= -396 * (y::rat)";
+
+test "(- ((2::rat) * x) <= 2 * y)";
+test "-99*x = -81 * (y::rat)";
+test "(-99*x) / (-81 * (y::rat)) = z";
+test "-99*x <= -81 * (y::rat)";
+test "-99*x < -81 * (y::rat)";
+
+test "-2 * x = -1 * (y::rat)";
+test "-2 * x = -(y::rat)";
+test "(-2 * x) / (-1 * (y::rat)) = z";
+test "-2 * x < -(y::rat)";
+test "-2 * x <= -1 * (y::rat)";
+test "-x < -23 * (y::rat)";
+test "-x <= -23 * (y::rat)";
+*)
+
(** Declarations for ExtractCommonTerm **)
@@ -178,13 +269,42 @@
val int_cancel_factor =
map Bin_Simprocs.prep_simproc
- [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
- ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
+ [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
+ EqCancelFactor.proc),
+ ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
DivideCancelFactor.proc)];
+(** Versions for all fields, including unordered ones (type complex).*)
+
+structure FieldEqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
+);
+
+structure FieldDivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+ val prove_conv = Bin_Simprocs.prove_conv
+ val mk_bal = HOLogic.mk_binop "HOL.divide"
+ val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
+ val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
+);
+
+val field_cancel_factor =
+ map Bin_Simprocs.prep_simproc
+ [("field_eq_cancel_factor",
+ ["(l::'a::field) * m = n", "(l::'a::field) = m * n"],
+ FieldEqCancelFactor.proc),
+ ("field_divide_cancel_factor",
+ ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
+ FieldDivideCancelFactor.proc)];
+
end;
Addsimprocs int_cancel_factor;
+Addsimprocs field_cancel_factor;
(*examples:
@@ -204,3 +324,23 @@
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
*)
+(*And the same examples for fields such as rat or real:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+
+test "x*k = k*(y::rat)";
+test "k = k*(y::rat)";
+test "a*(b*c) = (b::rat)";
+test "a*(b*c) = d*(b::rat)*(x*a)";
+
+
+test "(x*k) / (k*(y::rat)) = (uu::rat)";
+test "(k) / (k*(y::rat)) = (uu::rat)";
+test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
+test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
+
+(*FIXME: what do we do about this?*)
+test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
+*)
--- a/src/HOL/Integ/nat_simprocs.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Tue Feb 17 10:41:59 2004 +0100
@@ -512,7 +512,7 @@
Suc_eq_number_of,eq_number_of_Suc,
mult_Suc, mult_Suc_right,
eq_number_of_0, eq_0_number_of, less_0_number_of,
- nat_number_of, if_True, if_False];
+ of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@
Nat_Numeral_Simprocs.cancel_numerals;
--- a/src/HOL/Real/rat_arith.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Real/rat_arith.ML Tue Feb 17 10:41:59 2004 +0100
@@ -8,236 +8,20 @@
Instantiation of the generic linear arithmetic package for type rat.
*)
-(*FIXME DELETE*)
+(*FIXME: these monomorphic versions are necessary because of a bug in the arith
+ procedure*)
val rat_mult_strict_left_mono =
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
val rat_mult_left_mono =
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
- val le_number_of_eq = thm"le_number_of_eq";
-
-
-(****Common factor cancellation****)
-
-(*To quote from Provers/Arith/cancel_numeral_factor.ML:
-
-This simproc Cancels common coefficients in balanced expressions:
-
- u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
-
-where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
-and d = gcd(m,m') and n=m/d and n'=m'/d.
-*)
-
-val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq]
-
-local open Int_Numeral_Simprocs
-in
-
-structure CancelNumeralFactorCommon =
- struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val trans_tac = trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
- val simplify_meta_eq =
- Int_Numeral_Simprocs.simplify_meta_eq
- [add_0, add_0_right,
- mult_zero_left, mult_zero_right, mult_1, mult_1_right];
- end
-
-structure DivCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
- val cancel = mult_divide_cancel_left RS trans
- val neg_exchanges = false
-)
-
-structure EqCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val cancel = field_mult_cancel_left RS trans
- val neg_exchanges = false
-)
-
-structure LessCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <"
- val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
- val cancel = mult_less_cancel_left RS trans
- val neg_exchanges = true
-)
-
-structure LeCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binrel "op <="
- val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
- val cancel = mult_le_cancel_left RS trans
- val neg_exchanges = true
-)
-
-val field_cancel_numeral_factors_relations =
- map Bin_Simprocs.prep_simproc
- [("field_eq_cancel_numeral_factor",
- ["(l::'a::{field,number_ring}) * m = n",
- "(l::'a::{field,number_ring}) = m * n"],
- EqCancelNumeralFactor.proc),
- ("field_less_cancel_numeral_factor",
- ["(l::'a::{ordered_field,number_ring}) * m < n",
- "(l::'a::{ordered_field,number_ring}) < m * n"],
- LessCancelNumeralFactor.proc),
- ("field_le_cancel_numeral_factor",
- ["(l::'a::{ordered_field,number_ring}) * m <= n",
- "(l::'a::{ordered_field,number_ring}) <= m * n"],
- LeCancelNumeralFactor.proc)]
-
-val field_cancel_numeral_factors_divide =
- Bin_Simprocs.prep_simproc
- ("field_cancel_numeral_factor",
- ["((l::'a::{field,number_ring}) * m) / n",
- "(l::'a::{field,number_ring}) / (m * n)",
- "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
- DivCancelNumeralFactor.proc)
-
-val field_cancel_numeral_factors =
- field_cancel_numeral_factors_relations @
- [field_cancel_numeral_factors_divide]
-
-end;
-
-Addsimprocs field_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "0 <= (y::rat) * -2";
-test "9*x = 12 * (y::rat)";
-test "(9*x) / (12 * (y::rat)) = z";
-test "9*x < 12 * (y::rat)";
-test "9*x <= 12 * (y::rat)";
-
-test "-99*x = 132 * (y::rat)";
-test "(-99*x) / (132 * (y::rat)) = z";
-test "-99*x < 132 * (y::rat)";
-test "-99*x <= 132 * (y::rat)";
-
-test "999*x = -396 * (y::rat)";
-test "(999*x) / (-396 * (y::rat)) = z";
-test "999*x < -396 * (y::rat)";
-test "999*x <= -396 * (y::rat)";
-
-test "(- ((2::rat) * x) <= 2 * y)";
-test "-99*x = -81 * (y::rat)";
-test "(-99*x) / (-81 * (y::rat)) = z";
-test "-99*x <= -81 * (y::rat)";
-test "-99*x < -81 * (y::rat)";
-
-test "-2 * x = -1 * (y::rat)";
-test "-2 * x = -(y::rat)";
-test "(-2 * x) / (-1 * (y::rat)) = z";
-test "-2 * x < -(y::rat)";
-test "-2 * x <= -1 * (y::rat)";
-test "-x < -23 * (y::rat)";
-test "-x <= -23 * (y::rat)";
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local open Int_Numeral_Simprocs
-in
-
-structure CancelFactorCommon =
- struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
- end;
-
-(*This version works for all fields, including unordered ones (complex).
- The version declared in int_factor_simprocs.ML is for integers.*)
-structure EqCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
-);
-
-
-(*This version works for fields, with the generic divides operator (/).
- The version declared in int_factor_simprocs.ML for integers with div.*)
-structure DivideCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "HOL.divide"
- val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
-);
-
-val field_cancel_factor =
- map Bin_Simprocs.prep_simproc
- [("field_eq_cancel_factor",
- ["(l::'a::field) * m = n", "(l::'a::field) = m * n"],
- EqCancelFactor.proc),
- ("field_divide_cancel_factor",
- ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
- DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs field_cancel_factor;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x*k = k*(y::rat)";
-test "k = k*(y::rat)";
-test "a*(b*c) = (b::rat)";
-test "a*(b*c) = d*(b::rat)*(x*a)";
-
-
-test "(x*k) / (k*(y::rat)) = (uu::rat)";
-test "(k) / (k*(y::rat)) = (uu::rat)";
-test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
-test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
-*)
-
-
(****Instantiation of the generic linear arithmetic package for fields****)
-
local
-val simprocs = [field_cancel_numeral_factors_divide]
+val simprocs = field_cancel_numeral_factors
val mono_ss = simpset() addsimps
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
@@ -259,10 +43,11 @@
(rat_mult_left_mono,
cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
-val simps = [order_less_irrefl, True_implies_equals,
+val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
inst "a" "(number_of ?v)" right_distrib,
divide_1, divide_zero_left,
times_divide_eq_right, times_divide_eq_left,
+ minus_divide_left RS sym, minus_divide_right RS sym,
of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
of_int_mult, of_int_of_nat_eq];
--- a/src/HOL/Real/real_arith.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Real/real_arith.ML Tue Feb 17 10:41:59 2004 +0100
@@ -111,6 +111,8 @@
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
+val real_number_of = thm"real_number_of";
+val real_of_nat_number_of = thm"real_of_nat_number_of";
(****Instantiation of the generic linear arithmetic package****)
@@ -128,7 +130,8 @@
val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add,
real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
real_of_int_minus RS sym, real_of_int_diff RS sym,
- real_of_int_mult RS sym];
+ real_of_int_mult RS sym,
+ real_of_nat_number_of, real_number_of];
val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
real_of_int_inject RS iffD2];