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