src/HOL/Integ/NatSimprocs.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15228 4d332d10fa3d
permissions -rw-r--r--
import -> imports
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
nipkow@15131
    10
files "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
wenzelm@14577
   177
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
wenzelm@14577
   178
  strange, but then other simprocs simplify the quotient.*}
wenzelm@14577
   179
paulson@14288
   180
declare inverse_eq_divide [of "number_of w", standard, simp]
paulson@14288
   181
paulson@14288
   182
text{*These laws simplify inequalities, moving unary minus from a term
paulson@14288
   183
into the literal.*}
paulson@14288
   184
declare less_minus_iff [of "number_of v", standard, simp]
paulson@14288
   185
declare le_minus_iff [of "number_of v", standard, simp]
paulson@14288
   186
declare equation_minus_iff [of "number_of v", standard, simp]
paulson@14288
   187
paulson@14288
   188
declare minus_less_iff [of _ "number_of v", standard, simp]
paulson@14288
   189
declare minus_le_iff [of _ "number_of v", standard, simp]
paulson@14288
   190
declare minus_equation_iff [of _ "number_of v", standard, simp]
paulson@14288
   191
paulson@14288
   192
text{*These simplify inequalities where one side is the constant 1.*}
paulson@14288
   193
declare less_minus_iff [of 1, simplified, simp]
paulson@14288
   194
declare le_minus_iff [of 1, simplified, simp]
paulson@14288
   195
declare equation_minus_iff [of 1, simplified, simp]
paulson@14288
   196
paulson@14288
   197
declare minus_less_iff [of _ 1, simplified, simp]
paulson@14288
   198
declare minus_le_iff [of _ 1, simplified, simp]
paulson@14288
   199
declare minus_equation_iff [of _ 1, simplified, simp]
paulson@14288
   200
wenzelm@14577
   201
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
paulson@14288
   202
paulson@14288
   203
declare mult_less_cancel_left [of "number_of v", standard, simp]
paulson@14288
   204
declare mult_less_cancel_right [of _ "number_of v", standard, simp]
paulson@14288
   205
declare mult_le_cancel_left [of "number_of v", standard, simp]
paulson@14288
   206
declare mult_le_cancel_right [of _ "number_of v", standard, simp]
paulson@14288
   207
wenzelm@14577
   208
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
paulson@14288
   209
paulson@14288
   210
declare le_divide_eq [of _ _ "number_of w", standard, simp]
paulson@14288
   211
declare divide_le_eq [of _ "number_of w", standard, simp]
paulson@14288
   212
declare less_divide_eq [of _ _ "number_of w", standard, simp]
paulson@14288
   213
declare divide_less_eq [of _ "number_of w", standard, simp]
paulson@14288
   214
declare eq_divide_eq [of _ _ "number_of w", standard, simp]
paulson@14288
   215
declare divide_eq_eq [of _ "number_of w", standard, simp]
paulson@14288
   216
paulson@14288
   217
paulson@14387
   218
subsubsection{*Division By @{term "-1"}*}
paulson@14387
   219
paulson@14387
   220
lemma divide_minus1 [simp]:
paulson@14387
   221
     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" 
paulson@14387
   222
by simp
paulson@14387
   223
paulson@14387
   224
lemma minus1_divide [simp]:
paulson@14387
   225
     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
paulson@14430
   226
by (simp add: divide_inverse inverse_minus_eq)
paulson@14387
   227
paulson@14475
   228
lemma half_gt_zero_iff:
paulson@14475
   229
     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
paulson@14475
   230
by auto
paulson@14475
   231
paulson@14475
   232
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
paulson@14475
   233
paulson@14436
   234
paulson@14436
   235
paulson@14436
   236
paulson@14387
   237
ML
paulson@14387
   238
{*
paulson@14387
   239
val divide_minus1 = thm "divide_minus1";
paulson@14387
   240
val minus1_divide = thm "minus1_divide";
paulson@14387
   241
*}
paulson@14387
   242
paulson@8858
   243
end