generalized sort constraint of lemmas
authorhaftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 530647e3f39bc41df
parent 53063 8f7ac535892f
child 53065 de1816a7293e
generalized sort constraint of lemmas
src/HOL/Num.thy
     1.1 --- a/src/HOL/Num.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Num.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -529,6 +529,12 @@
     1.4  lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
     1.5    by (rule numeral_mult [symmetric])
     1.6  
     1.7 +lemma mult_2: "2 * z = z + z"
     1.8 +  unfolding one_add_one [symmetric] distrib_right by simp
     1.9 +
    1.10 +lemma mult_2_right: "z * 2 = z + z"
    1.11 +  unfolding one_add_one [symmetric] distrib_left by simp
    1.12 +
    1.13  end
    1.14  
    1.15  subsubsection {*
    1.16 @@ -544,12 +550,6 @@
    1.17    by (induct n,
    1.18      simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
    1.19  
    1.20 -lemma mult_2: "2 * z = z + z"
    1.21 -  unfolding one_add_one [symmetric] distrib_right by simp
    1.22 -
    1.23 -lemma mult_2_right: "z * 2 = z + z"
    1.24 -  unfolding one_add_one [symmetric] distrib_left by simp
    1.25 -
    1.26  end
    1.27  
    1.28  lemma nat_of_num_numeral [code_abbrev]: