# HG changeset patch
# User paulson
# Date 977235441 -3600
# Node ID ba98f00cec4f0b7e20890fe33b453080df0b5d6c
# Parent  9e6898befad4d7fe0736a0062843ffec5963e09f
inserting the simproc int_cancel_factor

diff -r 9e6898befad4 -r ba98f00cec4f src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 19 15:16:21 2000 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 19 15:17:21 2000 +0100
@@ -29,6 +29,11 @@
 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
@@ -137,3 +142,86 @@
 test "-x <= #-23 * (y::int)";
 *)
 
+
+(** Declarations for ExtractCommonTerm **)
+
+local
+  open Int_Numeral_Simprocs
+in
+
+
+(*this version ALWAYS includes a trailing one*)
+fun long_mk_prod []        = one
+  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
+
+(*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 
+        [zmult_1, zmult_1_right] 
+        (([th, cancel_th]) MRS trans);
+
+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@zmult_ac))
+  end;
+
+structure EqCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = prove_conv "int_eq_cancel_factor"
+  val mk_bal   = HOLogic.mk_eq
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
+  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
+);
+
+structure DivideCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = prove_conv "int_divide_cancel_factor"
+  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 prep_simproc
+   [("int_eq_cancel_factor",
+     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
+     EqCancelFactor.proc),
+    ("int_divide_cancel_factor", 
+     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
+     DivideCancelFactor.proc)];
+
+end;
+
+Addsimprocs int_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)";
+*)
+