1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Instance of bit ops for nat. Used by HaskellLib and AutoCorres. 8 * Lemmas about this instance should also go here. *) 9theory NatBitwise 10imports 11 "HOL-Word.Word" 12 Lib 13begin 14 15instantiation nat :: bit_operations 16begin 17 18(* NB: this is not useful, because NOT flips the sign, and hence this 19 * definition always produces 0. *) 20definition 21 "bitNOT = nat o bitNOT o int" 22 23definition 24 "bitAND x y = nat (bitAND (int x) (int y))" 25 26definition 27 "bitOR x y = nat (bitOR (int x) (int y))" 28 29definition 30 "bitXOR x y = nat (bitXOR (int x) (int y))" 31 32definition 33 "shiftl x y = nat (shiftl (int x) y)" 34 35definition 36 "shiftr x y = nat (shiftr (int x) y)" 37 38definition 39 "test_bit x y = test_bit (int x) y" 40 41definition 42 "lsb x = lsb (int x)" 43 44definition 45 "msb x = msb (int x)" 46 47definition 48 "set_bit x y z = nat (set_bit (int x) y z)" 49 50instance .. 51 52end 53 54lemma nat_2p_eq_shiftl: 55 "(2::nat)^x = 1 << x" 56 by (simp add: shiftl_nat_def int_2p_eq_shiftl) 57 58lemma shiftl_nat_alt_def: 59 "(x::nat) << n = x * 2^n" 60 by (simp add: shiftl_nat_def shiftl_int_def nat_int_mul) 61 62lemma nat_shiftl_less_cancel: 63 "n \<le> m \<Longrightarrow> ((x :: nat) << n < y << m) = (x < y << (m - n))" 64 by (simp add: nat_int_comparison(2) shiftl_nat_def int_shiftl_less_cancel) 65 66lemma nat_shiftl_lt_2p_bits: 67 "(x::nat) < 1 << n \<Longrightarrow> \<forall>i \<ge> n. \<not> x !! i" 68 apply (clarsimp simp: shiftl_nat_def test_bit_nat_def zless_nat_eq_int_zless) 69 apply (fastforce dest: int_shiftl_lt_2p_bits[rotated]) 70 done 71 72lemma nat_eq_test_bit: 73 "((x :: nat) = y) = (\<forall>i. test_bit x i = test_bit y i)" 74 apply (simp add: test_bit_nat_def) 75 apply (metis bin_eqI int_int_eq) 76 done 77lemmas nat_eq_test_bitI = nat_eq_test_bit[THEN iffD2, rule_format] 78 79end