--- 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") ] #>
--- 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