# HG changeset patch # User haftmann # Date 1602142202 0 # Node ID 48013583e8e60757ccb0c0d9d26047a73b97b627 # Parent 63e83aaec7a8743dd7e2fef064ef4f69cd3b6c8d factored out bit comprehension diff -r 63e83aaec7a8 -r 48013583e8e6 src/HOL/Library/Bit_Operations.thy --- a/src/HOL/Library/Bit_Operations.thy Thu Oct 08 10:33:38 2020 +0200 +++ b/src/HOL/Library/Bit_Operations.thy Thu Oct 08 07:30:02 2020 +0000 @@ -486,6 +486,74 @@ subsection \Instance \<^typ>\int\\ +lemma int_bit_bound: + fixes k :: int + obtains n where \\m. n \ m \ bit k m \ bit k n\ + and \n > 0 \ bit k (n - 1) \ bit k n\ +proof - + obtain q where *: \\m. q \ m \ bit k m \ bit k q\ + proof (cases \k \ 0\) + case True + moreover from power_gt_expt [of 2 \nat k\] + have \k < 2 ^ nat k\ by simp + ultimately have *: \k div 2 ^ nat k = 0\ + by simp + show thesis + proof (rule that [of \nat k\]) + fix m + assume \nat k \ m\ + then show \bit k m \ bit k (nat k)\ + by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex) + qed + next + case False + moreover from power_gt_expt [of 2 \nat (- k)\] + have \- k \ 2 ^ nat (- k)\ + by simp + ultimately have \- k div - (2 ^ nat (- k)) = - 1\ + by (subst div_pos_neg_trivial) simp_all + then have *: \k div 2 ^ nat (- k) = - 1\ + by simp + show thesis + proof (rule that [of \nat (- k)\]) + fix m + assume \nat (- k) \ m\ + then show \bit k m \ bit k (nat (- k))\ + by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex) + qed + qed + show thesis + proof (cases \\m. bit k m \ bit k q\) + case True + then have \bit k 0 \ bit k q\ + by blast + with True that [of 0] show thesis + by simp + next + case False + then obtain r where **: \bit k r \ bit k q\ + by blast + have \r < q\ + by (rule ccontr) (use * [of r] ** in simp) + define N where \N = {n. n < q \ bit k n \ bit k q}\ + moreover have \finite N\ \r \ N\ + using ** N_def \r < q\ by auto + moreover define n where \n = Suc (Max N)\ + ultimately have \\m. n \ m \ bit k m \ bit k n\ + apply auto + apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) + apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) + apply (metis "*" Max_ge Suc_n_not_le_n \finite N\ linorder_not_less mem_Collect_eq) + apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \finite N\ all_not_in_conv mem_Collect_eq not_le) + done + have \bit k (Max N) \ bit k n\ + by (metis (mono_tags, lifting) "*" Max_in N_def \\m. n \ m \ bit k m = bit k n\ \finite N\ \r \ N\ empty_iff le_cases mem_Collect_eq) + show thesis apply (rule that [of n]) + using \\m. n \ m \ bit k m = bit k n\ apply blast + using \bit k (Max N) \ bit k n\ n_def by auto + qed +qed + instantiation int :: ring_bit_operations begin diff -r 63e83aaec7a8 -r 48013583e8e6 src/HOL/Word/Bit_Comprehension.thy --- a/src/HOL/Word/Bit_Comprehension.thy Thu Oct 08 10:33:38 2020 +0200 +++ b/src/HOL/Word/Bit_Comprehension.thy Thu Oct 08 07:30:02 2020 +0000 @@ -5,26 +5,50 @@ section \Comprehension syntax for bit expressions\ theory Bit_Comprehension - imports "HOL-Library.Bit_Operations" + imports Word begin -class bit_comprehension = semiring_bits + - fixes set_bits :: "(nat \ bool) \ 'a" (binder "BITS " 10) +class bit_comprehension = ring_bit_operations + + fixes set_bits :: \(nat \ bool) \ 'a\ (binder \BITS \ 10) + assumes set_bits_bit_eq: \set_bits (bit a) = a\ +begin + +lemma set_bits_False_eq [simp]: + \(BITS _. False) = 0\ + using set_bits_bit_eq [of 0] by (simp add: bot_fun_def) + +end instantiation int :: bit_comprehension begin definition - "set_bits f = - (if \n. \n'\n. \ f n' then - let n = LEAST n. \n'\n. \ f n' - in horner_sum of_bool 2 (map f [0..n. \n'\n. f n' then - let n = LEAST n. \n'\n. f n' - in signed_take_bit n (horner_sum of_bool 2 (map f [0..set_bits f = ( + if \n. \m\n. f m = f n then + let n = LEAST n. \m\n. f m = f n + in signed_take_bit n (horner_sum of_bool 2 (map f [0.. -instance .. +instance proof + fix k :: int + from int_bit_bound [of k] + obtain n where *: \\m. n \ m \ bit k m \ bit k n\ + and **: \n > 0 \ bit k (n - 1) \ bit k n\ + by blast + then have ***: \\n. \n'\n. bit k n' \ bit k n\ + by meson + have l: \(LEAST q. \m\q. bit k m \ bit k q) = n\ + apply (rule Least_equality) + using * apply blast + apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq) + done + show \set_bits (bit k) = k\ + apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l) + apply simp + apply (rule bit_eqI) + apply (simp add: bit_signed_take_bit_iff min_def) + using "*" by blast +qed end @@ -32,6 +56,192 @@ by (simp add: set_bits_int_def) lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" - by (auto simp add: set_bits_int_def) + by (simp add: set_bits_int_def) + +instantiation word :: (len) bit_comprehension +begin + +definition word_set_bits_def: + \(BITS n. P n) = (horner_sum of_bool 2 (map P [0.. + +instance by standard + (simp add: word_set_bits_def horner_sum_bit_eq_take_bit) end + +lemma bit_set_bits_word_iff: + \bit (set_bits P :: 'a::len word) n \ n < LENGTH('a) \ P n\ + by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff) + +lemma set_bits_K_False [simp]: + \set_bits (\_. False) = (0 :: 'a :: len word)\ + by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff) + +lemma set_bits_int_unfold': + \set_bits f = + (if \n. \n'\n. \ f n' then + let n = LEAST n. \n'\n. \ f n' + in horner_sum of_bool 2 (map f [0..n. \n'\n. f n' then + let n = LEAST n. \n'\n. f n' + in signed_take_bit n (horner_sum of_bool 2 (map f [0.. +proof (cases \\n. \m\n. f m \ f n\) + case True + then obtain q where q: \\m\q. f m \ f q\ + by blast + define n where \n = (LEAST n. \m\n. f m \ f n)\ + have \\m\n. f m \ f n\ + unfolding n_def + using q by (rule LeastI [of _ q]) + then have n: \\m. n \ m \ f m \ f n\ + by blast + from n_def have n_eq: \(LEAST q. \m\q. f m \ f n) = n\ + by (smt Least_equality Least_le \\m\n. f m = f n\ dual_order.refl le_refl n order_refl) + show ?thesis + proof (cases \f n\) + case False + with n have *: \\n. \n'\n. \ f n'\ + by blast + have **: \(LEAST n. \n'\n. \ f n') = n\ + using False n_eq by simp + from * False show ?thesis + apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) + apply (auto simp add: take_bit_horner_sum_bit_eq + bit_horner_sum_bit_iff take_map + signed_take_bit_def set_bits_int_def + horner_sum_bit_eq_take_bit simp del: upt.upt_Suc) + done + next + case True + with n have *: \\n. \n'\n. f n'\ + by blast + have ***: \\ (\n. \n'\n. \ f n')\ + apply (rule ccontr) + using * nat_le_linear by auto + have **: \(LEAST n. \n'\n. f n') = n\ + using True n_eq by simp + from * *** True show ?thesis + apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) + apply (auto simp add: take_bit_horner_sum_bit_eq + bit_horner_sum_bit_iff take_map + signed_take_bit_def set_bits_int_def + horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc) + done + qed +next + case False + then show ?thesis + by (auto simp add: set_bits_int_def) +qed + +inductive wf_set_bits_int :: "(nat \ bool) \ bool" + for f :: "nat \ bool" +where + zeros: "\n' \ n. \ f n' \ wf_set_bits_int f" +| ones: "\n' \ n. f n' \ wf_set_bits_int f" + +lemma wf_set_bits_int_simps: "wf_set_bits_int f \ (\n. (\n'\n. \ f n') \ (\n'\n. f n'))" +by(auto simp add: wf_set_bits_int.simps) + +lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\_. b)" +by(cases b)(auto intro: wf_set_bits_int.intros) + +lemma wf_set_bits_int_fun_upd [simp]: + "wf_set_bits_int (f(n := b)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") +proof + assume ?lhs + then obtain n' + where "(\n''\n'. \ (f(n := b)) n'') \ (\n''\n'. (f(n := b)) n'')" + by(auto simp add: wf_set_bits_int_simps) + hence "(\n''\max (Suc n) n'. \ f n'') \ (\n''\max (Suc n) n'. f n'')" by auto + thus ?rhs by(auto simp only: wf_set_bits_int_simps) +next + assume ?rhs + then obtain n' where "(\n''\n'. \ f n'') \ (\n''\n'. f n'')" (is "?wf f n'") + by(auto simp add: wf_set_bits_int_simps) + hence "?wf (f(n := b)) (max (Suc n) n')" by auto + thus ?lhs by(auto simp only: wf_set_bits_int_simps) +qed + +lemma wf_set_bits_int_Suc [simp]: + "wf_set_bits_int (\n. f (Suc n)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") +by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D) + +context + fixes f + assumes wff: "wf_set_bits_int f" +begin + +lemma int_set_bits_unfold_BIT: + "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \ Suc)" +using wff proof cases + case (zeros n) + show ?thesis + proof(cases "\n. \ f n") + case True + hence "f = (\_. False)" by auto + thus ?thesis using True by(simp add: o_def) + next + case False + then obtain n' where "f n'" by blast + with zeros have "(LEAST n. \n'\n. \ f n') = Suc (LEAST n. \n'\Suc n. \ f n')" + by(auto intro: Least_Suc) + also have "(\n. \n'\Suc n. \ f n') = (\n. \n'\n. \ f (Suc n'))" by(auto dest: Suc_le_D) + also from zeros have "\n'\n. \ f (Suc n')" by auto + ultimately show ?thesis using zeros + apply (simp (no_asm_simp) add: set_bits_int_unfold' exI + del: upt.upt_Suc flip: map_map split del: if_split) + apply (simp only: map_Suc_upt upt_conv_Cons) + apply simp + done + qed +next + case (ones n) + show ?thesis + proof(cases "\n. f n") + case True + hence "f = (\_. True)" by auto + thus ?thesis using True by(simp add: o_def) + next + case False + then obtain n' where "\ f n'" by blast + with ones have "(LEAST n. \n'\n. f n') = Suc (LEAST n. \n'\Suc n. f n')" + by(auto intro: Least_Suc) + also have "(\n. \n'\Suc n. f n') = (\n. \n'\n. f (Suc n'))" by(auto dest: Suc_le_D) + also from ones have "\n'\n. f (Suc n')" by auto + moreover from ones have "(\n. \n'\n. \ f n') = False" + by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm) + moreover hence "(\n. \n'\n. \ f (Suc n')) = False" + by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D) + ultimately show ?thesis using ones + apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split) + apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc + not_le simp del: map_map) + done + qed +qed + +lemma bin_last_set_bits [simp]: + "bin_last (set_bits f) = f 0" + by (subst int_set_bits_unfold_BIT) simp_all + +lemma bin_rest_set_bits [simp]: + "bin_rest (set_bits f) = set_bits (f \ Suc)" + by (subst int_set_bits_unfold_BIT) simp_all + +lemma bin_nth_set_bits [simp]: + "bin_nth (set_bits f) m = f m" +using wff proof (induction m arbitrary: f) + case 0 + then show ?case + by (simp add: Bit_Comprehension.bin_last_set_bits) +next + case Suc + from Suc.IH [of "f \ Suc"] Suc.prems show ?case + by (simp add: Bit_Comprehension.bin_rest_set_bits comp_def bit_Suc) +qed + +end + +end diff -r 63e83aaec7a8 -r 48013583e8e6 src/HOL/Word/Misc_Typedef.thy --- a/src/HOL/Word/Misc_Typedef.thy Thu Oct 08 10:33:38 2020 +0200 +++ b/src/HOL/Word/Misc_Typedef.thy Thu Oct 08 07:30:02 2020 +0000 @@ -7,7 +7,7 @@ section \Type Definition Theorems\ theory Misc_Typedef - imports Main Word + imports Main Word Bit_Comprehension begin subsection "More lemmas about normal type definitions" @@ -349,8 +349,7 @@ set_bits "{f. \i. f i \ i < LENGTH('a::len)}" "(\h i. h i \ i < LENGTH('a::len))" - by standard - (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq) + by standard (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq) lemmas td_nth = test_bit.td_thm diff -r 63e83aaec7a8 -r 48013583e8e6 src/HOL/Word/More_Word.thy --- a/src/HOL/Word/More_Word.thy Thu Oct 08 10:33:38 2020 +0200 +++ b/src/HOL/Word/More_Word.thy Thu Oct 08 07:30:02 2020 +0000 @@ -9,6 +9,7 @@ Ancient_Numeral Reversed_Bit_Lists Bits_Int + Bit_Comprehension Misc_Auxiliary Misc_Arithmetic Misc_set_bit diff -r 63e83aaec7a8 -r 48013583e8e6 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Oct 08 10:33:38 2020 +0200 +++ b/src/HOL/Word/Word.thy Thu Oct 08 07:30:02 2020 +0000 @@ -11,7 +11,6 @@ "HOL-Library.Bit_Operations" Bits_Int Traditional_Syntax - Bit_Comprehension begin subsection \Preliminaries\ @@ -3915,31 +3914,6 @@ done -subsection \Bit comprehension\ - -instantiation word :: (len) bit_comprehension -begin - -definition word_set_bits_def: - \(BITS n. P n) = (horner_sum of_bool 2 (map P [0.. - -instance .. - -end - -lemma bit_set_bits_word_iff: - \bit (set_bits P :: 'a::len word) n \ n < LENGTH('a) \ P n\ - by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff) - -lemma set_bits_bit_eq: - \set_bits (bit w) = w\ for w :: \'a::len word\ - by (rule bit_word_eqI) (auto simp add: bit_set_bits_word_iff bit_imp_le_length) - -lemma set_bits_K_False [simp]: - \set_bits (\_. False) = (0 :: 'a :: len word)\ - by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff) - - subsection \Shifting, Rotating, and Splitting Words\ lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)" @@ -5311,9 +5285,6 @@ lemma mask_Suc_0: "mask (Suc 0) = 1" using mask_1 by simp -lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)" - by (simp add: mask_Suc_rec numeral_eq_Suc) - lemma bin_last_bintrunc: "bin_last (take_bit l n) = (l > 0 \ bin_last n)" by simp