src/HOL/Int.thy
changeset 61738 c4f6031f1310
parent 61694 6571c78c9667
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Int.thy	Sun Nov 22 23:19:43 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Nov 23 16:57:54 2015 +0000
     1.3 @@ -1263,27 +1263,29 @@
     1.4  
     1.5  text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
     1.6  
     1.7 -lemmas le_divide_eq_numeral1 [simp] =
     1.8 +named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
     1.9 +
    1.10 +lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
    1.11    pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
    1.12    neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    1.13  
    1.14 -lemmas divide_le_eq_numeral1 [simp] =
    1.15 +lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
    1.16    pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
    1.17    neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    1.18  
    1.19 -lemmas less_divide_eq_numeral1 [simp] =
    1.20 +lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
    1.21    pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
    1.22    neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    1.23  
    1.24 -lemmas divide_less_eq_numeral1 [simp] =
    1.25 +lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
    1.26    pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
    1.27    neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    1.28  
    1.29 -lemmas eq_divide_eq_numeral1 [simp] =
    1.30 +lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
    1.31    eq_divide_eq [of _ _ "numeral w"]
    1.32    eq_divide_eq [of _ _ "- numeral w"] for w
    1.33  
    1.34 -lemmas divide_eq_eq_numeral1 [simp] =
    1.35 +lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
    1.36    divide_eq_eq [of _ "numeral w"]
    1.37    divide_eq_eq [of _ "- numeral w"] for w
    1.38  
    1.39 @@ -1292,36 +1294,33 @@
    1.40  
    1.41  text\<open>Simplify quotients that are compared with a literal constant.\<close>
    1.42  
    1.43 -lemmas le_divide_eq_numeral =
    1.44 +lemmas le_divide_eq_numeral [divide_const_simps] =
    1.45    le_divide_eq [of "numeral w"]
    1.46    le_divide_eq [of "- numeral w"] for w
    1.47  
    1.48 -lemmas divide_le_eq_numeral =
    1.49 +lemmas divide_le_eq_numeral [divide_const_simps] =
    1.50    divide_le_eq [of _ _ "numeral w"]
    1.51    divide_le_eq [of _ _ "- numeral w"] for w
    1.52  
    1.53 -lemmas less_divide_eq_numeral =
    1.54 +lemmas less_divide_eq_numeral [divide_const_simps] =
    1.55    less_divide_eq [of "numeral w"]
    1.56    less_divide_eq [of "- numeral w"] for w
    1.57  
    1.58 -lemmas divide_less_eq_numeral =
    1.59 +lemmas divide_less_eq_numeral [divide_const_simps] =
    1.60    divide_less_eq [of _ _ "numeral w"]
    1.61    divide_less_eq [of _ _ "- numeral w"] for w
    1.62  
    1.63 -lemmas eq_divide_eq_numeral =
    1.64 +lemmas eq_divide_eq_numeral [divide_const_simps] =
    1.65    eq_divide_eq [of "numeral w"]
    1.66    eq_divide_eq [of "- numeral w"] for w
    1.67  
    1.68 -lemmas divide_eq_eq_numeral =
    1.69 +lemmas divide_eq_eq_numeral [divide_const_simps] =
    1.70    divide_eq_eq [of _ _ "numeral w"]
    1.71    divide_eq_eq [of _ _ "- numeral w"] for w
    1.72  
    1.73  
    1.74  text\<open>Not good as automatic simprules because they cause case splits.\<close>
    1.75 -lemmas divide_const_simps =
    1.76 -  le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
    1.77 -  divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
    1.78 -  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
    1.79 +lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 
    1.80  
    1.81  
    1.82  subsection \<open>The divides relation\<close>