src/HOL/Integ/int_factor_simprocs.ML

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

(*  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 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         = 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

(*Version for integer division*)
structure DivCancelNumeralFactor = CancelNumeralFactorFun
 (open CancelNumeralFactorCommon
  val prove_conv = Bin_Simprocs.prove_conv
  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
)

(*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 =" 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 <" 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 ring_cancel_numeral_factors =
  map Bin_Simprocs.prep_simproc
   [("ring_eq_cancel_numeral_factor",
     ["(l::'a::{ordered_idom,number_ring}) * m = n",
      "(l::'a::{ordered_idom,number_ring}) = m * n"],
     EqCancelNumeralFactor.proc),
    ("ring_less_cancel_numeral_factor",
     ["(l::'a::{ordered_idom,number_ring}) * m < n",
      "(l::'a::{ordered_idom,number_ring}) < m * n"],
     LessCancelNumeralFactor.proc),
    ("ring_le_cancel_numeral_factor",
     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
     LeCancelNumeralFactor.proc),
    ("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::{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)"],
     FieldDivCancelNumeralFactor.proc)]

end;

Addsimprocs ring_cancel_numeral_factors;
Addsimprocs field_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 past u []         = raise TERM("find_first", [])
  | find_first past u (t::terms) =
        if u aconv t then (rev past @ terms)
        else find_first (t::past) u terms
        handle TERM _ => find_first (t::past) u terms;

(*Final simplification: cancel + and *  *)
fun cancel_simplify_meta_eq cancel_th th =
    Int_Numeral_Simprocs.simplify_meta_eq
        [mult_1, mult_1_right]
        (([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 []
  val trans_tac         = trans_tac
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
  end;

(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
  rat_arith.ML works for all fields.*)
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 =" HOLogic.intT
  val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
);

(*int_mult_div_cancel_disj is for integer division (div). The version in
  rat_arith.ML works for all fields, using real division (/).*)
structure DivideCancelFactor = ExtractCommonTermFun
 (open CancelFactorCommon
  val prove_conv = Bin_Simprocs.prove_conv
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
);

val int_cancel_factor =
  map Bin_Simprocs.prep_simproc
   [("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
);

(*The number_ring class is necessary because the simprocs refer to the 
  binary number 1.  FIXME: probably they could use 1 instead.*)
val field_cancel_factor =
  map Bin_Simprocs.prep_simproc
   [("field_eq_cancel_factor",
     ["(l::'a::{field,number_ring}) * m = n",
      "(l::'a::{field,number_ring}) = m * n"], 
     FieldEqCancelFactor.proc),
    ("field_divide_cancel_factor",
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
     FieldDivideCancelFactor.proc)];

end;

Addsimprocs int_cancel_factor;
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::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";
*)