# HG changeset patch # User paulson # Date 1077010919 -3600 # Node ID 55fe71faaddafb538f1f447269ac5bb80d8d0681 # Parent 57c2d90936ba7bdf8cb62a5269e0c3bb3be2b4e3 further tweaks to the numeric theories diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Hyperreal/IntFloor.ML --- 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); diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Integ/IntArith.thy --- 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"; diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Integ/NatBin.thy --- 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\0"} and @{term "0\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 \ 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) \ 2*x + 1 = (0 \ x)" +by arith + +lemma of_nat_number_of_lemma: + "of_nat (number_of v :: nat) = + (if 0 \ (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"; diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Integ/int_arith1.ML --- 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, diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Integ/int_factor_simprocs.ML --- 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"; +*) diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Integ/nat_simprocs.ML --- 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; diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Real/rat_arith.ML --- 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]; diff -r 57c2d90936ba -r 55fe71faadda src/HOL/Real/real_arith.ML --- 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];