invoking CancelNumeralFactorFun
authorpaulson
Wed Nov 29 10:21:43 2000 +0100 (2000-11-29)
changeset 105368f34ecae1446
parent 10535 c00b1d0d46ac
child 10537 1d2f15504d38
invoking CancelNumeralFactorFun
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
     1.1 --- a/src/HOL/Integ/NatSimprocs.thy	Wed Nov 29 10:19:32 2000 +0100
     1.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Wed Nov 29 10:21:43 2000 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -
     1.5 +(*Loading further simprocs*)
     1.6  theory NatSimprocs = NatBin
     1.7 -files "nat_simprocs.ML":
     1.8 +files "int_factor_simprocs.ML" "nat_simprocs.ML":
     1.9  
    1.10  setup nat_simprocs_setup
    1.11  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Wed Nov 29 10:21:43 2000 +0100
     2.3 @@ -0,0 +1,139 @@
     2.4 +(*  Title:      HOL/int_factor_simprocs.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2000  University of Cambridge
     2.8 +
     2.9 +Factor cancellation simprocs for the integers.
    2.10 +
    2.11 +This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
    2.12 +*)
    2.13 +
    2.14 +(** Factor cancellation theorems for "int" **)
    2.15 +
    2.16 +Goal "!!k::int. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
    2.17 +by (stac zmult_zle_cancel1 1);
    2.18 +by Auto_tac;  
    2.19 +qed "int_mult_le_cancel1";
    2.20 +
    2.21 +Goal "!!k::int. (k*m < k*n) = ((#0 < k & m<n) | (k < #0 & n<m))";
    2.22 +by (stac zmult_zless_cancel1 1);
    2.23 +by Auto_tac;  
    2.24 +qed "int_mult_less_cancel1";
    2.25 +
    2.26 +Goal "!!k::int. (k*m = k*n) = (k = #0 | m=n)";
    2.27 +by Auto_tac;  
    2.28 +qed "int_mult_eq_cancel1";
    2.29 +
    2.30 +Goal "!!k::int. k~=#0 ==> (k*m) div (k*n) = (m div n)";
    2.31 +by (stac zdiv_zmult_zmult1 1); 
    2.32 +by Auto_tac;  
    2.33 +qed "int_mult_div_cancel1";
    2.34 +
    2.35 +local
    2.36 +  open Int_Numeral_Simprocs
    2.37 +in
    2.38 +
    2.39 +structure CancelNumeralFactorCommon =
    2.40 +  struct
    2.41 +  val mk_coeff		= mk_coeff
    2.42 +  val dest_coeff	= dest_coeff 1
    2.43 +  val trans_tac         = trans_tac
    2.44 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    2.45 +                 THEN ALLGOALS
    2.46 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    2.47 +                                               bin_simps@zmult_ac))
    2.48 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    2.49 +  val simplify_meta_eq  = simplify_meta_eq mult_1s
    2.50 +  end
    2.51 +
    2.52 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
    2.53 + (open CancelNumeralFactorCommon
    2.54 +  val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
    2.55 +  val mk_bal   = HOLogic.mk_binop "Divides.op div"
    2.56 +  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    2.57 +  val cancel = int_mult_div_cancel1 RS trans
    2.58 +  val neg_exchanges = false
    2.59 +)
    2.60 +
    2.61 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
    2.62 + (open CancelNumeralFactorCommon
    2.63 +  val prove_conv = prove_conv "inteq_cancel_numeral_factor"
    2.64 +  val mk_bal   = HOLogic.mk_eq
    2.65 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    2.66 +  val cancel = int_mult_eq_cancel1 RS trans
    2.67 +  val neg_exchanges = false
    2.68 +)
    2.69 +
    2.70 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
    2.71 + (open CancelNumeralFactorCommon
    2.72 +  val prove_conv = prove_conv "intless_cancel_numeral_factor"
    2.73 +  val mk_bal   = HOLogic.mk_binrel "op <"
    2.74 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    2.75 +  val cancel = int_mult_less_cancel1 RS trans
    2.76 +  val neg_exchanges = true
    2.77 +)
    2.78 +
    2.79 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
    2.80 + (open CancelNumeralFactorCommon
    2.81 +  val prove_conv = prove_conv "intle_cancel_numeral_factor"
    2.82 +  val mk_bal   = HOLogic.mk_binrel "op <="
    2.83 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    2.84 +  val cancel = int_mult_le_cancel1 RS trans
    2.85 +  val neg_exchanges = true
    2.86 +)
    2.87 +
    2.88 +val int_cancel_numeral_factors = 
    2.89 +  map prep_simproc
    2.90 +   [("inteq_cancel_numeral_factors",
    2.91 +     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    2.92 +     EqCancelNumeralFactor.proc),
    2.93 +    ("intless_cancel_numeral_factors", 
    2.94 +     prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    2.95 +     LessCancelNumeralFactor.proc),
    2.96 +    ("intle_cancel_numeral_factors", 
    2.97 +     prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    2.98 +     LeCancelNumeralFactor.proc),
    2.99 +    ("intdiv_cancel_numeral_factors", 
   2.100 +     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   2.101 +     DivCancelNumeralFactor.proc)];
   2.102 +
   2.103 +end;
   2.104 +
   2.105 +Addsimprocs int_cancel_numeral_factors;
   2.106 +
   2.107 +
   2.108 +(*examples:
   2.109 +print_depth 22;
   2.110 +set timing;
   2.111 +set trace_simp;
   2.112 +fun test s = (Goal s; by (Simp_tac 1)); 
   2.113 +
   2.114 +test "#9*x = #12 * (y::int)";
   2.115 +test "(#9*x) div (#12 * (y::int)) = z";
   2.116 +test "#9*x < #12 * (y::int)";
   2.117 +test "#9*x <= #12 * (y::int)";
   2.118 +
   2.119 +test "#-99*x = #132 * (y::int)";
   2.120 +test "(#-99*x) div (#132 * (y::int)) = z";
   2.121 +test "#-99*x < #132 * (y::int)";
   2.122 +test "#-99*x <= #132 * (y::int)";
   2.123 +
   2.124 +test "#999*x = #-396 * (y::int)";
   2.125 +test "(#999*x) div (#-396 * (y::int)) = z";
   2.126 +test "#999*x < #-396 * (y::int)";
   2.127 +test "#999*x <= #-396 * (y::int)";
   2.128 +
   2.129 +test "#-99*x = #-81 * (y::int)";
   2.130 +test "(#-99*x) div (#-81 * (y::int)) = z";
   2.131 +test "#-99*x <= #-81 * (y::int)";
   2.132 +test "#-99*x < #-81 * (y::int)";
   2.133 +
   2.134 +test "#-2 * x = #-1 * (y::int)";
   2.135 +test "#-2 * x = -(y::int)";
   2.136 +test "(#-2 * x) div (#-1 * (y::int)) = z";
   2.137 +test "#-2 * x < -(y::int)";
   2.138 +test "#-2 * x <= #-1 * (y::int)";
   2.139 +test "-x < #-23 * (y::int)";
   2.140 +test "-x <= #-23 * (y::int)";
   2.141 +*)
   2.142 +
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Wed Nov 29 10:19:32 2000 +0100
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Wed Nov 29 10:21:43 2000 +0100
     3.3 @@ -64,6 +64,25 @@
     3.4  qed "nat_le_add_iff2";
     3.5  
     3.6  
     3.7 +(** For cancel_numeral_factors **)
     3.8 +
     3.9 +Goal "(#0::nat) < k ==> (k*m <= k*n) = (m<=n)";
    3.10 +by Auto_tac;  
    3.11 +qed "nat_mult_le_cancel1";
    3.12 +
    3.13 +Goal "(#0::nat) < k ==> (k*m < k*n) = (m<n)";
    3.14 +by Auto_tac;  
    3.15 +qed "nat_mult_less_cancel1";
    3.16 +
    3.17 +Goal "(#0::nat) < k ==> (k*m = k*n) = (m=n)";
    3.18 +by Auto_tac;  
    3.19 +qed "nat_mult_eq_cancel1";
    3.20 +
    3.21 +Goal "(#0::nat) < k ==> (k*m) div (k*n) = (m div n)";
    3.22 +by Auto_tac;  
    3.23 +qed "nat_mult_div_cancel1";
    3.24 +
    3.25 +
    3.26  structure Nat_Numeral_Simprocs =
    3.27  struct
    3.28  
    3.29 @@ -117,7 +136,8 @@
    3.30  
    3.31  val bin_simps = [add_nat_number_of, nat_number_of_add_left,
    3.32                   diff_nat_number_of, le_nat_number_of_eq_not_less,
    3.33 -                 less_nat_number_of, Let_number_of, nat_number_of] @
    3.34 +                 less_nat_number_of, mult_nat_number_of, 
    3.35 +                 Let_number_of, nat_number_of] @
    3.36                  bin_arith_simps @ bin_rel_simps;
    3.37  
    3.38  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    3.39 @@ -172,6 +192,9 @@
    3.40           [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
    3.41           mult_0, mult_0_right, mult_1, mult_1_right];
    3.42  
    3.43 +
    3.44 +(*** Instantiating CancelNumeralsFun ***)
    3.45 +
    3.46  structure CancelNumeralsCommon =
    3.47    struct
    3.48    val mk_sum            = mk_sum
    3.49 @@ -252,6 +275,8 @@
    3.50       DiffCancelNumerals.proc)];
    3.51  
    3.52  
    3.53 +(*** Instantiating CombineNumeralsFun ***)
    3.54 +
    3.55  structure CombineNumeralsData =
    3.56    struct
    3.57    val add		= op + : int*int -> int 
    3.58 @@ -280,11 +305,78 @@
    3.59                    prep_pats ["(i::nat) + j", "Suc (i + j)"],
    3.60                    CombineNumerals.proc);
    3.61  
    3.62 +
    3.63 +(*** Instantiating CancelNumeralFactorFun ***)
    3.64 +
    3.65 +structure CancelNumeralFactorCommon =
    3.66 +  struct
    3.67 +  val mk_coeff		= mk_coeff
    3.68 +  val dest_coeff	= dest_coeff
    3.69 +  val trans_tac         = trans_tac
    3.70 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps 
    3.71 +                                             [Suc_eq_add_numeral_1]@mult_1s))
    3.72 +                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
    3.73 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    3.74 +  val simplify_meta_eq  = simplify_meta_eq
    3.75 +  end
    3.76 +
    3.77 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
    3.78 + (open CancelNumeralFactorCommon
    3.79 +  val prove_conv = prove_conv "natdiv_cancel_numeral_factor"
    3.80 +  val mk_bal   = HOLogic.mk_binop "Divides.op div"
    3.81 +  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
    3.82 +  val cancel = nat_mult_div_cancel1 RS trans
    3.83 +  val neg_exchanges = false
    3.84 +)
    3.85 +
    3.86 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
    3.87 + (open CancelNumeralFactorCommon
    3.88 +  val prove_conv = prove_conv "nateq_cancel_numeral_factor"
    3.89 +  val mk_bal   = HOLogic.mk_eq
    3.90 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    3.91 +  val cancel = nat_mult_eq_cancel1 RS trans
    3.92 +  val neg_exchanges = false
    3.93 +)
    3.94 +
    3.95 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
    3.96 + (open CancelNumeralFactorCommon
    3.97 +  val prove_conv = prove_conv "natless_cancel_numeral_factor"
    3.98 +  val mk_bal   = HOLogic.mk_binrel "op <"
    3.99 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
   3.100 +  val cancel = nat_mult_less_cancel1 RS trans
   3.101 +  val neg_exchanges = true
   3.102 +)
   3.103 +
   3.104 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
   3.105 + (open CancelNumeralFactorCommon
   3.106 +  val prove_conv = prove_conv "natle_cancel_numeral_factor"
   3.107 +  val mk_bal   = HOLogic.mk_binrel "op <="
   3.108 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
   3.109 +  val cancel = nat_mult_le_cancel1 RS trans
   3.110 +  val neg_exchanges = true
   3.111 +)
   3.112 +
   3.113 +val cancel_numeral_factors = 
   3.114 +  map prep_simproc
   3.115 +   [("nateq_cancel_numeral_factors",
   3.116 +     prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"], 
   3.117 +     EqCancelNumeralFactor.proc),
   3.118 +    ("natless_cancel_numeral_factors", 
   3.119 +     prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"], 
   3.120 +     LessCancelNumeralFactor.proc),
   3.121 +    ("natle_cancel_numeral_factors", 
   3.122 +     prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"], 
   3.123 +     LeCancelNumeralFactor.proc),
   3.124 +    ("natdiv_cancel_numeral_factors", 
   3.125 +     prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"], 
   3.126 +     DivCancelNumeralFactor.proc)];
   3.127 +
   3.128  end;
   3.129  
   3.130  
   3.131  Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   3.132  Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   3.133 +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   3.134  
   3.135  
   3.136  (*examples:
   3.137 @@ -344,6 +436,12 @@
   3.138  test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
   3.139  (*negative numerals: FAIL*)
   3.140  test "Suc (i + j + #-3 + k) = u";
   3.141 +
   3.142 +(*cancel_numeral_factor*)
   3.143 +test "#9*x = #12 * (y::nat)";
   3.144 +test "(#9*x) div (#12 * (y::nat)) = z";
   3.145 +test "#9*x < #12 * (y::nat)";
   3.146 +test "#9*x <= #12 * (y::nat)";
   3.147  *)
   3.148  
   3.149