3 *) |
3 *) |
4 |
4 |
5 section \<open>Comprehension syntax for bit expressions\<close> |
5 section \<open>Comprehension syntax for bit expressions\<close> |
6 |
6 |
7 theory Bit_Comprehension |
7 theory Bit_Comprehension |
8 imports "HOL-Library.Bit_Operations" |
8 imports Word |
9 begin |
9 begin |
10 |
10 |
11 class bit_comprehension = semiring_bits + |
11 class bit_comprehension = ring_bit_operations + |
12 fixes set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10) |
12 fixes set_bits :: \<open>(nat \<Rightarrow> bool) \<Rightarrow> 'a\<close> (binder \<open>BITS \<close> 10) |
|
13 assumes set_bits_bit_eq: \<open>set_bits (bit a) = a\<close> |
|
14 begin |
|
15 |
|
16 lemma set_bits_False_eq [simp]: |
|
17 \<open>(BITS _. False) = 0\<close> |
|
18 using set_bits_bit_eq [of 0] by (simp add: bot_fun_def) |
|
19 |
|
20 end |
13 |
21 |
14 instantiation int :: bit_comprehension |
22 instantiation int :: bit_comprehension |
15 begin |
23 begin |
16 |
24 |
17 definition |
25 definition |
18 "set_bits f = |
26 \<open>set_bits f = ( |
|
27 if \<exists>n. \<forall>m\<ge>n. f m = f n then |
|
28 let n = LEAST n. \<forall>m\<ge>n. f m = f n |
|
29 in signed_take_bit n (horner_sum of_bool 2 (map f [0..<Suc n])) |
|
30 else 0 :: int)\<close> |
|
31 |
|
32 instance proof |
|
33 fix k :: int |
|
34 from int_bit_bound [of k] |
|
35 obtain n where *: \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close> |
|
36 and **: \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close> |
|
37 by blast |
|
38 then have ***: \<open>\<exists>n. \<forall>n'\<ge>n. bit k n' \<longleftrightarrow> bit k n\<close> |
|
39 by meson |
|
40 have l: \<open>(LEAST q. \<forall>m\<ge>q. bit k m \<longleftrightarrow> bit k q) = n\<close> |
|
41 apply (rule Least_equality) |
|
42 using * apply blast |
|
43 apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq) |
|
44 done |
|
45 show \<open>set_bits (bit k) = k\<close> |
|
46 apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l) |
|
47 apply simp |
|
48 apply (rule bit_eqI) |
|
49 apply (simp add: bit_signed_take_bit_iff min_def) |
|
50 using "*" by blast |
|
51 qed |
|
52 |
|
53 end |
|
54 |
|
55 lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" |
|
56 by (simp add: set_bits_int_def) |
|
57 |
|
58 lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" |
|
59 by (simp add: set_bits_int_def) |
|
60 |
|
61 instantiation word :: (len) bit_comprehension |
|
62 begin |
|
63 |
|
64 definition word_set_bits_def: |
|
65 \<open>(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)\<close> |
|
66 |
|
67 instance by standard |
|
68 (simp add: word_set_bits_def horner_sum_bit_eq_take_bit) |
|
69 |
|
70 end |
|
71 |
|
72 lemma bit_set_bits_word_iff: |
|
73 \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close> |
|
74 by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff) |
|
75 |
|
76 lemma set_bits_K_False [simp]: |
|
77 \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close> |
|
78 by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff) |
|
79 |
|
80 lemma set_bits_int_unfold': |
|
81 \<open>set_bits f = |
19 (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then |
82 (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then |
20 let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' |
83 let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' |
21 in horner_sum of_bool 2 (map f [0..<n]) |
84 in horner_sum of_bool 2 (map f [0..<n]) |
22 else if \<exists>n. \<forall>n'\<ge>n. f n' then |
85 else if \<exists>n. \<forall>n'\<ge>n. f n' then |
23 let n = LEAST n. \<forall>n'\<ge>n. f n' |
86 let n = LEAST n. \<forall>n'\<ge>n. f n' |
24 in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) |
87 in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) |
25 else 0 :: int)" |
88 else 0 :: int)\<close> |
26 |
89 proof (cases \<open>\<exists>n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>) |
27 instance .. |
90 case True |
28 |
91 then obtain q where q: \<open>\<forall>m\<ge>q. f m \<longleftrightarrow> f q\<close> |
29 end |
92 by blast |
30 |
93 define n where \<open>n = (LEAST n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n)\<close> |
31 lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" |
94 have \<open>\<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close> |
32 by (simp add: set_bits_int_def) |
95 unfolding n_def |
33 |
96 using q by (rule LeastI [of _ q]) |
34 lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" |
97 then have n: \<open>\<And>m. n \<le> m \<Longrightarrow> f m \<longleftrightarrow> f n\<close> |
35 by (auto simp add: set_bits_int_def) |
98 by blast |
36 |
99 from n_def have n_eq: \<open>(LEAST q. \<forall>m\<ge>q. f m \<longleftrightarrow> f n) = n\<close> |
37 end |
100 by (smt Least_equality Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.refl le_refl n order_refl) |
|
101 show ?thesis |
|
102 proof (cases \<open>f n\<close>) |
|
103 case False |
|
104 with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. \<not> f n'\<close> |
|
105 by blast |
|
106 have **: \<open>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = n\<close> |
|
107 using False n_eq by simp |
|
108 from * False show ?thesis |
|
109 apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) |
|
110 apply (auto simp add: take_bit_horner_sum_bit_eq |
|
111 bit_horner_sum_bit_iff take_map |
|
112 signed_take_bit_def set_bits_int_def |
|
113 horner_sum_bit_eq_take_bit simp del: upt.upt_Suc) |
|
114 done |
|
115 next |
|
116 case True |
|
117 with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. f n'\<close> |
|
118 by blast |
|
119 have ***: \<open>\<not> (\<exists>n. \<forall>n'\<ge>n. \<not> f n')\<close> |
|
120 apply (rule ccontr) |
|
121 using * nat_le_linear by auto |
|
122 have **: \<open>(LEAST n. \<forall>n'\<ge>n. f n') = n\<close> |
|
123 using True n_eq by simp |
|
124 from * *** True show ?thesis |
|
125 apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) |
|
126 apply (auto simp add: take_bit_horner_sum_bit_eq |
|
127 bit_horner_sum_bit_iff take_map |
|
128 signed_take_bit_def set_bits_int_def |
|
129 horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc) |
|
130 done |
|
131 qed |
|
132 next |
|
133 case False |
|
134 then show ?thesis |
|
135 by (auto simp add: set_bits_int_def) |
|
136 qed |
|
137 |
|
138 inductive wf_set_bits_int :: "(nat \<Rightarrow> bool) \<Rightarrow> bool" |
|
139 for f :: "nat \<Rightarrow> bool" |
|
140 where |
|
141 zeros: "\<forall>n' \<ge> n. \<not> f n' \<Longrightarrow> wf_set_bits_int f" |
|
142 | ones: "\<forall>n' \<ge> n. f n' \<Longrightarrow> wf_set_bits_int f" |
|
143 |
|
144 lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))" |
|
145 by(auto simp add: wf_set_bits_int.simps) |
|
146 |
|
147 lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\<lambda>_. b)" |
|
148 by(cases b)(auto intro: wf_set_bits_int.intros) |
|
149 |
|
150 lemma wf_set_bits_int_fun_upd [simp]: |
|
151 "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs") |
|
152 proof |
|
153 assume ?lhs |
|
154 then obtain n' |
|
155 where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')" |
|
156 by(auto simp add: wf_set_bits_int_simps) |
|
157 hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto |
|
158 thus ?rhs by(auto simp only: wf_set_bits_int_simps) |
|
159 next |
|
160 assume ?rhs |
|
161 then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'") |
|
162 by(auto simp add: wf_set_bits_int_simps) |
|
163 hence "?wf (f(n := b)) (max (Suc n) n')" by auto |
|
164 thus ?lhs by(auto simp only: wf_set_bits_int_simps) |
|
165 qed |
|
166 |
|
167 lemma wf_set_bits_int_Suc [simp]: |
|
168 "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs") |
|
169 by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D) |
|
170 |
|
171 context |
|
172 fixes f |
|
173 assumes wff: "wf_set_bits_int f" |
|
174 begin |
|
175 |
|
176 lemma int_set_bits_unfold_BIT: |
|
177 "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \<circ> Suc)" |
|
178 using wff proof cases |
|
179 case (zeros n) |
|
180 show ?thesis |
|
181 proof(cases "\<forall>n. \<not> f n") |
|
182 case True |
|
183 hence "f = (\<lambda>_. False)" by auto |
|
184 thus ?thesis using True by(simp add: o_def) |
|
185 next |
|
186 case False |
|
187 then obtain n' where "f n'" by blast |
|
188 with zeros have "(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')" |
|
189 by(auto intro: Least_Suc) |
|
190 also have "(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))" by(auto dest: Suc_le_D) |
|
191 also from zeros have "\<forall>n'\<ge>n. \<not> f (Suc n')" by auto |
|
192 ultimately show ?thesis using zeros |
|
193 apply (simp (no_asm_simp) add: set_bits_int_unfold' exI |
|
194 del: upt.upt_Suc flip: map_map split del: if_split) |
|
195 apply (simp only: map_Suc_upt upt_conv_Cons) |
|
196 apply simp |
|
197 done |
|
198 qed |
|
199 next |
|
200 case (ones n) |
|
201 show ?thesis |
|
202 proof(cases "\<forall>n. f n") |
|
203 case True |
|
204 hence "f = (\<lambda>_. True)" by auto |
|
205 thus ?thesis using True by(simp add: o_def) |
|
206 next |
|
207 case False |
|
208 then obtain n' where "\<not> f n'" by blast |
|
209 with ones have "(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')" |
|
210 by(auto intro: Least_Suc) |
|
211 also have "(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))" by(auto dest: Suc_le_D) |
|
212 also from ones have "\<forall>n'\<ge>n. f (Suc n')" by auto |
|
213 moreover from ones have "(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False" |
|
214 by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm) |
|
215 moreover hence "(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False" |
|
216 by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D) |
|
217 ultimately show ?thesis using ones |
|
218 apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split) |
|
219 apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc |
|
220 not_le simp del: map_map) |
|
221 done |
|
222 qed |
|
223 qed |
|
224 |
|
225 lemma bin_last_set_bits [simp]: |
|
226 "bin_last (set_bits f) = f 0" |
|
227 by (subst int_set_bits_unfold_BIT) simp_all |
|
228 |
|
229 lemma bin_rest_set_bits [simp]: |
|
230 "bin_rest (set_bits f) = set_bits (f \<circ> Suc)" |
|
231 by (subst int_set_bits_unfold_BIT) simp_all |
|
232 |
|
233 lemma bin_nth_set_bits [simp]: |
|
234 "bin_nth (set_bits f) m = f m" |
|
235 using wff proof (induction m arbitrary: f) |
|
236 case 0 |
|
237 then show ?case |
|
238 by (simp add: Bit_Comprehension.bin_last_set_bits) |
|
239 next |
|
240 case Suc |
|
241 from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case |
|
242 by (simp add: Bit_Comprehension.bin_rest_set_bits comp_def bit_Suc) |
|
243 qed |
|
244 |
|
245 end |
|
246 |
|
247 end |