# HG changeset patch # User haftmann # Date 1592471249 0 # Node ID 5b8b1183c6416c28b57801b104599046546539f1 # Parent 6ede899d26d329324b9b41afec244dd55aebef34 dropped yet another duplicate diff -r 6ede899d26d3 -r 5b8b1183c641 NEWS --- a/NEWS Thu Jun 18 09:07:29 2020 +0000 +++ b/NEWS Thu Jun 18 09:07:29 2020 +0000 @@ -48,11 +48,12 @@ * For the natural numbers, Sup {} = 0. -* Session HOL-Word: Operations "bin_last", "bin_rest", "bintrunc" -and "max_word" are now mere input abbreviations. INCOMPATIBILITY. +* Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth", +"bintrunc" and "max_word" are now mere input abbreviations. +Minor INCOMPATIBILITY. * Session HOL-Word: Compound operation "bin_split" simplifies by default -into its components "drop_bit" and "take_bit". Minor INCOMPATIBILITY. +into its components "drop_bit" and "take_bit". INCOMPATIBILITY. *** FOL *** diff -r 6ede899d26d3 -r 5b8b1183c641 src/HOL/Word/Bits_Int.thy --- a/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000 +++ b/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000 @@ -311,49 +311,39 @@ subsection \Bit projection\ -primrec bin_nth :: "int \ nat \ bool" - where - Z: "bin_nth w 0 \ bin_last w" - | Suc: "bin_nth w (Suc n) \ bin_nth (bin_rest w) n" - -lemma bin_nth_iff: - \bin_nth = bit\ -proof (rule ext)+ - fix k and n - show \bin_nth k n \ bit k n\ - by (induction n arbitrary: k) (simp_all add: bit_Suc) -qed +abbreviation (input) bin_nth :: \int \ nat \ bool\ + where \bin_nth \ bit\ lemma bin_nth_eq_iff: "bin_nth x = bin_nth y \ x = y" - by (simp add: bin_nth_iff bit_eq_iff fun_eq_iff) + by (simp add: bit_eq_iff fun_eq_iff) lemma bin_eqI: "x = y" if "\n. bin_nth x n \ bin_nth y n" using that bin_nth_eq_iff [of x y] by (simp add: fun_eq_iff) lemma bin_eq_iff: "x = y \ (\n. bin_nth x n = bin_nth y n)" - using bin_nth_eq_iff by auto + by (fact bit_eq_iff) lemma bin_nth_zero [simp]: "\ bin_nth 0 n" - by (induct n) auto + by simp lemma bin_nth_1 [simp]: "bin_nth 1 n \ n = 0" - by (cases n) simp_all + by (cases n) (simp_all add: bit_Suc) lemma bin_nth_minus1 [simp]: "bin_nth (- 1) n" - by (induct n) auto + by (induction n) (simp_all add: bit_Suc) lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \ b" - by auto + by simp lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" - by auto + by (simp add: bit_Suc) lemma bin_nth_minus [simp]: "0 < n \ bin_nth (w BIT b) n = bin_nth w (n - 1)" - by (cases n) auto + by (cases n) (simp_all add: bit_Suc) lemma bin_nth_numeral: "bin_rest x = y \ bin_nth x (numeral n) = bin_nth y (pred_numeral n)" - by (simp add: numeral_eq_Suc) + by (simp add: numeral_eq_Suc bit_Suc) lemmas bin_nth_numeral_simps [simp] = bin_nth_numeral [OF bin_rest_numeral_simps(2)] @@ -363,22 +353,17 @@ bin_nth_numeral [OF bin_rest_numeral_simps(8)] lemmas bin_nth_simps = - bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1 + bit_0 bit_Suc bin_nth_zero bin_nth_minus1 bin_nth_numeral_simps lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)" \ \for use when simplifying with \bin_nth_Bit\\ - apply (induct n arbitrary: m) - apply clarsimp - apply safe - apply (case_tac m) - apply (auto simp: Bit_B0_2t [symmetric]) - done - + by (auto simp add: bit_exp_iff) + lemma nth_rest_power_bin: "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)" apply (induct k arbitrary: n) apply clarsimp apply clarsimp - apply (simp only: bin_nth.Suc [symmetric] add_Suc) + apply (simp only: bit_Suc [symmetric] add_Suc) done lemma bin_nth_numeral_unfold: @@ -479,19 +464,17 @@ by simp_all lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n" - apply (induct n arbitrary: bin) - apply (case_tac bin rule: bin_exhaust, case_tac b, auto) - done + by (induct n arbitrary: bin) (simp_all add: bit_Suc) lemma nth_bintr: "bin_nth (bintrunc m w) n \ n < m \ bin_nth w n" - by (simp add: bin_nth_iff bit_take_bit_iff) + by (fact bit_take_bit_iff) lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)" apply (induct n arbitrary: w m) apply (case_tac m) apply simp_all apply (case_tac m) - apply simp_all + apply (simp_all add: bit_Suc) done lemma bin_nth_Bit: "bin_nth (w BIT b) n \ n = 0 \ b \ (\m. n = Suc m \ bin_nth w m)" @@ -828,17 +811,18 @@ "bin_nth (bin_cat x k y) n = (if n < k then bin_nth y n else bin_nth x (n - k))" apply (induct k arbitrary: n y) - apply clarsimp - apply (case_tac n, auto) + apply simp + apply (case_tac n) + apply (simp_all add: bit_Suc) done lemma bin_nth_drop_bit_iff: \bin_nth (drop_bit n c) k \ bin_nth c (n + k)\ - by (simp add: bin_nth_iff bit_drop_bit_eq) + by (simp add: bit_drop_bit_eq) lemma bin_nth_take_bit_iff: \bin_nth (take_bit n c) k \ k < n \ bin_nth c k\ - by (simp add: bin_nth_iff bit_take_bit_iff) + by (fact bit_take_bit_iff) lemma bin_nth_split: "bin_split n c = (a, b) \ @@ -1006,8 +990,8 @@ apply clarsimp apply (erule allE) apply (erule (1) impE) - apply (simp add: bin_nth_iff bit_drop_bit_eq ac_simps) - apply (simp add: bin_nth_iff bit_take_bit_iff ac_simps) + apply (simp add: bit_drop_bit_eq ac_simps) + apply (simp add: bit_take_bit_iff ac_simps) done lemma bin_rsplit_all: "0 < nw \ nw \ n \ bin_rsplit n (nw, w) = [bintrunc n w]" @@ -1142,10 +1126,13 @@ done lemma bin_nth_sc_gen: "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)" - by (induct n arbitrary: w m) (case_tac [!] m, auto) + apply (induct n arbitrary: w m) + apply (case_tac m; simp add: bit_Suc) + apply (case_tac m; simp add: bit_Suc) + done lemma bin_sc_nth [simp]: "bin_sc n (bin_nth w n) w = w" - by (induct n arbitrary: w) auto + by (induct n arbitrary: w) (simp_all add: bit_Suc) lemma bin_sign_sc [simp]: "bin_sign (bin_sc n b w) = bin_sign w" by (induct n arbitrary: w) auto @@ -1328,7 +1315,7 @@ "\x y. bin_nth (x OR y) n \ bin_nth x n \ bin_nth y n" "\x y. bin_nth (x XOR y) n \ bin_nth x n \ bin_nth y n" "\x. bin_nth (NOT x) n \ \ bin_nth x n" - by (induct n) auto + by (induct n) (auto simp add: bit_Suc) subsubsection \Derived properties\ @@ -2109,7 +2096,7 @@ moreover have "(2 * x' + of_bool b - 2 * 2 ^ n') div 2 = x' + (- (2 ^ n') + of_bool b div 2)" by(simp only: add_diff_eq[symmetric] add.commute div_mult_self2[OF zero_neq_numeral[symmetric]]) ultimately show ?case using Suc.IH[of x' n'] Suc.prems - by(cases b)(simp_all add: Bit_def shiftl_int_def) + by (clarsimp simp add: Bit_def shiftl_int_def bit_Suc) qed lemma bin_clr_conv_NAND: @@ -2241,10 +2228,9 @@ apply (case_tac m, clarsimp) apply (clarsimp simp: bin_to_bl_def) apply (simp add: bin_to_bl_aux_alt) - apply clarsimp apply (case_tac m, clarsimp) apply (clarsimp simp: bin_to_bl_def) - apply (simp add: bin_to_bl_aux_alt) + apply (simp add: bin_to_bl_aux_alt bit_Suc) done lemma nth_bin_to_bl_aux: diff -r 6ede899d26d3 -r 5b8b1183c641 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 +++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000 @@ -723,7 +723,7 @@ next assume ?Q then have *: \bit (uint x) n \ bit (uint y) n\ if \n < LENGTH('a)\ for n - using that by (simp add: word_test_bit_def bin_nth_iff) + using that by (simp add: word_test_bit_def) show ?P proof (rule word_uint_eqI, rule bit_eqI, rule iffI) fix n @@ -2726,11 +2726,8 @@ lemmas nth_shiftl = nth_shiftl' [unfolded word_size] lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n" - apply (unfold shiftr1_def word_test_bit_def) - apply (simp add: nth_bintr word_ubin.eq_norm) - apply safe - apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp]) - apply simp + apply (auto simp add: shiftr1_def word_test_bit_def word_ubin.eq_norm bit_take_bit_iff bit_Suc) + apply (metis (no_types, hide_lams) add_Suc_right add_diff_cancel_left' bit_Suc diff_is_0_eq' le_Suc_ex less_imp_le linorder_not_le test_bit_bin word_test_bit_def) done lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)" @@ -2755,9 +2752,8 @@ lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)" apply (unfold sshiftr1_def word_test_bit_def) - apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size - del: bin_nth.simps) - apply (simp add: nth_bintr uint_sint del : bin_nth.simps) + apply (simp add: nth_bintr word_ubin.eq_norm bit_Suc [symmetric] word_size) + apply (simp add: nth_bintr uint_sint) apply (auto simp add: bin_nth_sint) done @@ -2895,8 +2891,7 @@ apply clarsimp apply (case_tac i) apply (simp_all add: hd_conv_nth length_0_conv [symmetric] - nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr - del: bin_nth.Suc) + nth_bin_to_bl bit_Suc [symmetric] nth_sbintr) apply force apply (rule impI) apply (rule_tac f = "bin_nth (uint w)" in arg_cong) @@ -3597,7 +3592,7 @@ apply (unfold word_split_bin' test_bit_bin) apply (clarify) apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits) - apply (auto simp add: bin_nth_iff bit_take_bit_iff bit_drop_bit_eq ac_simps bin_nth_uint_imp) + apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq ac_simps bin_nth_uint_imp) done lemma test_bit_split: @@ -4550,7 +4545,7 @@ lemma test_bit_1' [simp]: "(1 :: 'a :: len0 word) !! n \ 0 < LENGTH('a) \ n = 0" - by (cases n) (simp_all only: one_word_def test_bit_wi bin_nth.simps, simp_all) + by (cases n) (simp_all only: one_word_def test_bit_wi, simp_all) lemma mask_0 [simp]: "mask 0 = 0"