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