equal
deleted
inserted
replaced
51 |
51 |
52 instantiation bit :: "{field, division_by_zero}" |
52 instantiation bit :: "{field, division_by_zero}" |
53 begin |
53 begin |
54 |
54 |
55 definition plus_bit_def: |
55 definition plus_bit_def: |
56 "x + y = (case x of 0 \<Rightarrow> y | 1 \<Rightarrow> (case y of 0 \<Rightarrow> 1 | 1 \<Rightarrow> 0))" |
56 "x + y = bit_case y (bit_case 1 0 y) x" |
57 |
57 |
58 definition times_bit_def: |
58 definition times_bit_def: |
59 "x * y = (case x of 0 \<Rightarrow> 0 | 1 \<Rightarrow> y)" |
59 "x * y = bit_case 0 y x" |
60 |
60 |
61 definition uminus_bit_def [simp]: |
61 definition uminus_bit_def [simp]: |
62 "- x = (x :: bit)" |
62 "- x = (x :: bit)" |
63 |
63 |
64 definition minus_bit_def [simp]: |
64 definition minus_bit_def [simp]: |