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