src/HOL/Numeral_Simprocs.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 45607 16b4f5774621 child 47108 2a1953f0d20d permissions -rw-r--r--
```     1 (* Author: Various *)
```
```     2
```
```     3 header {* Combination and Cancellation Simprocs for Numeral Expressions *}
```
```     4
```
```     5 theory Numeral_Simprocs
```
```     6 imports Divides
```
```     7 uses
```
```     8   "~~/src/Provers/Arith/assoc_fold.ML"
```
```     9   "~~/src/Provers/Arith/cancel_numerals.ML"
```
```    10   "~~/src/Provers/Arith/combine_numerals.ML"
```
```    11   "~~/src/Provers/Arith/cancel_numeral_factor.ML"
```
```    12   "~~/src/Provers/Arith/extract_common_term.ML"
```
```    13   ("Tools/numeral_simprocs.ML")
```
```    14   ("Tools/nat_numeral_simprocs.ML")
```
```    15 begin
```
```    16
```
```    17 declare split_div [of _ _ "number_of k", arith_split] for k
```
```    18 declare split_mod [of _ _ "number_of k", arith_split] for k
```
```    19
```
```    20 text {* For @{text combine_numerals} *}
```
```    21
```
```    22 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
```
```    23 by (simp add: add_mult_distrib)
```
```    24
```
```    25 text {* For @{text cancel_numerals} *}
```
```    26
```
```    27 lemma nat_diff_add_eq1:
```
```    28      "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
```
```    29 by (simp split add: nat_diff_split add: add_mult_distrib)
```
```    30
```
```    31 lemma nat_diff_add_eq2:
```
```    32      "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
```
```    33 by (simp split add: nat_diff_split add: add_mult_distrib)
```
```    34
```
```    35 lemma nat_eq_add_iff1:
```
```    36      "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
```
```    37 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    38
```
```    39 lemma nat_eq_add_iff2:
```
```    40      "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
```
```    41 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    42
```
```    43 lemma nat_less_add_iff1:
```
```    44      "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
```
```    45 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    46
```
```    47 lemma nat_less_add_iff2:
```
```    48      "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
```
```    49 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    50
```
```    51 lemma nat_le_add_iff1:
```
```    52      "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
```
```    53 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    54
```
```    55 lemma nat_le_add_iff2:
```
```    56      "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
```
```    57 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    58
```
```    59 text {* For @{text cancel_numeral_factors} *}
```
```    60
```
```    61 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
```
```    62 by auto
```
```    63
```
```    64 lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
```
```    65 by auto
```
```    66
```
```    67 lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
```
```    68 by auto
```
```    69
```
```    70 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
```
```    71 by auto
```
```    72
```
```    73 lemma nat_mult_dvd_cancel_disj[simp]:
```
```    74   "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
```
```    75 by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
```
```    76
```
```    77 lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
```
```    78 by(auto)
```
```    79
```
```    80 text {* For @{text cancel_factor} *}
```
```    81
```
```    82 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
```
```    83 by auto
```
```    84
```
```    85 lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
```
```    86 by auto
```
```    87
```
```    88 lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
```
```    89 by auto
```
```    90
```
```    91 lemma nat_mult_div_cancel_disj[simp]:
```
```    92      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
```
```    93 by (simp add: nat_mult_div_cancel1)
```
```    94
```
```    95 use "Tools/numeral_simprocs.ML"
```
```    96
```
```    97 simproc_setup semiring_assoc_fold
```
```    98   ("(a::'a::comm_semiring_1_cancel) * b") =
```
```    99   {* fn phi => Numeral_Simprocs.assoc_fold *}
```
```   100
```
```   101 simproc_setup int_combine_numerals
```
```   102   ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
```
```   103   {* fn phi => Numeral_Simprocs.combine_numerals *}
```
```   104
```
```   105 simproc_setup field_combine_numerals
```
```   106   ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
```
```   107   |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
```
```   108   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
```
```   109
```
```   110 simproc_setup inteq_cancel_numerals
```
```   111   ("(l::'a::number_ring) + m = n"
```
```   112   |"(l::'a::number_ring) = m + n"
```
```   113   |"(l::'a::number_ring) - m = n"
```
```   114   |"(l::'a::number_ring) = m - n"
```
```   115   |"(l::'a::number_ring) * m = n"
```
```   116   |"(l::'a::number_ring) = m * n"
```
```   117   |"- (l::'a::number_ring) = m"
```
```   118   |"(l::'a::number_ring) = - m") =
```
```   119   {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
```
```   120
```
```   121 simproc_setup intless_cancel_numerals
```
```   122   ("(l::'a::{linordered_idom,number_ring}) + m < n"
```
```   123   |"(l::'a::{linordered_idom,number_ring}) < m + n"
```
```   124   |"(l::'a::{linordered_idom,number_ring}) - m < n"
```
```   125   |"(l::'a::{linordered_idom,number_ring}) < m - n"
```
```   126   |"(l::'a::{linordered_idom,number_ring}) * m < n"
```
```   127   |"(l::'a::{linordered_idom,number_ring}) < m * n"
```
```   128   |"- (l::'a::{linordered_idom,number_ring}) < m"
```
```   129   |"(l::'a::{linordered_idom,number_ring}) < - m") =
```
```   130   {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
```
```   131
```
```   132 simproc_setup intle_cancel_numerals
```
```   133   ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
```
```   134   |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
```
```   135   |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
```
```   136   |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
```
```   137   |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
```
```   138   |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
```
```   139   |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
```
```   140   |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
```
```   141   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
```
```   142
```
```   143 simproc_setup ring_eq_cancel_numeral_factor
```
```   144   ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
```
```   145   |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
```
```   146   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
```
```   147
```
```   148 simproc_setup ring_less_cancel_numeral_factor
```
```   149   ("(l::'a::{linordered_idom,number_ring}) * m < n"
```
```   150   |"(l::'a::{linordered_idom,number_ring}) < m * n") =
```
```   151   {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
```
```   152
```
```   153 simproc_setup ring_le_cancel_numeral_factor
```
```   154   ("(l::'a::{linordered_idom,number_ring}) * m <= n"
```
```   155   |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
```
```   156   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
```
```   157
```
```   158 simproc_setup int_div_cancel_numeral_factors
```
```   159   ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
```
```   160   |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
```
```   161   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
```
```   162
```
```   163 simproc_setup divide_cancel_numeral_factor
```
```   164   ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
```
```   165   |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
```
```   166   |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
```
```   167   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
```
```   168
```
```   169 simproc_setup ring_eq_cancel_factor
```
```   170   ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
```
```   171   {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
```
```   172
```
```   173 simproc_setup linordered_ring_le_cancel_factor
```
```   174   ("(l::'a::linordered_idom) * m <= n"
```
```   175   |"(l::'a::linordered_idom) <= m * n") =
```
```   176   {* fn phi => Numeral_Simprocs.le_cancel_factor *}
```
```   177
```
```   178 simproc_setup linordered_ring_less_cancel_factor
```
```   179   ("(l::'a::linordered_idom) * m < n"
```
```   180   |"(l::'a::linordered_idom) < m * n") =
```
```   181   {* fn phi => Numeral_Simprocs.less_cancel_factor *}
```
```   182
```
```   183 simproc_setup int_div_cancel_factor
```
```   184   ("((l::'a::semiring_div) * m) div n"
```
```   185   |"(l::'a::semiring_div) div (m * n)") =
```
```   186   {* fn phi => Numeral_Simprocs.div_cancel_factor *}
```
```   187
```
```   188 simproc_setup int_mod_cancel_factor
```
```   189   ("((l::'a::semiring_div) * m) mod n"
```
```   190   |"(l::'a::semiring_div) mod (m * n)") =
```
```   191   {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
```
```   192
```
```   193 simproc_setup dvd_cancel_factor
```
```   194   ("((l::'a::idom) * m) dvd n"
```
```   195   |"(l::'a::idom) dvd (m * n)") =
```
```   196   {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
```
```   197
```
```   198 simproc_setup divide_cancel_factor
```
```   199   ("((l::'a::field_inverse_zero) * m) / n"
```
```   200   |"(l::'a::field_inverse_zero) / (m * n)") =
```
```   201   {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
```
```   202
```
```   203 use "Tools/nat_numeral_simprocs.ML"
```
```   204
```
```   205 simproc_setup nat_combine_numerals
```
```   206   ("(i::nat) + j" | "Suc (i + j)") =
```
```   207   {* fn phi => Nat_Numeral_Simprocs.combine_numerals *}
```
```   208
```
```   209 simproc_setup nateq_cancel_numerals
```
```   210   ("(l::nat) + m = n" | "(l::nat) = m + n" |
```
```   211    "(l::nat) * m = n" | "(l::nat) = m * n" |
```
```   212    "Suc m = n" | "m = Suc n") =
```
```   213   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *}
```
```   214
```
```   215 simproc_setup natless_cancel_numerals
```
```   216   ("(l::nat) + m < n" | "(l::nat) < m + n" |
```
```   217    "(l::nat) * m < n" | "(l::nat) < m * n" |
```
```   218    "Suc m < n" | "m < Suc n") =
```
```   219   {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *}
```
```   220
```
```   221 simproc_setup natle_cancel_numerals
```
```   222   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
```
```   223    "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
```
```   224    "Suc m \<le> n" | "m \<le> Suc n") =
```
```   225   {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *}
```
```   226
```
```   227 simproc_setup natdiff_cancel_numerals
```
```   228   ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
```
```   229    "(l::nat) * m - n" | "(l::nat) - m * n" |
```
```   230    "Suc m - n" | "m - Suc n") =
```
```   231   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
```
```   232
```
```   233 simproc_setup nat_eq_cancel_numeral_factor
```
```   234   ("(l::nat) * m = n" | "(l::nat) = m * n") =
```
```   235   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
```
```   236
```
```   237 simproc_setup nat_less_cancel_numeral_factor
```
```   238   ("(l::nat) * m < n" | "(l::nat) < m * n") =
```
```   239   {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
```
```   240
```
```   241 simproc_setup nat_le_cancel_numeral_factor
```
```   242   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
```
```   243   {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
```
```   244
```
```   245 simproc_setup nat_div_cancel_numeral_factor
```
```   246   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
```
```   247   {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
```
```   248
```
```   249 simproc_setup nat_dvd_cancel_numeral_factor
```
```   250   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
```
```   251   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
```
```   252
```
```   253 simproc_setup nat_eq_cancel_factor
```
```   254   ("(l::nat) * m = n" | "(l::nat) = m * n") =
```
```   255   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
```
```   256
```
```   257 simproc_setup nat_less_cancel_factor
```
```   258   ("(l::nat) * m < n" | "(l::nat) < m * n") =
```
```   259   {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *}
```
```   260
```
```   261 simproc_setup nat_le_cancel_factor
```
```   262   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
```
```   263   {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
```
```   264
```
```   265 simproc_setup nat_div_cancel_factor
```
```   266   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
```
```   267   {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
```
```   268
```
```   269 simproc_setup nat_dvd_cancel_factor
```
```   270   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
```
```   271   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
```
```   272
```
```   273 declaration {*
```
```   274   K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
```
```   275   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
```
```   276      @{thm nat_0}, @{thm nat_1},
```
```   277      @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
```
```   278      @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
```
```   279      @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
```
```   280      @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
```
```   281      @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
```
```   282      @{thm mult_Suc}, @{thm mult_Suc_right},
```
```   283      @{thm add_Suc}, @{thm add_Suc_right},
```
```   284      @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
```
```   285      @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
```
```   286      @{thm if_True}, @{thm if_False}])
```
```   287   #> Lin_Arith.add_simprocs
```
```   288       [@{simproc semiring_assoc_fold},
```
```   289        @{simproc int_combine_numerals},
```
```   290        @{simproc inteq_cancel_numerals},
```
```   291        @{simproc intless_cancel_numerals},
```
```   292        @{simproc intle_cancel_numerals}]
```
```   293   #> Lin_Arith.add_simprocs
```
```   294       [@{simproc nat_combine_numerals},
```
```   295        @{simproc nateq_cancel_numerals},
```
```   296        @{simproc natless_cancel_numerals},
```
```   297        @{simproc natle_cancel_numerals},
```
```   298        @{simproc natdiff_cancel_numerals}])
```
```   299 *}
```
```   300
```
```   301 end
```