src/HOL/Numeral_Simprocs.thy
changeset 54489 03ff4d1e6784
parent 54249 ce00f2fef556
child 55375 d26d5f988d71
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4    if_False if_True
     1.5    add_0 add_Suc add_numeral_left
     1.6    add_neg_numeral_left mult_numeral_left
     1.7 -  numeral_1_eq_1 [symmetric] Suc_eq_plus1
     1.8 +  numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
     1.9    eq_numeral_iff_iszero not_iszero_Numeral1
    1.10  
    1.11  declare split_div [of _ _ "numeral k", arith_split] for k
    1.12 @@ -85,18 +85,19 @@
    1.13  
    1.14  text {* For @{text cancel_factor} *}
    1.15  
    1.16 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
    1.17 -by auto
    1.18 +lemmas nat_mult_le_cancel_disj = mult_le_cancel1
    1.19  
    1.20 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
    1.21 -by auto
    1.22 +lemmas nat_mult_less_cancel_disj = mult_less_cancel1
    1.23  
    1.24 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
    1.25 -by auto
    1.26 +lemma nat_mult_eq_cancel_disj:
    1.27 +  fixes k m n :: nat
    1.28 +  shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
    1.29 +  by auto
    1.30  
    1.31 -lemma nat_mult_div_cancel_disj[simp]:
    1.32 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    1.33 -by (simp add: nat_mult_div_cancel1)
    1.34 +lemma nat_mult_div_cancel_disj [simp]:
    1.35 +  fixes k m n :: nat
    1.36 +  shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
    1.37 +  by (fact div_mult_mult1_if)
    1.38  
    1.39  ML_file "Tools/numeral_simprocs.ML"
    1.40