src/HOL/Num.thy
changeset 47191 ebd8c46d156b
parent 47126 e980b14c347d
child 47192 0c0501cb6da6
     1.1 --- a/src/HOL/Num.thy	Thu Mar 29 08:59:56 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Thu Mar 29 11:47:30 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Binary Numerals *}
     1.5  
     1.6  theory Num
     1.7 -imports Datatype Power
     1.8 +imports Datatype
     1.9  begin
    1.10  
    1.11  subsection {* The @{text num} type *}
    1.12 @@ -221,7 +221,7 @@
    1.13  primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where
    1.14    "pow x One = x" |
    1.15    "pow x (Bit0 y) = sqr (pow x y)" |
    1.16 -  "pow x (Bit1 y) = x * sqr (pow x y)"
    1.17 +  "pow x (Bit1 y) = sqr (pow x y) * x"
    1.18  
    1.19  lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x"
    1.20    by (induct x, simp_all add: algebra_simps nat_of_num_add)
    1.21 @@ -864,51 +864,6 @@
    1.22    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    1.23    by (simp_all add: numeral.simps BitM_plus_one)
    1.24  
    1.25 -subsubsection {*
    1.26 -  Structures with exponentiation
    1.27 -*}
    1.28 -
    1.29 -context semiring_numeral
    1.30 -begin
    1.31 -
    1.32 -lemma numeral_sqr: "numeral (sqr n) = numeral n * numeral n"
    1.33 -  by (simp add: sqr_conv_mult numeral_mult)
    1.34 -
    1.35 -lemma numeral_pow: "numeral (pow m n) = numeral m ^ numeral n"
    1.36 -  by (induct n, simp_all add: numeral_class.numeral.simps
    1.37 -    power_add numeral_sqr numeral_mult)
    1.38 -
    1.39 -lemma power_numeral [simp]: "numeral m ^ numeral n = numeral (pow m n)"
    1.40 -  by (rule numeral_pow [symmetric])
    1.41 -
    1.42 -end
    1.43 -
    1.44 -context semiring_1
    1.45 -begin
    1.46 -
    1.47 -lemma power_zero_numeral [simp]: "(0::'a) ^ numeral n = 0"
    1.48 -  by (induct n, simp_all add: numeral_class.numeral.simps power_add)
    1.49 -
    1.50 -end
    1.51 -
    1.52 -context ring_1
    1.53 -begin
    1.54 -
    1.55 -lemma power_minus_Bit0: "(- x) ^ numeral (Bit0 n) = x ^ numeral (Bit0 n)"
    1.56 -  by (induct n, simp_all add: numeral_class.numeral.simps power_add)
    1.57 -
    1.58 -lemma power_minus_Bit1: "(- x) ^ numeral (Bit1 n) = - (x ^ numeral (Bit1 n))"
    1.59 -  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
    1.60 -
    1.61 -lemma power_neg_numeral_Bit0 [simp]:
    1.62 -  "neg_numeral m ^ numeral (Bit0 n) = numeral (pow m (Bit0 n))"
    1.63 -  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
    1.64 -
    1.65 -lemma power_neg_numeral_Bit1 [simp]:
    1.66 -  "neg_numeral m ^ numeral (Bit1 n) = neg_numeral (pow m (Bit1 n))"
    1.67 -  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
    1.68 -
    1.69 -end
    1.70  
    1.71  subsection {* Numeral equations as default simplification rules *}
    1.72