equal
deleted
inserted
replaced
88 unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
88 unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
89 |
89 |
90 lemma le_Bits: |
90 lemma le_Bits: |
91 "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" |
91 "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" |
92 unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
92 unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
93 |
|
94 lemma no_no [simp]: "number_of (number_of i) = i" |
|
95 unfolding number_of_eq by simp |
|
96 |
93 |
97 lemma Bit_B0: |
94 lemma Bit_B0: |
98 "k BIT (0::bit) = k + k" |
95 "k BIT (0::bit) = k + k" |
99 by (unfold Bit_def) simp |
96 by (unfold Bit_def) simp |
100 |
97 |