wneuper/isa: src/HOL/Integ/int_factor_simprocs.ML@3d51fbf81c17

     1 (*  Title:      HOL/int_factor_simprocs.ML

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   2000  University of Cambridge

     6 Factor cancellation simprocs for the integers.

     8 This file can't be combined with int_arith1,2 because it requires IntDiv.thy.

     9 *)

    11 (** Factor cancellation theorems for "int" **)

    13 Goal "!!k::int. (k*m <= k*n) = ((Numeral0 < k --> m<=n) & (k < Numeral0 --> n<=m))";

    14 by (stac zmult_zle_cancel1 1);

    15 by Auto_tac;

    16 qed "int_mult_le_cancel1";

    18 Goal "!!k::int. (k*m < k*n) = ((Numeral0 < k & m<n) | (k < Numeral0 & n<m))";

    19 by (stac zmult_zless_cancel1 1);

    20 by Auto_tac;

    21 qed "int_mult_less_cancel1";

    23 Goal "!!k::int. (k*m = k*n) = (k = Numeral0 | m=n)";

    24 by Auto_tac;

    25 qed "int_mult_eq_cancel1";

    27 Goal "!!k::int. k~=Numeral0 ==> (k*m) div (k*n) = (m div n)";

    28 by (stac zdiv_zmult_zmult1 1);

    29 by Auto_tac;

    30 qed "int_mult_div_cancel1";

    32 (*For ExtractCommonTermFun, cancelling common factors*)

    33 Goal "(k*m) div (k*n) = (if k = (Numeral0::int) then Numeral0 else m div n)";

    34 by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);

    35 qed "int_mult_div_cancel_disj";

    37 local

    38   open Int_Numeral_Simprocs

    39 in

    41 structure CancelNumeralFactorCommon =

    42   struct

    43   val mk_coeff		= mk_coeff

    44   val dest_coeff	= dest_coeff 1

    45   val trans_tac         = trans_tac

    46   val norm_tac =

    47      ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))

    48      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))

    49      THEN ALLGOALS

    50             (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac))

    51   val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))

    52   val simplify_meta_eq  = simplify_meta_eq mult_1s

    53   end

    55 structure DivCancelNumeralFactor = CancelNumeralFactorFun

    56  (open CancelNumeralFactorCommon

    57   val prove_conv = prove_conv "intdiv_cancel_numeral_factor"

    58   val mk_bal   = HOLogic.mk_binop "Divides.op div"

    59   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT

    60   val cancel = int_mult_div_cancel1 RS trans

    61   val neg_exchanges = false

    62 )

    64 structure EqCancelNumeralFactor = CancelNumeralFactorFun

    65  (open CancelNumeralFactorCommon

    66   val prove_conv = prove_conv "inteq_cancel_numeral_factor"

    67   val mk_bal   = HOLogic.mk_eq

    68   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT

    69   val cancel = int_mult_eq_cancel1 RS trans

    70   val neg_exchanges = false

    71 )

    73 structure LessCancelNumeralFactor = CancelNumeralFactorFun

    74  (open CancelNumeralFactorCommon

    75   val prove_conv = prove_conv "intless_cancel_numeral_factor"

    76   val mk_bal   = HOLogic.mk_binrel "op <"

    77   val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT

    78   val cancel = int_mult_less_cancel1 RS trans

    79   val neg_exchanges = true

    80 )

    82 structure LeCancelNumeralFactor = CancelNumeralFactorFun

    83  (open CancelNumeralFactorCommon

    84   val prove_conv = prove_conv "intle_cancel_numeral_factor"

    85   val mk_bal   = HOLogic.mk_binrel "op <="

    86   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT

    87   val cancel = int_mult_le_cancel1 RS trans

    88   val neg_exchanges = true

    89 )

    91 val int_cancel_numeral_factors =

    92   map prep_simproc

    93    [("inteq_cancel_numeral_factors",

    94      prep_pats ["(l::int) * m = n", "(l::int) = m * n"],

    95      EqCancelNumeralFactor.proc),

    96     ("intless_cancel_numeral_factors",

    97      prep_pats ["(l::int) * m < n", "(l::int) < m * n"],

    98      LessCancelNumeralFactor.proc),

    99     ("intle_cancel_numeral_factors",

   100      prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"],

   101      LeCancelNumeralFactor.proc),

   102     ("intdiv_cancel_numeral_factors",

   103      prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"],

   104      DivCancelNumeralFactor.proc)];

   106 end;

   108 Addsimprocs int_cancel_numeral_factors;

   111 (*examples:

   112 print_depth 22;

   113 set timing;

   114 set trace_simp;

   115 fun test s = (Goal s; by (Simp_tac 1));

   117 test "# 9*x = # 12 * (y::int)";

   118 test "(# 9*x) div (# 12 * (y::int)) = z";

   119 test "# 9*x < # 12 * (y::int)";

   120 test "# 9*x <= # 12 * (y::int)";

   122 test "# -99*x = # 132 * (y::int)";

   123 test "(# -99*x) div (# 132 * (y::int)) = z";

   124 test "# -99*x < # 132 * (y::int)";

   125 test "# -99*x <= # 132 * (y::int)";

   127 test "# 999*x = # -396 * (y::int)";

   128 test "(# 999*x) div (# -396 * (y::int)) = z";

   129 test "# 999*x < # -396 * (y::int)";

   130 test "# 999*x <= # -396 * (y::int)";

   132 test "# -99*x = # -81 * (y::int)";

   133 test "(# -99*x) div (# -81 * (y::int)) = z";

   134 test "# -99*x <= # -81 * (y::int)";

   135 test "# -99*x < # -81 * (y::int)";

   137 test "# -2 * x = # -1 * (y::int)";

   138 test "# -2 * x = -(y::int)";

   139 test "(# -2 * x) div (# -1 * (y::int)) = z";

   140 test "# -2 * x < -(y::int)";

   141 test "# -2 * x <= # -1 * (y::int)";

   142 test "-x < # -23 * (y::int)";

   143 test "-x <= # -23 * (y::int)";

   144 *)

   147 (** Declarations for ExtractCommonTerm **)

   149 local

   150   open Int_Numeral_Simprocs

   151 in

   154 (*this version ALWAYS includes a trailing one*)

   155 fun long_mk_prod []        = one

   156   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);

   158 (*Find first term that matches u*)

   159 fun find_first past u []         = raise TERM("find_first", [])

   160   | find_first past u (t::terms) =

   161 	if u aconv t then (rev past @ terms)

   162         else find_first (t::past) u terms

   163 	handle TERM _ => find_first (t::past) u terms;

   165 (*Final simplification: cancel + and *  *)

   166 fun cancel_simplify_meta_eq cancel_th th =

   167     Int_Numeral_Simprocs.simplify_meta_eq

   168         [zmult_1, zmult_1_right]

   169         (([th, cancel_th]) MRS trans);

   171 structure CancelFactorCommon =

   172   struct

   173   val mk_sum    	= long_mk_prod

   174   val dest_sum		= dest_prod

   175   val mk_coeff		= mk_coeff

   176   val dest_coeff	= dest_coeff

   177   val find_first	= find_first []

   178   val trans_tac         = trans_tac

   179   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))

   180   end;

   182 structure EqCancelFactor = ExtractCommonTermFun

   183  (open CancelFactorCommon

   184   val prove_conv = prove_conv "int_eq_cancel_factor"

   185   val mk_bal   = HOLogic.mk_eq

   186   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT

   187   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1

   188 );

   190 structure DivideCancelFactor = ExtractCommonTermFun

   191  (open CancelFactorCommon

   192   val prove_conv = prove_conv "int_divide_cancel_factor"

   193   val mk_bal   = HOLogic.mk_binop "Divides.op div"

   194   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT

   195   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj

   196 );

   198 val int_cancel_factor =

   199   map prep_simproc

   200    [("int_eq_cancel_factor",

   201      prep_pats ["(l::int) * m = n", "(l::int) = m * n"],

   202      EqCancelFactor.proc),

   203     ("int_divide_cancel_factor",

   204      prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"],

   205      DivideCancelFactor.proc)];

   207 end;

   209 Addsimprocs int_cancel_factor;

   212 (*examples:

   213 print_depth 22;

   214 set timing;

   215 set trace_simp;

   216 fun test s = (Goal s; by (Asm_simp_tac 1));

   218 test "x*k = k*(y::int)";

   219 test "k = k*(y::int)";

   220 test "a*(b*c) = (b::int)";

   221 test "a*(b*c) = d*(b::int)*(x*a)";

   223 test "(x*k) div (k*(y::int)) = (uu::int)";

   224 test "(k) div (k*(y::int)) = (uu::int)";

   225 test "(a*(b*c)) div ((b::int)) = (uu::int)";

   226 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";

   227 *)

author	wenzelm
	Fri, 05 Oct 2001 21:52:39 +0200
changeset 11701	3d51fbf81c17
parent 10713	69c9fc1d11f2
child 11704	3c50a2cd6f00
permissions	-rw-r--r--