--- 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 ***
--- 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 \<open>Bit projection\<close>
-primrec bin_nth :: "int \<Rightarrow> nat \<Rightarrow> bool"
- where
- Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
- | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
-
-lemma bin_nth_iff:
- \<open>bin_nth = bit\<close>
-proof (rule ext)+
- fix k and n
- show \<open>bin_nth k n \<longleftrightarrow> bit k n\<close>
- by (induction n arbitrary: k) (simp_all add: bit_Suc)
-qed
+abbreviation (input) bin_nth :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where \<open>bin_nth \<equiv> bit\<close>
lemma bin_nth_eq_iff: "bin_nth x = bin_nth y \<longleftrightarrow> 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 "\<And>n. bin_nth x n \<longleftrightarrow> 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 \<longleftrightarrow> (\<forall>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]: "\<not> bin_nth 0 n"
- by (induct n) auto
+ by simp
lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
- 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 \<longleftrightarrow> n < m \<and> 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 \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> 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:
\<open>bin_nth (drop_bit n c) k \<longleftrightarrow> bin_nth c (n + k)\<close>
- by (simp add: bin_nth_iff bit_drop_bit_eq)
+ by (simp add: bit_drop_bit_eq)
lemma bin_nth_take_bit_iff:
\<open>bin_nth (take_bit n c) k \<longleftrightarrow> k < n \<and> bin_nth c k\<close>
- 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) \<Longrightarrow>
@@ -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 \<Longrightarrow> nw \<le> n \<Longrightarrow> 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 @@
"\<And>x y. bin_nth (x OR y) n \<longleftrightarrow> bin_nth x n \<or> bin_nth y n"
"\<And>x y. bin_nth (x XOR y) n \<longleftrightarrow> bin_nth x n \<noteq> bin_nth y n"
"\<And>x. bin_nth (NOT x) n \<longleftrightarrow> \<not> bin_nth x n"
- by (induct n) auto
+ by (induct n) (auto simp add: bit_Suc)
subsubsection \<open>Derived properties\<close>
@@ -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:
--- 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 *: \<open>bit (uint x) n \<longleftrightarrow> bit (uint y) n\<close> if \<open>n < LENGTH('a)\<close> 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 \<longleftrightarrow> 0 < LENGTH('a) \<and> 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"