blob: 22c35e1fb52a2f057068abc08ca128f17e23f286 (
plain)
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
theory "Sail_operators_mwords_lemmas"
imports Sail_operators_mwords
begin
lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def
lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def
lemma bools_of_bits_oracle_just_list[simp]:
assumes "just_list (map bool_of_bitU bus) = Some bs"
shows "bools_of_bits_oracle bus = return bs"
proof -
have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_oracle b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)"
if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools
proof (use that in \<open>induction bus arbitrary: bs bools\<close>)
case (Cons bu bus bs)
obtain b bs' where bs: "bs = b # bs'" and bu: "bool_of_bitU bu = Some b"
using Cons.prems by (cases bu) (auto split: option.splits)
then show ?case
using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"]
by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits)
qed auto
then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def
by auto
qed
lemma of_bits_mword_return_of_bl[simp]:
assumes "just_list (map bool_of_bitU bus) = Some bs"
shows "of_bits_oracle BC_mword bus = return (of_bl bs)"
and "of_bits_fail BC_mword bus = return (of_bl bs)"
by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs)
lemma vec_of_bits_of_bl[simp]:
assumes "just_list (map bool_of_bitU bus) = Some bs"
shows "vec_of_bits_maybe bus = Some (of_bl bs)"
and "vec_of_bits_fail bus = return (of_bl bs)"
and "vec_of_bits_oracle bus = return (of_bl bs)"
and "vec_of_bits_failwith bus = of_bl bs"
and "vec_of_bits bus = of_bl bs"
unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def
vec_of_bits_failwith_def vec_of_bits_def
by (auto simp: assms)
lemmas access_vec_dec_test_bit[simp] = access_bv_dec_mword[folded access_vec_dec_def]
lemma access_vec_inc_test_bit[simp]:
fixes w :: "('a::len) word"
assumes "n \<ge> 0" and "nat n < LENGTH('a)"
shows "access_vec_inc w n = bitU_of_bool (w !! (LENGTH('a) - 1 - nat n))"
using assms
by (auto simp: access_vec_inc_def access_bv_inc_def access_list_def BC_mword_defs rev_nth test_bit_bl)
lemma bool_of_bitU_monadic_simps[simp]:
"bool_of_bitU_fail B0 = return False"
"bool_of_bitU_fail B1 = return True"
"bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
"bool_of_bitU_oracle B0 = return False"
"bool_of_bitU_oracle B1 = return True"
"bool_of_bitU_oracle BU = undefined_bool ()"
unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def
by auto
lemma update_vec_dec_simps[simp]:
"update_vec_dec_maybe w i B0 = Some (set_bit w (nat i) False)"
"update_vec_dec_maybe w i B1 = Some (set_bit w (nat i) True)"
"update_vec_dec_maybe w i BU = None"
"update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)"
"update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)"
"update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
"update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)"
"update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)"
"update_vec_dec_oracle w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
"update_vec_dec w i B0 = set_bit w (nat i) False"
"update_vec_dec w i B1 = set_bit w (nat i) True"
unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_oracle_def update_vec_dec_def
by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def)
lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]:
"n \<ge> 0 \<Longrightarrow> nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)"
by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq)
declare extz_vec_def[simp]
declare exts_vec_def[simp]
declare concat_vec_def[simp]
lemma msb_Bits_msb[simp]:
"msb w = bitU_of_bool (Bits.msb w)"
by (auto simp: msb_def most_significant_def BC_mword_defs word_msb_alt split: list.splits)
declare and_vec_def[simp]
declare or_vec_def[simp]
declare xor_vec_def[simp]
declare not_vec_def[simp]
lemma arith_vec_simps[simp]:
"add_vec l r = l + r"
"sub_vec l r = l - r"
"mult_vec l r = (ucast l) * (ucast r)"
unfolding add_vec_def sub_vec_def mult_vec_def
by (auto simp: int_of_mword_def word_add_def word_sub_wi word_mult_def)
declare adds_vec_def[simp]
declare subs_vec_def[simp]
declare mults_vec_def[simp]
lemma arith_vec_int_simps[simp]:
"add_vec_int l r = l + (word_of_int r)"
"sub_vec_int l r = l - (word_of_int r)"
"mult_vec_int l r = (ucast l) * (word_of_int r)"
unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def
by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def)
end
|
