--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Wed Oct 28 08:41:07 2020 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Thu Oct 29 09:59:40 2020 +0000
@@ -5,7 +5,7 @@
section \<open>Word examples for for SMT binding\<close>
theory SMT_Word_Examples
-imports "HOL-Word.Word" "HOL-Word.Traditional_Syntax"
+imports "HOL-Word.Word"
begin
declare [[smt_oracle = true]]
@@ -44,9 +44,9 @@
lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt
lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
-lemma "0b10011 << 2 = (0b1001100::8 word)" by smt
-lemma "0b11001 >> 2 = (0b110::8 word)" by smt
-lemma "0b10011 >>> 2 = (0b100::8 word)" by smt
+lemma "push_bit 2 0b10011 = (0b1001100::8 word)" by smt
+lemma "drop_bit 2 0b11001 = (0b110::8 word)" by smt
+lemma "signed_drop_bit 2 0b10011 = (0b100::8 word)" by smt
lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
--- a/src/HOL/SPARK/Manual/Reference.thy Wed Oct 28 08:41:07 2020 +0100
+++ b/src/HOL/SPARK/Manual/Reference.thy Thu Oct 29 09:59:40 2020 +0000
@@ -1,8 +1,11 @@
(*<*)
theory Reference
-imports "HOL-SPARK.SPARK" "HOL-Word.Bits_Int"
+imports "HOL-SPARK.SPARK"
begin
+lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int
+ by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod)
+
syntax (my_constrain output)
"_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
(*>*)
--- a/src/HOL/Word/Tools/smt_word.ML Wed Oct 28 08:41:07 2020 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML Thu Oct 29 09:59:40 2020 +0000
@@ -56,6 +56,18 @@
val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
+ 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 (Term.range_type T)
+ in
+ (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
+ (true, SOME i) =>
+ SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T))
+ | _ => NONE) (* FIXME: also support non-numerical shifts *)
+ end
+
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)
@@ -68,18 +80,6 @@
| _ => 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) 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_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
fun extract m n T ts =
--- a/src/HOL/Word/Traditional_Syntax.thy Wed Oct 28 08:41:07 2020 +0100
+++ b/src/HOL/Word/Traditional_Syntax.thy Thu Oct 29 09:59:40 2020 +0000
@@ -523,12 +523,4 @@
"x << 0 = (x :: 'a :: len word)"
by (fact shiftl_x_0)
-setup \<open>
- Context.theory_map (fold SMT_Word.add_word_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")
- ])
-\<close>
-
end