diff --git a/thys/JinjaThreads/Execute/Java2Jinja.thy b/thys/JinjaThreads/Execute/Java2Jinja.thy
--- a/thys/JinjaThreads/Execute/Java2Jinja.thy
+++ b/thys/JinjaThreads/Execute/Java2Jinja.thy
@@ -1,85 +1,88 @@
 (*  Title:      JinjaThreads/Execute/Java2Jinja.thy
     Author:     Andreas Lochbihler
 *)
 
 section \<open>Setup for converter Java2Jinja\<close>
 
 theory Java2Jinja 
 imports
   Code_Generation
   ToString
 begin
 
 code_identifier
   code_module Java2Jinja \<rightharpoonup> (SML) Code_Generation
 
 definition j_Program :: "addr J_mb cdecl list \<Rightarrow> addr J_prog"
 where "j_Program = Program"
 
 export_code wf_J_prog' j_Program in SML file \<open>JWellForm.ML\<close> 
 
 text \<open>Functions for extracting calls to the native print method\<close>
 
 definition purge where
   "\<And>run.
   purge run = 
   lmap (\<lambda>obs. case obs of ExternalCall _ _ (Cons (Intg i) _) v \<Rightarrow> i)
   (lfilter
     (\<lambda>obs. case obs of ExternalCall _ M (Cons (Intg i) Nil) _ \<Rightarrow> M = print | _ \<Rightarrow> False) 
     (lconcat (lmap (llist_of \<circ> snd) (llist_of_tllist run))))"
 
 text \<open>Various other functions\<close>
 
 instantiation heapobj :: toString begin
 primrec toString_heapobj :: "heapobj \<Rightarrow> String.literal" where
   "toString (Obj C fs) = sum_list [STR ''(Obj '', toString C, STR '', '', toString fs, STR '')'']"
 | "toString (Arr T si fs el) = 
    sum_list [STR ''(['', toString si, STR '']'', toString T, STR '', '', toString fs, STR '', '', toString (map snd (rm_to_list el)), STR '')'']"
 instance proof qed
 end
 
 definition case_llist' where "case_llist' = case_llist"
 definition case_tllist' where "case_tllist' = case_tllist"
 definition terminal' where "terminal' = terminal"
 definition llist_of_tllist' where "llist_of_tllist' = llist_of_tllist"
 definition thr' where "thr' = thr"
 definition shr' where "shr' = shr"
 
 definition heap_toString :: "heap \<Rightarrow> String.literal"
 where "heap_toString = toString"
 
 definition thread_toString :: "(thread_id, (addr expr \<times> addr locals) \<times> (addr \<Rightarrow>f nat)) rbt \<Rightarrow> String.literal"
 where "thread_toString = toString"
 
 definition thread_toString' :: "(thread_id, addr jvm_thread_state' \<times> (addr \<Rightarrow>f nat)) rbt \<Rightarrow> String.literal"
 where "thread_toString' = toString"
 
 definition trace_toString :: "thread_id \<times> (addr, thread_id) obs_event list \<Rightarrow> String.literal"
 where "trace_toString = toString"
 
 code_identifier
   code_module Cardinality \<rightharpoonup> (SML) Set
 | code_module Conditionally_Complete_Lattices \<rightharpoonup> (SML) Set
 | code_module List \<rightharpoonup> (SML) Set
 | code_module Predicate \<rightharpoonup> (SML) Set
-| constant member_i_i \<rightharpoonup> (SML) "Set.member_i_i"
+| code_module Parity \<rightharpoonup> (SML) Bit_Operations
+| type_class semiring_parity \<rightharpoonup> (SML) Bit_Operations.semiring_parity
+| class_instance int :: semiring_parity \<rightharpoonup> (SML) Bit_Operations.semiring_parity_int
+| constant member_i_i \<rightharpoonup> (SML) Set.member_i_i
 
 export_code
   wf_J_prog' exec_J_rr exec_J_rnd 
   j_Program
   purge case_llist' case_tllist' terminal' llist_of_tllist'
   thr' shr' heap_toString thread_toString trace_toString
   in SML
   file \<open>J_Execute.ML\<close>
 
 definition j2jvm :: "addr J_prog \<Rightarrow> addr jvm_prog" where "j2jvm = J2JVM"
 
 export_code
   wf_jvm_prog' exec_JVM_rr exec_JVM_rnd j2jvm
   j_Program 
   purge case_llist' case_tllist' terminal' llist_of_tllist'
   thr' shr' heap_toString thread_toString' trace_toString
   in SML
   file \<open>JVM_Execute2.ML\<close>
 
 end
diff --git a/thys/Native_Word/Code_Symbolic_Bits_Int.thy b/thys/Native_Word/Code_Symbolic_Bits_Int.thy
--- a/thys/Native_Word/Code_Symbolic_Bits_Int.thy
+++ b/thys/Native_Word/Code_Symbolic_Bits_Int.thy
@@ -1,143 +1,124 @@
 (*  Title:      Code_Symbolic_Bits_Int.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Symbolic implementation of bit operations on int\<close>
 
 theory Code_Symbolic_Bits_Int
 imports
   "HOL-Word.Misc_set_bit" "HOL-Word.Misc_lsb" More_Bits_Int
 begin
 
 section \<open>Implementations of bit operations on \<^typ>\<open>int\<close> operating on symbolic representation\<close>
 
 lemma not_minus_numeral_inc_eq:
   \<open>NOT (- numeral (Num.inc n)) = (numeral n :: int)\<close>
   by (simp add: not_int_def sub_inc_One_eq)
 
 lemma [code_abbrev]:
   \<open>test_bit = (bit :: int \<Rightarrow> nat \<Rightarrow> bool)\<close>
   by (simp add: fun_eq_iff)
 
 lemma test_bit_int_code [code]:
   "test_bit (0::int)          n = False"
   "test_bit (Int.Neg num.One) n = True"
   "test_bit (Int.Pos num.One)      0 = True"
   "test_bit (Int.Pos (num.Bit0 m)) 0 = False"
   "test_bit (Int.Pos (num.Bit1 m)) 0 = True"
   "test_bit (Int.Neg (num.Bit0 m)) 0 = False"
   "test_bit (Int.Neg (num.Bit1 m)) 0 = True"
   "test_bit (Int.Pos num.One)      (Suc n) = False"
   "test_bit (Int.Pos (num.Bit0 m)) (Suc n) = test_bit (Int.Pos m) n"
   "test_bit (Int.Pos (num.Bit1 m)) (Suc n) = test_bit (Int.Pos m) n"
   "test_bit (Int.Neg (num.Bit0 m)) (Suc n) = test_bit (Int.Neg m) n"
   "test_bit (Int.Neg (num.Bit1 m)) (Suc n) = test_bit (Int.Neg (Num.inc m)) n"
   by (simp_all add: Num.add_One bit_Suc)
 
 lemma int_not_code [code]:
   "NOT (0 :: int) = -1"
   "NOT (Int.Pos n) = Int.Neg (Num.inc n)"
   "NOT (Int.Neg n) = Num.sub n num.One"
 by(simp_all add: Num.add_One int_not_def)
 
 lemma int_and_code [code]: fixes i j :: int shows
   "0 AND j = 0"
   "i AND 0 = 0"
   "Int.Pos n AND Int.Pos m = (case bitAND_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')"
   "Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)"
   "Int.Pos n AND Int.Neg num.One = Int.Pos n"
   "Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (bitORN_num (Num.BitM m) n) num.One"
   "Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (bitORN_num (num.Bit0 m) n) num.One"
   "Int.Neg num.One AND Int.Pos m = Int.Pos m"
   "Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (bitORN_num (Num.BitM n) m) num.One"
   "Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (bitORN_num (num.Bit0 n) m) num.One"
            apply (simp_all add: int_numeral_bitAND_num Num.add_One
               sub_inc_One_eq inc_BitM_eq not_minus_numeral_inc_eq
               flip: int_not_neg_numeral int_or_not_bitORN_num split: option.split)
    apply (simp_all add: ac_simps)
   done
 
 lemma int_or_code [code]: fixes i j :: int shows
   "0 OR j = j"
   "i OR 0 = i"
   "Int.Pos n OR Int.Pos m = Int.Pos (bitOR_num n m)"
   "Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)"
   "Int.Pos n OR Int.Neg num.One = Int.Neg num.One"
   "Int.Pos n OR Int.Neg (num.Bit0 m) = (case bitANDN_num (Num.BitM m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))"
   "Int.Pos n OR Int.Neg (num.Bit1 m) = (case bitANDN_num (num.Bit0 m) n of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))"
   "Int.Neg num.One OR Int.Pos m = Int.Neg num.One"
   "Int.Neg (num.Bit0 n) OR Int.Pos m = (case bitANDN_num (Num.BitM n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))"
   "Int.Neg (num.Bit1 n) OR Int.Pos m = (case bitANDN_num (num.Bit0 n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))"
            apply (simp_all add: int_numeral_bitOR_num flip: int_not_neg_numeral)
      apply (simp_all add: or_int_def int_and_comm int_not_and_bitANDN_num del: int_not_simps(4) split: option.split)
      apply (simp_all add: Num.add_One)
   done
 
 lemma int_xor_code [code]: fixes i j :: int shows
   "0 XOR j = j"
   "i XOR 0 = i"
   "Int.Pos n XOR Int.Pos m = (case bitXOR_num n m of None \<Rightarrow> 0 | Some n' \<Rightarrow> Int.Pos n')"
   "Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One"
   "Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)"
   "Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)"
   by(fold int_not_neg_numeral)(simp_all add: int_numeral_bitXOR_num int_xor_not cong: option.case_cong)
 
 lemma bin_rest_code: "bin_rest i = i >> 1"
   by (simp add: shiftr_int_def)
 
-lemma sbintrunc_code [code]:
-  "sbintrunc n bin =
-  (let bin' = bin AND bin_mask (n + 1)
-   in if bin' !! n then bin' - (2 << n) else bin')"
-proof (induction n arbitrary: bin)
-  case 0
-  then show ?case
-    by (simp add: mod_2_eq_odd and_one_eq)
-next
-  case (Suc n)
-  have *: \<open>(4 * 2 ^ n - 1) div 2 = 2 * 2 ^ n - (1::int)\<close>
-    by simp
-  from Suc [of \<open>bin div 2\<close>]
-  show ?case 
-    by (auto simp add: Let_def bin_mask_conv_pow2 shiftl_int_def algebra_simps *
-      and_int_rec [of \<open>_ + _ * 2\<close>] and_int_rec [of \<open>_ * 2\<close>]
-      bit_double_iff even_bit_succ_iff elim!: evenE oddE)
-qed
-
 lemma set_bits_code [code]: 
   "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\<lambda>_. set_bits :: _ \<Rightarrow> int)"
 by simp
 
 lemma fixes i :: int 
   shows int_set_bit_True_conv_OR [code]: "set_bit i n True = i OR (1 << n)"
   and int_set_bit_False_conv_NAND [code]: "set_bit i n False = i AND NOT (1 << n)"
   and int_set_bit_conv_ops: "set_bit i n b = (if b then i OR (1 << n) else i AND NOT (1 << n))"
 by(simp_all add: set_bit_int_def bin_set_conv_OR bin_clr_conv_NAND)
 
 lemma int_shiftr_code [code]: fixes i :: int shows
   "i >> 0 = i"
   "0 >> Suc n = (0 :: int)"
   "Int.Pos num.One >> Suc n = 0"
   "Int.Pos (num.Bit0 m) >> Suc n = Int.Pos m >> n"
   "Int.Pos (num.Bit1 m) >> Suc n = Int.Pos m >> n"
   "Int.Neg num.One >> Suc n = -1"
   "Int.Neg (num.Bit0 m) >> Suc n = Int.Neg m >> n"
   "Int.Neg (num.Bit1 m) >> Suc n = Int.Neg (Num.inc m) >> n"
   by (simp_all add: shiftr_eq_drop_bit drop_bit_Suc add_One)
 
 lemma int_shiftl_code [code]:
   "i << 0 = i"
   "i << Suc n = Int.dup i << n"
   by (simp_all add: shiftl_int_def)
 
 lemma int_lsb_code [code]:
   "lsb (0 :: int) = False"
   "lsb (Int.Pos num.One) = True"
   "lsb (Int.Pos (num.Bit0 w)) = False"
   "lsb (Int.Pos (num.Bit1 w)) = True"
   "lsb (Int.Neg num.One) = True"
   "lsb (Int.Neg (num.Bit0 w)) = False"
   "lsb (Int.Neg (num.Bit1 w)) = True"
   by simp_all
 
 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,279 +1,281 @@
 (*  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)
       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 simp del: map_map)
-       apply (metis bin_last_bl_to_bin last.simps list.distinct(1))
-      apply (metis (no_types, lifting) Nil_is_append_conv bin_last_bl_to_bin last_ConsR last_snoc list.distinct(1))
+      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)
       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