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