src/HOL/Numeral_Simprocs.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 47159 978c00c20a59 child 48891 c0eafbd55de3 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
```     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 lemmas semiring_norm =
```
```    18   Let_def arith_simps nat_arith rel_simps
```
```    19   if_False if_True
```
```    20   add_0 add_Suc add_numeral_left
```
```    21   add_neg_numeral_left mult_numeral_left
```
```    22   numeral_1_eq_1 [symmetric] Suc_eq_plus1
```
```    23   eq_numeral_iff_iszero not_iszero_Numeral1
```
```    24
```
```    25 declare split_div [of _ _ "numeral k", arith_split] for k
```
```    26 declare split_mod [of _ _ "numeral k", arith_split] for k
```
```    27
```
```    28 text {* For @{text combine_numerals} *}
```
```    29
```
```    30 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
```
```    31 by (simp add: add_mult_distrib)
```
```    32
```
```    33 text {* For @{text cancel_numerals} *}
```
```    34
```
```    35 lemma nat_diff_add_eq1:
```
```    36      "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
```
```    37 by (simp split add: nat_diff_split add: add_mult_distrib)
```
```    38
```
```    39 lemma nat_diff_add_eq2:
```
```    40      "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
```
```    41 by (simp split add: nat_diff_split add: add_mult_distrib)
```
```    42
```
```    43 lemma nat_eq_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_eq_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_less_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_less_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 lemma nat_le_add_iff1:
```
```    60      "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
```
```    61 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    62
```
```    63 lemma nat_le_add_iff2:
```
```    64      "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
```
```    65 by (auto split add: nat_diff_split simp add: add_mult_distrib)
```
```    66
```
```    67 text {* For @{text cancel_numeral_factors} *}
```
```    68
```
```    69 lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
```
```    70 by auto
```
```    71
```
```    72 lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
```
```    73 by auto
```
```    74
```
```    75 lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
```
```    76 by auto
```
```    77
```
```    78 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
```
```    79 by auto
```
```    80
```
```    81 lemma nat_mult_dvd_cancel_disj[simp]:
```
```    82   "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
```
```    83 by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)
```
```    84
```
```    85 lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
```
```    86 by(auto)
```
```    87
```
```    88 text {* For @{text cancel_factor} *}
```
```    89
```
```    90 lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
```
```    91 by auto
```
```    92
```
```    93 lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
```
```    94 by auto
```
```    95
```
```    96 lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
```
```    97 by auto
```
```    98
```
```    99 lemma nat_mult_div_cancel_disj[simp]:
```
```   100      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
```
```   101 by (simp add: nat_mult_div_cancel1)
```
```   102
```
```   103 use "Tools/numeral_simprocs.ML"
```
```   104
```
```   105 simproc_setup semiring_assoc_fold
```
```   106   ("(a::'a::comm_semiring_1_cancel) * b") =
```
```   107   {* fn phi => Numeral_Simprocs.assoc_fold *}
```
```   108
```
```   109 (* TODO: see whether the type class can be generalized further *)
```
```   110 simproc_setup int_combine_numerals
```
```   111   ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
```
```   112   {* fn phi => Numeral_Simprocs.combine_numerals *}
```
```   113
```
```   114 simproc_setup field_combine_numerals
```
```   115   ("(i::'a::{field_inverse_zero,ring_char_0}) + j"
```
```   116   |"(i::'a::{field_inverse_zero,ring_char_0}) - j") =
```
```   117   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
```
```   118
```
```   119 simproc_setup inteq_cancel_numerals
```
```   120   ("(l::'a::comm_ring_1) + m = n"
```
```   121   |"(l::'a::comm_ring_1) = m + n"
```
```   122   |"(l::'a::comm_ring_1) - m = n"
```
```   123   |"(l::'a::comm_ring_1) = m - n"
```
```   124   |"(l::'a::comm_ring_1) * m = n"
```
```   125   |"(l::'a::comm_ring_1) = m * n"
```
```   126   |"- (l::'a::comm_ring_1) = m"
```
```   127   |"(l::'a::comm_ring_1) = - m") =
```
```   128   {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
```
```   129
```
```   130 simproc_setup intless_cancel_numerals
```
```   131   ("(l::'a::linordered_idom) + m < n"
```
```   132   |"(l::'a::linordered_idom) < m + n"
```
```   133   |"(l::'a::linordered_idom) - m < n"
```
```   134   |"(l::'a::linordered_idom) < m - n"
```
```   135   |"(l::'a::linordered_idom) * m < n"
```
```   136   |"(l::'a::linordered_idom) < m * n"
```
```   137   |"- (l::'a::linordered_idom) < m"
```
```   138   |"(l::'a::linordered_idom) < - m") =
```
```   139   {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
```
```   140
```
```   141 simproc_setup intle_cancel_numerals
```
```   142   ("(l::'a::linordered_idom) + m \<le> n"
```
```   143   |"(l::'a::linordered_idom) \<le> m + n"
```
```   144   |"(l::'a::linordered_idom) - m \<le> n"
```
```   145   |"(l::'a::linordered_idom) \<le> m - n"
```
```   146   |"(l::'a::linordered_idom) * m \<le> n"
```
```   147   |"(l::'a::linordered_idom) \<le> m * n"
```
```   148   |"- (l::'a::linordered_idom) \<le> m"
```
```   149   |"(l::'a::linordered_idom) \<le> - m") =
```
```   150   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
```
```   151
```
```   152 simproc_setup ring_eq_cancel_numeral_factor
```
```   153   ("(l::'a::{idom,ring_char_0}) * m = n"
```
```   154   |"(l::'a::{idom,ring_char_0}) = m * n") =
```
```   155   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
```
```   156
```
```   157 simproc_setup ring_less_cancel_numeral_factor
```
```   158   ("(l::'a::linordered_idom) * m < n"
```
```   159   |"(l::'a::linordered_idom) < m * n") =
```
```   160   {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
```
```   161
```
```   162 simproc_setup ring_le_cancel_numeral_factor
```
```   163   ("(l::'a::linordered_idom) * m <= n"
```
```   164   |"(l::'a::linordered_idom) <= m * n") =
```
```   165   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
```
```   166
```
```   167 (* TODO: remove comm_ring_1 constraint if possible *)
```
```   168 simproc_setup int_div_cancel_numeral_factors
```
```   169   ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
```
```   170   |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
```
```   171   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
```
```   172
```
```   173 simproc_setup divide_cancel_numeral_factor
```
```   174   ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n"
```
```   175   |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)"
```
```   176   |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") =
```
```   177   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
```
```   178
```
```   179 simproc_setup ring_eq_cancel_factor
```
```   180   ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
```
```   181   {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
```
```   182
```
```   183 simproc_setup linordered_ring_le_cancel_factor
```
```   184   ("(l::'a::linordered_idom) * m <= n"
```
```   185   |"(l::'a::linordered_idom) <= m * n") =
```
```   186   {* fn phi => Numeral_Simprocs.le_cancel_factor *}
```
```   187
```
```   188 simproc_setup linordered_ring_less_cancel_factor
```
```   189   ("(l::'a::linordered_idom) * m < n"
```
```   190   |"(l::'a::linordered_idom) < m * n") =
```
```   191   {* fn phi => Numeral_Simprocs.less_cancel_factor *}
```
```   192
```
```   193 simproc_setup int_div_cancel_factor
```
```   194   ("((l::'a::semiring_div) * m) div n"
```
```   195   |"(l::'a::semiring_div) div (m * n)") =
```
```   196   {* fn phi => Numeral_Simprocs.div_cancel_factor *}
```
```   197
```
```   198 simproc_setup int_mod_cancel_factor
```
```   199   ("((l::'a::semiring_div) * m) mod n"
```
```   200   |"(l::'a::semiring_div) mod (m * n)") =
```
```   201   {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
```
```   202
```
```   203 simproc_setup dvd_cancel_factor
```
```   204   ("((l::'a::idom) * m) dvd n"
```
```   205   |"(l::'a::idom) dvd (m * n)") =
```
```   206   {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
```
```   207
```
```   208 simproc_setup divide_cancel_factor
```
```   209   ("((l::'a::field_inverse_zero) * m) / n"
```
```   210   |"(l::'a::field_inverse_zero) / (m * n)") =
```
```   211   {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
```
```   212
```
```   213 use "Tools/nat_numeral_simprocs.ML"
```
```   214
```
```   215 simproc_setup nat_combine_numerals
```
```   216   ("(i::nat) + j" | "Suc (i + j)") =
```
```   217   {* fn phi => Nat_Numeral_Simprocs.combine_numerals *}
```
```   218
```
```   219 simproc_setup nateq_cancel_numerals
```
```   220   ("(l::nat) + m = n" | "(l::nat) = m + n" |
```
```   221    "(l::nat) * m = n" | "(l::nat) = m * n" |
```
```   222    "Suc m = n" | "m = Suc n") =
```
```   223   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *}
```
```   224
```
```   225 simproc_setup natless_cancel_numerals
```
```   226   ("(l::nat) + m < n" | "(l::nat) < m + n" |
```
```   227    "(l::nat) * m < n" | "(l::nat) < m * n" |
```
```   228    "Suc m < n" | "m < Suc n") =
```
```   229   {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *}
```
```   230
```
```   231 simproc_setup natle_cancel_numerals
```
```   232   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
```
```   233    "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
```
```   234    "Suc m \<le> n" | "m \<le> Suc n") =
```
```   235   {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *}
```
```   236
```
```   237 simproc_setup natdiff_cancel_numerals
```
```   238   ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
```
```   239    "(l::nat) * m - n" | "(l::nat) - m * n" |
```
```   240    "Suc m - n" | "m - Suc n") =
```
```   241   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
```
```   242
```
```   243 simproc_setup nat_eq_cancel_numeral_factor
```
```   244   ("(l::nat) * m = n" | "(l::nat) = m * n") =
```
```   245   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
```
```   246
```
```   247 simproc_setup nat_less_cancel_numeral_factor
```
```   248   ("(l::nat) * m < n" | "(l::nat) < m * n") =
```
```   249   {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
```
```   250
```
```   251 simproc_setup nat_le_cancel_numeral_factor
```
```   252   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
```
```   253   {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
```
```   254
```
```   255 simproc_setup nat_div_cancel_numeral_factor
```
```   256   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
```
```   257   {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
```
```   258
```
```   259 simproc_setup nat_dvd_cancel_numeral_factor
```
```   260   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
```
```   261   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
```
```   262
```
```   263 simproc_setup nat_eq_cancel_factor
```
```   264   ("(l::nat) * m = n" | "(l::nat) = m * n") =
```
```   265   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
```
```   266
```
```   267 simproc_setup nat_less_cancel_factor
```
```   268   ("(l::nat) * m < n" | "(l::nat) < m * n") =
```
```   269   {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *}
```
```   270
```
```   271 simproc_setup nat_le_cancel_factor
```
```   272   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
```
```   273   {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
```
```   274
```
```   275 simproc_setup nat_div_cancel_factor
```
```   276   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
```
```   277   {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
```
```   278
```
```   279 simproc_setup nat_dvd_cancel_factor
```
```   280   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
```
```   281   {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
```
```   282
```
```   283 (* FIXME: duplicate rule warnings for:
```
```   284   ring_distribs
```
```   285   numeral_plus_numeral numeral_times_numeral
```
```   286   numeral_eq_iff numeral_less_iff numeral_le_iff
```
```   287   numeral_neq_zero zero_neq_numeral zero_less_numeral
```
```   288   if_True if_False *)
```
```   289 declaration {*
```
```   290   K (Lin_Arith.add_simps ([@{thm Suc_numeral}, @{thm int_numeral}])
```
```   291   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1},
```
```   292      @{thm nat_0}, @{thm nat_1},
```
```   293      @{thm numeral_plus_numeral}, @{thm diff_nat_numeral}, @{thm numeral_times_numeral},
```
```   294      @{thm numeral_eq_iff}, @{thm numeral_less_iff}, @{thm numeral_le_iff},
```
```   295      @{thm le_Suc_numeral}, @{thm le_numeral_Suc},
```
```   296      @{thm less_Suc_numeral}, @{thm less_numeral_Suc},
```
```   297      @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc},
```
```   298      @{thm mult_Suc}, @{thm mult_Suc_right},
```
```   299      @{thm add_Suc}, @{thm add_Suc_right},
```
```   300      @{thm numeral_neq_zero}, @{thm zero_neq_numeral}, @{thm zero_less_numeral},
```
```   301      @{thm of_int_numeral}, @{thm of_nat_numeral}, @{thm nat_numeral},
```
```   302      @{thm if_True}, @{thm if_False}])
```
```   303   #> Lin_Arith.add_simprocs
```
```   304       [@{simproc semiring_assoc_fold},
```
```   305        @{simproc int_combine_numerals},
```
```   306        @{simproc inteq_cancel_numerals},
```
```   307        @{simproc intless_cancel_numerals},
```
```   308        @{simproc intle_cancel_numerals}]
```
```   309   #> Lin_Arith.add_simprocs
```
```   310       [@{simproc nat_combine_numerals},
```
```   311        @{simproc nateq_cancel_numerals},
```
```   312        @{simproc natless_cancel_numerals},
```
```   313        @{simproc natle_cancel_numerals},
```
```   314        @{simproc natdiff_cancel_numerals}])
```
```   315 *}
```
```   316
```
```   317 end
```