src/HOL/Library/Bit.thy
changeset 55416 dd7992d4a61a
parent 54489 03ff4d1e6784
child 58306 117ba6cbe414
equal deleted inserted replaced
55415:05f5fdb8d093 55416:dd7992d4a61a
   100 
   100 
   101 instantiation bit :: field_inverse_zero
   101 instantiation bit :: field_inverse_zero
   102 begin
   102 begin
   103 
   103 
   104 definition plus_bit_def:
   104 definition plus_bit_def:
   105   "x + y = bit_case y (bit_case 1 0 y) x"
   105   "x + y = case_bit y (case_bit 1 0 y) x"
   106 
   106 
   107 definition times_bit_def:
   107 definition times_bit_def:
   108   "x * y = bit_case 0 y x"
   108   "x * y = case_bit 0 y x"
   109 
   109 
   110 definition uminus_bit_def [simp]:
   110 definition uminus_bit_def [simp]:
   111   "- x = (x :: bit)"
   111   "- x = (x :: bit)"
   112 
   112 
   113 definition minus_bit_def [simp]:
   113 definition minus_bit_def [simp]:
   165 context zero_neq_one
   165 context zero_neq_one
   166 begin
   166 begin
   167 
   167 
   168 definition of_bit :: "bit \<Rightarrow> 'a"
   168 definition of_bit :: "bit \<Rightarrow> 'a"
   169 where
   169 where
   170   "of_bit b = bit_case 0 1 b" 
   170   "of_bit b = case_bit 0 1 b" 
   171 
   171 
   172 lemma of_bit_eq [simp, code]:
   172 lemma of_bit_eq [simp, code]:
   173   "of_bit 0 = 0"
   173   "of_bit 0 = 0"
   174   "of_bit 1 = 1"
   174   "of_bit 1 = 1"
   175   by (simp_all add: of_bit_def)
   175   by (simp_all add: of_bit_def)