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