src/HOL/Tools/int_factor_simprocs.ML
 changeset 30649 57753e0ec1d4 parent 30518 07b45c1aa788 child 30685 dd5fe091ff04
```     1.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Sat Mar 21 12:37:13 2009 +0100
1.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 19:36:04 2009 +0100
1.3 @@ -218,9 +218,30 @@
1.4  val simplify_one = Arith_Data.simplify_meta_eq
1.5    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
1.6
1.7 -fun cancel_simplify_meta_eq cancel_th ss th =
1.8 +fun cancel_simplify_meta_eq ss cancel_th th =
1.9      simplify_one ss (([th, cancel_th]) MRS trans);
1.10
1.11 +local
1.12 +  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
1.13 +  fun Eq_True_elim Eq =
1.14 +    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
1.15 +in
1.16 +fun sign_conv pos_th neg_th ss t =
1.17 +  let val T = fastype_of t;
1.18 +      val zero = Const(@{const_name HOL.zero}, T);
1.19 +      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
1.20 +      val pos = less \$ zero \$ t and neg = less \$ t \$ zero
1.21 +      fun prove p =
1.22 +        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
1.23 +        handle THM _ => NONE
1.24 +    in case prove pos of
1.25 +         SOME th => SOME(th RS pos_th)
1.26 +       | NONE => (case prove neg of
1.27 +                    SOME th => SOME(th RS neg_th)
1.28 +                  | NONE => NONE)
1.29 +    end;
1.30 +end
1.31 +
1.32  structure CancelFactorCommon =
1.33    struct
1.34    val mk_sum            = long_mk_prod
1.35 @@ -231,6 +252,7 @@
1.36    val trans_tac         = K Arith_Data.trans_tac
1.37    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
1.38    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
1.39 +  val simplify_meta_eq  = cancel_simplify_meta_eq
1.40    end;
1.41
1.42  (*mult_cancel_left requires a ring with no zero divisors.*)
1.43 @@ -239,7 +261,27 @@
1.44    val prove_conv = Arith_Data.prove_conv
1.45    val mk_bal   = HOLogic.mk_eq
1.46    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
1.47 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
1.48 +  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
1.49 +);
1.50 +
1.51 +(*for ordered rings*)
1.52 +structure LeCancelFactor = ExtractCommonTermFun
1.53 + (open CancelFactorCommon
1.54 +  val prove_conv = Arith_Data.prove_conv
1.55 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
1.56 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
1.57 +  val simp_conv = sign_conv
1.58 +    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
1.59 +);
1.60 +
1.61 +(*for ordered rings*)
1.62 +structure LessCancelFactor = ExtractCommonTermFun
1.63 + (open CancelFactorCommon
1.64 +  val prove_conv = Arith_Data.prove_conv
1.65 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
1.66 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
1.67 +  val simp_conv = sign_conv
1.68 +    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
1.69  );
1.70
1.71  (*zdiv_zmult_zmult1_if is for integer division (div).*)
1.72 @@ -248,7 +290,7 @@
1.73    val prove_conv = Arith_Data.prove_conv
1.74    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
1.75    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
1.76 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
1.77 +  val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
1.78  );
1.79
1.80  structure IntModCancelFactor = ExtractCommonTermFun
1.81 @@ -256,7 +298,7 @@
1.82    val prove_conv = Arith_Data.prove_conv
1.83    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
1.84    val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
1.85 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
1.86 +  val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
1.87  );
1.88
1.89  structure IntDvdCancelFactor = ExtractCommonTermFun
1.90 @@ -264,7 +306,7 @@
1.91    val prove_conv = Arith_Data.prove_conv
1.92    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
1.93    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
1.94 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
1.95 +  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
1.96  );
1.97
1.98  (*Version for all fields, including unordered ones (type complex).*)
1.99 @@ -273,7 +315,7 @@
1.100    val prove_conv = Arith_Data.prove_conv
1.101    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
1.102    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
1.103 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
1.104 +  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
1.105  );
1.106
1.107  val cancel_factors =
1.108 @@ -281,7 +323,15 @@
1.109     [("ring_eq_cancel_factor",
1.110       ["(l::'a::{idom}) * m = n",
1.111        "(l::'a::{idom}) = m * n"],
1.112 -    K EqCancelFactor.proc),
1.113 +     K EqCancelFactor.proc),
1.114 +    ("ordered_ring_le_cancel_factor",
1.115 +     ["(l::'a::ordered_ring) * m <= n",
1.116 +      "(l::'a::ordered_ring) <= m * n"],
1.117 +     K LeCancelFactor.proc),
1.118 +    ("ordered_ring_less_cancel_factor",
1.119 +     ["(l::'a::ordered_ring) * m < n",
1.120 +      "(l::'a::ordered_ring) < m * n"],
1.121 +     K LessCancelFactor.proc),
1.122      ("int_div_cancel_factor",
1.123       ["((l::int) * m) div n", "(l::int) div (m * n)"],
1.124       K IntDivCancelFactor.proc),
```