src/HOL/Numeral_Simprocs.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 33366 b0096ac3b731 child 37886 2f9d3fc1a8ac permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
```     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", standard, arith_split]
```
```    18 declare split_mod [of _ _ "number_of k", standard, arith_split]
```
```    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
```
```    96 use "Tools/numeral_simprocs.ML"
```
```    97
```
```    98 use "Tools/nat_numeral_simprocs.ML"
```
```    99
```
```   100 declaration {*
```
```   101   K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
```
```   102   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
```
```   103      @{thm nat_0}, @{thm nat_1},
```
```   104      @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
```
```   105      @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
```
```   106      @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
```
```   107      @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
```
```   108      @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
```
```   109      @{thm mult_Suc}, @{thm mult_Suc_right},
```
```   110      @{thm add_Suc}, @{thm add_Suc_right},
```
```   111      @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
```
```   112      @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
```
```   113      @{thm if_True}, @{thm if_False}])
```
```   114   #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
```
```   115       :: Numeral_Simprocs.combine_numerals
```
```   116       :: Numeral_Simprocs.cancel_numerals)
```
```   117   #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
```
```   118 *}
```
```   119
```
`   120 end`