diff --git a/thys/Native_Word/Code_Target_Word_Base.thy b/thys/Native_Word/Code_Target_Word_Base.thy
--- a/thys/Native_Word/Code_Target_Word_Base.thy
+++ b/thys/Native_Word/Code_Target_Word_Base.thy
@@ -1,443 +1,439 @@
 (*  Title:      Code_Target_Word_Base.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Common base for target language implementations of word types\<close>
 
 theory Code_Target_Word_Base imports
   "HOL-Word.Word"
   Bits_Integer
 begin
 
 text \<open>More lemmas\<close>
 
 lemma nat_div_eq_Suc_0_iff: "n div m = Suc 0 \<longleftrightarrow> m \<le> n \<and> n < 2 * m"
   apply auto
   using div_greater_zero_iff apply fastforce
    apply (metis One_nat_def div_greater_zero_iff dividend_less_div_times mult.right_neutral mult_Suc mult_numeral_1 numeral_2_eq_2 zero_less_numeral)
   apply (simp add: div_nat_eqI)
   done
 
 lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)"
   by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power)
 
 lemma div_half_nat:
   fixes x y :: nat
   assumes "y \<noteq> 0"
   shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y \<le> r then (q + 1, r - y) else (q, r))"
 proof -
   let ?q = "2 * (x div 2 div y)"
   have q: "?q = x div y - x div y mod 2"
     by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric])
   let ?r = "x - ?q * y"
   have r: "?r = x mod y + x div y mod 2 * y"
     by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute)
 
   show ?thesis
   proof(cases "y \<le> x - ?q * y")
     case True
     with assms q have "x div y mod 2 \<noteq> 0" unfolding r
       by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1)) 
     hence "x div y = ?q + 1" unfolding q
       by simp
     moreover hence "x mod y = ?r - y"
       by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc)
     ultimately show ?thesis using True by(simp add: Let_def)
   next
     case False
     hence "x div y mod 2 = 0" unfolding r
       by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute)
     hence "x div y = ?q" unfolding q by simp
     moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric])
     ultimately show ?thesis using False by(simp add: Let_def)
   qed
 qed
 
 lemma unat_p2: "n < LENGTH('a :: len) \<Longrightarrow> unat (2 ^ n :: 'a word) = 2 ^ n"
 proof(induct n)
   case 0 thus ?case by simp
 next
   case (Suc n)
   then obtain n' where "LENGTH('a) = Suc n'" by(cases "LENGTH('a)") simp_all
   with Suc show ?case by (simp add: unat_word_ariths bintrunc_mod2p)
 qed
 
 lemma word_div_lt_eq_0:
   "x < y \<Longrightarrow> x div y = 0" for x :: "'a :: len word"
   by (simp add: word_eq_iff word_less_def word_test_bit_def uint_div)
 
 lemma word_div_eq_1_iff: "n div m = 1 \<longleftrightarrow> n \<ge> m \<and> unat n < 2 * unat (m :: 'a :: len word)"
 apply(simp only: word_arith_nat_defs word_le_nat_alt nat_div_eq_Suc_0_iff[symmetric])
 apply(rule word_unat.Abs_inject)
  apply(simp only: unat_div[symmetric] word_unat.Rep)
 apply(simp add: unats_def Suc_0_lt_2p_len_of)
 done
 
 lemma div_half_word:
   fixes x y :: "'a :: len word"
   assumes "y \<noteq> 0"
   shows "(x div y, x mod y) = (let q = (x >> 1) div y << 1; r = x - q * y in if y \<le> r then (q + 1, r - y) else (q, r))"
 proof -
   obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (cases x)
   moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)" by (cases y)
   ultimately have [simp]: \<open>unat (of_nat n :: 'a word) = n\<close> \<open>unat (of_nat m :: 'a word) = m\<close>
     by (simp add: unat_def, transfer, simp_all add: take_bit_of_nat take_bit_eq_self)+
   let ?q = "(x >> 1) div y << 1"
   let ?q' = "2 * (n div 2 div m)"
   have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse unat_lt2p uno_simps(2))
   hence q: "?q = of_nat ?q'" using n m
     apply (auto simp add: shiftr_word_eq drop_bit_eq_div shiftl_t2n word_arith_nat_div uno_simps)
     apply (metis \<open>unat (of_nat n) = n\<close> uno_simps(2))
     done
   from assms have "m \<noteq> 0" using m by -(rule notI, simp)
 
   from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)"
     by(metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unat_lt2p uno_simps(2))
   moreover
   have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric]
     by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq)
   moreover have "2 * (n div 2 div m) * m \<le> n"
     by (metis div_mult2_eq dtle mult.assoc mult.left_commute)
   ultimately
   have r: "x - ?q * y = of_nat (n - ?q' * m)"
     and "y \<le> x - ?q * y \<Longrightarrow> of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)"
     using n m unfolding q
     by (simp_all add: word_sub_wi word_mult_def uint_nat unat_of_nat of_nat_mult [symmetric] word_of_nat[symmetric] of_nat_diff word_le_nat_alt del: of_nat_mult)
       (metis diff_diff_left less_imp_diff_less of_nat_diff of_nat_inverse word_of_nat)
   thus ?thesis using n m div_half_nat[OF \<open>m \<noteq> 0\<close>, of n] unfolding q
     by(simp add: word_le_nat_alt word_div_def word_mod_def uint_nat unat_of_nat zmod_int[symmetric] zdiv_int[symmetric] word_of_nat[symmetric])(simp add: Let_def split del: if_split split: if_split_asm)
 qed
 
 lemma word_test_bit_set_bits: "(BITS n. f n :: 'a :: len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> f n"
-by(auto simp add: word_set_bits_def test_bit_bl word_bl.Abs_inverse word_size)
+  by (simp add: test_bit_eq_bit bit_set_bits_word_iff)
 
 lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. i !! n)"
   by (rule word_eqI) (auto simp add: word_test_bit_set_bits test_bit.eq_norm)
 
 lemma word_and_mask_or_conv_and_mask:
   "n !! index \<Longrightarrow> (n AND mask index) OR (1 << index) = n AND mask (index + 1)"
 by(rule word_eqI)(auto simp add: word_ao_nth word_size nth_shiftl simp del: shiftl_1)
 
 lemma uint_and_mask_or_full:
   fixes n :: "'a :: len word"
   assumes "n !! (LENGTH('a) - 1)"
   and "mask1 = mask (LENGTH('a) - 1)"
   and "mask2 = 1 << LENGTH('a) - 1"
   shows "uint (n AND mask1) OR mask2 = uint n"
 proof -
   have "mask2 = uint (1 << LENGTH('a) - 1 :: 'a word)" using assms
     by (simp add: uint_shiftl word_size bintrunc_shiftl del: shiftl_1)
   hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (1 << LENGTH('a) - 1 :: 'a word))"
     by(simp add: uint_or)
   also have "\<dots> = uint (n AND mask (LENGTH('a) - 1 + 1))"
     using assms by(simp only: word_and_mask_or_conv_and_mask)
   also have "\<dots> = uint n" by simp
   finally show ?thesis .
 qed
 
 
 text \<open>Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.\<close>
 
 definition word_sdiv :: "'a :: len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixl "sdiv" 70)
 where [code]:
   "x sdiv y =
    (let x' = sint x; y' = sint y;
         negative = (x' < 0) \<noteq> (y' < 0);
         result = abs x' div abs y'
     in word_of_int (if negative then -result else result))"
 
 definition word_smod :: "'a :: len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixl "smod" 70)
 where [code]:
   "x smod y =
    (let x' = sint x; y' = sint y;
         negative = (x' < 0);
         result = abs x' mod abs y'
     in word_of_int (if negative then -result else result))"
 
 lemma sdiv_smod_id: "(a sdiv b) * b + (a smod b) = a"
 proof -
   note [simp] = word_sdiv_def word_smod_def
   have F5: "\<forall>u::'a word. - (- u) = u" by (metis minus_minus)
   have F7: "\<forall>v u::'a word. u + v = v + u" by(metis add.left_commute add_0_right)
   have F8: "\<forall>(w::'a word) (v::int) u::int. word_of_int u + word_of_int v * w = word_of_int (u + v * sint w)"
     by (metis word_sint.Rep_inverse wi_hom_syms(1) wi_hom_syms(3))
   have "\<exists>u. u = - sint b \<and> word_of_int (sint a mod u + - (- u * (sint a div u))) = a"
     using F5 by (metis minus_minus word_sint.Rep_inverse' mult_minus_left add.commute mult_div_mod_eq [symmetric])
   hence "word_of_int (sint a mod - sint b + - (sint b * (sint a div - sint b))) = a" by (metis equation_minus_iff)
   hence "word_of_int (sint a mod - sint b) + word_of_int (- (sint a div - sint b)) * b = a"
     using F8 by(metis mult.commute mult_minus_left)
   hence eq: "word_of_int (- (sint a div - sint b)) * b + word_of_int (sint a mod - sint b) = a" using F7 by metis
 
   show ?thesis
   proof(cases "sint a < 0")
     case True note a = this
     show ?thesis
     proof(cases "sint b < 0")
       case True
       with a show ?thesis
         by simp (metis F7 F8 eq minus_equation_iff minus_mult_minus mod_div_mult_eq)
     next
       case False
       from eq have "word_of_int (- (- sint a div sint b)) * b + word_of_int (- (- sint a mod sint b)) = a"
         by (metis div_minus_right mod_minus_right)
       with a False show ?thesis by simp
     qed
   next
     case False note a = this
     show ?thesis
     proof(cases "sint b < 0")
       case True
       with a eq show ?thesis by simp
     next
       case False with a show ?thesis
         by simp (metis wi_hom_add wi_hom_mult add.commute mult.commute word_sint.Rep_inverse add.commute mult_div_mod_eq [symmetric])
     qed
   qed
 qed
 
 text \<open>
   This algorithm implements unsigned division in terms of signed division.
   Taken from Hacker's Delight.
 \<close>
 
 lemma divmod_via_sdivmod:
   fixes x y :: "'a :: len word"
   assumes "y \<noteq> 0"
   shows
   "(x div y, x mod y) =
   (if 1 << (LENGTH('a) - 1) \<le> y then if x < y then (0, x) else (1, x - y)
    else let q = ((x >> 1) sdiv y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 proof(cases "1 << (LENGTH('a) - 1) \<le> y")
   case True
   note y = this
   show ?thesis
   proof(cases "x < y")
     case True
     then have "x mod y = x"
       by (cases x, cases y) (simp add: word_less_def word_mod_def)
     thus ?thesis using True y by(simp add: word_div_lt_eq_0)
   next
     case False
     obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)" by(cases y)
     have "unat x < 2 ^ LENGTH('a)" by(rule unat_lt2p)
     also have "\<dots> = 2 * 2 ^ (LENGTH('a) - 1)"
       by(metis Suc_pred len_gt_0 power_Suc One_nat_def)
     also have "\<dots> \<le> 2 * n" using y n
       by(simp add: word_le_nat_alt unat_of_nat unat_p2)
     finally have div: "x div of_nat n = 1" using False n
       by(simp add: word_div_eq_1_iff not_less word_le_nat_alt unat_of_nat)
     moreover have "x mod y = x - x div y * y"
       by (simp add: minus_div_mult_eq_mod)
     with div n have "x mod y = x - y" by simp
     ultimately show ?thesis using False y n by simp
   qed
 next
   case False
   note y = this
   obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by(cases x)
   hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
     by (cases "LENGTH('a)")
       (simp_all, simp only: of_nat_numeral [where ?'a = int, symmetric]
       zdiv_int [symmetric] of_nat_power [symmetric])
   with y n have "sint (x >> 1) = uint (x >> 1)"
     by (simp add: sint_uint sbintrunc_mod2p shiftr_div_2n) (simp add: uint_nat unat_of_nat)
   moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
     using y by (cases "LENGTH('a)")
       (simp_all add: not_le word_2p_lem word_size)
   then have "sint y = uint y"
     by (simp add: sint_uint sbintrunc_mod2p)
   ultimately show ?thesis using y
     by(subst div_half_word[OF assms])(simp add: word_sdiv_def uint_div[symmetric])
 qed
 
 
 text \<open>More implementations tailored towards target-language implementations\<close>
 
 context
 includes integer.lifting
 begin
 lift_definition word_of_integer :: "integer \<Rightarrow> 'a :: len word" is word_of_int .
 
 lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)"
 by(simp add: word_of_integer.rep_eq)
 end
 
 lemma word_of_int_code [code abstract]:
   "uint (word_of_int x :: 'a word) = x AND bin_mask (LENGTH('a :: len))"
 by(simp add: uint_word_of_int and_bin_mask_conv_mod)
 
 context fixes f :: "nat \<Rightarrow> bool" begin
 
-lemma bit_set_bits_word_iff:
-  \<open>bit (set_bits f :: 'a word) n \<longleftrightarrow> n < LENGTH('a::len) \<and> f n\<close>
-  by (auto simp add: of_nth_def test_bit_of_bl simp flip: test_bit_word_eq)
-
 definition set_bits_aux :: \<open>'a word \<Rightarrow> nat \<Rightarrow> 'a :: len word\<close>
   where \<open>set_bits_aux w n = push_bit n w OR take_bit n (set_bits f)\<close>
 
 lemma set_bits_aux_conv:
   \<open>set_bits_aux w n = (w << n) OR (set_bits f AND mask n)\<close>
   by (rule bit_word_eqI)
     (auto simp add: set_bits_aux_def shiftl_word_eq mask_eq_mask bit_and_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_mask_iff bit_set_bits_word_iff exp_eq_zero_iff)
 
 corollary set_bits_conv_set_bits_aux:
   \<open>set_bits f = (set_bits_aux 0 (LENGTH('a)) :: 'a :: len word)\<close>
   by (simp add: set_bits_aux_conv)
 
 lemma set_bits_aux_0 [simp]:
   \<open>set_bits_aux w 0 = w\<close>
   by  (simp add: set_bits_aux_conv)
 
 lemma set_bits_aux_Suc [simp]:
   \<open>set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n\<close>
   by (simp add: set_bits_aux_def shiftl_word_eq bit_eq_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_set_bits_word_iff)
     (auto simp add: bit_exp_iff not_less bit_1_iff less_Suc_eq_le exp_eq_zero_iff)
 
 lemma set_bits_aux_simps [code]:
   \<open>set_bits_aux w 0 = w\<close>
   \<open>set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n\<close>
   by simp_all
 
 end
 
 lemma word_of_int_via_signed:
   fixes mask
   assumes mask_def: "mask = bin_mask (LENGTH('a))"
   and shift_def: "shift = 1 << LENGTH('a)"
   and index_def: "index = LENGTH('a) - 1"
   and overflow_def:"overflow = 1 << (LENGTH('a) - 1)"
   and least_def: "least = - overflow"
   shows
   "(word_of_int i :: 'a :: len word) =
    (let i' = i AND mask
     in if i' !! index then
          if i' - shift < least \<or> overflow \<le> i' - shift then arbitrary1 i' else word_of_int (i' - shift)
        else if i' < least \<or> overflow \<le> i' then arbitrary2 i' else word_of_int i')"
 proof -
   define i' where "i' = i AND mask"
   have "shift = mask + 1" unfolding assms by(simp add: bin_mask_p1_conv_shift)
   hence "i' < shift" by(simp add: mask_def i'_def int_and_le)
   show ?thesis
   proof(cases "i' !! index")
     case True
     hence unf: "i' = overflow OR i'" unfolding assms i'_def
       by(auto intro!: bin_eqI simp add: bin_nth_ops)
     have "overflow \<le> i'" by(subst unf)(rule le_int_or, simp add: bin_sign_and assms i'_def)
     hence "i' - shift < least \<longleftrightarrow> False" unfolding assms
       by(cases "LENGTH('a)")(simp_all add: not_less)
     moreover
     have "overflow \<le> i' - shift \<longleftrightarrow> False" using \<open>i' < shift\<close> unfolding assms
       by(cases "LENGTH('a)")(auto simp add: not_le elim: less_le_trans)
     moreover
     have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using \<open>i' < shift\<close>
       by(auto intro!: word_eqI simp add: i'_def shift_def mask_def bin_nth_ops bin_nth_minus_p2 bin_sign_and)
     ultimately show ?thesis using True by(simp add: Let_def i'_def)
   next
     case False
     hence "i' = i AND bin_mask (LENGTH('a) - 1)" unfolding assms i'_def
       by(clarsimp simp add: i'_def bin_nth_ops intro!: bin_eqI)(cases "LENGTH('a)", auto simp add: less_Suc_eq)
     also have "\<dots> \<le> bin_mask (LENGTH('a) - 1)" by(rule int_and_le) simp
     also have "\<dots> < overflow" unfolding overflow_def
       by(simp add: bin_mask_p1_conv_shift[symmetric])
     also
     have "least \<le> 0" unfolding least_def overflow_def by simp
     have "0 \<le> i'" by(simp add: i'_def mask_def bin_mask_ge0)
     hence "least \<le> i'" using \<open>least \<le> 0\<close> by simp
     moreover
     have "word_of_int i' = (word_of_int i :: 'a word)"
       by(rule word_eqI)(auto simp add: i'_def bin_nth_ops mask_def)
     ultimately show ?thesis using False by(simp add: Let_def i'_def)
   qed
 qed
 
 
 
 text \<open>Quickcheck conversion functions\<close>
 
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 definition qc_random_cnv ::
   "(natural \<Rightarrow> 'a::term_of) \<Rightarrow> natural \<Rightarrow> Random.seed
     \<Rightarrow> ('a \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
   where "qc_random_cnv a_of_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
        let n = a_of_natural k
        in (n, \<lambda>_. Code_Evaluation.term_of n)))"
 
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 definition qc_exhaustive_cnv :: "(natural \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> (bool \<times> term list) option)
   \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
 where
   "qc_exhaustive_cnv a_of_natural f d =
    Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d"
 
 definition qc_full_exhaustive_cnv ::
   "(natural \<Rightarrow> ('a::term_of)) \<Rightarrow> ('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
   \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
 where
   "qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive
   (%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d"
 
 declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]]
 
 definition qc_narrowing_drawn_from :: "'a list \<Rightarrow> integer \<Rightarrow> _"
 where
   "qc_narrowing_drawn_from xs =
    foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))"
 
 locale quickcheck_narrowing_samples =
   fixes a_of_integer :: "integer \<Rightarrow> 'a \<times> 'a :: {partial_term_of, term_of}"
   and zero :: "'a"
   and tr :: "typerep"
 begin
 
 function narrowing_samples :: "integer \<Rightarrow> 'a list"
 where
   "narrowing_samples i =
    (if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])"
 by pat_completeness auto
 termination including integer.lifting
 proof(relation "measure nat_of_integer")
   fix i :: integer
   assume "0 < i"
   thus "(i - 1, i) \<in> measure nat_of_integer"
     by simp(transfer, simp)
 qed simp
 
 definition partial_term_of_sample :: "integer \<Rightarrow> 'a"
 where
   "partial_term_of_sample i =
   (if i < 0 then undefined
    else if i = 0 then zero
    else if i mod 2 = 0 then snd (a_of_integer (i div 2))
    else fst (a_of_integer (i div 2 + 1)))"
 
 lemma partial_term_of_code:
   "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') tr"
   "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) \<equiv>
    Code_Evaluation.term_of (partial_term_of_sample i)"
 by (rule partial_term_of_anything)+
 
 end
 
 lemmas [code] =
   quickcheck_narrowing_samples.narrowing_samples.simps
   quickcheck_narrowing_samples.partial_term_of_sample_def
 
 
 text \<open>
   The separate code target \<open>SML_word\<close> collects setups for the
   code generator that PolyML does not provide.
 \<close>
 
 setup \<open>Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])\<close>
 
 code_identifier code_module Code_Target_Word_Base \<rightharpoonup>
   (SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word
 
 export_code sbintrunc bin_mask in SML module_name Code
 
 end
diff --git a/thys/Native_Word/More_Bits_Int.thy b/thys/Native_Word/More_Bits_Int.thy
--- a/thys/Native_Word/More_Bits_Int.thy
+++ b/thys/Native_Word/More_Bits_Int.thy
@@ -1,281 +1,280 @@
 (*  Title:      Bits_Int.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>More bit operations on integers\<close>
 
 theory More_Bits_Int
 imports
   "HOL-Word.Bits_Int"
   "HOL-Word.Bit_Comprehension"
 begin
 
 text \<open>Preliminaries\<close>
 
 lemma last_rev' [simp]: "last (rev xs) = hd xs" \<comment> \<open>TODO define \<open>last []\<close> as \<open>hd []\<close>?\<close>
   by (cases xs) (simp add: last_def hd_def, simp)
 
 lemma nat_LEAST_True: "(LEAST _ :: nat. True) = 0"
   by (rule Least_equality) simp_all
 
 text \<open>
   Use this function to convert numeral @{typ integer}s quickly into @{typ int}s.
   By default, it works only for symbolic evaluation; normally generated code raises
   an exception at run-time. If theory \<open>Code_Target_Bits_Int\<close> is imported,
   it works again, because then @{typ int} is implemented in terms of @{typ integer}
   even for symbolic evaluation.
 \<close>
 
 definition int_of_integer_symbolic :: "integer \<Rightarrow> int"
   where "int_of_integer_symbolic = int_of_integer"
 
 lemma int_of_integer_symbolic_aux_code [code nbe]:
   "int_of_integer_symbolic 0 = 0"
   "int_of_integer_symbolic (Code_Numeral.Pos n) = Int.Pos n"
   "int_of_integer_symbolic (Code_Numeral.Neg n) = Int.Neg n"
   by (simp_all add: int_of_integer_symbolic_def)
 
 code_identifier
   code_module Bits_Int \<rightharpoonup>
   (SML) Bit_Operations and (OCaml) Bit_Operations and (Haskell) Bit_Operations and (Scala) Bit_Operations
 | code_module More_Bits_Int \<rightharpoonup>
   (SML) Bit_Operations and (OCaml) Bit_Operations and (Haskell) Bit_Operations and (Scala) Bit_Operations
 | constant take_bit \<rightharpoonup>
   (SML) Bit_Operations.take_bit and (OCaml) Bit_Operations.take_bit and (Haskell) Bit_Operations.take_bit and (Scala) Bit_Operations.take_bit
 
 
 section \<open>Symbolic bit operations on numerals and @{typ int}s\<close>
 
 fun bitOR_num :: "num \<Rightarrow> num \<Rightarrow> num"
 where
   "bitOR_num num.One num.One = num.One"
 | "bitOR_num num.One (num.Bit0 n) = num.Bit1 n"
 | "bitOR_num num.One (num.Bit1 n) = num.Bit1 n"
 | "bitOR_num (num.Bit0 m) num.One = num.Bit1 m"
 | "bitOR_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (bitOR_num m n)"
 | "bitOR_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"
 | "bitOR_num (num.Bit1 m) num.One = num.Bit1 m"
 | "bitOR_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (bitOR_num m n)"
 | "bitOR_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"
 
 fun bitAND_num :: "num \<Rightarrow> num \<Rightarrow> num option"
 where
   "bitAND_num num.One num.One = Some num.One"
 | "bitAND_num num.One (num.Bit0 n) = None"
 | "bitAND_num num.One (num.Bit1 n) = Some num.One"
 | "bitAND_num (num.Bit0 m) num.One = None"
 | "bitAND_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
 | "bitAND_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitAND_num m n)"
 | "bitAND_num (num.Bit1 m) num.One = Some num.One"
 | "bitAND_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
 | "bitAND_num (num.Bit1 m) (num.Bit1 n) = (case bitAND_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))"
 
 fun bitXOR_num :: "num \<Rightarrow> num \<Rightarrow> num option"
 where
   "bitXOR_num num.One num.One = None"
 | "bitXOR_num num.One (num.Bit0 n) = Some (num.Bit1 n)"
 | "bitXOR_num num.One (num.Bit1 n) = Some (num.Bit0 n)"
 | "bitXOR_num (num.Bit0 m) num.One = Some (num.Bit1 m)"
 | "bitXOR_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitXOR_num m n)"
 | "bitXOR_num (num.Bit0 m) (num.Bit1 n) = Some (case bitXOR_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')"
 | "bitXOR_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
 | "bitXOR_num (num.Bit1 m) (num.Bit0 n) = Some (case bitXOR_num m n of None \<Rightarrow> num.One | Some n' \<Rightarrow> num.Bit1 n')"
 | "bitXOR_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitXOR_num m n)"
 
 fun bitORN_num :: "num \<Rightarrow> num \<Rightarrow> num"
 where
   "bitORN_num num.One num.One = num.One"
 | "bitORN_num num.One (num.Bit0 m) = num.Bit1 m"
 | "bitORN_num num.One (num.Bit1 m) = num.Bit1 m"
 | "bitORN_num (num.Bit0 n) num.One = num.Bit0 num.One"
 | "bitORN_num (num.Bit0 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
 | "bitORN_num (num.Bit0 n) (num.Bit1 m) = num.Bit0 (bitORN_num n m)"
 | "bitORN_num (num.Bit1 n) num.One = num.One"
 | "bitORN_num (num.Bit1 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
 | "bitORN_num (num.Bit1 n) (num.Bit1 m) = Num.BitM (bitORN_num n m)"
 
 fun bitANDN_num :: "num \<Rightarrow> num \<Rightarrow> num option"
 where
   "bitANDN_num num.One num.One = None"
 | "bitANDN_num num.One (num.Bit0 n) = Some num.One"
 | "bitANDN_num num.One (num.Bit1 n) = None"
 | "bitANDN_num (num.Bit0 m) num.One = Some (num.Bit0 m)"
 | "bitANDN_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitANDN_num m n)"
 | "bitANDN_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"
 | "bitANDN_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
 | "bitANDN_num (num.Bit1 m) (num.Bit0 n) = (case bitANDN_num m n of None \<Rightarrow> Some num.One | Some n' \<Rightarrow> Some (num.Bit1 n'))"
 | "bitANDN_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"
 
 lemma int_numeral_bitOR_num: "numeral n OR numeral m = (numeral (bitOR_num n m) :: int)"
 by(induct n m rule: bitOR_num.induct) simp_all
 
 lemma int_numeral_bitAND_num: "numeral n AND numeral m = (case bitAND_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')"
 by(induct n m rule: bitAND_num.induct)(simp_all split: option.split)
 
 lemma int_numeral_bitXOR_num:
   "numeral m XOR numeral n = (case bitXOR_num m n of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')"
 by(induct m n rule: bitXOR_num.induct)(simp_all split: option.split)
 
 lemma int_or_not_bitORN_num:
   "numeral n OR NOT (numeral m) = (- numeral (bitORN_num n m) :: int)"
   by (induction n m rule: bitORN_num.induct) (simp_all add: add_One BitM_inc_eq)
 
 lemma int_and_not_bitANDN_num:
   "numeral n AND NOT (numeral m) = (case bitANDN_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')"
   by (induction n m rule: bitANDN_num.induct) (simp_all add: add_One BitM_inc_eq split: option.split)
 
 lemma int_not_and_bitANDN_num:
   "NOT (numeral m) AND numeral n = (case bitANDN_num n m of None \<Rightarrow> 0 :: int | Some n' \<Rightarrow> numeral n')"
 by(simp add: int_and_not_bitANDN_num[symmetric] int_and_comm)
 
 
 section \<open>Bit masks of type \<^typ>\<open>int\<close>\<close>
 
 primrec bin_mask :: "nat \<Rightarrow> int" 
 where
   "bin_mask 0 = 0"
 | "bin_mask (Suc n) = 1 + 2 * bin_mask n"
 
 lemma bin_mask_conv_pow2:
   "bin_mask n = 2 ^ n - 1"
   by (induct n) simp_all
 
 lemma bin_mask_eq_mask:
   \<open>bin_mask = Bit_Operations.mask\<close>
   by (simp add: bin_mask_conv_pow2 [abs_def] mask_eq_exp_minus_1 [abs_def])
   
 lemma bin_mask_ge0: "bin_mask n \<ge> 0"
 by(induct n) simp_all
 
 lemma and_bin_mask_conv_mod: "x AND bin_mask n = x mod 2 ^ n"
   by (rule bit_eqI)
     (simp add: bin_mask_eq_mask bit_and_iff bit_mask_iff bit_take_bit_iff ac_simps flip: take_bit_eq_mod)
 
 lemma bin_mask_numeral: 
   "bin_mask (numeral n) = 1 + 2 * bin_mask (pred_numeral n)"
 by(simp add: numeral_eq_Suc)
 
 lemma bin_nth_mask [simp]: "bin_nth (bin_mask n) i \<longleftrightarrow> i < n"
   by (simp add: bin_mask_eq_mask bit_mask_iff)
 
 lemma bin_sign_mask [simp]: "bin_sign (bin_mask n) = 0"
   by (simp add: bin_sign_def bin_mask_conv_pow2)
 
 lemma bin_mask_p1_conv_shift: "bin_mask n + 1 = 1 << n"
   by (simp add: bin_mask_conv_pow2 shiftl_int_def)
 
 
 section \<open>More on bit comprehension\<close>
 
 inductive wf_set_bits_int :: "(nat \<Rightarrow> bool) \<Rightarrow> bool" 
   for f :: "nat \<Rightarrow> bool"
 where
   zeros: "\<forall>n' \<ge> n. \<not> f n' \<Longrightarrow> wf_set_bits_int f"
 | ones: "\<forall>n' \<ge> n. f n' \<Longrightarrow> wf_set_bits_int f"
 
 lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))"
 by(auto simp add: wf_set_bits_int.simps)
 
 lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\<lambda>_. b)"
 by(cases b)(auto intro: wf_set_bits_int.intros)
 
 lemma wf_set_bits_int_fun_upd [simp]: 
   "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
   then obtain n'
     where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')"
     by(auto simp add: wf_set_bits_int_simps)
   hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto
   thus ?rhs by(auto simp only: wf_set_bits_int_simps)
 next
   assume ?rhs
   then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'")
     by(auto simp add: wf_set_bits_int_simps)
   hence "?wf (f(n := b)) (max (Suc n) n')" by auto
   thus ?lhs by(auto simp only: wf_set_bits_int_simps)
 qed
 
 lemma wf_set_bits_int_Suc [simp]:
   "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
 by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D)
 
 context
   fixes f
   assumes wff: "wf_set_bits_int f"
 begin
 
 lemma int_set_bits_unfold_BIT:
   "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \<circ> Suc)"
 using wff proof cases
   case (zeros n)
   show ?thesis
   proof(cases "\<forall>n. \<not> f n")
     case True
     hence "f = (\<lambda>_. False)" by auto
     thus ?thesis using True by(simp add: o_def)
   next
     case False
     then obtain n' where "f n'" by blast
     with zeros have "(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')"
       by(auto intro: Least_Suc)
     also have "(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))" by(auto dest: Suc_le_D)
     also from zeros have "\<forall>n'\<ge>n. \<not> f (Suc n')" by auto
     ultimately show ?thesis using zeros
-      apply (simp (no_asm_simp) add: set_bits_int_def exI split del: if_split)
-      apply clarsimp apply (safe; rule bin_rl_eqI)
-         apply (auto simp add: bin_last_bl_to_bin hd_map bin_rest_bl_to_bin map_tl[symmetric] map_map[symmetric] map_Suc_upt simp del: map_map)
+      apply (simp (no_asm_simp) add: set_bits_int_def exI
+        del: upt.upt_Suc flip: map_map split del: if_split)
+      apply (simp only: map_Suc_upt upt_conv_Cons)
+      apply simp
       done
   qed
 next
   case (ones n)
   show ?thesis
   proof(cases "\<forall>n. f n")
     case True
     hence "f = (\<lambda>_. True)" by auto
     thus ?thesis using True by(simp add: o_def)
   next
     case False
     then obtain n' where "\<not> f n'" by blast
     with ones have "(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')"
       by(auto intro: Least_Suc)
     also have "(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))" by(auto dest: Suc_le_D)
     also from ones have "\<forall>n'\<ge>n. f (Suc n')" by auto
     moreover from ones have "(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False"
       by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm)
     moreover hence "(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False"
       by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D)
     ultimately show ?thesis using ones
       apply (simp (no_asm_simp) add: set_bits_int_def exI split del: if_split)
-      apply (auto simp add: Let_def bin_last_bl_to_bin hd_map bin_rest_bl_to_bin map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc simp del: map_map)
-         apply (metis bin_last_bl_to_bin last.simps list.simps(3) parity_cases)
-        apply (metis bin_last_bl_to_bin last_ConsL last_ConsR list.simps(3) parity_cases)
-       apply (metis (no_types, lifting) append_is_Nil_conv bin_last_bl_to_bin last_ConsR last_snoc list.distinct(1) odd_iff_mod_2_eq_one)
-      apply (metis (no_types, lifting) append_is_Nil_conv bin_last_bl_to_bin last_ConsR last_snoc list.distinct(1) not_mod_2_eq_1_eq_0 odd_iff_mod_2_eq_one)
+      apply (auto simp add: Let_def bin_last_bl_to_bin hd_map bin_rest_bl_to_bin map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc
+        not_le
+        simp del: map_map)
       done
   qed
 qed
 
 lemma bin_last_set_bits [simp]:
   "bin_last (set_bits f) = f 0"
   by (subst int_set_bits_unfold_BIT) simp_all
 
 lemma bin_rest_set_bits [simp]:
   "bin_rest (set_bits f) = set_bits (f \<circ> Suc)"
   by (subst int_set_bits_unfold_BIT) simp_all
 
 lemma bin_nth_set_bits [simp]:
   "bin_nth (set_bits f) m = f m"
 using wff proof (induction m arbitrary: f)
   case 0 
   then show ?case
     by (simp add: More_Bits_Int.bin_last_set_bits)
 next
   case Suc
   from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case
     by (simp add: More_Bits_Int.bin_rest_set_bits comp_def bit_Suc)
 qed
 
 end
 
 end