equal
deleted
inserted
replaced
2599 done |
2599 done |
2600 |
2600 |
2601 lemma shiftl1_0 [simp] : "shiftl1 0 = 0" |
2601 lemma shiftl1_0 [simp] : "shiftl1 0 = 0" |
2602 unfolding word_0_no shiftl1_number by (auto simp: BIT_simps) |
2602 unfolding word_0_no shiftl1_number by (auto simp: BIT_simps) |
2603 |
2603 |
2604 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def] |
2604 lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)" |
|
2605 by (simp only: word_number_of_def shiftl1_def) |
2605 |
2606 |
2606 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)" |
2607 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)" |
2607 by (rule trans [OF _ shiftl1_number]) simp |
2608 by (rule trans [OF _ shiftl1_number]) simp |
2608 |
2609 |
2609 lemma shiftr1_0 [simp] : "shiftr1 0 = 0" |
2610 lemma shiftr1_0 [simp] : "shiftr1 0 = 0" |