# HG changeset patch
# User haftmann
# Date 1603965580 0
# Node ID d8661799afb25ef1be44ca5605849707d8854813
# Parent  75f5c63f6cfa170468744a3bb0a8a00f28b25649
removed dependency

diff -r 75f5c63f6cfa -r d8661799afb2 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- 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
diff -r 75f5c63f6cfa -r d8661799afb2 src/HOL/SPARK/Manual/Reference.thy
--- 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)
 (*>*)
diff -r 75f5c63f6cfa -r d8661799afb2 src/HOL/Word/Tools/smt_word.ML
--- 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 =
diff -r 75f5c63f6cfa -r d8661799afb2 src/HOL/Word/Traditional_Syntax.thy
--- 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