# HG changeset patch # User paulson # Date 975489703 -3600 # Node ID 8f34ecae14468fc1d5d6ecebb061f9c98c172a98 # Parent c00b1d0d46ac559799733f5f49ac832993d1339b invoking CancelNumeralFactorFun diff -r c00b1d0d46ac -r 8f34ecae1446 src/HOL/Integ/NatSimprocs.thy --- a/src/HOL/Integ/NatSimprocs.thy Wed Nov 29 10:19:32 2000 +0100 +++ b/src/HOL/Integ/NatSimprocs.thy Wed Nov 29 10:21:43 2000 +0100 @@ -1,6 +1,6 @@ - +(*Loading further simprocs*) theory NatSimprocs = NatBin -files "nat_simprocs.ML": +files "int_factor_simprocs.ML" "nat_simprocs.ML": setup nat_simprocs_setup diff -r c00b1d0d46ac -r 8f34ecae1446 src/HOL/Integ/int_factor_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Integ/int_factor_simprocs.ML Wed Nov 29 10:21:43 2000 +0100 @@ -0,0 +1,139 @@ +(* Title: HOL/int_factor_simprocs.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + +Factor cancellation simprocs for the integers. + +This file can't be combined with int_arith1,2 because it requires IntDiv.thy. +*) + +(** Factor cancellation theorems for "int" **) + +Goal "!!k::int. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))"; +by (stac zmult_zle_cancel1 1); +by Auto_tac; +qed "int_mult_le_cancel1"; + +Goal "!!k::int. (k*m < k*n) = ((#0 < k & m (k*m) div (k*n) = (m div n)"; +by (stac zdiv_zmult_zmult1 1); +by Auto_tac; +qed "int_mult_div_cancel1"; + +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 mult_1s)) + THEN ALLGOALS + (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ + bin_simps@zmult_ac)) + val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) + val simplify_meta_eq = simplify_meta_eq mult_1s + end + +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "intdiv_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binop "Divides.op div" + val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT + val cancel = int_mult_div_cancel1 RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "inteq_cancel_numeral_factor" + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT + val cancel = int_mult_eq_cancel1 RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "intless_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT + val cancel = int_mult_less_cancel1 RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "intle_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT + val cancel = int_mult_le_cancel1 RS trans + val neg_exchanges = true +) + +val int_cancel_numeral_factors = + map prep_simproc + [("inteq_cancel_numeral_factors", + prep_pats ["(l::int) * m = n", "(l::int) = m * n"], + EqCancelNumeralFactor.proc), + ("intless_cancel_numeral_factors", + prep_pats ["(l::int) * m < n", "(l::int) < m * n"], + LessCancelNumeralFactor.proc), + ("intle_cancel_numeral_factors", + prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], + LeCancelNumeralFactor.proc), + ("intdiv_cancel_numeral_factors", + prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], + DivCancelNumeralFactor.proc)]; + +end; + +Addsimprocs int_cancel_numeral_factors; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +test "#9*x = #12 * (y::int)"; +test "(#9*x) div (#12 * (y::int)) = z"; +test "#9*x < #12 * (y::int)"; +test "#9*x <= #12 * (y::int)"; + +test "#-99*x = #132 * (y::int)"; +test "(#-99*x) div (#132 * (y::int)) = z"; +test "#-99*x < #132 * (y::int)"; +test "#-99*x <= #132 * (y::int)"; + +test "#999*x = #-396 * (y::int)"; +test "(#999*x) div (#-396 * (y::int)) = z"; +test "#999*x < #-396 * (y::int)"; +test "#999*x <= #-396 * (y::int)"; + +test "#-99*x = #-81 * (y::int)"; +test "(#-99*x) div (#-81 * (y::int)) = z"; +test "#-99*x <= #-81 * (y::int)"; +test "#-99*x < #-81 * (y::int)"; + +test "#-2 * x = #-1 * (y::int)"; +test "#-2 * x = -(y::int)"; +test "(#-2 * x) div (#-1 * (y::int)) = z"; +test "#-2 * x < -(y::int)"; +test "#-2 * x <= #-1 * (y::int)"; +test "-x < #-23 * (y::int)"; +test "-x <= #-23 * (y::int)"; +*) + diff -r c00b1d0d46ac -r 8f34ecae1446 src/HOL/Integ/nat_simprocs.ML --- a/src/HOL/Integ/nat_simprocs.ML Wed Nov 29 10:19:32 2000 +0100 +++ b/src/HOL/Integ/nat_simprocs.ML Wed Nov 29 10:21:43 2000 +0100 @@ -64,6 +64,25 @@ qed "nat_le_add_iff2"; +(** For cancel_numeral_factors **) + +Goal "(#0::nat) < k ==> (k*m <= k*n) = (m<=n)"; +by Auto_tac; +qed "nat_mult_le_cancel1"; + +Goal "(#0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)"; +by Auto_tac; +qed "nat_mult_eq_cancel1"; + +Goal "(#0::nat) < k ==> (k*m) div (k*n) = (m div n)"; +by Auto_tac; +qed "nat_mult_div_cancel1"; + + structure Nat_Numeral_Simprocs = struct @@ -117,7 +136,8 @@ val bin_simps = [add_nat_number_of, nat_number_of_add_left, diff_nat_number_of, le_nat_number_of_eq_not_less, - less_nat_number_of, Let_number_of, nat_number_of] @ + less_nat_number_of, mult_nat_number_of, + Let_number_of, nat_number_of] @ bin_arith_simps @ bin_rel_simps; fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; @@ -172,6 +192,9 @@ [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right, mult_0, mult_0_right, mult_1, mult_1_right]; + +(*** Instantiating CancelNumeralsFun ***) + structure CancelNumeralsCommon = struct val mk_sum = mk_sum @@ -252,6 +275,8 @@ DiffCancelNumerals.proc)]; +(*** Instantiating CombineNumeralsFun ***) + structure CombineNumeralsData = struct val add = op + : int*int -> int @@ -280,11 +305,78 @@ prep_pats ["(i::nat) + j", "Suc (i + j)"], CombineNumerals.proc); + +(*** Instantiating CancelNumeralFactorFun ***) + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val trans_tac = trans_tac + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps + [Suc_eq_add_numeral_1]@mult_1s)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac)) + val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) + val simplify_meta_eq = simplify_meta_eq + end + +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "natdiv_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binop "Divides.op div" + val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT + val cancel = nat_mult_div_cancel1 RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "nateq_cancel_numeral_factor" + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val cancel = nat_mult_eq_cancel1 RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "natless_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT + val cancel = nat_mult_less_cancel1 RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = prove_conv "natle_cancel_numeral_factor" + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT + val cancel = nat_mult_le_cancel1 RS trans + val neg_exchanges = true +) + +val cancel_numeral_factors = + map prep_simproc + [("nateq_cancel_numeral_factors", + prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"], + EqCancelNumeralFactor.proc), + ("natless_cancel_numeral_factors", + prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"], + LessCancelNumeralFactor.proc), + ("natle_cancel_numeral_factors", + prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"], + LeCancelNumeralFactor.proc), + ("natdiv_cancel_numeral_factors", + prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"], + DivCancelNumeralFactor.proc)]; + end; Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; (*examples: @@ -344,6 +436,12 @@ test "(#2*n*m) + (#3*(m*n)) = (u::nat)"; (*negative numerals: FAIL*) test "Suc (i + j + #-3 + k) = u"; + +(*cancel_numeral_factor*) +test "#9*x = #12 * (y::nat)"; +test "(#9*x) div (#12 * (y::nat)) = z"; +test "#9*x < #12 * (y::nat)"; +test "#9*x <= #12 * (y::nat)"; *)