src/HOL/Int.thy
changeset 54249 ce00f2fef556
parent 54230 b1d955791529
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Int.thy	Mon Nov 04 18:08:47 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Nov 04 20:10:06 2013 +0100
     1.3 @@ -424,6 +424,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma diff_nat_numeral [simp]: 
     1.8 +  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
     1.9 +  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.10 +
    1.11 +
    1.12  text {* For termination proofs: *}
    1.13  lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
    1.14  
    1.15 @@ -747,14 +752,11 @@
    1.16  
    1.17  subsection {* Setting up simplification procedures *}
    1.18  
    1.19 +lemmas of_int_simps =
    1.20 +  of_int_0 of_int_1 of_int_add of_int_mult
    1.21 +
    1.22  lemmas int_arith_rules =
    1.23 -  neg_le_iff_le numeral_One
    1.24 -  minus_zero left_minus right_minus
    1.25 -  mult_zero_left mult_zero_right mult_1_left mult_1_right
    1.26 -  mult_minus_left mult_minus_right
    1.27 -  minus_add_distrib minus_minus mult_assoc
    1.28 -  of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    1.29 -  of_int_0 of_int_1 of_int_add of_int_mult
    1.30 +  numeral_One more_arith_simps of_nat_simps of_int_simps
    1.31  
    1.32  ML_file "Tools/int_arith.ML"
    1.33  declaration {* K Int_Arith.setup *}
    1.34 @@ -875,16 +877,10 @@
    1.35                if d < 0 then 0 else nat d)"
    1.36  by (simp add: Let_def nat_diff_distrib [symmetric])
    1.37  
    1.38 -lemma diff_nat_numeral [simp]: 
    1.39 -  "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    1.40 -  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.41 -
    1.42  lemma nat_numeral_diff_1 [simp]:
    1.43    "numeral v - (1::nat) = nat (numeral v - 1)"
    1.44    using diff_nat_numeral [of v Num.One] by simp
    1.45  
    1.46 -lemmas nat_arith = diff_nat_numeral
    1.47 -
    1.48  
    1.49  subsection "Induction principles for int"
    1.50