# HG changeset patch
# User haftmann
# Date 1602954640 -7200
# Node ID a1366ce413682b2654410e3846b7b08add83766d
# Parent  ee659bca8955baf931be1c9a9618e58e1f1aedb1
early and more complete setup of tools

diff -r ee659bca8955 -r a1366ce41368 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Sat Oct 17 18:56:36 2020 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML	Sat Oct 17 19:10:40 2020 +0200
@@ -51,13 +51,25 @@
 
   val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
 
-  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+  fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+    | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts)
+
+  fun shift' m n T ts =
+    let val U = Term.domain_type T
+    in
+      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
+        (true, SOME i) =>
+          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T))
+      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
+    end
+
+  fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t
     | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
 
   fun shift m n T ts =
     let val U = Term.domain_type T
     in
-      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
+      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
@@ -110,6 +122,10 @@
     (\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
     (\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
   fold (add_word_fun shift) [
+    (\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
+    (\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
+    (\<^term>\<open>signed_drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
+  fold (add_word_fun shift') [
     (\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
     (\<^term>\<open>shiftr :: 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
     (\<^term>\<open>sshiftr :: 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
diff -r ee659bca8955 -r a1366ce41368 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Oct 17 18:56:36 2020 +0200
+++ b/src/HOL/Word/Word.thy	Sat Oct 17 19:10:40 2020 +0200
@@ -130,6 +130,11 @@
   by transfer simp
 
 
+subsubsection \<open>Basic tool setup\<close>
+
+ML_file \<open>Tools/word_lib.ML\<close>
+
+
 subsubsection \<open>Basic code generation setup\<close>
 
 context
@@ -5095,9 +5100,8 @@
   by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I)
 
 
-subsection \<open>Misc\<close>
-
-ML_file \<open>Tools/word_lib.ML\<close>
+subsection \<open>SMT support\<close>
+
 ML_file \<open>Tools/smt_word.ML\<close>
 
 end