--- a/NEWS Wed Oct 07 11:31:51 2020 +0200
+++ b/NEWS Wed Oct 07 10:39:14 2020 +0200
@@ -120,6 +120,10 @@
* Session HOL-Word: Uniform polymorphic "mask" operation for both
types int and word. INCOMPATIBILITY.
+* Session HOL-Word: Syntax for signed compare operators has been
+consolidated with syntax of regular compare operators.
+Minor INCOMPATIBILITY.
+
* Session HOL-Word: Operations lsb, msb and set_bit are separated
into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
INCOMPATIBILITY.
--- a/src/HOL/Word/Misc_msb.thy Wed Oct 07 11:31:51 2020 +0200
+++ b/src/HOL/Word/Misc_msb.thy Wed Oct 07 10:39:14 2020 +0200
@@ -73,6 +73,11 @@
end
+lemma msb_word_iff_bit:
+ \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close>
+ for w :: \<open>'a::len word\<close>
+ by (simp add: msb_word_def bin_sign_def bit_uint_iff)
+
lemma word_msb_def:
"msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
by (simp add: msb_word_def sint_uint)
@@ -80,6 +85,10 @@
lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
by (simp add: msb_word_eq bit_last_iff)
+lemma msb_word_iff_sless_0:
+ \<open>msb w \<longleftrightarrow> w <s 0\<close>
+ by (simp add: word_msb_sint word_sless_alt)
+
lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
--- a/src/HOL/Word/More_Word.thy Wed Oct 07 11:31:51 2020 +0200
+++ b/src/HOL/Word/More_Word.thy Wed Oct 07 10:39:14 2020 +0200
@@ -26,7 +26,7 @@
lemmas shiftl1_def = shiftl1_eq
lemmas shiftr1_def = shiftr1_eq
lemmas sshiftr1_def = sshiftr1_eq
-lemmas sshiftr_def = sshiftr_eq
+lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1
lemmas to_bl_def = to_bl_eq
lemmas ucast_def = ucast_eq
lemmas unat_def = unat_eq_nat_uint
--- a/src/HOL/Word/Reversed_Bit_Lists.thy Wed Oct 07 11:31:51 2020 +0200
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy Wed Oct 07 10:39:14 2020 +0200
@@ -1478,12 +1478,9 @@
lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
for w :: "'a::len word"
- apply (unfold sshiftr_eq)
- apply (induct n)
- prefer 2
- apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
- apply (rule butlast_take [THEN trans])
- apply (auto simp: word_size)
+ apply (simp_all add: word_size sshiftr_eq)
+ apply (rule nth_equalityI)
+ apply (simp_all add: word_size nth_to_bl bit_signed_drop_bit_iff)
done
lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
@@ -1495,17 +1492,15 @@
apply (auto simp: word_size)
done
-lemma take_sshiftr' [rule_format] :
- "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
+lemma take_sshiftr':
+ "n \<le> size w \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
for w :: "'a::len word"
- apply (unfold sshiftr_eq)
- apply (induct n)
- prefer 2
- apply (simp add: bl_sshiftr1)
- apply (rule impI)
- apply (rule take_butlast [THEN trans])
- apply (auto simp: word_size)
+ apply (auto simp add: sshiftr_eq hd_bl_sign_sint bin_sign_def not_le word_size sint_signed_drop_bit_eq)
+ apply (rule nth_equalityI)
+ apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
+ apply (rule nth_equalityI)
+ apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
done
lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
--- a/src/HOL/Word/Word.thy Wed Oct 07 11:31:51 2020 +0200
+++ b/src/HOL/Word/Word.thy Wed Oct 07 10:39:14 2020 +0200
@@ -1306,6 +1306,10 @@
by (simp add: of_nat_div)
qed
+lemma unat_drop_bit_eq:
+ \<open>unat (drop_bit n w) = drop_bit n (unat w)\<close>
+ by (rule bit_eqI) (simp add: bit_unsigned_iff bit_drop_bit_eq)
+
lemma uint_mod_distrib:
\<open>uint (v mod w) = uint v mod uint w\<close>
proof -
@@ -1605,38 +1609,54 @@
subsection \<open>Ordering\<close>
-lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <=s _)\<close> [50, 51] 50)
- is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k \<le> signed_take_bit (LENGTH('a) - 1) l\<close>
+lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
+ is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k \<le> signed_take_bit (LENGTH('a) - Suc 0) l\<close>
+ by (simp flip: signed_take_bit_decr_length_iff)
+
+lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
+ is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k < signed_take_bit (LENGTH('a) - Suc 0) l\<close>
by (simp flip: signed_take_bit_decr_length_iff)
+notation
+ word_sle ("'(\<le>s')") and
+ word_sle ("(_/ \<le>s _)" [51, 51] 50) and
+ word_sless ("'(<s')") and
+ word_sless ("(_/ <s _)" [51, 51] 50)
+
+notation (input)
+ word_sle ("(_/ <=s _)" [51, 51] 50)
+
lemma word_sle_eq [code]:
\<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
by transfer simp
-
-lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <s _)\<close> [50, 51] 50)
- is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k < signed_take_bit (LENGTH('a) - 1) l\<close>
- by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma word_sless_eq:
- \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
- by transfer (simp add: signed_take_bit_decr_length_iff less_le)
lemma [code]:
\<open>a <s b \<longleftrightarrow> sint a < sint b\<close>
by transfer simp
+lemma signed_ordering: \<open>ordering word_sle word_sless\<close>
+ apply (standard; transfer)
+ apply simp_all
+ using signed_take_bit_decr_length_iff apply force
+ using signed_take_bit_decr_length_iff apply force
+ done
+
+lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
+ by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
+
+interpretation signed: linorder word_sle word_sless
+ by (fact signed_linorder)
+
+lemma word_sless_eq:
+ \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
+ by (fact signed.less_le)
+
lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
by (fact word_less_def)
-lemma signed_linorder: "class.linorder word_sle word_sless"
- by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
-
-interpretation signed: linorder "word_sle" "word_sless"
- by (rule signed_linorder)
-
lemma word_zero_le [simp]: "0 \<le> y"
for y :: "'a::len word"
- by transfer simp
+ by (fact word_coorder.extremum)
lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
@@ -1996,6 +2016,32 @@
subsection \<open>More shift operations\<close>
+lift_definition signed_drop_bit :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a::len word\<close>
+ is \<open>\<lambda>n. drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)\<close>
+ using signed_take_bit_decr_length_iff
+ by (simp add: take_bit_drop_bit) force
+
+lemma bit_signed_drop_bit_iff:
+ \<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
+ for w :: \<open>'a::len word\<close>
+ apply transfer
+ apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
+ apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff)
+ apply (metis le_antisym less_eq_decr_length_iff)
+ done
+
+lemma signed_drop_bit_0 [simp]:
+ \<open>signed_drop_bit 0 w = w\<close>
+ by transfer simp
+
+lemma sint_signed_drop_bit_eq:
+ \<open>sint (signed_drop_bit n w) = drop_bit n (sint w)\<close>
+ apply (cases \<open>LENGTH('a)\<close>; cases n)
+ apply simp_all
+ apply (rule bit_eqI)
+ apply (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
+ done
+
lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) k div 2)\<close>
by (simp flip: signed_take_bit_decr_length_iff)
@@ -2012,7 +2058,7 @@
\<open>sshiftr1 w = word_of_int (sint w div 2)\<close>
by transfer simp
-lemma sshiftr_eq:
+lemma sshiftr_eq_funpow_sshiftr1:
\<open>w >>> n = (sshiftr1 ^^ n) w\<close>
proof -
have *: \<open>(\<lambda>k::int. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
@@ -3981,6 +4027,10 @@
using le_less_Suc_eq apply fastforce
done
+lemma sshiftr_eq:
+ \<open>w >>> m = signed_drop_bit m w\<close>
+ by (rule bit_eqI) (simp add: bit_signed_drop_bit_iff bit_sshiftr_word_iff)
+
lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
apply transfer
apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc)