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