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),