invoking CancelNumeralFactorFun
authorpaulson
Wed, 29 Nov 2000 10:21:43 +0100
changeset 10536 8f34ecae1446
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
--- 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
 
--- /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<n) | (k < #0 & n<m))";
+by (stac zmult_zless_cancel1 1);
+by Auto_tac;  
+qed "int_mult_less_cancel1";
+
+Goal "!!k::int. (k*m = k*n) = (k = #0 | m=n)";
+by Auto_tac;  
+qed "int_mult_eq_cancel1";
+
+Goal "!!k::int. k~=#0 ==> (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)";
+*)
+
--- 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<n)";
+by Auto_tac;  
+qed "nat_mult_less_cancel1";
+
+Goal "(#0::nat) < k ==> (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)";
 *)