diff --git a/lib/Word_Lib/Bits_Int.thy b/lib/Word_Lib/Bits_Int.thy index f94fa54a9..989218fee 100644 --- a/lib/Word_Lib/Bits_Int.thy +++ b/lib/Word_Lib/Bits_Int.thy @@ -86,10 +86,6 @@ lemma bin_nth_numeral: "bin_rest x = y \ bin_nth x (numeral n) = by (simp add: numeral_eq_Suc bit_Suc) lemmas bin_nth_numeral_simps [simp] = - bin_nth_numeral [OF bin_rest_numeral_simps(2)] - bin_nth_numeral [OF bin_rest_numeral_simps(5)] - bin_nth_numeral [OF bin_rest_numeral_simps(6)] - bin_nth_numeral [OF bin_rest_numeral_simps(7)] bin_nth_numeral [OF bin_rest_numeral_simps(8)] lemmas bin_nth_simps = @@ -207,7 +203,7 @@ lemma bin_nth_Bit1: by auto lemma bintrunc_bintrunc_l: "n \ m \ bintrunc m (bintrunc n w) = bintrunc n w" - by (simp add: min.absorb2) + by simp lemma sbintrunc_sbintrunc_l: "n \ m \ sbintrunc m (sbintrunc n w) = sbintrunc n w" by (simp add: min_def) @@ -216,10 +212,10 @@ lemma bintrunc_bintrunc_ge: "n \ m \ bintrunc n (bintrunc m by (rule bin_eqI) (auto simp: nth_bintr) lemma bintrunc_bintrunc_min [simp]: "bintrunc m (bintrunc n w) = bintrunc (min m n) w" - by (rule bin_eqI) (auto simp: nth_bintr) + by (rule take_bit_take_bit) lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" - by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2) + by (rule signed_take_bit_signed_take_bit) lemmas sbintrunc_Suc_Pls = signed_take_bit_Suc [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps] @@ -262,7 +258,7 @@ lemma sbintrunc_Suc_Is: by auto lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \ m = Suc n \ sbintrunc m x = y" - by auto + by (rule ssubst) lemmas sbintrunc_Suc_Ialts = sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] @@ -271,9 +267,7 @@ lemma sbintrunc_bintrunc_lt: "m > n \ sbintrunc n (bintrunc m w) by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) lemma bintrunc_sbintrunc_le: "m \ Suc n \ bintrunc m (sbintrunc n w) = bintrunc m w" - apply (rule bin_eqI) - using le_Suc_eq less_Suc_eq_le apply (auto simp: nth_sbintr nth_bintr) - done + by (rule take_bit_signed_take_bit) lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] diff --git a/lib/Word_Lib/Bitwise.thy b/lib/Word_Lib/Bitwise.thy index 57f069d77..29de7a9f3 100644 --- a/lib/Word_Lib/Bitwise.thy +++ b/lib/Word_Lib/Bitwise.thy @@ -427,7 +427,7 @@ val word_len_simproc = fun nat_get_Suc_simproc_fn n_sucs ctxt ct = let - val (f $ arg) = Thm.term_of ct; + val (f, arg) = dest_comb (Thm.term_of ct); val n = (case arg of \<^term>\nat\ $ n => n | n => n) |> HOLogic.dest_number |> snd; diff --git a/lib/Word_Lib/Generic_set_bit.thy b/lib/Word_Lib/Generic_set_bit.thy index 0a36f5c03..b4d01ba76 100644 --- a/lib/Word_Lib/Generic_set_bit.thy +++ b/lib/Word_Lib/Generic_set_bit.thy @@ -89,7 +89,7 @@ lemma set_bit_unfold: lemma bit_set_bit_word_iff [bit_simps]: \bit (set_bit w m b) n \ (if m = n then n < LENGTH('a) \ b else bit w n)\ for w :: \'a::len word\ - by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length) + by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff not_le bit_imp_le_length) lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w" for w :: "'a::len word" diff --git a/lib/Word_Lib/More_Word_Operations.thy b/lib/Word_Lib/More_Word_Operations.thy index 50e6eb358..9d1798509 100644 --- a/lib/Word_Lib/More_Word_Operations.thy +++ b/lib/Word_Lib/More_Word_Operations.thy @@ -238,13 +238,11 @@ lemma word_log2_max: lemma word_clz_0[simp]: "word_clz (0::'a::len word) = LENGTH('a)" - unfolding word_clz_def - by (simp add: takeWhile_replicate) + unfolding word_clz_def by simp lemma word_clz_minus_one[simp]: "word_clz (-1::'a::len word) = 0" - unfolding word_clz_def - by (simp add: takeWhile_replicate) + unfolding word_clz_def by simp lemma is_aligned_alignUp[simp]: "is_aligned (alignUp p n) n" @@ -334,7 +332,7 @@ next apply (subst unat_word_ariths) apply simp apply (subst mult_mod_left) - apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power min.absorb2) + apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power) done ultimately have lt: "2 ^ n * (unat a div 2 ^ n + 1) < 2 ^ LENGTH('a)" by simp @@ -527,8 +525,7 @@ proof - hence allj: "\j\set(to_bl w). \ j" by (metis a length_takeWhile_less less_irrefl_nat word_clz_def) hence "to_bl w = replicate (length (to_bl w)) False" - by (auto simp add: to_bl_unfold rev_map simp flip: map_replicate_trivial) - (metis allj eq_zero_set_bl nz) + using eq_zero_set_bl nz by fastforce hence "w = 0" by (metis to_bl_0 word_bl.Rep_eqD word_bl_Rep') with nz have False by simp diff --git a/lib/Word_Lib/Reversed_Bit_Lists.thy b/lib/Word_Lib/Reversed_Bit_Lists.thy index deedc5a44..20447c1c9 100644 --- a/lib/Word_Lib/Reversed_Bit_Lists.thy +++ b/lib/Word_Lib/Reversed_Bit_Lists.thy @@ -936,7 +936,7 @@ lemma bin_cat_foldl_lem: apply (drule meta_spec) apply (erule trans) apply (drule_tac x = "bin_cat y n a" in meta_spec) - apply (simp add: bin_cat_assoc_sym min.absorb2) + apply (simp add: bin_cat_assoc_sym) done lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))" diff --git a/lib/Word_Lib/Traditional_Infix_Syntax.thy b/lib/Word_Lib/Traditional_Infix_Syntax.thy index 27b45ad40..e0e7d166f 100644 --- a/lib/Word_Lib/Traditional_Infix_Syntax.thy +++ b/lib/Word_Lib/Traditional_Infix_Syntax.thy @@ -173,7 +173,7 @@ qed lemma bit_shiftl_word_iff [bit_simps]: \bit (w << m) n \ m \ n \ n < LENGTH('a) \ bit w (n - m)\ for w :: \'a::len word\ - by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) + by (simp add: shiftl_word_eq bit_push_bit_iff not_le) lemma bit_shiftr_word_iff [bit_simps]: \bit (w >> m) n \ bit w (m + n)\ @@ -473,9 +473,8 @@ lemma test_bit_split': (\n m. b !! n = (n < size b \ c !! n) \ a !! m = (m < size a \ c !! (m + size b)))" - by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size - bit_drop_bit_eq ac_simps exp_eq_zero_iff - dest: bit_imp_le_length) + by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size bit_drop_bit_eq ac_simps + dest: bit_imp_le_length) lemma test_bit_split: "word_split c = (a, b) \