33366

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)) = (((ij)*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  ((ji)*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) = ((ij)*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 = (ji)*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) = ((ij)*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 < (ji)*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) = ((ij)*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 <= (ji)*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 
use "Tools/nat_numeral_simprocs.ML"


98 


99 
declaration {*


100 
K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])


101 
#> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},


102 
@{thm nat_0}, @{thm nat_1},


103 
@{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},


104 
@{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},


105 
@{thm le_Suc_number_of}, @{thm le_number_of_Suc},


106 
@{thm less_Suc_number_of}, @{thm less_number_of_Suc},


107 
@{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},


108 
@{thm mult_Suc}, @{thm mult_Suc_right},


109 
@{thm add_Suc}, @{thm add_Suc_right},


110 
@{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},


111 
@{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},


112 
@{thm if_True}, @{thm if_False}])


113 
#> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc


114 
:: Numeral_Simprocs.combine_numerals


115 
:: Numeral_Simprocs.cancel_numerals)


116 
#> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))


117 
*}


118 

37886

119 
end
