src/HOL/int_factor_simprocs.ML

+(*  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 (and for fields).
+
+This file can't be combined with int_arith1 because it requires IntDiv.thy.
+*)
+
+
+(*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 @{thm zdiv_zmult_zmult1} 1);
+by Auto_tac;
+qed "int_mult_div_cancel1";
+
+(*For ExtractCommonTermFun, cancelling common factors*)
+Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
+by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
+qed "int_mult_div_cancel_disj";
+
+
+local
+  open Int_Numeral_Simprocs
+in
+
+structure CancelNumeralFactorCommon =
+  struct
+  val mk_coeff          = mk_coeff
+  val dest_coeff        = dest_coeff 1
+  val trans_tac         = fn _ => trans_tac
+
+  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
+  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
+  val norm_ss3 = HOL_ss addsimps mult_ac
+  fun norm_tac ss =
+    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
+    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
+
+  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
+  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
+  val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
+    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
+      @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
+  end
+
+(*Version for integer division*)
+structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
+  val cancel = int_mult_div_cancel1 RS trans
+  val neg_exchanges = false
+)
+
+(*Version for fields*)
+structure DivideCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+  val cancel = @{thm mult_divide_cancel_left} RS trans
+  val neg_exchanges = false
+)
+
+structure EqCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_eq
+  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+  val cancel = @{thm mult_cancel_left} RS trans
+  val neg_exchanges = false
+)
+
+structure LessCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val cancel = @{thm mult_less_cancel_left} RS trans
+  val neg_exchanges = true
+)
+
+structure LeCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val cancel = @{thm mult_le_cancel_left} RS trans
+  val neg_exchanges = true
+)
+
+val cancel_numeral_factors =
+  map Int_Numeral_Base_Simprocs.prep_simproc
+   [("ring_eq_cancel_numeral_factor",
+     ["(l::'a::{idom,number_ring}) * m = n",
+      "(l::'a::{idom,number_ring}) = m * n"],
+     K EqCancelNumeralFactor.proc),
+    ("ring_less_cancel_numeral_factor",
+     ["(l::'a::{ordered_idom,number_ring}) * m < n",
+      "(l::'a::{ordered_idom,number_ring}) < m * n"],
+     K LessCancelNumeralFactor.proc),
+    ("ring_le_cancel_numeral_factor",
+     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
+      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
+     K LeCancelNumeralFactor.proc),
+    ("int_div_cancel_numeral_factors",
+     ["((l::int) * m) div n", "(l::int) div (m * n)"],
+     K IntDivCancelNumeralFactor.proc),
+    ("divide_cancel_numeral_factor",
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
+      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
+     K DivideCancelNumeralFactor.proc)];
+
+(* referenced by rat_arith.ML *)
+val field_cancel_numeral_factors =
+  map Int_Numeral_Base_Simprocs.prep_simproc
+   [("field_eq_cancel_numeral_factor",
+     ["(l::'a::{field,number_ring}) * m = n",
+      "(l::'a::{field,number_ring}) = m * n"],
+     K EqCancelNumeralFactor.proc),
+    ("field_cancel_numeral_factor",
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
+      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
+     K DivideCancelNumeralFactor.proc)]
+
+end;
+
+Addsimprocs 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)";
+*)
+
+(*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 **)
+
+local
+  open Int_Numeral_Simprocs
+in
+
+(*Find first term that matches u*)
+fun find_first_t past u []         = raise TERM ("find_first_t", [])
+  | find_first_t past u (t::terms) =
+        if u aconv t then (rev past @ terms)
+        else find_first_t (t::past) u terms
+        handle TERM _ => find_first_t (t::past) u terms;
+
+(** Final simplification for the CancelFactor simprocs **)
+val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
+  [@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];
+
+fun cancel_simplify_meta_eq cancel_th ss th =
+    simplify_one ss (([th, cancel_th]) MRS trans);
+
+(*At present, long_mk_prod creates Numeral1, so this requires the axclass
+  number_ring*)
+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_t []
+  val trans_tac         = fn _ => trans_tac
+  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+  end;
+
+(*mult_cancel_left requires a ring with no zero divisors.*)
+structure EqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Int_Numeral_Base_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 @{thm mult_cancel_left}
+);
+
+(*int_mult_div_cancel_disj is for integer division (div).*)
+structure IntDivCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
+  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
+);
+
+(*Version for all fields, including unordered ones (type complex).*)
+structure DivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
+);
+
+(*The number_ring class is necessary because the simprocs refer to the
+  binary number 1.  FIXME: probably they could use 1 instead.*)
+val cancel_factors =
+  map Int_Numeral_Base_Simprocs.prep_simproc
+   [("ring_eq_cancel_factor",
+     ["(l::'a::{idom,number_ring}) * m = n",
+      "(l::'a::{idom,number_ring}) = m * n"],
+    K EqCancelFactor.proc),
+    ("int_div_cancel_factor",
+     ["((l::int) * m) div n", "(l::int) div (m * n)"],
+     K IntDivCancelFactor.proc),
+    ("divide_cancel_factor",
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
+     K DivideCancelFactor.proc)];
+
+end;
+
+Addsimprocs cancel_factors;
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+
+test "x*k = k*(y::int)";
+test "k = k*(y::int)";
+test "a*(b*c) = (b::int)";
+test "a*(b*c) = d*(b::int)*(x*a)";
+
+test "(x*k) div (k*(y::int)) = (uu::int)";
+test "(k) div (k*(y::int)) = (uu::int)";
+test "(a*(b*c)) div ((b::int)) = (uu::int)";
+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";
+*)