# HG changeset patch
# User haftmann
# Date 1602059954 -7200
# Node ID 633d14bd1e59eefaa76f502055dd8d773555b83b
# Parent  04be6716cac617d72c557eb13b866eea8b1c0299
consolidated for the sake of documentation

diff -r 04be6716cac6 -r 633d14bd1e59 NEWS
--- 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.
diff -r 04be6716cac6 -r 633d14bd1e59 src/HOL/Word/Misc_msb.thy
--- 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)
 
diff -r 04be6716cac6 -r 633d14bd1e59 src/HOL/Word/More_Word.thy
--- 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
diff -r 04be6716cac6 -r 633d14bd1e59 src/HOL/Word/Reversed_Bit_Lists.thy
--- 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]
diff -r 04be6716cac6 -r 633d14bd1e59 src/HOL/Word/Word.thy
--- 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)