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