src/HOL/NatSimprocs.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23164 69e55066dbca
child 23252 67268bb40b21
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
wenzelm@23164
     1
(*  Title:      HOL/NatSimprocs.thy
wenzelm@23164
     2
    ID:         $Id$
wenzelm@23164
     3
    Copyright   2003 TU Muenchen
wenzelm@23164
     4
*)
wenzelm@23164
     5
wenzelm@23164
     6
header {*Simprocs for the Naturals*}
wenzelm@23164
     7
wenzelm@23164
     8
theory NatSimprocs
wenzelm@23164
     9
imports NatBin
wenzelm@23164
    10
uses "int_factor_simprocs.ML" "nat_simprocs.ML"
wenzelm@23164
    11
begin
wenzelm@23164
    12
wenzelm@23164
    13
setup nat_simprocs_setup
wenzelm@23164
    14
wenzelm@23164
    15
subsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
wenzelm@23164
    16
wenzelm@23164
    17
text{*Where K above is a literal*}
wenzelm@23164
    18
wenzelm@23164
    19
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
wenzelm@23164
    20
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
wenzelm@23164
    21
wenzelm@23164
    22
text {*Now just instantiating @{text n} to @{text "number_of v"} does
wenzelm@23164
    23
  the right simplification, but with some redundant inequality
wenzelm@23164
    24
  tests.*}
wenzelm@23164
    25
lemma neg_number_of_pred_iff_0:
wenzelm@23164
    26
  "neg (number_of (Numeral.pred v)::int) = (number_of v = (0::nat))"
wenzelm@23164
    27
apply (subgoal_tac "neg (number_of (Numeral.pred v)) = (number_of v < Suc 0) ")
wenzelm@23164
    28
apply (simp only: less_Suc_eq_le le_0_eq)
wenzelm@23164
    29
apply (subst less_number_of_Suc, simp)
wenzelm@23164
    30
done
wenzelm@23164
    31
wenzelm@23164
    32
text{*No longer required as a simprule because of the @{text inverse_fold}
wenzelm@23164
    33
   simproc*}
wenzelm@23164
    34
lemma Suc_diff_number_of:
wenzelm@23164
    35
     "neg (number_of (uminus v)::int) ==>  
wenzelm@23164
    36
      Suc m - (number_of v) = m - (number_of (Numeral.pred v))"
wenzelm@23164
    37
apply (subst Suc_diff_eq_diff_pred)
wenzelm@23164
    38
apply simp
wenzelm@23164
    39
apply (simp del: nat_numeral_1_eq_1)
wenzelm@23164
    40
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
wenzelm@23164
    41
                        neg_number_of_pred_iff_0)
wenzelm@23164
    42
done
wenzelm@23164
    43
wenzelm@23164
    44
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
wenzelm@23164
    45
by (simp add: numerals split add: nat_diff_split)
wenzelm@23164
    46
wenzelm@23164
    47
wenzelm@23164
    48
subsection{*For @{term nat_case} and @{term nat_rec}*}
wenzelm@23164
    49
wenzelm@23164
    50
lemma nat_case_number_of [simp]:
wenzelm@23164
    51
     "nat_case a f (number_of v) =  
wenzelm@23164
    52
        (let pv = number_of (Numeral.pred v) in  
wenzelm@23164
    53
         if neg pv then a else f (nat pv))"
wenzelm@23164
    54
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
wenzelm@23164
    55
wenzelm@23164
    56
lemma nat_case_add_eq_if [simp]:
wenzelm@23164
    57
     "nat_case a f ((number_of v) + n) =  
wenzelm@23164
    58
       (let pv = number_of (Numeral.pred v) in  
wenzelm@23164
    59
         if neg pv then nat_case a f n else f (nat pv + n))"
wenzelm@23164
    60
apply (subst add_eq_if)
wenzelm@23164
    61
apply (simp split add: nat.split
wenzelm@23164
    62
            del: nat_numeral_1_eq_1
wenzelm@23164
    63
	    add: numeral_1_eq_Suc_0 [symmetric] Let_def 
wenzelm@23164
    64
                 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
wenzelm@23164
    65
done
wenzelm@23164
    66
wenzelm@23164
    67
lemma nat_rec_number_of [simp]:
wenzelm@23164
    68
     "nat_rec a f (number_of v) =  
wenzelm@23164
    69
        (let pv = number_of (Numeral.pred v) in  
wenzelm@23164
    70
         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
wenzelm@23164
    71
apply (case_tac " (number_of v) ::nat")
wenzelm@23164
    72
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
wenzelm@23164
    73
apply (simp split add: split_if_asm)
wenzelm@23164
    74
done
wenzelm@23164
    75
wenzelm@23164
    76
lemma nat_rec_add_eq_if [simp]:
wenzelm@23164
    77
     "nat_rec a f (number_of v + n) =  
wenzelm@23164
    78
        (let pv = number_of (Numeral.pred v) in  
wenzelm@23164
    79
         if neg pv then nat_rec a f n  
wenzelm@23164
    80
                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
wenzelm@23164
    81
apply (subst add_eq_if)
wenzelm@23164
    82
apply (simp split add: nat.split
wenzelm@23164
    83
            del: nat_numeral_1_eq_1
wenzelm@23164
    84
            add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
wenzelm@23164
    85
                 neg_number_of_pred_iff_0)
wenzelm@23164
    86
done
wenzelm@23164
    87
wenzelm@23164
    88
wenzelm@23164
    89
subsection{*Various Other Lemmas*}
wenzelm@23164
    90
wenzelm@23164
    91
subsubsection{*Evens and Odds, for Mutilated Chess Board*}
wenzelm@23164
    92
wenzelm@23164
    93
text{*Lemmas for specialist use, NOT as default simprules*}
wenzelm@23164
    94
lemma nat_mult_2: "2 * z = (z+z::nat)"
wenzelm@23164
    95
proof -
wenzelm@23164
    96
  have "2*z = (1 + 1)*z" by simp
wenzelm@23164
    97
  also have "... = z+z" by (simp add: left_distrib)
wenzelm@23164
    98
  finally show ?thesis .
wenzelm@23164
    99
qed
wenzelm@23164
   100
wenzelm@23164
   101
lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
wenzelm@23164
   102
by (subst mult_commute, rule nat_mult_2)
wenzelm@23164
   103
wenzelm@23164
   104
text{*Case analysis on @{term "n<2"}*}
wenzelm@23164
   105
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
wenzelm@23164
   106
by arith
wenzelm@23164
   107
wenzelm@23164
   108
lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
wenzelm@23164
   109
by arith
wenzelm@23164
   110
wenzelm@23164
   111
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
wenzelm@23164
   112
by (simp add: nat_mult_2 [symmetric])
wenzelm@23164
   113
wenzelm@23164
   114
lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
wenzelm@23164
   115
apply (subgoal_tac "m mod 2 < 2")
wenzelm@23164
   116
apply (erule less_2_cases [THEN disjE])
wenzelm@23164
   117
apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
wenzelm@23164
   118
done
wenzelm@23164
   119
wenzelm@23164
   120
lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
wenzelm@23164
   121
apply (subgoal_tac "m mod 2 < 2")
wenzelm@23164
   122
apply (force simp del: mod_less_divisor, simp) 
wenzelm@23164
   123
done
wenzelm@23164
   124
wenzelm@23164
   125
subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
wenzelm@23164
   126
wenzelm@23164
   127
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
wenzelm@23164
   128
by simp
wenzelm@23164
   129
wenzelm@23164
   130
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
wenzelm@23164
   131
by simp
wenzelm@23164
   132
wenzelm@23164
   133
text{*Can be used to eliminate long strings of Sucs, but not by default*}
wenzelm@23164
   134
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
wenzelm@23164
   135
by simp
wenzelm@23164
   136
wenzelm@23164
   137
wenzelm@23164
   138
text{*These lemmas collapse some needless occurrences of Suc:
wenzelm@23164
   139
    at least three Sucs, since two and fewer are rewritten back to Suc again!
wenzelm@23164
   140
    We already have some rules to simplify operands smaller than 3.*}
wenzelm@23164
   141
wenzelm@23164
   142
lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
wenzelm@23164
   143
by (simp add: Suc3_eq_add_3)
wenzelm@23164
   144
wenzelm@23164
   145
lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
wenzelm@23164
   146
by (simp add: Suc3_eq_add_3)
wenzelm@23164
   147
wenzelm@23164
   148
lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
wenzelm@23164
   149
by (simp add: Suc3_eq_add_3)
wenzelm@23164
   150
wenzelm@23164
   151
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
wenzelm@23164
   152
by (simp add: Suc3_eq_add_3)
wenzelm@23164
   153
wenzelm@23164
   154
lemmas Suc_div_eq_add3_div_number_of =
wenzelm@23164
   155
    Suc_div_eq_add3_div [of _ "number_of v", standard]
wenzelm@23164
   156
declare Suc_div_eq_add3_div_number_of [simp]
wenzelm@23164
   157
wenzelm@23164
   158
lemmas Suc_mod_eq_add3_mod_number_of =
wenzelm@23164
   159
    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
wenzelm@23164
   160
declare Suc_mod_eq_add3_mod_number_of [simp]
wenzelm@23164
   161
wenzelm@23164
   162
wenzelm@23164
   163
wenzelm@23164
   164
subsection{*Special Simplification for Constants*}
wenzelm@23164
   165
wenzelm@23164
   166
text{*These belong here, late in the development of HOL, to prevent their
wenzelm@23164
   167
interfering with proofs of abstract properties of instances of the function
wenzelm@23164
   168
@{term number_of}*}
wenzelm@23164
   169
wenzelm@23164
   170
text{*These distributive laws move literals inside sums and differences.*}
wenzelm@23164
   171
lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
wenzelm@23164
   172
declare left_distrib_number_of [simp]
wenzelm@23164
   173
wenzelm@23164
   174
lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
wenzelm@23164
   175
declare right_distrib_number_of [simp]
wenzelm@23164
   176
wenzelm@23164
   177
wenzelm@23164
   178
lemmas left_diff_distrib_number_of =
wenzelm@23164
   179
    left_diff_distrib [of _ _ "number_of v", standard]
wenzelm@23164
   180
declare left_diff_distrib_number_of [simp]
wenzelm@23164
   181
wenzelm@23164
   182
lemmas right_diff_distrib_number_of =
wenzelm@23164
   183
    right_diff_distrib [of "number_of v", standard]
wenzelm@23164
   184
declare right_diff_distrib_number_of [simp]
wenzelm@23164
   185
wenzelm@23164
   186
wenzelm@23164
   187
text{*These are actually for fields, like real: but where else to put them?*}
wenzelm@23164
   188
lemmas zero_less_divide_iff_number_of =
wenzelm@23164
   189
    zero_less_divide_iff [of "number_of w", standard]
wenzelm@23164
   190
declare zero_less_divide_iff_number_of [simp]
wenzelm@23164
   191
wenzelm@23164
   192
lemmas divide_less_0_iff_number_of =
wenzelm@23164
   193
    divide_less_0_iff [of "number_of w", standard]
wenzelm@23164
   194
declare divide_less_0_iff_number_of [simp]
wenzelm@23164
   195
wenzelm@23164
   196
lemmas zero_le_divide_iff_number_of =
wenzelm@23164
   197
    zero_le_divide_iff [of "number_of w", standard]
wenzelm@23164
   198
declare zero_le_divide_iff_number_of [simp]
wenzelm@23164
   199
wenzelm@23164
   200
lemmas divide_le_0_iff_number_of =
wenzelm@23164
   201
    divide_le_0_iff [of "number_of w", standard]
wenzelm@23164
   202
declare divide_le_0_iff_number_of [simp]
wenzelm@23164
   203
wenzelm@23164
   204
wenzelm@23164
   205
(****
wenzelm@23164
   206
IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
wenzelm@23164
   207
then these special-case declarations may be useful.
wenzelm@23164
   208
wenzelm@23164
   209
text{*These simprules move numerals into numerators and denominators.*}
wenzelm@23164
   210
lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
wenzelm@23164
   211
by (simp add: times_divide_eq)
wenzelm@23164
   212
wenzelm@23164
   213
lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
wenzelm@23164
   214
by (simp add: times_divide_eq)
wenzelm@23164
   215
wenzelm@23164
   216
lemmas times_divide_eq_right_number_of =
wenzelm@23164
   217
    times_divide_eq_right [of "number_of w", standard]
wenzelm@23164
   218
declare times_divide_eq_right_number_of [simp]
wenzelm@23164
   219
wenzelm@23164
   220
lemmas times_divide_eq_right_number_of =
wenzelm@23164
   221
    times_divide_eq_right [of _ _ "number_of w", standard]
wenzelm@23164
   222
declare times_divide_eq_right_number_of [simp]
wenzelm@23164
   223
wenzelm@23164
   224
lemmas times_divide_eq_left_number_of =
wenzelm@23164
   225
    times_divide_eq_left [of _ "number_of w", standard]
wenzelm@23164
   226
declare times_divide_eq_left_number_of [simp]
wenzelm@23164
   227
wenzelm@23164
   228
lemmas times_divide_eq_left_number_of =
wenzelm@23164
   229
    times_divide_eq_left [of _ _ "number_of w", standard]
wenzelm@23164
   230
declare times_divide_eq_left_number_of [simp]
wenzelm@23164
   231
wenzelm@23164
   232
****)
wenzelm@23164
   233
wenzelm@23164
   234
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
wenzelm@23164
   235
  strange, but then other simprocs simplify the quotient.*}
wenzelm@23164
   236
wenzelm@23164
   237
lemmas inverse_eq_divide_number_of =
wenzelm@23164
   238
    inverse_eq_divide [of "number_of w", standard]
wenzelm@23164
   239
declare inverse_eq_divide_number_of [simp]
wenzelm@23164
   240
wenzelm@23164
   241
wenzelm@23164
   242
subsubsection{*These laws simplify inequalities, moving unary minus from a term
wenzelm@23164
   243
into the literal.*}
wenzelm@23164
   244
lemmas less_minus_iff_number_of =
wenzelm@23164
   245
    less_minus_iff [of "number_of v", standard]
wenzelm@23164
   246
declare less_minus_iff_number_of [simp]
wenzelm@23164
   247
wenzelm@23164
   248
lemmas le_minus_iff_number_of =
wenzelm@23164
   249
    le_minus_iff [of "number_of v", standard]
wenzelm@23164
   250
declare le_minus_iff_number_of [simp]
wenzelm@23164
   251
wenzelm@23164
   252
lemmas equation_minus_iff_number_of =
wenzelm@23164
   253
    equation_minus_iff [of "number_of v", standard]
wenzelm@23164
   254
declare equation_minus_iff_number_of [simp]
wenzelm@23164
   255
wenzelm@23164
   256
wenzelm@23164
   257
lemmas minus_less_iff_number_of =
wenzelm@23164
   258
    minus_less_iff [of _ "number_of v", standard]
wenzelm@23164
   259
declare minus_less_iff_number_of [simp]
wenzelm@23164
   260
wenzelm@23164
   261
lemmas minus_le_iff_number_of =
wenzelm@23164
   262
    minus_le_iff [of _ "number_of v", standard]
wenzelm@23164
   263
declare minus_le_iff_number_of [simp]
wenzelm@23164
   264
wenzelm@23164
   265
lemmas minus_equation_iff_number_of =
wenzelm@23164
   266
    minus_equation_iff [of _ "number_of v", standard]
wenzelm@23164
   267
declare minus_equation_iff_number_of [simp]
wenzelm@23164
   268
wenzelm@23164
   269
wenzelm@23164
   270
subsubsection{*To Simplify Inequalities Where One Side is the Constant 1*}
wenzelm@23164
   271
wenzelm@23164
   272
lemma less_minus_iff_1 [simp]: 
wenzelm@23164
   273
  fixes b::"'b::{ordered_idom,number_ring}" 
wenzelm@23164
   274
  shows "(1 < - b) = (b < -1)"
wenzelm@23164
   275
by auto
wenzelm@23164
   276
wenzelm@23164
   277
lemma le_minus_iff_1 [simp]: 
wenzelm@23164
   278
  fixes b::"'b::{ordered_idom,number_ring}" 
wenzelm@23164
   279
  shows "(1 \<le> - b) = (b \<le> -1)"
wenzelm@23164
   280
by auto
wenzelm@23164
   281
wenzelm@23164
   282
lemma equation_minus_iff_1 [simp]: 
wenzelm@23164
   283
  fixes b::"'b::number_ring" 
wenzelm@23164
   284
  shows "(1 = - b) = (b = -1)"
wenzelm@23164
   285
by (subst equation_minus_iff, auto) 
wenzelm@23164
   286
wenzelm@23164
   287
lemma minus_less_iff_1 [simp]: 
wenzelm@23164
   288
  fixes a::"'b::{ordered_idom,number_ring}" 
wenzelm@23164
   289
  shows "(- a < 1) = (-1 < a)"
wenzelm@23164
   290
by auto
wenzelm@23164
   291
wenzelm@23164
   292
lemma minus_le_iff_1 [simp]: 
wenzelm@23164
   293
  fixes a::"'b::{ordered_idom,number_ring}" 
wenzelm@23164
   294
  shows "(- a \<le> 1) = (-1 \<le> a)"
wenzelm@23164
   295
by auto
wenzelm@23164
   296
wenzelm@23164
   297
lemma minus_equation_iff_1 [simp]: 
wenzelm@23164
   298
  fixes a::"'b::number_ring" 
wenzelm@23164
   299
  shows "(- a = 1) = (a = -1)"
wenzelm@23164
   300
by (subst minus_equation_iff, auto) 
wenzelm@23164
   301
wenzelm@23164
   302
wenzelm@23164
   303
subsubsection {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
wenzelm@23164
   304
wenzelm@23164
   305
lemmas mult_less_cancel_left_number_of =
wenzelm@23164
   306
    mult_less_cancel_left [of "number_of v", standard]
wenzelm@23164
   307
declare mult_less_cancel_left_number_of [simp]
wenzelm@23164
   308
wenzelm@23164
   309
lemmas mult_less_cancel_right_number_of =
wenzelm@23164
   310
    mult_less_cancel_right [of _ "number_of v", standard]
wenzelm@23164
   311
declare mult_less_cancel_right_number_of [simp]
wenzelm@23164
   312
wenzelm@23164
   313
lemmas mult_le_cancel_left_number_of =
wenzelm@23164
   314
    mult_le_cancel_left [of "number_of v", standard]
wenzelm@23164
   315
declare mult_le_cancel_left_number_of [simp]
wenzelm@23164
   316
wenzelm@23164
   317
lemmas mult_le_cancel_right_number_of =
wenzelm@23164
   318
    mult_le_cancel_right [of _ "number_of v", standard]
wenzelm@23164
   319
declare mult_le_cancel_right_number_of [simp]
wenzelm@23164
   320
wenzelm@23164
   321
wenzelm@23164
   322
subsubsection {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
wenzelm@23164
   323
wenzelm@23164
   324
lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
wenzelm@23164
   325
declare le_divide_eq_number_of [simp]
wenzelm@23164
   326
wenzelm@23164
   327
lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard]
wenzelm@23164
   328
declare divide_le_eq_number_of [simp]
wenzelm@23164
   329
wenzelm@23164
   330
lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard]
wenzelm@23164
   331
declare less_divide_eq_number_of [simp]
wenzelm@23164
   332
wenzelm@23164
   333
lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard]
wenzelm@23164
   334
declare divide_less_eq_number_of [simp]
wenzelm@23164
   335
wenzelm@23164
   336
lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard]
wenzelm@23164
   337
declare eq_divide_eq_number_of [simp]
wenzelm@23164
   338
wenzelm@23164
   339
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard]
wenzelm@23164
   340
declare divide_eq_eq_number_of [simp]
wenzelm@23164
   341
wenzelm@23164
   342
wenzelm@23164
   343
wenzelm@23164
   344
subsection{*Optional Simplification Rules Involving Constants*}
wenzelm@23164
   345
wenzelm@23164
   346
text{*Simplify quotients that are compared with a literal constant.*}
wenzelm@23164
   347
wenzelm@23164
   348
lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
wenzelm@23164
   349
lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
wenzelm@23164
   350
lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
wenzelm@23164
   351
lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
wenzelm@23164
   352
lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
wenzelm@23164
   353
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
wenzelm@23164
   354
wenzelm@23164
   355
wenzelm@23164
   356
text{*Not good as automatic simprules because they cause case splits.*}
wenzelm@23164
   357
lemmas divide_const_simps =
wenzelm@23164
   358
  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
wenzelm@23164
   359
  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
wenzelm@23164
   360
  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
wenzelm@23164
   361
wenzelm@23164
   362
subsubsection{*Division By @{text "-1"}*}
wenzelm@23164
   363
wenzelm@23164
   364
lemma divide_minus1 [simp]:
wenzelm@23164
   365
     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" 
wenzelm@23164
   366
by simp
wenzelm@23164
   367
wenzelm@23164
   368
lemma minus1_divide [simp]:
wenzelm@23164
   369
     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
wenzelm@23164
   370
by (simp add: divide_inverse inverse_minus_eq)
wenzelm@23164
   371
wenzelm@23164
   372
lemma half_gt_zero_iff:
wenzelm@23164
   373
     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
wenzelm@23164
   374
by auto
wenzelm@23164
   375
wenzelm@23164
   376
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
wenzelm@23164
   377
declare half_gt_zero [simp]
wenzelm@23164
   378
wenzelm@23164
   379
(* The following lemma should appear in Divides.thy, but there the proof
wenzelm@23164
   380
   doesn't work. *)
wenzelm@23164
   381
wenzelm@23164
   382
lemma nat_dvd_not_less:
wenzelm@23164
   383
  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
wenzelm@23164
   384
  by (unfold dvd_def) auto
wenzelm@23164
   385
wenzelm@23164
   386
ML {*
wenzelm@23164
   387
val divide_minus1 = @{thm divide_minus1};
wenzelm@23164
   388
val minus1_divide = @{thm minus1_divide};
wenzelm@23164
   389
*}
wenzelm@23164
   390
wenzelm@23164
   391
end