src/HOL/Numeral_Simprocs.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 37886 2f9d3fc1a8ac child 45284 ae78a4ffa81d permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
 haftmann@33366 ` 1` ```(* Author: Various *) ``` haftmann@33366 ` 2` haftmann@33366 ` 3` ```header {* Combination and Cancellation Simprocs for Numeral Expressions *} ``` haftmann@33366 ` 4` haftmann@33366 ` 5` ```theory Numeral_Simprocs ``` haftmann@33366 ` 6` ```imports Divides ``` haftmann@33366 ` 7` ```uses ``` haftmann@33366 ` 8` ``` "~~/src/Provers/Arith/assoc_fold.ML" ``` haftmann@33366 ` 9` ``` "~~/src/Provers/Arith/cancel_numerals.ML" ``` haftmann@33366 ` 10` ``` "~~/src/Provers/Arith/combine_numerals.ML" ``` haftmann@33366 ` 11` ``` "~~/src/Provers/Arith/cancel_numeral_factor.ML" ``` haftmann@33366 ` 12` ``` "~~/src/Provers/Arith/extract_common_term.ML" ``` haftmann@33366 ` 13` ``` ("Tools/numeral_simprocs.ML") ``` haftmann@33366 ` 14` ``` ("Tools/nat_numeral_simprocs.ML") ``` haftmann@33366 ` 15` ```begin ``` haftmann@33366 ` 16` haftmann@33366 ` 17` ```declare split_div [of _ _ "number_of k", standard, arith_split] ``` haftmann@33366 ` 18` ```declare split_mod [of _ _ "number_of k", standard, arith_split] ``` haftmann@33366 ` 19` haftmann@33366 ` 20` ```text {* For @{text combine_numerals} *} ``` haftmann@33366 ` 21` haftmann@33366 ` 22` ```lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" ``` haftmann@33366 ` 23` ```by (simp add: add_mult_distrib) ``` haftmann@33366 ` 24` haftmann@33366 ` 25` ```text {* For @{text cancel_numerals} *} ``` haftmann@33366 ` 26` haftmann@33366 ` 27` ```lemma nat_diff_add_eq1: ``` haftmann@33366 ` 28` ``` "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" ``` haftmann@33366 ` 29` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 30` haftmann@33366 ` 31` ```lemma nat_diff_add_eq2: ``` haftmann@33366 ` 32` ``` "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" ``` haftmann@33366 ` 33` ```by (simp split add: nat_diff_split add: add_mult_distrib) ``` haftmann@33366 ` 34` haftmann@33366 ` 35` ```lemma nat_eq_add_iff1: ``` haftmann@33366 ` 36` ``` "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)" ``` haftmann@33366 ` 37` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 38` haftmann@33366 ` 39` ```lemma nat_eq_add_iff2: ``` haftmann@33366 ` 40` ``` "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)" ``` haftmann@33366 ` 41` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 42` haftmann@33366 ` 43` ```lemma nat_less_add_iff1: ``` haftmann@33366 ` 44` ``` "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)" ``` haftmann@33366 ` 45` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 46` haftmann@33366 ` 47` ```lemma nat_less_add_iff2: ``` haftmann@33366 ` 48` ``` "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)" ``` haftmann@33366 ` 49` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 50` haftmann@33366 ` 51` ```lemma nat_le_add_iff1: ``` haftmann@33366 ` 52` ``` "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" ``` haftmann@33366 ` 53` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 54` haftmann@33366 ` 55` ```lemma nat_le_add_iff2: ``` haftmann@33366 ` 56` ``` "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" ``` haftmann@33366 ` 57` ```by (auto split add: nat_diff_split simp add: add_mult_distrib) ``` haftmann@33366 ` 58` haftmann@33366 ` 59` ```text {* For @{text cancel_numeral_factors} *} ``` haftmann@33366 ` 60` haftmann@33366 ` 61` ```lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" ``` haftmann@33366 ` 62` ```by auto ``` haftmann@33366 ` 63` haftmann@33366 ` 64` ```lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m (k*m = k*n) = (m=n)" ``` haftmann@33366 ` 68` ```by auto ``` haftmann@33366 ` 69` haftmann@33366 ` 70` ```lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" ``` haftmann@33366 ` 71` ```by auto ``` haftmann@33366 ` 72` haftmann@33366 ` 73` ```lemma nat_mult_dvd_cancel_disj[simp]: ``` haftmann@33366 ` 74` ``` "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" ``` haftmann@33366 ` 75` ```by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric]) ``` haftmann@33366 ` 76` haftmann@33366 ` 77` ```lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" ``` haftmann@33366 ` 78` ```by(auto) ``` haftmann@33366 ` 79` haftmann@33366 ` 80` ```text {* For @{text cancel_factor} *} ``` haftmann@33366 ` 81` haftmann@33366 ` 82` ```lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)" ``` haftmann@33366 ` 83` ```by auto ``` haftmann@33366 ` 84` haftmann@33366 ` 85` ```lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, ``` haftmann@33366 ` 102` ``` @{thm nat_0}, @{thm nat_1}, ``` haftmann@33366 ` 103` ``` @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, ``` haftmann@33366 ` 104` ``` @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, ``` haftmann@33366 ` 105` ``` @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, ``` haftmann@33366 ` 106` ``` @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, ``` haftmann@33366 ` 107` ``` @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, ``` haftmann@33366 ` 108` ``` @{thm mult_Suc}, @{thm mult_Suc_right}, ``` haftmann@33366 ` 109` ``` @{thm add_Suc}, @{thm add_Suc_right}, ``` haftmann@33366 ` 110` ``` @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, ``` haftmann@33366 ` 111` ``` @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, ``` haftmann@33366 ` 112` ``` @{thm if_True}, @{thm if_False}]) ``` haftmann@33366 ` 113` ``` #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc ``` haftmann@33366 ` 114` ``` :: Numeral_Simprocs.combine_numerals ``` haftmann@33366 ` 115` ``` :: Numeral_Simprocs.cancel_numerals) ``` haftmann@33366 ` 116` ``` #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals)) ``` haftmann@33366 ` 117` ```*} ``` haftmann@33366 ` 118` haftmann@37886 ` 119` ```end ```