inserting the simproc int_cancel_factor
authorpaulson
Tue Dec 19 15:17:21 2000 +0100 (2000-12-19)
changeset 10703ba98f00cec4f
parent 10702 9e6898befad4
child 10704 c1643c077df4
inserting the simproc int_cancel_factor
src/HOL/Integ/int_factor_simprocs.ML
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 19 15:16:21 2000 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Dec 19 15:17:21 2000 +0100
     1.3 @@ -29,6 +29,11 @@
     1.4  by Auto_tac;  
     1.5  qed "int_mult_div_cancel1";
     1.6  
     1.7 +(*For ExtractCommonTermFun, cancelling common factors*)
     1.8 +Goal "(k*m) div (k*n) = (if k = (#0::int) then #0 else m div n)";
     1.9 +by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); 
    1.10 +qed "int_mult_div_cancel_disj";
    1.11 +
    1.12  local
    1.13    open Int_Numeral_Simprocs
    1.14  in
    1.15 @@ -137,3 +142,86 @@
    1.16  test "-x <= #-23 * (y::int)";
    1.17  *)
    1.18  
    1.19 +
    1.20 +(** Declarations for ExtractCommonTerm **)
    1.21 +
    1.22 +local
    1.23 +  open Int_Numeral_Simprocs
    1.24 +in
    1.25 +
    1.26 +
    1.27 +(*this version ALWAYS includes a trailing one*)
    1.28 +fun long_mk_prod []        = one
    1.29 +  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
    1.30 +
    1.31 +(*Find first term that matches u*)
    1.32 +fun find_first past u []         = raise TERM("find_first", []) 
    1.33 +  | find_first past u (t::terms) =
    1.34 +	if u aconv t then (rev past @ terms)
    1.35 +        else find_first (t::past) u terms
    1.36 +	handle TERM _ => find_first (t::past) u terms;
    1.37 +
    1.38 +(*Final simplification: cancel + and *  *)
    1.39 +fun cancel_simplify_meta_eq cancel_th th = 
    1.40 +    Int_Numeral_Simprocs.simplify_meta_eq 
    1.41 +        [zmult_1, zmult_1_right] 
    1.42 +        (([th, cancel_th]) MRS trans);
    1.43 +
    1.44 +structure CancelFactorCommon =
    1.45 +  struct
    1.46 +  val mk_sum    	= long_mk_prod
    1.47 +  val dest_sum		= dest_prod
    1.48 +  val mk_coeff		= mk_coeff
    1.49 +  val dest_coeff	= dest_coeff
    1.50 +  val find_first	= find_first []
    1.51 +  val trans_tac         = trans_tac
    1.52 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
    1.53 +  end;
    1.54 +
    1.55 +structure EqCancelFactor = ExtractCommonTermFun
    1.56 + (open CancelFactorCommon
    1.57 +  val prove_conv = prove_conv "int_eq_cancel_factor"
    1.58 +  val mk_bal   = HOLogic.mk_eq
    1.59 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.60 +  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
    1.61 +);
    1.62 +
    1.63 +structure DivideCancelFactor = ExtractCommonTermFun
    1.64 + (open CancelFactorCommon
    1.65 +  val prove_conv = prove_conv "int_divide_cancel_factor"
    1.66 +  val mk_bal   = HOLogic.mk_binop "Divides.op div"
    1.67 +  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    1.68 +  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
    1.69 +);
    1.70 +
    1.71 +val int_cancel_factor = 
    1.72 +  map prep_simproc
    1.73 +   [("int_eq_cancel_factor",
    1.74 +     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    1.75 +     EqCancelFactor.proc),
    1.76 +    ("int_divide_cancel_factor", 
    1.77 +     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
    1.78 +     DivideCancelFactor.proc)];
    1.79 +
    1.80 +end;
    1.81 +
    1.82 +Addsimprocs int_cancel_factor;
    1.83 +
    1.84 +
    1.85 +(*examples:
    1.86 +print_depth 22;
    1.87 +set timing;
    1.88 +set trace_simp;
    1.89 +fun test s = (Goal s; by (Asm_simp_tac 1)); 
    1.90 +
    1.91 +test "x*k = k*(y::int)";
    1.92 +test "k = k*(y::int)"; 
    1.93 +test "a*(b*c) = (b::int)";
    1.94 +test "a*(b*c) = d*(b::int)*(x*a)";
    1.95 +
    1.96 +test "(x*k) div (k*(y::int)) = (uu::int)";
    1.97 +test "(k) div (k*(y::int)) = (uu::int)"; 
    1.98 +test "(a*(b*c)) div ((b::int)) = (uu::int)";
    1.99 +test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   1.100 +*)
   1.101 +