1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Bitwise tactic for Signed Words"
8
9theory WordBitwise_Signed
10imports
11  "HOL-Word.More_Word"
12  Signed_Words
13begin
14
15ML \<open>fun bw_tac_signed ctxt = let
16  val (ss, sss) = Word_Bitwise_Tac.expand_word_eq_sss
17  val sss = nth_map 2 (fn ss => put_simpset ss ctxt addsimps @{thms len_signed} |> simpset_of) sss
18in
19    foldr1 (op THEN_ALL_NEW)
20      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
21        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
22  end;
23\<close>
24
25method_setup word_bitwise_signed =
26  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (bw_tac_signed ctxt 1))\<close>
27  "decomposer for word equalities and inequalities into bit propositions"
28
29end
30