src/HOL/Library/Bit.thy
changeset 47108 2a1953f0d20d
parent 45701 615da8b8d758
child 49834 b27bbb021df1
equal deleted inserted replaced
47107:35807a5d8dc2 47108:2a1953f0d20d
    94   unfolding plus_bit_def by (simp split: bit.split)
    94   unfolding plus_bit_def by (simp split: bit.split)
    95 
    95 
    96 
    96 
    97 subsection {* Numerals at type @{typ bit} *}
    97 subsection {* Numerals at type @{typ bit} *}
    98 
    98 
    99 instantiation bit :: number_ring
       
   100 begin
       
   101 
       
   102 definition number_of_bit_def:
       
   103   "(number_of w :: bit) = of_int w"
       
   104 
       
   105 instance proof
       
   106 qed (rule number_of_bit_def)
       
   107 
       
   108 end
       
   109 
       
   110 text {* All numerals reduce to either 0 or 1. *}
    99 text {* All numerals reduce to either 0 or 1. *}
   111 
   100 
   112 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
   101 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
   113   by (simp only: number_of_Min uminus_bit_def)
   102   by (simp only: minus_one [symmetric] uminus_bit_def)
   114 
   103 
   115 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)"
   104 lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
   116   by (simp only: number_of_Bit0 add_0_left bit_add_self)
   105   by (simp only: neg_numeral_def uminus_bit_def)
   117 
   106 
   118 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)"
   107 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   119   by (simp only: number_of_Bit1 add_assoc bit_add_self
   108   by (simp only: numeral_Bit0 bit_add_self)
   120                  monoid_add_class.add_0_right)
   109 
       
   110 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
       
   111   by (simp only: numeral_Bit1 bit_add_self add_0_left)
   121 
   112 
   122 end
   113 end