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,270 +1,158 @@
 (*  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>
 
 lemma bin_mask_conv_pow2:
   "mask n = 2 ^ n - (1 :: int)"
   by (fact mask_eq_exp_minus_1)
   
 lemma bin_mask_ge0: "mask n \<ge> (0 :: int)"
   by (fact mask_nonnegative_int)
 
 lemma and_bin_mask_conv_mod: "x AND mask n = x mod 2 ^ n"
   for x :: int
   by (simp flip: take_bit_eq_mod add: take_bit_eq_mask)
 
 lemma bin_mask_numeral: 
   "mask (numeral n) = (1 :: int) + 2 * mask (pred_numeral n)"
   by (fact mask_numeral)
 
 lemma bin_nth_mask [simp]: "bit (mask n :: int) i \<longleftrightarrow> i < n"
   by (simp add: bit_mask_iff)
 
 lemma bin_sign_mask [simp]: "bin_sign (mask n) = 0"
   by (simp add: bin_sign_def bin_mask_conv_pow2)
 
 lemma bin_mask_p1_conv_shift: "mask n + 1 = (1 :: int) << 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
-        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 hd_map 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
diff --git a/thys/Native_Word/Uint.thy b/thys/Native_Word/Uint.thy
--- a/thys/Native_Word/Uint.thy
+++ b/thys/Native_Word/Uint.thy
@@ -1,875 +1,875 @@
 (*  Title:      Uint.thy
     Author:     Peter Lammich, TU Munich
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of default size\<close>
 
 theory Uint imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   This theory provides access to words in the target languages of the code generator
   whose bit width is the default of the target language. To that end, the type \<open>uint\<close>
   models words of width \<open>dflt_size\<close>, but \<open>dflt_size\<close> is known only to be positive.
 
   Usage restrictions:
   Default-size words (type \<open>uint\<close>) cannot be used for evaluation, because 
   the results depend on the particular choice of word size in the target language
   and implementation. Symbolic evaluation has not yet been set up for \<open>uint\<close>.
 \<close>
 
 text \<open>The default size type\<close>
 typedecl dflt_size
 
 instantiation dflt_size :: typerep begin
 definition "typerep_class.typerep \<equiv>  \<lambda>_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []"
 instance ..
 end
 
 consts dflt_size_aux :: "nat"
 specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0"
   by auto
 hide_fact dflt_size_aux_def
 
 instantiation dflt_size :: len begin
 definition "len_of_dflt_size (_ :: dflt_size itself) \<equiv> dflt_size_aux"
 instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0)
 end
 
 abbreviation "dflt_size \<equiv> len_of (TYPE (dflt_size))"
 
 context includes integer.lifting begin
 lift_definition dflt_size_integer :: integer is "int dflt_size" .
 declare dflt_size_integer_def[code del]
   \<comment> \<open>The code generator will substitute a machine-dependent value for this constant\<close>
 
 lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer"
 by transfer simp
 
 lemma dflt_size[simp]: 
   "dflt_size > 0"
   "dflt_size \<ge> Suc 0"
   "\<not> dflt_size < Suc 0"
   using len_gt_0[where 'a=dflt_size]
   by (simp_all del: len_gt_0)
 end
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint = "UNIV :: dflt_size word set" .. 
 
 setup_lifting type_definition_uint
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint}.\<close>
 declare Rep_uint_inverse[code abstype]
 
 declare Quotient_uint[transfer_rule]
 
 instantiation uint :: comm_ring_1
 begin
 lift_definition zero_uint :: uint is "0 :: dflt_size word" .
 lift_definition one_uint :: uint is "1" .
 lift_definition plus_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(+) :: dflt_size word \<Rightarrow> _" .
 lift_definition minus_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(-)" .
 lift_definition uminus_uint :: "uint \<Rightarrow> uint" is uminus .
 lift_definition times_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint :: semiring_modulo
 begin
 lift_definition divide_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(div)" .
 lift_definition modulo_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint :: linorder begin
 lift_definition less_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint.rep_eq less_eq_uint.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint :: semiring_bits
 begin
 
 lift_definition bit_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is push_bit .
 lift_definition drop_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is drop_bit .
 lift_definition take_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint :: ring_bit_operations
 begin
 lift_definition not_uint :: \<open>uint \<Rightarrow> uint\<close> is NOT .
 lift_definition and_uint :: \<open>uint \<Rightarrow> uint \<Rightarrow> uint\<close> is \<open>(AND)\<close> .
 lift_definition or_uint :: \<open>uint \<Rightarrow> uint \<Rightarrow> uint\<close> is \<open>(OR)\<close> .
 lift_definition xor_uint :: \<open>uint \<Rightarrow> uint \<Rightarrow> uint\<close> is \<open>(XOR)\<close> .
 lift_definition mask_uint :: \<open>nat \<Rightarrow> uint\<close> is mask .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
 end
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: uint
   by (fact take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: uint) OR mask n\<close>
   \<open>mask 0 = (0 :: uint)\<close>
   by (simp_all add: mask_Suc_exp push_bit_of_1)
 
 instantiation uint:: semiring_bit_syntax
 begin
 lift_definition test_bit_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> bool\<close> is test_bit .
 lift_definition shiftl_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> uint\<close> is shiftl .
 lift_definition shiftr_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> uint\<close> is shiftr .
 instance by (standard; transfer)
   (fact test_bit_eq_bit shiftl_word_eq shiftr_word_eq)+
 end
 
 instantiation uint :: lsb
 begin
 lift_definition lsb_uint :: \<open>uint \<Rightarrow> bool\<close> is lsb .
 instance by (standard; transfer)
   (fact lsb_odd)
 end
 
 instantiation uint :: msb
 begin
 lift_definition msb_uint :: \<open>uint \<Rightarrow> bool\<close> is msb .
 instance ..
 end
 
 instantiation uint :: set_bit
 begin
 lift_definition set_bit_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint\<close> is set_bit .
 instance
   apply standard
   apply (unfold Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply (simp add: set_bit_eq Bit_Operations.set_bit_def unset_bit_def)
   done
 end
 
 instantiation uint :: bit_comprehension begin
 lift_definition set_bits_uint :: "(nat \<Rightarrow> bool) \<Rightarrow> uint" is "set_bits" .
-instance ..
+instance by (standard; transfer) (fact set_bits_bit_eq)
 end
 
 lemmas [code] = test_bit_uint.rep_eq lsb_uint.rep_eq msb_uint.rep_eq
 
 instantiation uint :: equal begin
 lift_definition equal_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint.rep_eq
 
 instantiation uint :: size begin
 lift_definition size_uint :: "uint \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint.rep_eq
 
 lift_definition sshiftr_uint :: "uint \<Rightarrow> nat \<Rightarrow> uint" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint_of_int :: "int \<Rightarrow> uint" is "word_of_int" .
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint :: "integer \<Rightarrow> uint" is "word_of_int" .
 
 lemma Rep_uint_numeral [simp]: "Rep_uint (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint_def Abs_uint_inverse numeral.simps plus_uint_def)
 
 lemma numeral_uint_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint) numeral numeral"
 by(auto simp add: cr_uint_def)
 
 lemma numeral_uint [code_unfold]: "numeral n = Uint (numeral n)"
 by transfer simp
 
 lemma Rep_uint_neg_numeral [simp]: "Rep_uint (- numeral n) = - numeral n"
 by(simp only: uminus_uint_def)(simp add: Abs_uint_inverse)
 
 lemma neg_numeral_uint [code_unfold]: "- numeral n = Uint (- numeral n)"
 by transfer(simp add: cr_uint_def)
 
 end
 
 lemma Abs_uint_numeral [code_post]: "Abs_uint (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint_def numeral.simps plus_uint_def Abs_uint_inverse)
 
 lemma Abs_uint_0 [code_post]: "Abs_uint 0 = 0"
 by(simp add: zero_uint_def)
 
 lemma Abs_uint_1 [code_post]: "Abs_uint 1 = 1"
 by(simp add: one_uint_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint \<rightharpoonup> (SML)
 \<open>
 structure Uint : sig
   val set_bit : Word.word -> IntInf.int -> bool -> Word.word
   val shiftl : Word.word -> IntInf.int -> Word.word
   val shiftr : Word.word -> IntInf.int -> Word.word
   val shiftr_signed : Word.word -> IntInf.int -> Word.word
   val test_bit : Word.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word.orb (x, mask)
      else Word.andb (x, Word.notb mask)
   end
 
 fun shiftl x n =
   Word.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0
 
 end; (* struct Uint *)\<close>
 code_reserved SML Uint
 
 code_printing code_module Uint \<rightharpoonup> (Haskell)
  \<open>module Uint(Int, Word, dflt_size) where
 
   import qualified Prelude
   import Data.Int(Int)
   import Data.Word(Word)
   import qualified Data.Bits
 
   dflt_size :: Prelude.Integer
   dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where
     bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
     bitSize_aux = Data.Bits.bitSize\<close>
   and (Haskell_Quickcheck)
  \<open>module Uint(Int, Word, dflt_size) where
 
   import qualified Prelude
   import Data.Int(Int)
   import Data.Word(Word)
   import qualified Data.Bits
 
   dflt_size :: Prelude.Int
   dflt_size = bitSize_aux (0::Word) where
     bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
     bitSize_aux = Data.Bits.bitSize
 \<close>
 code_reserved Haskell Uint dflt_size
 
 text \<open>
   OCaml and Scala provide only signed bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 
 code_printing code_module "Uint" \<rightharpoonup> (OCaml)
 \<open>module Uint : sig
   type t = int
   val dflt_size : Z.t
   val less : t -> t -> bool
   val less_eq : t -> t -> bool
   val set_bit : t -> Z.t -> bool -> t
   val shiftl : t -> Z.t -> t
   val shiftr : t -> Z.t -> t
   val shiftr_signed : t -> Z.t -> t
   val test_bit : t -> Z.t -> bool
   val int_mask : int
   val int32_mask : int32
   val int64_mask : int64
 end = struct
 
 type t = int
 
 let dflt_size = Z.of_int Sys.int_size;;
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if x<0 then
     y<0 && x<y
   else y < 0 || x < y;;
 
 let less_eq x y =
   if x < 0 then
     y < 0 &&  x <= y
   else y < 0 || x <= y;;
 
 let set_bit x n b =
   let mask = 1 lsl (Z.to_int n)
   in if b then x lor mask
      else x land (lnot mask);;
 
 let shiftl x n = x lsl (Z.to_int n);;
 
 let shiftr x n = x lsr (Z.to_int n);;
 
 let shiftr_signed x n = x asr (Z.to_int n);;
 
 let test_bit x n = x land (1 lsl (Z.to_int n)) <> 0;;
 
 let int_mask =
   if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;;
 
 let int32_mask = 
   if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size)
   else Int32.of_string "0xFFFFFFFF";;
 
 let int64_mask = 
   if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size)
   else Int64.of_string "0xFFFFFFFFFFFFFFFF";;
 
 end;; (*struct Uint*)\<close>
 code_reserved OCaml Uint
 
 code_printing code_module Uint \<rightharpoonup> (Scala)
 \<open>object Uint {
 def dflt_size : BigInt = BigInt(32)
 
 def less(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
   if (b)
     x | (1 << n.intValue)
   else
     x & (1 << n.intValue).unary_~
 
 def shiftl(x: Int, n: BigInt) : Int = x << n.intValue
 
 def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue
 
 def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue
 
 def test_bit(x: Int, n: BigInt) : Boolean =
   (x & (1 << n.intValue)) != 0
 
 } /* object Uint */\<close>
 code_reserved Scala Uint
 
 
 text \<open>
   OCaml's conversion from Big\_int to int demands that the value fits into a signed integer.
   The following justifies the implementation.
 \<close>
 
 context includes integer.lifting begin
 definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1"
 lift_definition wivs_mask_integer :: integer is wivs_mask .
 lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1"
   by transfer (simp add: wivs_mask_def)
 
 definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size"
 lift_definition wivs_shift_integer :: integer is wivs_shift .
 lemma [code]: "wivs_shift_integer = 2 ^ dflt_size"
   by transfer (simp add: wivs_shift_def)
 
 definition wivs_index :: nat where "wivs_index == dflt_size - 1"
 lift_definition wivs_index_integer :: integer is "int wivs_index".
 lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1"
   by transfer (simp add: wivs_index_def of_nat_diff)
 
 definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)"
 lift_definition wivs_overflow_integer :: integer is wivs_overflow .
 lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)"
   by transfer (simp add: wivs_overflow_def)
 
 definition wivs_least :: int where "wivs_least == - wivs_overflow"
 lift_definition wivs_least_integer :: integer is wivs_least .
 lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))"
   by transfer (simp add: wivs_overflow_def wivs_least_def)
 
 definition Uint_signed :: "integer \<Rightarrow> uint" where
   "Uint_signed i = (if i < wivs_least_integer \<or> wivs_overflow_integer \<le> i then undefined Uint i else Uint i)"
 
 lemma Uint_code [code]:
   "Uint i = 
   (let i' = i AND wivs_mask_integer in 
    if i' !! wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')"
   including undefined_transfer 
   unfolding Uint_signed_def
   apply transfer
   apply (rule word_of_int_via_signed)
   by (simp_all add: wivs_mask_def wivs_shift_def wivs_index_def wivs_overflow_def 
     wivs_least_def bin_mask_conv_pow2 shiftl_int_def)
 
 lemma Uint_signed_code [code abstract]:
   "Rep_uint (Uint_signed i) = 
   (if i < wivs_least_integer \<or> i \<ge> wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))"
   unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def word_of_integer_def
   by(simp add: Abs_uint_inverse)
 end
 
 text \<open>
   Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint}.
 
   The new destructor @{term Rep_uint'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint} 
   ([code abstract] equations for @{typ uint} may use @{term Rep_uint} because
   these instances will be folded away.)
 \<close>
 
 definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint"
 
 lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. x !! n)"
 unfolding Rep_uint'_def by transfer simp
 
 lift_definition Abs_uint' :: "dflt_size word \<Rightarrow> uint" is "\<lambda>x :: dflt_size word. x" .
 
 lemma Abs_uint'_code [code]:
   "Abs_uint' x = Uint (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint \<Rightarrow> _"]]
 
 lemma term_of_uint_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'')  [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []]))
        (term_of_class.term_of (Rep_uint' x))"
   by(simp add: term_of_anything)
 
 text \<open>Important:
   We must prevent the reflection oracle (eval-tac) to 
   use our machine-dependent type.
 \<close>
 
 code_printing
   type_constructor uint \<rightharpoonup>
   (SML) "Word.word" and
   (Haskell) "Uint.Word" and
   (OCaml) "Uint.t" and
   (Scala) "Int" and
   (Eval) "*** \"Error: Machine dependent type\" ***" and
   (Quickcheck) "Word.word" 
 | constant dflt_size_integer \<rightharpoonup>
   (SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.wordSize" and
   (Haskell) "Uint.dflt'_size" and
   (OCaml) "Uint.dflt'_size" and
   (Scala) "Uint.dflt'_size"
 | constant Uint \<rightharpoonup>
   (SML) "Word.fromLargeInt (IntInf.toLarge _)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.fromInt" and
   (Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and
   (Scala) "_.intValue"
 | constant Uint_signed \<rightharpoonup>
   (OCaml) "Z.to'_int"
 | constant "0 :: uint" \<rightharpoonup>
   (SML) "(Word.fromInt 0)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "(Word.fromInt 0)" and
   (Haskell) "(0 :: Uint.Word)" and
   (OCaml) "0" and
   (Scala) "0"
 | constant "1 :: uint" \<rightharpoonup>
   (SML) "(Word.fromInt 1)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "(Word.fromInt 1)" and
   (Haskell) "(1 :: Uint.Word)" and
   (OCaml) "1" and
   (Scala) "1"
 | constant "plus :: uint \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Word.+ ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Pervasives.(+)" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.~" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.~" and
   (Haskell) "negate" and
   (OCaml) "Pervasives.(~-)" and
   (Scala) "!(- _)"
 | constant "minus :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.- ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Pervasives.(-)" and
   (Scala) infixl 7 "-"
 | constant "times :: uint \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.* ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Pervasives.( * )" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Word.word) = _)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "!((_ : Word.word) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and
   (Scala) infixl 5 "=="
 | class_instance uint :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word.<= ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint.less'_eq" and
   (Scala) "Uint.less'_eq"
 | constant "less :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word.< ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint.less" and
   (Scala) "Uint.less"
 | constant "NOT :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.notb" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Pervasives.lnot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.andb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Pervasives.(land)" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.orb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Pervasives.(lor)" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.xorb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Pervasives.(lxor)" and
   (Scala) infixl 2 "^"
 
 definition uint_divmod :: "uint \<Rightarrow> uint \<Rightarrow> uint \<times> uint" where
   "uint_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint), undefined ((mod) :: uint \<Rightarrow> _) x (0 :: uint)) 
   else (x div y, x mod y))"
 
 definition uint_div :: "uint \<Rightarrow> uint \<Rightarrow> uint" 
 where "uint_div x y = fst (uint_divmod x y)"
 
 definition uint_mod :: "uint \<Rightarrow> uint \<Rightarrow> uint" 
 where "uint_mod x y = snd (uint_divmod x y)"
 
 lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)"
 including undefined_transfer unfolding uint_divmod_def uint_div_def
 by transfer(simp add: word_div_def)
 
 lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)"
 including undefined_transfer unfolding uint_mod_def uint_divmod_def
 by transfer(simp add: word_mod_def)
 
 definition uint_sdiv :: "uint \<Rightarrow> uint \<Rightarrow> uint"
 where [code del]:
   "uint_sdiv x y =
    (if y = 0 then undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint)
     else Abs_uint (Rep_uint x sdiv Rep_uint y))"
 
 definition div0_uint :: "uint \<Rightarrow> uint"
 where [code del]: "div0_uint x = undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint)"
 declare [[code abort: div0_uint]]
 
 definition mod0_uint :: "uint \<Rightarrow> uint"
 where [code del]: "mod0_uint x = undefined ((mod) :: uint \<Rightarrow> _) x (0 :: uint)"
 declare [[code abort: mod0_uint]]
 
 definition wivs_overflow_uint :: uint 
   where "wivs_overflow_uint \<equiv> 1 << (dflt_size - 1)"
 
 lemma uint_divmod_code [code]:
   "uint_divmod x y =
   (if wivs_overflow_uint \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint x, mod0_uint x)
    else let q = (uint_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
   including undefined_transfer 
   unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def
     wivs_overflow_uint_def
   apply transfer
   apply (simp add: divmod_via_sdivmod)
   done
 
 lemma uint_sdiv_code [code abstract]:
   "Rep_uint (uint_sdiv x y) =
    (if y = 0 then Rep_uint (undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint))
     else Rep_uint x sdiv Rep_uint y)"
 unfolding uint_sdiv_def by(simp add: Abs_uint_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint_div \<rightharpoonup>
   (SML) "Word.div ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.div ((_), (_))" and
   (Haskell) "Prelude.div"
 | constant uint_mod \<rightharpoonup>
   (SML) "Word.mod ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.mod ((_), (_))" and
   (Haskell) "Prelude.mod"
 | constant uint_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint_sdiv \<rightharpoonup>
   (OCaml) "Pervasives.('/)" and
   (Scala) "_ '/ _"
 
 definition uint_test_bit :: "uint \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint_test_bit x n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (test_bit :: uint \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint [code]:
   \<open>test_bit = (bit :: uint \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint_code [code]:
   "test_bit x n \<longleftrightarrow> n < dflt_size \<and> uint_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint_test_bit_code [code]:
   "uint_test_bit w n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (test_bit :: uint \<Rightarrow> _) w n else Rep_uint w !! nat_of_integer n)"
 unfolding uint_test_bit_def
 by(simp add: test_bit_uint.rep_eq)
 
 code_printing constant uint_test_bit \<rightharpoonup>
   (SML) "Uint.test'_bit" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint.test'_bit" and
   (Scala) "Uint.test'_bit"
 
 definition uint_set_bit :: "uint \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint"
 where [code del]:
   "uint_set_bit x n b =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (set_bit :: uint \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint_code [code]:
   "set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)"
   including undefined_transfer integer.lifting unfolding uint_set_bit_def
   by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint_set_bit_code [code abstract]:
   "Rep_uint (uint_set_bit w n b) = 
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (set_bit :: uint \<Rightarrow> _) w n b)
    else set_bit (Rep_uint w) (nat_of_integer n) b)"
 including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp
 
 code_printing constant uint_set_bit \<rightharpoonup>
   (SML) "Uint.set'_bit" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint.set'_bit" and
   (Scala) "Uint.set'_bit"
 
 lift_definition uint_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint \<Rightarrow> nat \<Rightarrow> uint" is set_bits_aux .
 
 lemma uint_set_bits_code [code]:
   "uint_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint [code]:
   "(BITS n. f n) = uint_set_bits f 0 dflt_size"
   by transfer (simp add: set_bits_conv_set_bits_aux)
 
 lemma lsb_code [code]: fixes x :: uint shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 definition uint_shiftl :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_shiftl x n = (if n < 0 \<or> dflt_size_integer \<le> n then undefined (shiftl :: uint \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint_code [code]: "x << n = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint_shiftl_code [code abstract]:
   "Rep_uint (uint_shiftl w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (shiftl :: uint \<Rightarrow> _) w n) else Rep_uint w << (nat_of_integer n))"
 including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp
 
 code_printing constant uint_shiftl \<rightharpoonup>
   (SML) "Uint.shiftl" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint.shiftl" and
   (Scala) "Uint.shiftl"
 
 definition uint_shiftr :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_shiftr x n = (if n < 0 \<or> dflt_size_integer \<le> n then undefined (shiftr :: uint \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint_code [code]: "x >> n = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint_shiftr_code [code abstract]:
   "Rep_uint (uint_shiftr w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (shiftr :: uint \<Rightarrow> _) w n) else Rep_uint w >> nat_of_integer n)"
 including undefined_transfer unfolding uint_shiftr_def by transfer simp
 
 code_printing constant uint_shiftr \<rightharpoonup>
   (SML) "Uint.shiftr" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint.shiftr" and
   (Scala) "Uint.shiftr"
 
 definition uint_sshiftr :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_sshiftr x n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined sshiftr_uint x n else sshiftr_uint x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint_code [code]:
   "x >>> n = 
   (if n < dflt_size then uint_sshiftr x (integer_of_nat n) else 
     if x !! wivs_index then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size wivs_index_def)
 
 lemma uint_sshiftr_code [code abstract]:
   "Rep_uint (uint_sshiftr w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined sshiftr_uint w n) else Rep_uint w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint_sshiftr_def by transfer simp
 
 code_printing constant uint_sshiftr \<rightharpoonup>
   (SML) "Uint.shiftr'_signed" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and
   (OCaml) "Uint.shiftr'_signed" and
   (Scala) "Uint.shiftr'_signed"
 
 lemma uint_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint) !! wivs_index"
 by transfer(simp add: msb_nth wivs_index_def)
 
 lemma msb_uint_code [code]: "msb x \<longleftrightarrow> uint_test_bit x wivs_index_integer"
   apply(simp add: uint_test_bit_def uint_msb_test_bit 
   wivs_index_integer_code dflt_size_integer_def wivs_index_def)
   by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0 
     nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def)
 
 lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. i !! n)"
 by transfer(simp add: word_of_int_conv_set_bits test_bit_int_def[abs_def])
 
 section \<open>Quickcheck setup\<close>
 
 definition uint_of_natural :: "natural \<Rightarrow> uint"
 where "uint_of_natural x \<equiv> Uint (integer_of_natural x)"
 
 instantiation uint :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint \<equiv> qc_random_cnv uint_of_natural"
 definition "exhaustive_uint \<equiv> qc_exhaustive_cnv uint_of_natural"
 definition "full_exhaustive_uint \<equiv> qc_full_exhaustive_cnv uint_of_natural"
 instance ..
 end
 
 instantiation uint :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. (Uint i, Uint (- i))" "0"
   "Typerep.Typerep (STR ''Uint.uint'') []" .
 
 definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint16.thy b/thys/Native_Word/Uint16.thy
--- a/thys/Native_Word/Uint16.thy
+++ b/thys/Native_Word/Uint16.thy
@@ -1,618 +1,618 @@
 (*  Title:      Uint16.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 16 bits\<close>
 
 theory Uint16 imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   Restriction for ML code generation:
   This theory assumes that the ML system provides a Word16
   implementation (mlton does, but PolyML 5.5 does not).
   Therefore, the code setup lives in the target \<open>SML_word\<close>
   rather than \<open>SML\<close>.  This ensures that code generation still
   works as long as \<open>uint16\<close> is not involved.
   For the target \<open>SML\<close> itself, no special code generation 
   for this type is set up. Nevertheless, it should work by emulation via @{typ "16 word"} 
   if the theory \<open>Code_Target_Bits_Int\<close> is imported.
 
   Restriction for OCaml code generation:
   OCaml does not provide an int16 type, so no special code generation 
   for this type is set up.
 \<close>
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint16 = "UNIV :: 16 word set" ..
 
 setup_lifting type_definition_uint16
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint16}.\<close>
 declare Rep_uint16_inverse[code abstype]
 
 declare Quotient_uint16[transfer_rule]
 
 instantiation uint16 :: comm_ring_1
 begin
 lift_definition zero_uint16 :: uint16 is "0 :: 16 word" .
 lift_definition one_uint16 :: uint16 is "1" .
 lift_definition plus_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" is "(+) :: 16 word \<Rightarrow> _" .
 lift_definition minus_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" is "(-)" .
 lift_definition uminus_uint16 :: "uint16 \<Rightarrow> uint16" is uminus .
 lift_definition times_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint16 :: semiring_modulo
 begin
 lift_definition divide_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" is "(div)" .
 lift_definition modulo_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint16 :: linorder begin
 lift_definition less_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint16.rep_eq less_eq_uint16.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint16) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint16) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint16 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint16 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint16 :: semiring_bits
 begin
 
 lift_definition bit_uint16 :: \<open>uint16 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint16 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint16 :: \<open>nat \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is push_bit .
 lift_definition drop_bit_uint16 :: \<open>nat \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is drop_bit .
 lift_definition take_bit_uint16 :: \<open>nat \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint16 :: ring_bit_operations
 begin
 lift_definition not_uint16 :: \<open>uint16 \<Rightarrow> uint16\<close> is NOT .
 lift_definition and_uint16 :: \<open>uint16 \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is \<open>(AND)\<close> .
 lift_definition or_uint16 :: \<open>uint16 \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is \<open>(OR)\<close> .
 lift_definition xor_uint16 :: \<open>uint16 \<Rightarrow> uint16 \<Rightarrow> uint16\<close> is \<open>(XOR)\<close> .
 lift_definition mask_uint16 :: \<open>nat \<Rightarrow> uint16\<close> is mask .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
 end
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: uint16
   by (fact take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: uint16) OR mask n\<close>
   \<open>mask 0 = (0 :: uint16)\<close>
   by (simp_all add: mask_Suc_exp push_bit_of_1)
 
 instantiation uint16:: semiring_bit_syntax
 begin
 lift_definition test_bit_uint16 :: \<open>uint16 \<Rightarrow> nat \<Rightarrow> bool\<close> is test_bit .
 lift_definition shiftl_uint16 :: \<open>uint16 \<Rightarrow> nat \<Rightarrow> uint16\<close> is shiftl .
 lift_definition shiftr_uint16 :: \<open>uint16 \<Rightarrow> nat \<Rightarrow> uint16\<close> is shiftr .
 instance by (standard; transfer)
   (fact test_bit_eq_bit shiftl_word_eq shiftr_word_eq)+
 end
 
 instantiation uint16 :: lsb
 begin
 lift_definition lsb_uint16 :: \<open>uint16 \<Rightarrow> bool\<close> is lsb .
 instance by (standard; transfer)
   (fact lsb_odd)
 end
 
 instantiation uint16 :: msb
 begin
 lift_definition msb_uint16 :: \<open>uint16 \<Rightarrow> bool\<close> is msb .
 instance ..
 end
 
 instantiation uint16 :: set_bit
 begin
 lift_definition set_bit_uint16 :: \<open>uint16 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint16\<close> is set_bit .
 instance
   apply standard
   apply (unfold Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply (simp add: set_bit_eq Bit_Operations.set_bit_def unset_bit_def)
   done
 end
 
 instantiation uint16 :: bit_comprehension begin
 lift_definition set_bits_uint16 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint16" is "set_bits" .
-instance ..
+instance by (standard; transfer) (fact set_bits_bit_eq)
 end
 
 lemmas [code] = test_bit_uint16.rep_eq lsb_uint16.rep_eq msb_uint16.rep_eq
 
 instantiation uint16 :: equal begin
 lift_definition equal_uint16 :: "uint16 \<Rightarrow> uint16 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint16.rep_eq
 
 instantiation uint16 :: size begin
 lift_definition size_uint16 :: "uint16 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint16.rep_eq
 
 lift_definition sshiftr_uint16 :: "uint16 \<Rightarrow> nat \<Rightarrow> uint16" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint16_of_int :: "int \<Rightarrow> uint16" is "word_of_int" .
 
 definition uint16_of_nat :: "nat \<Rightarrow> uint16"
 where "uint16_of_nat = uint16_of_int \<circ> int"
 
 lift_definition int_of_uint16 :: "uint16 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint16 :: "uint16 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint16 :: "uint16 \<Rightarrow> integer"
 where "integer_of_uint16 = integer_of_int o int_of_uint16"
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint16 :: "integer \<Rightarrow> uint16" is "word_of_int" .
 
 lemma Rep_uint16_numeral [simp]: "Rep_uint16 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint16_def Abs_uint16_inverse numeral.simps plus_uint16_def)
 
 lemma Rep_uint16_neg_numeral [simp]: "Rep_uint16 (- numeral n) = - numeral n"
 by(simp only: uminus_uint16_def)(simp add: Abs_uint16_inverse)
 
 lemma numeral_uint16_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint16) numeral numeral"
 by(auto simp add: cr_uint16_def)
 
 lemma numeral_uint16 [code_unfold]: "numeral n = Uint16 (numeral n)"
 by transfer simp
 
 lemma neg_numeral_uint16 [code_unfold]: "- numeral n = Uint16 (- numeral n)"
 by transfer(simp add: cr_uint16_def)
 
 end
 
 lemma Abs_uint16_numeral [code_post]: "Abs_uint16 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint16_def numeral.simps plus_uint16_def Abs_uint16_inverse)
 
 lemma Abs_uint16_0 [code_post]: "Abs_uint16 0 = 0"
 by(simp add: zero_uint16_def)
 
 lemma Abs_uint16_1 [code_post]: "Abs_uint16 1 = 1"
 by(simp add: one_uint16_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint16 \<rightharpoonup> (SML_word)
 \<open>(* Test that words can handle numbers between 0 and 15 *)
 val _ = if 4 <= Word.wordSize then () else raise (Fail ("wordSize less than 4"));
 
 structure Uint16 : sig
   val set_bit : Word16.word -> IntInf.int -> bool -> Word16.word
   val shiftl : Word16.word -> IntInf.int -> Word16.word
   val shiftr : Word16.word -> IntInf.int -> Word16.word
   val shiftr_signed : Word16.word -> IntInf.int -> Word16.word
   val test_bit : Word16.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word16.orb (x, mask)
      else Word16.andb (x, Word16.notb mask)
   end
 
 fun shiftl x n =
   Word16.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word16.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word16.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word16.andb (x, Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word16.fromInt 0
 
 end; (* struct Uint16 *)\<close>
 code_reserved SML_word Uint16
 
 code_printing code_module Uint16 \<rightharpoonup> (Haskell)
  \<open>module Uint16(Int16, Word16) where
 
   import Data.Int(Int16)
   import Data.Word(Word16)\<close>
 code_reserved Haskell Uint16
 
 text \<open>Scala provides unsigned 16-bit numbers as Char.\<close>
 
 code_printing code_module Uint16 \<rightharpoonup> (Scala)
 \<open>object Uint16 {
 
 def set_bit(x: scala.Char, n: BigInt, b: Boolean) : scala.Char =
   if (b)
     (x | (1.toChar << n.intValue)).toChar
   else
     (x & (1.toChar << n.intValue).unary_~).toChar
 
 def shiftl(x: scala.Char, n: BigInt) : scala.Char = (x << n.intValue).toChar
 
 def shiftr(x: scala.Char, n: BigInt) : scala.Char = (x >>> n.intValue).toChar
 
 def shiftr_signed(x: scala.Char, n: BigInt) : scala.Char = (x.toShort >> n.intValue).toChar
 
 def test_bit(x: scala.Char, n: BigInt) : Boolean = (x & (1.toChar << n.intValue)) != 0
 
 } /* object Uint16 */\<close>
 code_reserved Scala Uint16
 
 text \<open>
   Avoid @{term Abs_uint16} in generated code, use @{term Rep_uint16'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint16}.
 
   The new destructor @{term Rep_uint16'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint16} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint16} 
   ([code abstract] equations for @{typ uint16} may use @{term Rep_uint16} because
   these instances will be folded away.)
 
   To convert @{typ "16 word"} values into @{typ uint16}, use @{term "Abs_uint16'"}.
 \<close>
 
 definition Rep_uint16' where [simp]: "Rep_uint16' = Rep_uint16"
 
 lemma Rep_uint16'_transfer [transfer_rule]:
   "rel_fun cr_uint16 (=) (\<lambda>x. x) Rep_uint16'"
 unfolding Rep_uint16'_def by(rule uint16.rep_transfer)
 
 lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint16' :: "16 word \<Rightarrow> uint16" is "\<lambda>x :: 16 word. x" .
 
 lemma Abs_uint16'_code [code]:
   "Abs_uint16' x = Uint16 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint16 \<Rightarrow> _"]]
 
 lemma term_of_uint16_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint16.uint16.Abs_uint16'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]], TR (STR ''Uint16.uint16'') []]))
        (term_of_class.term_of (Rep_uint16' x))"
 by(simp add: term_of_anything)
 
 lemma Uin16_code [code abstract]: "Rep_uint16 (Uint16 i) = word_of_int (int_of_integer_symbolic i)"
 unfolding Uint16_def int_of_integer_symbolic_def by(simp add: Abs_uint16_inverse)
 
 code_printing
   type_constructor uint16 \<rightharpoonup>
   (SML_word) "Word16.word" and
   (Haskell) "Uint16.Word16" and
   (Scala) "scala.Char"
 | constant Uint16 \<rightharpoonup>
   (SML_word) "Word16.fromLargeInt (IntInf.toLarge _)" and
   (Haskell) "(Prelude.fromInteger _ :: Uint16.Word16)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Word16)" and
   (Scala) "_.charValue"
 | constant "0 :: uint16" \<rightharpoonup>
   (SML_word) "(Word16.fromInt 0)" and
   (Haskell) "(0 :: Uint16.Word16)" and
   (Scala) "0"
 | constant "1 :: uint16" \<rightharpoonup>
   (SML_word) "(Word16.fromInt 1)" and
   (Haskell) "(1 :: Uint16.Word16)" and
   (Scala) "1"
 | constant "plus :: uint16 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (Scala) "(_ +/ _).toChar"
 | constant "uminus :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.~" and
   (Haskell) "negate" and
   (Scala) "(- _).toChar"
 | constant "minus :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (Scala) "(_ -/ _).toChar"
 | constant "times :: uint16 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (Scala) "(_ */ _).toChar"
 | constant "HOL.equal :: uint16 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML_word) "!((_ : Word16.word) = _)" and
   (Haskell) infix 4 "==" and
   (Scala) infixl 5 "=="
 | class_instance uint16 :: equal \<rightharpoonup> (Haskell) -
 | constant "less_eq :: uint16 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML_word) "Word16.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (Scala) infixl 4 "<="
 | constant "less :: uint16 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML_word) "Word16.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (Scala) infixl 4 "<"
 | constant "NOT :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.notb" and
   (Haskell) "Data'_Bits.complement" and
   (Scala) "_.unary'_~.toChar"
 | constant "(AND) :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (Scala) "(_ & _).toChar"
 | constant "(OR) :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (Scala) "(_ | _).toChar"
 | constant "(XOR) :: uint16 \<Rightarrow> _" \<rightharpoonup>
   (SML_word) "Word16.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (Scala) "(_ ^ _).toChar"
 
 definition uint16_div :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" 
 where "uint16_div x y = (if y = 0 then undefined ((div) :: uint16 \<Rightarrow> _) x (0 :: uint16) else x div y)"
 
 definition uint16_mod :: "uint16 \<Rightarrow> uint16 \<Rightarrow> uint16" 
 where "uint16_mod x y = (if y = 0 then undefined ((mod) :: uint16 \<Rightarrow> _) x (0 :: uint16) else x mod y)"
 
 context includes undefined_transfer begin
 
 lemma div_uint16_code [code]: "x div y = (if y = 0 then 0 else uint16_div x y)"
 unfolding uint16_div_def by transfer (simp add: word_div_def)
 
 lemma mod_uint16_code [code]: "x mod y = (if y = 0 then x else uint16_mod x y)"
 unfolding uint16_mod_def by transfer (simp add: word_mod_def)
 
 lemma uint16_div_code [code abstract]:
   "Rep_uint16 (uint16_div x y) =
   (if y = 0 then Rep_uint16 (undefined ((div) :: uint16 \<Rightarrow> _) x (0 :: uint16)) else Rep_uint16 x div Rep_uint16 y)"
 unfolding uint16_div_def by transfer simp
 
 lemma uint16_mod_code [code abstract]:
   "Rep_uint16 (uint16_mod x y) =
   (if y = 0 then Rep_uint16 (undefined ((mod) :: uint16 \<Rightarrow> _) x (0 :: uint16)) else Rep_uint16 x mod Rep_uint16 y)"
 unfolding uint16_mod_def by transfer simp
 
 end
 
 code_printing constant uint16_div \<rightharpoonup>
   (SML_word) "Word16.div ((_), (_))" and
   (Haskell) "Prelude.div" and
   (Scala) "(_ '/ _).toChar"
 | constant uint16_mod \<rightharpoonup>
   (SML_word) "Word16.mod ((_), (_))" and
   (Haskell) "Prelude.mod" and
   (Scala) "(_ % _).toChar"
 
 definition uint16_test_bit :: "uint16 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint16_test_bit x n =
   (if n < 0 \<or> 15 < n then undefined (test_bit :: uint16 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint16 [code]:
   \<open>test_bit = (bit :: uint16 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint16_code [code]:
   "bit x n \<longleftrightarrow> n < 16 \<and> uint16_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint16_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint16_test_bit_code [code]:
   "uint16_test_bit w n =
   (if n < 0 \<or> 15 < n then undefined (test_bit :: uint16 \<Rightarrow> _) w n else Rep_uint16 w !! nat_of_integer n)"
 unfolding uint16_test_bit_def by(simp add: test_bit_uint16.rep_eq)
 
 code_printing constant uint16_test_bit \<rightharpoonup>
   (SML_word) "Uint16.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (Scala) "Uint16.test'_bit"
 
 definition uint16_set_bit :: "uint16 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint16"
 where [code del]:
   "uint16_set_bit x n b =
   (if n < 0 \<or> 15 < n then undefined (set_bit :: uint16 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint16_code [code]:
   "set_bit x n b = (if n < 16 then uint16_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint16_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint16_set_bit_code [code abstract]:
   "Rep_uint16 (uint16_set_bit w n b) = 
   (if n < 0 \<or> 15 < n then Rep_uint16 (undefined (set_bit :: uint16 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint16 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint16_set_bit_def by transfer simp
 
 code_printing constant uint16_set_bit \<rightharpoonup>
   (SML_word) "Uint16.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (Scala) "Uint16.set'_bit"
 
 lift_definition uint16_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint16 \<Rightarrow> nat \<Rightarrow> uint16" is set_bits_aux .
 
 lemma uint16_set_bits_code [code]:
   "uint16_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint16_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint16 [code]:
   "(BITS n. f n) = uint16_set_bits f 0 16"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint16 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint16_shiftl :: "uint16 \<Rightarrow> integer \<Rightarrow> uint16"
 where [code del]:
   "uint16_shiftl x n = (if n < 0 \<or> 16 \<le> n then undefined (shiftl :: uint16 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint16_code [code]: "x << n = (if n < 16 then uint16_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint16_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint16_shiftl_code [code abstract]:
   "Rep_uint16 (uint16_shiftl w n) =
   (if n < 0 \<or> 16 \<le> n then Rep_uint16 (undefined (shiftl :: uint16 \<Rightarrow> _) w n)
    else Rep_uint16 w << nat_of_integer n)"
 including undefined_transfer unfolding uint16_shiftl_def by transfer simp
 
 code_printing constant uint16_shiftl \<rightharpoonup>
   (SML_word) "Uint16.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (Scala) "Uint16.shiftl"
 
 definition uint16_shiftr :: "uint16 \<Rightarrow> integer \<Rightarrow> uint16"
 where [code del]:
   "uint16_shiftr x n = (if n < 0 \<or> 16 \<le> n then undefined (shiftr :: uint16 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint16_code [code]: "x >> n = (if n < 16 then uint16_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint16_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint16_shiftr_code [code abstract]:
   "Rep_uint16 (uint16_shiftr w n) =
   (if n < 0 \<or> 16 \<le> n then Rep_uint16 (undefined (shiftr :: uint16 \<Rightarrow> _) w n)
    else Rep_uint16 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint16_shiftr_def by transfer simp
 
 code_printing constant uint16_shiftr \<rightharpoonup>
   (SML_word) "Uint16.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (Scala) "Uint16.shiftr"
 
 definition uint16_sshiftr :: "uint16 \<Rightarrow> integer \<Rightarrow> uint16"
 where [code del]:
   "uint16_sshiftr x n =
   (if n < 0 \<or> 16 \<le> n then undefined sshiftr_uint16 x n else sshiftr_uint16 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint16_code [code]:
   "x >>> n = 
   (if n < 16 then uint16_sshiftr x (integer_of_nat n) else if x !! 15 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint16_sshiftr_def
 by transfer (simp add: not_less sshiftr_beyond word_size)
 
 lemma uint16_sshiftr_code [code abstract]:
   "Rep_uint16 (uint16_sshiftr w n) =
   (if n < 0 \<or> 16 \<le> n then Rep_uint16 (undefined sshiftr_uint16 w n)
    else Rep_uint16 w >>> nat_of_integer n)"
 including undefined_transfer unfolding uint16_sshiftr_def by transfer simp
 
 code_printing constant uint16_sshiftr \<rightharpoonup>
   (SML_word) "Uint16.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Int16) _)) :: Uint16.Word16)" and
   (Scala) "Uint16.shiftr'_signed"
 
 lemma uint16_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint16) !! 15"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint16_code [code]: "msb x \<longleftrightarrow> uint16_test_bit x 15"
 by(simp add: uint16_test_bit_def uint16_msb_test_bit)
 
 lemma uint16_of_int_code [code]: "uint16_of_int i = Uint16 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint16_code [code]:
   "int_of_uint16 x = int_of_integer (integer_of_uint16 x)"
 by(simp add: integer_of_uint16_def)
 
 lemma nat_of_uint16_code [code]:
   "nat_of_uint16 x = nat_of_integer (integer_of_uint16 x)"
 unfolding integer_of_uint16_def including integer.lifting by transfer simp
 
 lemma integer_of_uint16_code [code]:
   "integer_of_uint16 n = integer_of_int (uint (Rep_uint16' n))"
 unfolding integer_of_uint16_def by transfer auto
 
 code_printing
   constant "integer_of_uint16" \<rightharpoonup>
   (SML_word) "Word16.toInt _ : IntInf.int" and
   (Haskell) "Prelude.toInteger" and
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint16_of_natural :: "natural \<Rightarrow> uint16"
 where "uint16_of_natural x \<equiv> Uint16 (integer_of_natural x)"
 
 instantiation uint16 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint16 \<equiv> qc_random_cnv uint16_of_natural"
 definition "exhaustive_uint16 \<equiv> qc_exhaustive_cnv uint16_of_natural"
 definition "full_exhaustive_uint16 \<equiv> qc_full_exhaustive_cnv uint16_of_natural"
 instance ..
 end
 
 instantiation uint16 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint16 i in (x, 0xFFFF - x)" "0"
   "Typerep.Typerep (STR ''Uint16.uint16'') []" .
 
 definition "narrowing_uint16 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint16 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint16 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint16 (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint32.thy b/thys/Native_Word/Uint32.thy
--- a/thys/Native_Word/Uint32.thy
+++ b/thys/Native_Word/Uint32.thy
@@ -1,748 +1,748 @@
 (*  Title:      Uint32.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 32 bits\<close>
 
 theory Uint32 imports
   Code_Target_Word_Base
 begin
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint32 = "UNIV :: 32 word set" .. 
 
 setup_lifting type_definition_uint32
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint32}.\<close>
 declare Rep_uint32_inverse[code abstype]
 
 declare Quotient_uint32[transfer_rule]
 
 instantiation uint32 :: comm_ring_1
 begin
 lift_definition zero_uint32 :: uint32 is "0 :: 32 word" .
 lift_definition one_uint32 :: uint32 is "1" .
 lift_definition plus_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(+) :: 32 word \<Rightarrow> _" .
 lift_definition minus_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(-)" .
 lift_definition uminus_uint32 :: "uint32 \<Rightarrow> uint32" is uminus .
 lift_definition times_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint32 :: semiring_modulo
 begin
 lift_definition divide_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(div)" .
 lift_definition modulo_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint32 :: linorder begin
 lift_definition less_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint32.rep_eq less_eq_uint32.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint32) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint32) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint32 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint32 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint32:: semiring_bits
 begin
 
 lift_definition bit_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint32 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is push_bit .
 lift_definition drop_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is drop_bit .
 lift_definition take_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint32 :: ring_bit_operations
 begin
 lift_definition not_uint32 :: \<open>uint32 \<Rightarrow> uint32\<close> is NOT .
 lift_definition and_uint32 :: \<open>uint32 \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is \<open>(AND)\<close> .
 lift_definition or_uint32 :: \<open>uint32 \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is \<open>(OR)\<close> .
 lift_definition xor_uint32 :: \<open>uint32 \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is \<open>(XOR)\<close> .
 lift_definition mask_uint32 :: \<open>nat \<Rightarrow> uint32\<close> is mask .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
 end
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: uint32
   by (fact take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: uint32) OR mask n\<close>
   \<open>mask 0 = (0 :: uint32)\<close>
   by (simp_all add: mask_Suc_exp push_bit_of_1)
 
 instantiation uint32:: semiring_bit_syntax
 begin
 lift_definition test_bit_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> bool\<close> is test_bit .
 lift_definition shiftl_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> uint32\<close> is shiftl .
 lift_definition shiftr_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> uint32\<close> is shiftr .
 instance by (standard; transfer)
   (fact test_bit_eq_bit shiftl_word_eq shiftr_word_eq)+
 end
 
 instantiation uint32 :: lsb
 begin
 lift_definition lsb_uint32 :: \<open>uint32 \<Rightarrow> bool\<close> is lsb .
 instance by (standard; transfer)
   (fact lsb_odd)
 end
 
 instantiation uint32 :: msb
 begin
 lift_definition msb_uint32 :: \<open>uint32 \<Rightarrow> bool\<close> is msb .
 instance ..
 end
 
 instantiation uint32 :: set_bit
 begin
 lift_definition set_bit_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint32\<close> is set_bit .
 instance
   apply standard
   apply (unfold Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply (simp add: set_bit_eq Bit_Operations.set_bit_def unset_bit_def)
   done
 end
 
 instantiation uint32 :: bit_comprehension begin
 lift_definition set_bits_uint32 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint32" is "set_bits" .
-instance ..
+instance by (standard; transfer) (fact set_bits_bit_eq)
 end
 
 lemmas [code] = test_bit_uint32.rep_eq lsb_uint32.rep_eq msb_uint32.rep_eq
 
 instantiation uint32 :: equal begin
 lift_definition equal_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint32.rep_eq
 
 instantiation uint32 :: size begin
 lift_definition size_uint32 :: "uint32 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint32.rep_eq                                                    
 
 lift_definition sshiftr_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> uint32" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint32_of_int :: "int \<Rightarrow> uint32" is "word_of_int" .
 
 definition uint32_of_nat :: "nat \<Rightarrow> uint32"
 where "uint32_of_nat = uint32_of_int \<circ> int"
 
 lift_definition int_of_uint32 :: "uint32 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint32 :: "uint32 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint32 :: "uint32 \<Rightarrow> integer"
 where "integer_of_uint32 = integer_of_int o int_of_uint32"
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint32 :: "integer \<Rightarrow> uint32" is "word_of_int" .
 
 lemma Rep_uint32_numeral [simp]: "Rep_uint32 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint32_def Abs_uint32_inverse numeral.simps plus_uint32_def)
 
 lemma numeral_uint32_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint32) numeral numeral"
 by(auto simp add: cr_uint32_def)
 
 lemma numeral_uint32 [code_unfold]: "numeral n = Uint32 (numeral n)"
 by transfer simp
 
 lemma Rep_uint32_neg_numeral [simp]: "Rep_uint32 (- numeral n) = - numeral n"
 by(simp only: uminus_uint32_def)(simp add: Abs_uint32_inverse)
 
 lemma neg_numeral_uint32 [code_unfold]: "- numeral n = Uint32 (- numeral n)"
 by transfer(simp add: cr_uint32_def)
 
 end
 
 lemma Abs_uint32_numeral [code_post]: "Abs_uint32 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint32_def numeral.simps plus_uint32_def Abs_uint32_inverse)
 
 lemma Abs_uint32_0 [code_post]: "Abs_uint32 0 = 0"
 by(simp add: zero_uint32_def)
 
 lemma Abs_uint32_1 [code_post]: "Abs_uint32 1 = 1"
 by(simp add: one_uint32_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint32 \<rightharpoonup> (SML)
 \<open>(* Test that words can handle numbers between 0 and 31 *)
 val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));
 
 structure Uint32 : sig
   val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
   val shiftl : Word32.word -> IntInf.int -> Word32.word
   val shiftr : Word32.word -> IntInf.int -> Word32.word
   val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
   val test_bit : Word32.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word32.orb (x, mask)
      else Word32.andb (x, Word32.notb mask)
   end
 
 fun shiftl x n =
   Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0
 
 end; (* struct Uint32 *)\<close>
 code_reserved SML Uint32
 
 code_printing code_module Uint32 \<rightharpoonup> (Haskell)
  \<open>module Uint32(Int32, Word32) where
 
   import Data.Int(Int32)
   import Data.Word(Word32)\<close>
 code_reserved Haskell Uint32
 
 text \<open>
   OCaml and Scala provide only signed 32bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 code_printing code_module "Uint32" \<rightharpoonup> (OCaml)
 \<open>module Uint32 : sig
   val less : int32 -> int32 -> bool
   val less_eq : int32 -> int32 -> bool
   val set_bit : int32 -> Z.t -> bool -> int32
   val shiftl : int32 -> Z.t -> int32
   val shiftr : int32 -> Z.t -> int32
   val shiftr_signed : int32 -> Z.t -> int32
   val test_bit : int32 -> Z.t -> bool
 end = struct
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if Int32.compare x Int32.zero < 0 then
     Int32.compare y Int32.zero < 0 && Int32.compare x y < 0
   else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;;
 
 let less_eq x y =
   if Int32.compare x Int32.zero < 0 then
     Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0
   else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;;
 
 let set_bit x n b =
   let mask = Int32.shift_left Int32.one (Z.to_int n)
   in if b then Int32.logor x mask
      else Int32.logand x (Int32.lognot mask);;
 
 let shiftl x n = Int32.shift_left x (Z.to_int n);;
 
 let shiftr x n = Int32.shift_right_logical x (Z.to_int n);;
 
 let shiftr_signed x n = Int32.shift_right x (Z.to_int n);;
 
 let test_bit x n =
   Int32.compare 
     (Int32.logand x (Int32.shift_left Int32.one (Z.to_int n)))
     Int32.zero
   <> 0;;
 
 end;; (*struct Uint32*)\<close>
 code_reserved OCaml Uint32
 
 code_printing code_module Uint32 \<rightharpoonup> (Scala)
 \<open>object Uint32 {
 
 def less(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
   if (b)
     x | (1 << n.intValue)
   else
     x & (1 << n.intValue).unary_~
 
 def shiftl(x: Int, n: BigInt) : Int = x << n.intValue
 
 def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue
 
 def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue
 
 def test_bit(x: Int, n: BigInt) : Boolean =
   (x & (1 << n.intValue)) != 0
 
 } /* object Uint32 */\<close>
 code_reserved Scala Uint32
 
 text \<open>
   OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer.
   The following justifies the implementation.
 \<close>
 
 definition Uint32_signed :: "integer \<Rightarrow> uint32" 
 where "Uint32_signed i = (if i < -(0x80000000) \<or> i \<ge> 0x80000000 then undefined Uint32 i else Uint32 i)"
 
 lemma Uint32_code [code]:
   "Uint32 i = 
   (let i' = i AND 0xFFFFFFFF
    in if i' !! 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')"
 including undefined_transfer integer.lifting unfolding Uint32_signed_def
 by transfer(rule word_of_int_via_signed, simp_all add: bin_mask_numeral)
 
 lemma Uint32_signed_code [code abstract]:
   "Rep_uint32 (Uint32_signed i) = 
   (if i < -(0x80000000) \<or> i \<ge> 0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))"
 unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def word_of_integer_def
 by(simp add: Abs_uint32_inverse)
 
 text \<open>
   Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint32}.
 
   The new destructor @{term Rep_uint32'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint32} 
   ([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because
   these instances will be folded away.)
 
   To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}.
 \<close>
 
 definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32"
 
 lemma Rep_uint32'_transfer [transfer_rule]:
   "rel_fun cr_uint32 (=) (\<lambda>x. x) Rep_uint32'"
 unfolding Rep_uint32'_def by(rule uint32.rep_transfer)
 
 lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint32' :: "32 word \<Rightarrow> uint32" is "\<lambda>x :: 32 word. x" .
 
 lemma Abs_uint32'_code [code]:
   "Abs_uint32' x = Uint32 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint32 \<Rightarrow> _"]]
 
 lemma term_of_uint32_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
        (term_of_class.term_of (Rep_uint32' x))"
 by(simp add: term_of_anything)
 
 code_printing
   type_constructor uint32 \<rightharpoonup>
   (SML) "Word32.word" and
   (Haskell) "Uint32.Word32" and
   (OCaml) "int32" and
   (Scala) "Int" and
   (Eval) "Word32.word"
 | constant Uint32 \<rightharpoonup>
   (SML) "Word32.fromLargeInt (IntInf.toLarge _)" and
   (Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and
   (Scala) "_.intValue"
 | constant Uint32_signed \<rightharpoonup>
   (OCaml) "Z.to'_int32"
 | constant "0 :: uint32" \<rightharpoonup>
   (SML) "(Word32.fromInt 0)" and
   (Haskell) "(0 :: Uint32.Word32)" and
   (OCaml) "Int32.zero" and
   (Scala) "0"
 | constant "1 :: uint32" \<rightharpoonup>
   (SML) "(Word32.fromInt 1)" and
   (Haskell) "(1 :: Uint32.Word32)" and
   (OCaml) "Int32.one" and
   (Scala) "1"
 | constant "plus :: uint32 \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Word32.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Int32.add" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.~" and
   (Haskell) "negate" and
   (OCaml) "Int32.neg" and
   (Scala) "!(- _)"
 | constant "minus :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Int32.sub" and
   (Scala) infixl 7 "-"
 | constant "times :: uint32 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Int32.mul" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Word32.word) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Int32.compare _ _ = 0)" and
   (Scala) infixl 5 "=="
 | class_instance uint32 :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word32.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint32.less'_eq" and
   (Scala) "Uint32.less'_eq"
 | constant "less :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word32.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint32.less" and
   (Scala) "Uint32.less"
 | constant "NOT :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Int32.lognot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Int32.logand" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Int32.logor" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Int32.logxor" and
   (Scala) infixl 2 "^"
 
 definition uint32_divmod :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32 \<times> uint32" where
   "uint32_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32), undefined ((mod) :: uint32 \<Rightarrow> _) x (0 :: uint32)) 
   else (x div y, x mod y))"
 
 definition uint32_div :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" 
 where "uint32_div x y = fst (uint32_divmod x y)"
 
 definition uint32_mod :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" 
 where "uint32_mod x y = snd (uint32_divmod x y)"
 
 lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)"
 including undefined_transfer unfolding uint32_divmod_def uint32_div_def
 by transfer (simp add: word_div_def)
 
 lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)"
 including undefined_transfer unfolding uint32_mod_def uint32_divmod_def
 by transfer (simp add: word_mod_def)
 
 definition uint32_sdiv :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32"
 where [code del]:
   "uint32_sdiv x y =
    (if y = 0 then undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32)
     else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))"
 
 definition div0_uint32 :: "uint32 \<Rightarrow> uint32"
 where [code del]: "div0_uint32 x = undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32)"
 declare [[code abort: div0_uint32]]
 
 definition mod0_uint32 :: "uint32 \<Rightarrow> uint32"
 where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32 \<Rightarrow> _) x (0 :: uint32)"
 declare [[code abort: mod0_uint32]]
 
 lemma uint32_divmod_code [code]:
   "uint32_divmod x y =
   (if 0x80000000 \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint32 x, mod0_uint32 x)
    else let q = (uint32_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def
 by transfer(simp add: divmod_via_sdivmod)
 
 lemma uint32_sdiv_code [code abstract]:
   "Rep_uint32 (uint32_sdiv x y) =
    (if y = 0 then Rep_uint32 (undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32))
     else Rep_uint32 x sdiv Rep_uint32 y)"
 unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint32_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint32_div \<rightharpoonup>
   (SML) "Word32.div ((_), (_))" and
   (Haskell) "Prelude.div"
 | constant uint32_mod \<rightharpoonup>
   (SML) "Word32.mod ((_), (_))" and
   (Haskell) "Prelude.mod"
 | constant uint32_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint32_sdiv \<rightharpoonup>
   (OCaml) "Int32.div" and
   (Scala) "_ '/ _"
 
 definition uint32_test_bit :: "uint32 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint32_test_bit x n =
   (if n < 0 \<or> 31 < n then undefined (test_bit :: uint32 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint32 [code]:
   \<open>test_bit = (bit :: uint32 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint32_code [code]:
   "bit x n \<longleftrightarrow> n < 32 \<and> uint32_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint32_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint32_test_bit_code [code]:
   "uint32_test_bit w n =
   (if n < 0 \<or> 31 < n then undefined (test_bit :: uint32 \<Rightarrow> _) w n else Rep_uint32 w !! nat_of_integer n)"
 unfolding uint32_test_bit_def
 by(simp add: test_bit_uint32.rep_eq)
 
 code_printing constant uint32_test_bit \<rightharpoonup>
   (SML) "Uint32.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint32.test'_bit" and
   (Scala) "Uint32.test'_bit" and
   (Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)"
 
 definition uint32_set_bit :: "uint32 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint32"
 where [code del]:
   "uint32_set_bit x n b =
   (if n < 0 \<or> 31 < n then undefined (set_bit :: uint32 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint32_code [code]:
   "set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint32_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint32_set_bit_code [code abstract]:
   "Rep_uint32 (uint32_set_bit w n b) = 
   (if n < 0 \<or> 31 < n then Rep_uint32 (undefined (set_bit :: uint32 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint32 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint32_set_bit_def by transfer simp
 
 code_printing constant uint32_set_bit \<rightharpoonup>
   (SML) "Uint32.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint32.set'_bit" and
   (Scala) "Uint32.set'_bit" and
   (Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)"
 
 lift_definition uint32_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint32 \<Rightarrow> nat \<Rightarrow> uint32" is set_bits_aux .
 
 lemma uint32_set_bits_code [code]:
   "uint32_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint32_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint32 [code]:
   "(BITS n. f n) = uint32_set_bits f 0 32"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint32 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint32_shiftl :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_shiftl x n = (if n < 0 \<or> 32 \<le> n then undefined (shiftl :: uint32 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint32_code [code]: "x << n = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint32_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint32_shiftl_code [code abstract]:
   "Rep_uint32 (uint32_shiftl w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined (shiftl :: uint32 \<Rightarrow> _) w n) else Rep_uint32 w << (nat_of_integer n))"
 including undefined_transfer unfolding uint32_shiftl_def by transfer simp
 
 code_printing constant uint32_shiftl \<rightharpoonup>
   (SML) "Uint32.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint32.shiftl" and
   (Scala) "Uint32.shiftl" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)"
 
 definition uint32_shiftr :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_shiftr x n = (if n < 0 \<or> 32 \<le> n then undefined (shiftr :: uint32 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint32_code [code]: "x >> n = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint32_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint32_shiftr_code [code abstract]:
   "Rep_uint32 (uint32_shiftr w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined (shiftr :: uint32 \<Rightarrow> _) w n) else Rep_uint32 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint32_shiftr_def by transfer simp
 
 code_printing constant uint32_shiftr \<rightharpoonup>
   (SML) "Uint32.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint32.shiftr" and
   (Scala) "Uint32.shiftr" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)"
 
 definition uint32_sshiftr :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_sshiftr x n =
   (if n < 0 \<or> 32 \<le> n then undefined sshiftr_uint32 x n else sshiftr_uint32 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint32_code [code]:
   "x >>> n = 
   (if n < 32 then uint32_sshiftr x (integer_of_nat n) else if x !! 31 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint32_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size)
 
 lemma uint32_sshiftr_code [code abstract]:
   "Rep_uint32 (uint32_sshiftr w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined sshiftr_uint32 w n) else Rep_uint32 w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint32_sshiftr_def by transfer simp
 
 code_printing constant uint32_sshiftr \<rightharpoonup>
   (SML) "Uint32.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and
   (OCaml) "Uint32.shiftr'_signed" and
   (Scala) "Uint32.shiftr'_signed" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)"
 
 lemma uint32_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint32) !! 31"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint32_code [code]: "msb x \<longleftrightarrow> uint32_test_bit x 31"
 by(simp add: uint32_test_bit_def uint32_msb_test_bit)
 
 lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint32_code [code]:
   "int_of_uint32 x = int_of_integer (integer_of_uint32 x)"
 by(simp add: integer_of_uint32_def)
 
 lemma nat_of_uint32_code [code]:
   "nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)"
 unfolding integer_of_uint32_def including integer.lifting by transfer simp
 
 definition integer_of_uint32_signed :: "uint32 \<Rightarrow> integer"
 where
   "integer_of_uint32_signed n = (if n !! 31 then undefined integer_of_uint32 n else integer_of_uint32 n)"
 
 lemma integer_of_uint32_signed_code [code]:
   "integer_of_uint32_signed n =
   (if n !! 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))"
 unfolding integer_of_uint32_signed_def integer_of_uint32_def
 including undefined_transfer by transfer simp
 
 lemma integer_of_uint32_code [code]:
   "integer_of_uint32 n =
   (if n !! 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)"
 unfolding integer_of_uint32_def integer_of_uint32_signed_def o_def
 including undefined_transfer integer.lifting
 by transfer(auto simp add: word_ao_nth uint_and_mask_or_full mask_numeral mask_Suc_0 intro!: uint_and_mask_or_full[symmetric])
 
 code_printing
   constant "integer_of_uint32" \<rightharpoonup>
   (SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and
   (Haskell) "Prelude.toInteger"
 | constant "integer_of_uint32_signed" \<rightharpoonup>
   (OCaml) "Z.of'_int32" and
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint32_of_natural :: "natural \<Rightarrow> uint32"
 where "uint32_of_natural x \<equiv> Uint32 (integer_of_natural x)"
 
 instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint32 \<equiv> qc_random_cnv uint32_of_natural"
 definition "exhaustive_uint32 \<equiv> qc_exhaustive_cnv uint32_of_natural"
 definition "full_exhaustive_uint32 \<equiv> qc_full_exhaustive_cnv uint32_of_natural"
 instance ..
 end
 
 instantiation uint32 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0"
   "Typerep.Typerep (STR ''Uint32.uint32'') []" .
 
 definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint32 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint32 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint32 (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy
--- a/thys/Native_Word/Uint64.thy
+++ b/thys/Native_Word/Uint64.thy
@@ -1,949 +1,949 @@
 (*  Title:      Uint64.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 64 bits\<close>
 
 theory Uint64 imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode.
   Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and
   masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations
   directly to the \verb$Word64$ structure provided by the Standard ML implementations.
 
   The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at
   runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit 
   version which does not suffer from a division bug found in PolyML 5.6.
 \<close>
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint64 = "UNIV :: 64 word set" .. 
 
 setup_lifting type_definition_uint64
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint64}.\<close>
 declare Rep_uint64_inverse[code abstype]
 
 declare Quotient_uint64[transfer_rule]
 
 instantiation uint64 :: comm_ring_1
 begin
 lift_definition zero_uint64 :: uint64 is "0 :: 64 word" .
 lift_definition one_uint64 :: uint64 is "1" .
 lift_definition plus_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(+) :: 64 word \<Rightarrow> _" .
 lift_definition minus_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(-)" .
 lift_definition uminus_uint64 :: "uint64 \<Rightarrow> uint64" is uminus .
 lift_definition times_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint64 :: semiring_modulo
 begin
 lift_definition divide_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(div)" .
 lift_definition modulo_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint64 :: linorder begin
 lift_definition less_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint64.rep_eq less_eq_uint64.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint64) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint64) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint64 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint64 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint64 :: semiring_bits
 begin
 
 lift_definition bit_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint64 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is push_bit .
 lift_definition drop_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is drop_bit .
 lift_definition take_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint64 :: ring_bit_operations
 begin
 lift_definition not_uint64 :: \<open>uint64 \<Rightarrow> uint64\<close> is NOT .
 lift_definition and_uint64 :: \<open>uint64 \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is \<open>(AND)\<close> .
 lift_definition or_uint64 :: \<open>uint64 \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is \<open>(OR)\<close> .
 lift_definition xor_uint64 :: \<open>uint64 \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is \<open>(XOR)\<close> .
 lift_definition mask_uint64 :: \<open>nat \<Rightarrow> uint64\<close> is mask .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
 end
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: uint64
   by (fact take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: uint64) OR mask n\<close>
   \<open>mask 0 = (0 :: uint64)\<close>
   by (simp_all add: mask_Suc_exp push_bit_of_1)
 
 instantiation uint64:: semiring_bit_syntax
 begin
 lift_definition test_bit_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> bool\<close> is test_bit .
 lift_definition shiftl_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> uint64\<close> is shiftl .
 lift_definition shiftr_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> uint64\<close> is shiftr .
 instance by (standard; transfer)
   (fact test_bit_eq_bit shiftl_word_eq shiftr_word_eq)+
 end
 
 instantiation uint64 :: lsb
 begin
 lift_definition lsb_uint64 :: \<open>uint64 \<Rightarrow> bool\<close> is lsb .
 instance by (standard; transfer)
   (fact lsb_odd)
 end
 
 instantiation uint64 :: msb
 begin
 lift_definition msb_uint64 :: \<open>uint64 \<Rightarrow> bool\<close> is msb .
 instance ..
 end
 
 instantiation uint64 :: set_bit
 begin
 lift_definition set_bit_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint64\<close> is set_bit .
 instance
   apply standard
   apply (unfold Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply (simp add: set_bit_eq Bit_Operations.set_bit_def unset_bit_def)
   done
 end
 
 instantiation uint64 :: bit_comprehension begin
 lift_definition set_bits_uint64 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint64" is "set_bits" .
-instance ..
+instance by (standard; transfer) (fact set_bits_bit_eq)
 end
 
 lemmas [code] = test_bit_uint64.rep_eq lsb_uint64.rep_eq msb_uint64.rep_eq
 
 instantiation uint64 :: equal begin
 lift_definition equal_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint64.rep_eq
 
 instantiation uint64 :: size begin
 lift_definition size_uint64 :: "uint64 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint64.rep_eq
 
 lift_definition sshiftr_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> uint64" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint64_of_int :: "int \<Rightarrow> uint64" is "word_of_int" .
 
 definition uint64_of_nat :: "nat \<Rightarrow> uint64"
 where "uint64_of_nat = uint64_of_int \<circ> int"
 
 lift_definition int_of_uint64 :: "uint64 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint64 :: "uint64 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint64 :: "uint64 \<Rightarrow> integer"
 where "integer_of_uint64 = integer_of_int o int_of_uint64"
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint64 :: "integer \<Rightarrow> uint64" is "word_of_int" .
 
 lemma Rep_uint64_numeral [simp]: "Rep_uint64 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint64_def Abs_uint64_inverse numeral.simps plus_uint64_def)
 
 lemma numeral_uint64_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint64) numeral numeral"
 by(auto simp add: cr_uint64_def)
 
 lemma numeral_uint64 [code_unfold]: "numeral n = Uint64 (numeral n)"
 by transfer simp
 
 lemma Rep_uint64_neg_numeral [simp]: "Rep_uint64 (- numeral n) = - numeral n"
 by(simp only: uminus_uint64_def)(simp add: Abs_uint64_inverse)
 
 lemma neg_numeral_uint64 [code_unfold]: "- numeral n = Uint64 (- numeral n)"
 by transfer(simp add: cr_uint64_def)
 
 end
 
 lemma Abs_uint64_numeral [code_post]: "Abs_uint64 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint64_def numeral.simps plus_uint64_def Abs_uint64_inverse)
 
 lemma Abs_uint64_0 [code_post]: "Abs_uint64 0 = 0"
 by(simp add: zero_uint64_def)
 
 lemma Abs_uint64_1 [code_post]: "Abs_uint64 1 = 1"
 by(simp add: one_uint64_def)
 
 section \<open>Code setup\<close>
 
 text \<open> For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$.
   If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume
   that there is also a \<open>Word64\<close> structure available and accordingly replace the implementation
   for the target \verb$Eval$.
 \<close>
 code_printing code_module "Uint64" \<rightharpoonup> (SML) \<open>(* Test that words can handle numbers between 0 and 63 *)
 val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6"));
 
 structure Uint64 : sig
   eqtype uint64;
   val zero : uint64;
   val one : uint64;
   val fromInt : IntInf.int -> uint64;
   val toInt : uint64 -> IntInf.int;
   val toLarge : uint64 -> LargeWord.word;
   val fromLarge : LargeWord.word -> uint64
   val plus : uint64 -> uint64 -> uint64;
   val minus : uint64 -> uint64 -> uint64;
   val times : uint64 -> uint64 -> uint64;
   val divide : uint64 -> uint64 -> uint64;
   val modulus : uint64 -> uint64 -> uint64;
   val negate : uint64 -> uint64;
   val less_eq : uint64 -> uint64 -> bool;
   val less : uint64 -> uint64 -> bool;
   val notb : uint64 -> uint64;
   val andb : uint64 -> uint64 -> uint64;
   val orb : uint64 -> uint64 -> uint64;
   val xorb : uint64 -> uint64 -> uint64;
   val shiftl : uint64 -> IntInf.int -> uint64;
   val shiftr : uint64 -> IntInf.int -> uint64;
   val shiftr_signed : uint64 -> IntInf.int -> uint64;
   val set_bit : uint64 -> IntInf.int -> bool -> uint64;
   val test_bit : uint64 -> IntInf.int -> bool;
 end = struct
 
 type uint64 = IntInf.int;
 
 val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int;
 
 val zero = 0 : IntInf.int;
 
 val one = 1 : IntInf.int;
 
 fun fromInt x = IntInf.andb(x, mask);
 
 fun toInt x = x
 
 fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x);
 
 fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x);
 
 fun plus x y = IntInf.andb(IntInf.+(x, y), mask);
 
 fun minus x y = IntInf.andb(IntInf.-(x, y), mask);
 
 fun negate x = IntInf.andb(IntInf.~(x), mask);
 
 fun times x y = IntInf.andb(IntInf.*(x, y), mask);
 
 fun divide x y = IntInf.div(x, y);
 
 fun modulus x y = IntInf.mod(x, y);
 
 fun less_eq x y = IntInf.<=(x, y);
 
 fun less x y = IntInf.<(x, y);
 
 fun notb x = IntInf.andb(IntInf.notb(x), mask);
 
 fun orb x y = IntInf.orb(x, y);
 
 fun andb x y = IntInf.andb(x, y);
 
 fun xorb x y = IntInf.xorb(x, y);
 
 val maxWord = IntInf.pow (2, Word.wordSize);
 
 fun shiftl x n = 
   if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask)
   else 0;
 
 fun shiftr x n =
   if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
   else 0;
 
 val msb_mask = 0x8000000000000000 : IntInf.int;
 
 fun shiftr_signed x i =
   if IntInf.andb(x, msb_mask) = 0 then shiftr x i
   else if i >= 64 then 0xFFFFFFFFFFFFFFFF
   else let
     val x' = shiftr x i
     val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask)
   in IntInf.orb(x', m') end;
 
 fun test_bit x n =
   if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
   else false;
 
 fun set_bit x n b =
   if n < 64 then
     if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
     else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
   else x;
 
 end
 \<close>
 code_reserved SML Uint64
 
 setup \<open>
 let
   val polyml64 = LargeWord.wordSize > 63;
   (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain
      from using Word64 in that case. Testing is done with dynamic code evaluation such that
      the compiler does not choke on the Word64 structure, which need not be present in a 32bit
      environment. *)
   val error_msg = "Buggy Word64 structure";
   val test_code = 
    "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^
    "else raise (Fail \"" ^ error_msg ^ "\");";
   val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code))
   val use_Word64 = polyml64 andalso
     (case f () of 
        Exn.Res _ => true
      | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e
      | Exn.Exn e => Exn.reraise e)
     ;
 
   val newline = "\n";
   val content = 
     "structure Uint64 : sig" ^ newline ^
     "  eqtype uint64;" ^ newline ^
     "  val zero : uint64;" ^ newline ^
     "  val one : uint64;" ^ newline ^
     "  val fromInt : IntInf.int -> uint64;" ^ newline ^
     "  val toInt : uint64 -> IntInf.int;" ^ newline ^
     "  val toLarge : uint64 -> LargeWord.word;" ^ newline ^
     "  val fromLarge : LargeWord.word -> uint64" ^ newline ^
     "  val plus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val minus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val times : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val divide : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val modulus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val negate : uint64 -> uint64;" ^ newline ^
     "  val less_eq : uint64 -> uint64 -> bool;" ^ newline ^
     "  val less : uint64 -> uint64 -> bool;" ^ newline ^
     "  val notb : uint64 -> uint64;" ^ newline ^
     "  val andb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val orb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val xorb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^
     "  val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^
     "end = struct" ^ newline ^
     "" ^ newline ^
     "type uint64 = Word64.word;" ^ newline ^
     "" ^ newline ^
     "val zero = (0wx0 : uint64);" ^ newline ^
     "" ^ newline ^
     "val one = (0wx1 : uint64);" ^ newline ^
     "" ^ newline ^
     "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^
     "" ^ newline ^
     "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);"  ^ newline ^
     "" ^ newline ^
     "fun fromLarge x = Word64.fromLarge x;" ^ newline ^
     "" ^ newline ^
     "fun toLarge x = Word64.toLarge x;"  ^ newline ^
     "" ^ newline ^
     "fun plus x y = Word64.+(x, y);" ^ newline ^
     "" ^ newline ^
     "fun minus x y = Word64.-(x, y);" ^ newline ^
     "" ^ newline ^
     "fun negate x = Word64.~(x);" ^ newline ^
     "" ^ newline ^
     "fun times x y = Word64.*(x, y);" ^ newline ^
     "" ^ newline ^
     "fun divide x y = Word64.div(x, y);" ^ newline ^
     "" ^ newline ^
     "fun modulus x y = Word64.mod(x, y);" ^ newline ^
     "" ^ newline ^
     "fun less_eq x y = Word64.<=(x, y);" ^ newline ^
     "" ^ newline ^
     "fun less x y = Word64.<(x, y);" ^ newline ^
     "" ^ newline ^
     "fun set_bit x n b =" ^ newline ^
     "  let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "  in if b then Word64.orb (x, mask)" ^ newline ^
     "     else Word64.andb (x, Word64.notb mask)" ^ newline ^
     "  end" ^ newline ^
     "" ^ newline ^
     "fun shiftl x n =" ^ newline ^
     "  Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun shiftr x n =" ^ newline ^
     "  Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun shiftr_signed x n =" ^ newline ^
     "  Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun test_bit x n =" ^ newline ^
     "  Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^
     "" ^ newline ^
     "val notb = Word64.notb" ^ newline ^
     "" ^ newline ^
     "fun andb x y = Word64.andb(x, y);" ^ newline ^
     "" ^ newline ^
     "fun orb x y = Word64.orb(x, y);" ^ newline ^
     "" ^ newline ^
     "fun xorb x y = Word64.xorb(x, y);" ^ newline ^
     "" ^ newline ^
     "end (*struct Uint64*)"
   val target_SML64 = "SML_word";
 in
   (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I)
   #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))]))
 end
 \<close>
 
 code_printing code_module Uint64 \<rightharpoonup> (Haskell)
  \<open>module Uint64(Int64, Word64) where
 
   import Data.Int(Int64)
   import Data.Word(Word64)\<close>
 code_reserved Haskell Uint64
 
 text \<open>
   OCaml and Scala provide only signed 64bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 code_printing code_module "Uint64" \<rightharpoonup> (OCaml)
 \<open>module Uint64 : sig
   val less : int64 -> int64 -> bool
   val less_eq : int64 -> int64 -> bool
   val set_bit : int64 -> Z.t -> bool -> int64
   val shiftl : int64 -> Z.t -> int64
   val shiftr : int64 -> Z.t -> int64
   val shiftr_signed : int64 -> Z.t -> int64
   val test_bit : int64 -> Z.t -> bool
 end = struct
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if Int64.compare x Int64.zero < 0 then
     Int64.compare y Int64.zero < 0 && Int64.compare x y < 0
   else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;;
 
 let less_eq x y =
   if Int64.compare x Int64.zero < 0 then
     Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0
   else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;;
 
 let set_bit x n b =
   let mask = Int64.shift_left Int64.one (Z.to_int n)
   in if b then Int64.logor x mask
      else Int64.logand x (Int64.lognot mask);;
 
 let shiftl x n = Int64.shift_left x (Z.to_int n);;
 
 let shiftr x n = Int64.shift_right_logical x (Z.to_int n);;
 
 let shiftr_signed x n = Int64.shift_right x (Z.to_int n);;
 
 let test_bit x n =
   Int64.compare 
     (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n)))
     Int64.zero
   <> 0;;
 
 end;; (*struct Uint64*)\<close>
 code_reserved OCaml Uint64
 
 code_printing code_module Uint64 \<rightharpoonup> (Scala)
 \<open>object Uint64 {
 
 def less(x: Long, y: Long) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Long, y: Long) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Long, n: BigInt, b: Boolean) : Long =
   if (b)
     x | (1L << n.intValue)
   else
     x & (1L << n.intValue).unary_~
 
 def shiftl(x: Long, n: BigInt) : Long = x << n.intValue
 
 def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue
 
 def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue
 
 def test_bit(x: Long, n: BigInt) : Boolean =
   (x & (1L << n.intValue)) != 0
 
 } /* object Uint64 */\<close>
 code_reserved Scala Uint64
 
 text \<open>
   OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer.
   The following justifies the implementation.
 \<close>
 
 definition Uint64_signed :: "integer \<Rightarrow> uint64" 
 where "Uint64_signed i = (if i < -(0x8000000000000000) \<or> i \<ge> 0x8000000000000000 then undefined Uint64 i else Uint64 i)"
 
 lemma Uint64_code [code]:
   "Uint64 i = 
   (let i' = i AND 0xFFFFFFFFFFFFFFFF
    in if i' !! 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')"
 including undefined_transfer integer.lifting unfolding Uint64_signed_def
 by transfer(rule word_of_int_via_signed, simp_all add: bin_mask_numeral)
 
 lemma Uint64_signed_code [code abstract]:
   "Rep_uint64 (Uint64_signed i) = 
   (if i < -(0x8000000000000000) \<or> i \<ge> 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))"
 unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def word_of_integer_def
 by(simp add: Abs_uint64_inverse)
 
 text \<open>
   Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint64}.
 
   The new destructor @{term Rep_uint64'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint64} 
   ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because
   these instances will be folded away.)
 
   To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}.
 \<close>
 
 definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64"
 
 lemma Rep_uint64'_transfer [transfer_rule]:
   "rel_fun cr_uint64 (=) (\<lambda>x. x) Rep_uint64'"
 unfolding Rep_uint64'_def by(rule uint64.rep_transfer)
 
 lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint64' :: "64 word \<Rightarrow> uint64" is "\<lambda>x :: 64 word. x" .
 
 lemma Abs_uint64'_code [code]:
   "Abs_uint64' x = Uint64 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint64 \<Rightarrow> _"]]
 
 lemma term_of_uint64_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []]))
        (term_of_class.term_of (Rep_uint64' x))"
 by(simp add: term_of_anything)
 
 code_printing
   type_constructor uint64 \<rightharpoonup>
   (SML) "Uint64.uint64" and
   (Haskell) "Uint64.Word64" and
   (OCaml) "int64" and
   (Scala) "Long"
 | constant Uint64 \<rightharpoonup>
   (SML) "Uint64.fromInt" and
   (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and
   (Scala) "_.longValue"
 | constant Uint64_signed \<rightharpoonup>
   (OCaml) "Z.to'_int64"
 | constant "0 :: uint64" \<rightharpoonup>
   (SML) "Uint64.zero" and
   (Haskell) "(0 :: Uint64.Word64)" and
   (OCaml) "Int64.zero" and
   (Scala) "0"
 | constant "1 :: uint64" \<rightharpoonup>
   (SML) "Uint64.one" and
   (Haskell) "(1 :: Uint64.Word64)" and
   (OCaml) "Int64.one" and
   (Scala) "1"
 | constant "plus :: uint64 \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Uint64.plus" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Int64.add" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.negate" and
   (Haskell) "negate" and
   (OCaml) "Int64.neg" and
   (Scala) "!(- _)"
 | constant "minus :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.minus" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Int64.sub" and
   (Scala) infixl 7 "-"
 | constant "times :: uint64 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.times" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Int64.mul" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Uint64.uint64) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Int64.compare _ _ = 0)" and
   (Scala) infixl 5 "=="
 | class_instance uint64 :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Uint64.less'_eq" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint64.less'_eq" and
   (Scala) "Uint64.less'_eq"
 | constant "less :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Uint64.less" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint64.less" and
   (Scala) "Uint64.less"
 | constant "NOT :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Int64.lognot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.andb" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Int64.logand" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.orb" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Int64.logor" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.xorb" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Int64.logxor" and
   (Scala) infixl 2 "^"
 
 definition uint64_divmod :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64 \<times> uint64" where
   "uint64_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64), undefined ((mod) :: uint64 \<Rightarrow> _) x (0 :: uint64)) 
   else (x div y, x mod y))"
 
 definition uint64_div :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" 
 where "uint64_div x y = fst (uint64_divmod x y)"
 
 definition uint64_mod :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" 
 where "uint64_mod x y = snd (uint64_divmod x y)"
 
 lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)"
 including undefined_transfer unfolding uint64_divmod_def uint64_div_def
 by transfer (simp add: word_div_def)
 
 lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)"
 including undefined_transfer unfolding uint64_mod_def uint64_divmod_def
 by transfer (simp add: word_mod_def)
 
 definition uint64_sdiv :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64"
 where [code del]:
   "uint64_sdiv x y =
    (if y = 0 then undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64)
     else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))"
 
 definition div0_uint64 :: "uint64 \<Rightarrow> uint64"
 where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64)"
 declare [[code abort: div0_uint64]]
 
 definition mod0_uint64 :: "uint64 \<Rightarrow> uint64"
 where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \<Rightarrow> _) x (0 :: uint64)"
 declare [[code abort: mod0_uint64]]
 
 lemma uint64_divmod_code [code]:
   "uint64_divmod x y =
   (if 0x8000000000000000 \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint64 x, mod0_uint64 x)
    else let q = (uint64_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def
 by transfer(simp add: divmod_via_sdivmod)
 
 lemma uint64_sdiv_code [code abstract]:
   "Rep_uint64 (uint64_sdiv x y) =
    (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64))
     else Rep_uint64 x sdiv Rep_uint64 y)"
 unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint64_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint64_div \<rightharpoonup>
   (SML) "Uint64.divide" and
   (Haskell) "Prelude.div"
 | constant uint64_mod \<rightharpoonup>
   (SML) "Uint64.modulus" and
   (Haskell) "Prelude.mod"
 | constant uint64_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint64_sdiv \<rightharpoonup>
   (OCaml) "Int64.div" and
   (Scala) "_ '/ _"
 
 definition uint64_test_bit :: "uint64 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint64_test_bit x n =
   (if n < 0 \<or> 63 < n then undefined (test_bit :: uint64 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint64 [code]:
   \<open>test_bit = (bit :: uint64 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma bit_uint64_code [code]:
   "bit x n \<longleftrightarrow> n < 64 \<and> uint64_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint64_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint64_test_bit_code [code]:
   "uint64_test_bit w n =
   (if n < 0 \<or> 63 < n then undefined (test_bit :: uint64 \<Rightarrow> _) w n else Rep_uint64 w !! nat_of_integer n)"
 unfolding uint64_test_bit_def
 by(simp add: test_bit_uint64.rep_eq)
 
 code_printing constant uint64_test_bit \<rightharpoonup>
   (SML) "Uint64.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint64.test'_bit" and
   (Scala) "Uint64.test'_bit" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)"
 
 definition uint64_set_bit :: "uint64 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint64"
 where [code del]:
   "uint64_set_bit x n b =
   (if n < 0 \<or> 63 < n then undefined (set_bit :: uint64 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint64_code [code]:
   "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint64_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint64_set_bit_code [code abstract]:
   "Rep_uint64 (uint64_set_bit w n b) = 
   (if n < 0 \<or> 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint64 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint64_set_bit_def by transfer simp
 
 code_printing constant uint64_set_bit \<rightharpoonup>
   (SML) "Uint64.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint64.set'_bit" and
   (Scala) "Uint64.set'_bit" and
   (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)"
 
 lift_definition uint64_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint64 \<Rightarrow> nat \<Rightarrow> uint64" is set_bits_aux .
 
 lemma uint64_set_bits_code [code]:
   "uint64_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint64_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint64 [code]:
   "(BITS n. f n) = uint64_set_bits f 0 64"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint64 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint64_shiftl :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_shiftl x n = (if n < 0 \<or> 64 \<le> n then undefined (shiftl :: uint64 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint64_code [code]: "x << n = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint64_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint64_shiftl_code [code abstract]:
   "Rep_uint64 (uint64_shiftl w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined (shiftl :: uint64 \<Rightarrow> _) w n) else Rep_uint64 w << (nat_of_integer n))"
 including undefined_transfer unfolding uint64_shiftl_def by transfer simp
 
 code_printing constant uint64_shiftl \<rightharpoonup>
   (SML) "Uint64.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint64.shiftl" and
   (Scala) "Uint64.shiftl" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)"
 
 
 definition uint64_shiftr :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_shiftr x n = (if n < 0 \<or> 64 \<le> n then undefined (shiftr :: uint64 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint64_code [code]: "x >> n = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint64_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint64_shiftr_code [code abstract]:
   "Rep_uint64 (uint64_shiftr w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined (shiftr :: uint64 \<Rightarrow> _) w n) else Rep_uint64 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint64_shiftr_def by transfer simp
 
 code_printing constant uint64_shiftr \<rightharpoonup>
   (SML) "Uint64.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint64.shiftr" and
   (Scala) "Uint64.shiftr" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)"
 
 
 definition uint64_sshiftr :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_sshiftr x n =
   (if n < 0 \<or> 64 \<le> n then undefined sshiftr_uint64 x n else sshiftr_uint64 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint64_code [code]:
   "x >>> n = 
   (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if x !! 63 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint64_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size)
 
 lemma uint64_sshiftr_code [code abstract]:
   "Rep_uint64 (uint64_sshiftr w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined sshiftr_uint64 w n) else Rep_uint64 w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint64_sshiftr_def by transfer simp
 
 code_printing constant uint64_sshiftr \<rightharpoonup>
   (SML) "Uint64.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and
   (OCaml) "Uint64.shiftr'_signed" and
   (Scala) "Uint64.shiftr'_signed" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)"
 
 
 lemma uint64_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint64) !! 63"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint64_code [code]: "msb x \<longleftrightarrow> uint64_test_bit x 63"
 by(simp add: uint64_test_bit_def uint64_msb_test_bit)
 
 lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint64_code [code]:
   "int_of_uint64 x = int_of_integer (integer_of_uint64 x)"
 by(simp add: integer_of_uint64_def)
 
 lemma nat_of_uint64_code [code]:
   "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)"
 unfolding integer_of_uint64_def including integer.lifting by transfer simp
 
 definition integer_of_uint64_signed :: "uint64 \<Rightarrow> integer"
 where
   "integer_of_uint64_signed n = (if n !! 63 then undefined integer_of_uint64 n else integer_of_uint64 n)"
 
 lemma integer_of_uint64_signed_code [code]:
   "integer_of_uint64_signed n =
   (if n !! 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))"
 unfolding integer_of_uint64_signed_def integer_of_uint64_def
 including undefined_transfer by transfer simp
 
 lemma integer_of_uint64_code [code]:
   "integer_of_uint64 n =
   (if n !! 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)"
 unfolding integer_of_uint64_def integer_of_uint64_signed_def o_def
 including undefined_transfer integer.lifting
 by transfer(auto simp add: word_ao_nth uint_and_mask_or_full mask_numeral mask_Suc_0 intro!: uint_and_mask_or_full[symmetric])
 
 code_printing
   constant "integer_of_uint64" \<rightharpoonup>
   (SML) "Uint64.toInt" and
   (Haskell) "Prelude.toInteger"
 | constant "integer_of_uint64_signed" \<rightharpoonup>
   (OCaml) "Z.of'_int64" and
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint64_of_natural :: "natural \<Rightarrow> uint64"
 where "uint64_of_natural x \<equiv> Uint64 (integer_of_natural x)"
 
 instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint64 \<equiv> qc_random_cnv uint64_of_natural"
 definition "exhaustive_uint64 \<equiv> qc_exhaustive_cnv uint64_of_natural"
 definition "full_exhaustive_uint64 \<equiv> qc_full_exhaustive_cnv uint64_of_natural"
 instance ..
 end
 
 instantiation uint64 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0"
   "Typerep.Typerep (STR ''Uint64.uint64'') []" .
 
 definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint64 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint64 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint64 (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint8.thy b/thys/Native_Word/Uint8.thy
--- a/thys/Native_Word/Uint8.thy
+++ b/thys/Native_Word/Uint8.thy
@@ -1,672 +1,672 @@
 (*  Title:      Uint8.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 8 bits\<close>
 
 theory Uint8 imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   Restriction for OCaml code generation:
   OCaml does not provide an int8 type, so no special code generation 
   for this type is set up. If the theory \<open>Code_Target_Bits_Int\<close>
   is imported, the type \<open>uint8\<close> is emulated via @{typ "8 word"}.
 \<close>
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint8 = "UNIV :: 8 word set" ..
 
 setup_lifting type_definition_uint8
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint8}.\<close>
 declare Rep_uint8_inverse[code abstype]
 
 declare Quotient_uint8[transfer_rule]
 
 instantiation uint8 :: comm_ring_1
 begin
 lift_definition zero_uint8 :: uint8 is "0 :: 8 word" .
 lift_definition one_uint8 :: uint8 is "1" .
 lift_definition plus_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" is "(+) :: 8 word \<Rightarrow> _" .
 lift_definition minus_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" is "(-)" .
 lift_definition uminus_uint8 :: "uint8 \<Rightarrow> uint8" is uminus .
 lift_definition times_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint8 :: semiring_modulo
 begin
 lift_definition divide_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" is "(div)" .
 lift_definition modulo_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint8 :: linorder begin
 lift_definition less_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint8.rep_eq less_eq_uint8.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint8) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint8) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint8 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint8 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint8 :: semiring_bits
 begin
 
 lift_definition bit_uint8 :: \<open>uint8 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint8 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint8 :: \<open>nat \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is push_bit .
 lift_definition drop_bit_uint8 :: \<open>nat \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is drop_bit .
 lift_definition take_bit_uint8 :: \<open>nat \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint8 :: ring_bit_operations
 begin
 lift_definition not_uint8 :: \<open>uint8 \<Rightarrow> uint8\<close> is NOT .
 lift_definition and_uint8 :: \<open>uint8 \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is \<open>(AND)\<close> .
 lift_definition or_uint8 :: \<open>uint8 \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is \<open>(OR)\<close> .
 lift_definition xor_uint8 :: \<open>uint8 \<Rightarrow> uint8 \<Rightarrow> uint8\<close> is \<open>(XOR)\<close> .
 lift_definition mask_uint8 :: \<open>nat \<Rightarrow> uint8\<close> is mask .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
 end
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: uint8
   by (fact take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: uint8) OR mask n\<close>
   \<open>mask 0 = (0 :: uint8)\<close>
   by (simp_all add: mask_Suc_exp push_bit_of_1)
 
 instantiation uint8:: semiring_bit_syntax
 begin
 lift_definition test_bit_uint8 :: \<open>uint8 \<Rightarrow> nat \<Rightarrow> bool\<close> is test_bit .
 lift_definition shiftl_uint8 :: \<open>uint8 \<Rightarrow> nat \<Rightarrow> uint8\<close> is shiftl .
 lift_definition shiftr_uint8 :: \<open>uint8 \<Rightarrow> nat \<Rightarrow> uint8\<close> is shiftr .
 instance by (standard; transfer)
   (fact test_bit_eq_bit shiftl_word_eq shiftr_word_eq)+
 end
 
 instantiation uint8 :: lsb
 begin
 lift_definition lsb_uint8 :: \<open>uint8 \<Rightarrow> bool\<close> is lsb .
 instance by (standard; transfer)
   (fact lsb_odd)
 end
 
 instantiation uint8 :: msb
 begin
 lift_definition msb_uint8 :: \<open>uint8 \<Rightarrow> bool\<close> is msb .
 instance ..
 end
 
 instantiation uint8 :: set_bit
 begin
 lift_definition set_bit_uint8 :: \<open>uint8 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint8\<close> is set_bit .
 instance
   apply standard
   apply (unfold Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply (simp add: set_bit_eq Bit_Operations.set_bit_def unset_bit_def)
   done
 end
 
 instantiation uint8 :: bit_comprehension begin
 lift_definition set_bits_uint8 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint8" is "set_bits" .
-instance ..
+instance by (standard; transfer) (fact set_bits_bit_eq)
 end
 
 lemmas [code] = test_bit_uint8.rep_eq lsb_uint8.rep_eq msb_uint8.rep_eq
 
 instantiation uint8 :: equal begin
 lift_definition equal_uint8 :: "uint8 \<Rightarrow> uint8 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint8.rep_eq
 
 instantiation uint8 :: size begin
 lift_definition size_uint8 :: "uint8 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint8.rep_eq
 
 lift_definition sshiftr_uint8 :: "uint8 \<Rightarrow> nat \<Rightarrow> uint8" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint8_of_int :: "int \<Rightarrow> uint8" is "word_of_int" .
 
 definition uint8_of_nat :: "nat \<Rightarrow> uint8"
 where "uint8_of_nat = uint8_of_int \<circ> int"
 
 lift_definition int_of_uint8 :: "uint8 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint8 :: "uint8 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint8 :: "uint8 \<Rightarrow> integer"
 where "integer_of_uint8 = integer_of_int o int_of_uint8"
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint8 :: "integer \<Rightarrow> uint8" is "word_of_int" .
 
 lemma Rep_uint8_numeral [simp]: "Rep_uint8 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint8_def Abs_uint8_inverse numeral.simps plus_uint8_def)
 
 lemma numeral_uint8_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint8) numeral numeral"
 by(auto simp add: cr_uint8_def)
 
 lemma numeral_uint8 [code_unfold]: "numeral n = Uint8 (numeral n)"
 by transfer simp
 
 lemma Rep_uint8_neg_numeral [simp]: "Rep_uint8 (- numeral n) = - numeral n"
 by(simp only: uminus_uint8_def)(simp add: Abs_uint8_inverse)
 
 lemma neg_numeral_uint8 [code_unfold]: "- numeral n = Uint8 (- numeral n)"
 by transfer(simp add: cr_uint8_def)
 
 end
 
 lemma Abs_uint8_numeral [code_post]: "Abs_uint8 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint8_def numeral.simps plus_uint8_def Abs_uint8_inverse)
 
 lemma Abs_uint8_0 [code_post]: "Abs_uint8 0 = 0"
 by(simp add: zero_uint8_def)
 
 lemma Abs_uint8_1 [code_post]: "Abs_uint8 1 = 1"
 by(simp add: one_uint8_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint8 \<rightharpoonup> (SML)
 \<open>(* Test that words can handle numbers between 0 and 3 *)
 val _ = if 3 <= Word.wordSize then () else raise (Fail ("wordSize less than 3"));
 
 structure Uint8 : sig
   val set_bit : Word8.word -> IntInf.int -> bool -> Word8.word
   val shiftl : Word8.word -> IntInf.int -> Word8.word
   val shiftr : Word8.word -> IntInf.int -> Word8.word
   val shiftr_signed : Word8.word -> IntInf.int -> Word8.word
   val test_bit : Word8.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word8.orb (x, mask)
      else Word8.andb (x, Word8.notb mask)
   end
 
 fun shiftl x n =
   Word8.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word8.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word8.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word8.andb (x, Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word8.fromInt 0
 
 end; (* struct Uint8 *)\<close>
 code_reserved SML Uint8
 
 code_printing code_module Uint8 \<rightharpoonup> (Haskell)
  \<open>module Uint8(Int8, Word8) where
 
   import Data.Int(Int8)
   import Data.Word(Word8)\<close>
 code_reserved Haskell Uint8
 
 text \<open>
   Scala provides only signed 8bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 
 code_printing code_module Uint8 \<rightharpoonup> (Scala)
 \<open>object Uint8 {
 
 def less(x: Byte, y: Byte) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Byte, y: Byte) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Byte, n: BigInt, b: Boolean) : Byte =
   if (b)
     (x | (1 << n.intValue)).toByte
   else
     (x & (1 << n.intValue).unary_~).toByte
 
 def shiftl(x: Byte, n: BigInt) : Byte = (x << n.intValue).toByte
 
 def shiftr(x: Byte, n: BigInt) : Byte = ((x & 255) >>> n.intValue).toByte
 
 def shiftr_signed(x: Byte, n: BigInt) : Byte = (x >> n.intValue).toByte
 
 def test_bit(x: Byte, n: BigInt) : Boolean =
   (x & (1 << n.intValue)) != 0
 
 } /* object Uint8 */\<close>
 code_reserved Scala Uint8
 
 text \<open>
   Avoid @{term Abs_uint8} in generated code, use @{term Rep_uint8'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint8}.
 
   The new destructor @{term Rep_uint8'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint8} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint8} 
   ([code abstract] equations for @{typ uint8} may use @{term Rep_uint8} because
   these instances will be folded away.)
 
   To convert @{typ "8 word"} values into @{typ uint8}, use @{term "Abs_uint8'"}.
 \<close>
 
 definition Rep_uint8' where [simp]: "Rep_uint8' = Rep_uint8"
 
 lemma Rep_uint8'_transfer [transfer_rule]:
   "rel_fun cr_uint8 (=) (\<lambda>x. x) Rep_uint8'"
 unfolding Rep_uint8'_def by(rule uint8.rep_transfer)
 
 lemma Rep_uint8'_code [code]: "Rep_uint8' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint8' :: "8 word \<Rightarrow> uint8" is "\<lambda>x :: 8 word. x" .
 
 lemma Abs_uint8'_code [code]: "Abs_uint8' x = Uint8 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint8 \<Rightarrow> _"]]
 
 lemma term_of_uint8_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint8.uint8.Abs_uint8'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]], TR (STR ''Uint8.uint8'') []]))
        (term_of_class.term_of (Rep_uint8' x))"
 by(simp add: term_of_anything)
 
 lemma Uin8_code [code abstract]: "Rep_uint8 (Uint8 i) = word_of_int (int_of_integer_symbolic i)"
 unfolding Uint8_def int_of_integer_symbolic_def by(simp add: Abs_uint8_inverse)
 
 code_printing type_constructor uint8 \<rightharpoonup>
   (SML) "Word8.word" and
   (Haskell) "Uint8.Word8" and
   (Scala) "Byte"
 | constant Uint8 \<rightharpoonup> 
   (SML) "Word8.fromLargeInt (IntInf.toLarge _)" and
   (Haskell) "(Prelude.fromInteger _ :: Uint8.Word8)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Word8)" and
   (Scala) "_.byteValue"
 | constant "0 :: uint8" \<rightharpoonup>
   (SML) "(Word8.fromInt 0)" and
   (Haskell) "(0 :: Uint8.Word8)" and
   (Scala) "0.toByte"
 | constant "1 :: uint8" \<rightharpoonup>
   (SML) "(Word8.fromInt 1)" and
   (Haskell) "(1 :: Uint8.Word8)" and
   (Scala) "1.toByte"
 | constant "plus :: uint8 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (Scala) "(_ +/ _).toByte"
 | constant "uminus :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.~" and
   (Haskell) "negate" and
   (Scala) "(- _).toByte"
 | constant "minus :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (Scala) "(_ -/ _).toByte"
 | constant "times :: uint8 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (Scala) "(_ */ _).toByte"
 | constant "HOL.equal :: uint8 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Word8.word) = _)" and
   (Haskell) infix 4 "==" and
   (Scala) infixl 5 "=="
 | class_instance uint8 :: equal \<rightharpoonup> (Haskell) -
 | constant "less_eq :: uint8 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word8.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (Scala) "Uint8.less'_eq"
 | constant "less :: uint8 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word8.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (Scala) "Uint8.less"
 | constant "NOT :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.notb" and
   (Haskell) "Data'_Bits.complement" and
   (Scala) "_.unary'_~.toByte"
 | constant "(AND) :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (Scala) "(_ & _).toByte"
 | constant "(OR) :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (Scala) "(_ | _).toByte"
 | constant "(XOR) :: uint8 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word8.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (Scala) "(_ ^ _).toByte"
 
 definition uint8_divmod :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8 \<times> uint8" where
   "uint8_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint8 \<Rightarrow> _) x (0 :: uint8), undefined ((mod) :: uint8 \<Rightarrow> _) x (0 :: uint8)) 
   else (x div y, x mod y))"
 
 definition uint8_div :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" 
 where "uint8_div x y = fst (uint8_divmod x y)"
 
 definition uint8_mod :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8" 
 where "uint8_mod x y = snd (uint8_divmod x y)"
 
 lemma div_uint8_code [code]: "x div y = (if y = 0 then 0 else uint8_div x y)"
 including undefined_transfer unfolding uint8_divmod_def uint8_div_def
 by transfer (simp add: word_div_def)
 
 lemma mod_uint8_code [code]: "x mod y = (if y = 0 then x else uint8_mod x y)"
 including undefined_transfer unfolding uint8_mod_def uint8_divmod_def
 by transfer (simp add: word_mod_def)
 
 definition uint8_sdiv :: "uint8 \<Rightarrow> uint8 \<Rightarrow> uint8"
 where
   "uint8_sdiv x y =
    (if y = 0 then undefined ((div) :: uint8 \<Rightarrow> _) x (0 :: uint8)
     else Abs_uint8 (Rep_uint8 x sdiv Rep_uint8 y))"
 
 definition div0_uint8 :: "uint8 \<Rightarrow> uint8"
 where [code del]: "div0_uint8 x = undefined ((div) :: uint8 \<Rightarrow> _) x (0 :: uint8)"
 declare [[code abort: div0_uint8]]
 
 definition mod0_uint8 :: "uint8 \<Rightarrow> uint8"
 where [code del]: "mod0_uint8 x = undefined ((mod) :: uint8 \<Rightarrow> _) x (0 :: uint8)"
 declare [[code abort: mod0_uint8]]
 
 lemma uint8_divmod_code [code]:
   "uint8_divmod x y =
   (if 0x80 \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint8 x, mod0_uint8 x)
    else let q = (uint8_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 including undefined_transfer unfolding uint8_divmod_def uint8_sdiv_def div0_uint8_def mod0_uint8_def
 by transfer(simp add: divmod_via_sdivmod)
 
 lemma uint8_sdiv_code [code abstract]:
   "Rep_uint8 (uint8_sdiv x y) =
    (if y = 0 then Rep_uint8 (undefined ((div) :: uint8 \<Rightarrow> _) x (0 :: uint8))
     else Rep_uint8 x sdiv Rep_uint8 y)"
 unfolding uint8_sdiv_def by(simp add: Abs_uint8_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint8_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint8_div \<rightharpoonup>
   (SML) "Word8.div ((_), (_))" and
   (Haskell) "Prelude.div"
 | constant uint8_mod \<rightharpoonup>
   (SML) "Word8.mod ((_), (_))" and
   (Haskell) "Prelude.mod"
 | constant uint8_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint8_sdiv \<rightharpoonup>
   (Scala) "(_ '/ _).toByte"
 
 definition uint8_test_bit :: "uint8 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint8_test_bit x n =
   (if n < 0 \<or> 7 < n then undefined (test_bit :: uint8 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint8 [code]:
   \<open>test_bit = (bit :: uint8 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint8_code [code]:
   "test_bit x n \<longleftrightarrow> n < 8 \<and> uint8_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint8_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint8_test_bit_code [code]:
   "uint8_test_bit w n =
   (if n < 0 \<or> 7 < n then undefined (test_bit :: uint8 \<Rightarrow> _) w n else Rep_uint8 w !! nat_of_integer n)"
 unfolding uint8_test_bit_def by(simp add: test_bit_uint8.rep_eq)
 
 code_printing constant uint8_test_bit \<rightharpoonup>
   (SML) "Uint8.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (Scala) "Uint8.test'_bit" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_test'_bit out of bounds\") else Uint8.test'_bit x i)"
 
 
 definition uint8_set_bit :: "uint8 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint8"
 where [code del]:
   "uint8_set_bit x n b =
   (if n < 0 \<or> 7 < n then undefined (set_bit :: uint8 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint8_code [code]:
   "set_bit x n b = (if n < 8 then uint8_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint8_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint8_set_bit_code [code abstract]:
   "Rep_uint8 (uint8_set_bit w n b) = 
   (if n < 0 \<or> 7 < n then Rep_uint8 (undefined (set_bit :: uint8 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint8 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint8_set_bit_def by transfer simp
 
 code_printing constant uint8_set_bit \<rightharpoonup>
   (SML) "Uint8.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (Scala) "Uint8.set'_bit" and
   (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_set'_bit out of bounds\") else Uint8.set'_bit x i b)"
 
 
 lift_definition uint8_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint8 \<Rightarrow> nat \<Rightarrow> uint8" is set_bits_aux .
 
 lemma uint8_set_bits_code [code]:
   "uint8_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint8_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint8 [code]:
   "(BITS n. f n) = uint8_set_bits f 0 8"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint8 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint8_shiftl :: "uint8 \<Rightarrow> integer \<Rightarrow> uint8"
 where [code del]:
   "uint8_shiftl x n = (if n < 0 \<or> 8 \<le> n then undefined (shiftl :: uint8 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint8_code [code]: "x << n = (if n < 8 then uint8_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint8_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint8_shiftl_code [code abstract]:
   "Rep_uint8 (uint8_shiftl w n) =
   (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined (shiftl :: uint8 \<Rightarrow> _) w n)
    else Rep_uint8 w << nat_of_integer n)"
 including undefined_transfer unfolding uint8_shiftl_def by transfer simp
 
 code_printing constant uint8_shiftl \<rightharpoonup>
   (SML) "Uint8.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (Scala) "Uint8.shiftl" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftl out of bounds\") else Uint8.shiftl x i)"
 
 definition uint8_shiftr :: "uint8 \<Rightarrow> integer \<Rightarrow> uint8"
 where [code del]:
   "uint8_shiftr x n = (if n < 0 \<or> 8 \<le> n then undefined (shiftr :: uint8 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint8_code [code]: "x >> n = (if n < 8 then uint8_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint8_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint8_shiftr_code [code abstract]:
   "Rep_uint8 (uint8_shiftr w n) =
   (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined (shiftr :: uint8 \<Rightarrow> _) w n) 
    else Rep_uint8 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint8_shiftr_def by transfer simp
 
 code_printing constant uint8_shiftr \<rightharpoonup>
   (SML) "Uint8.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (Scala) "Uint8.shiftr" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftr out of bounds\") else Uint8.shiftr x i)"
 
 definition uint8_sshiftr :: "uint8 \<Rightarrow> integer \<Rightarrow> uint8"
 where [code del]:
   "uint8_sshiftr x n =
   (if n < 0 \<or> 8 \<le> n then undefined sshiftr_uint8 x n else sshiftr_uint8 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint8_code [code]:
   "x >>> n = 
   (if n < 8 then uint8_sshiftr x (integer_of_nat n) else if x !! 7 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint8_sshiftr_def
 by transfer (simp add: not_less sshiftr_beyond word_size)
 
 lemma uint8_sshiftr_code [code abstract]:
   "Rep_uint8 (uint8_sshiftr w n) =
   (if n < 0 \<or> 8 \<le> n then Rep_uint8 (undefined sshiftr_uint8 w n)
    else Rep_uint8 w >>> nat_of_integer n)"
 including undefined_transfer unfolding uint8_sshiftr_def by transfer simp
 
 code_printing constant uint8_sshiftr \<rightharpoonup>
   (SML) "Uint8.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Int8) _)) :: Uint8.Word8)" and
   (Scala) "Uint8.shiftr'_signed" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_sshiftr out of bounds\") else Uint8.shiftr'_signed x i)"
 
 
 lemma uint8_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint8) !! 7"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint16_code [code]: "msb x \<longleftrightarrow> uint8_test_bit x 7"
 by(simp add: uint8_test_bit_def uint8_msb_test_bit)
 
 lemma uint8_of_int_code [code]: "uint8_of_int i = Uint8 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint8_code [code]:
   "int_of_uint8 x = int_of_integer (integer_of_uint8 x)"
 by(simp add: integer_of_uint8_def)
 
 lemma nat_of_uint8_code [code]:
   "nat_of_uint8 x = nat_of_integer (integer_of_uint8 x)"
 unfolding integer_of_uint8_def including integer.lifting by transfer simp
 
 definition integer_of_uint8_signed :: "uint8 \<Rightarrow> integer"
 where
   "integer_of_uint8_signed n = (if n !! 7 then undefined integer_of_uint8 n else integer_of_uint8 n)"
 
 lemma integer_of_uint8_signed_code [code]:
   "integer_of_uint8_signed n =
   (if n !! 7 then undefined integer_of_uint8 n else integer_of_int (uint (Rep_uint8' n)))"
 unfolding integer_of_uint8_signed_def integer_of_uint8_def
 including undefined_transfer by transfer simp
 
 lemma integer_of_uint8_code [code]:
   "integer_of_uint8 n =
   (if n !! 7 then integer_of_uint8_signed (n AND 0x7F) OR 0x80 else integer_of_uint8_signed n)"
 unfolding integer_of_uint8_def integer_of_uint8_signed_def o_def
 including undefined_transfer integer.lifting
 by transfer(auto simp add: word_ao_nth uint_and_mask_or_full mask_numeral mask_Suc_0 intro!: uint_and_mask_or_full[symmetric])
 
 code_printing
   constant "integer_of_uint8" \<rightharpoonup>
   (SML) "IntInf.fromLarge (Word8.toLargeInt _)" and
   (Haskell) "Prelude.toInteger"
 | constant "integer_of_uint8_signed" \<rightharpoonup>
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint8_of_natural :: "natural \<Rightarrow> uint8"
 where "uint8_of_natural x \<equiv> Uint8 (integer_of_natural x)"
 
 instantiation uint8 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint8 \<equiv> qc_random_cnv uint8_of_natural"
 definition "exhaustive_uint8 \<equiv> qc_exhaustive_cnv uint8_of_natural"
 definition "full_exhaustive_uint8 \<equiv> qc_full_exhaustive_cnv uint8_of_natural"
 instance ..
 end
 
 instantiation uint8 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint8 i in (x, 0xFF - x)" "0"
   "Typerep.Typerep (STR ''Uint8.uint8'') []" .
 
 definition "narrowing_uint8 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint8 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint8 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint8 (infixl ">>>" 55)
 
 end
diff --git a/thys/Word_Lib/Guide.thy b/thys/Word_Lib/Guide.thy
--- a/thys/Word_Lib/Guide.thy
+++ b/thys/Word_Lib/Guide.thy
@@ -1,295 +1,301 @@
 (*<*)
 theory Guide
   imports Main Word_Lemmas Word_Lemmas_32 Word_Lemmas_64
 begin
 
 hide_const (open) Misc_set_bit.set_bit
 
 (*>*)
 section \<open>A short overview over bit operations and word types\<close>
 
 subsection \<open>Basic theories and key ideas\<close>
 
 text \<open>
   When formalizing bit operations, it is tempting to represent
   bit values as explicit lists over a binary type. This however
   is a bad idea, mainly due to the inherent ambiguities in
   representation concerning repeating leading bits.
 
   Hence this approach avoids such explicit lists altogether
   following an algebraic path:
 
     \<^item> Bit values are represented by numeric types: idealized
       unbounded bit values can be represented by type \<^typ>\<open>int\<close>,
       bounded bit values by quotient types over \<^typ>\<open>int\<close>, aka \<^typ>\<open>'a word\<close>.
 
     \<^item> (A special case are idealized unbounded bit values ending
       in @{term [source] 0} which can be represented by type \<^typ>\<open>nat\<close> but
       only support a restricted set of operations).
 
   The most fundamental ideas are developed in theory \<^theory>\<open>HOL.Parity\<close>
   (which is part of \<^theory>\<open>Main\<close>):
 
     \<^item> Multiplication by \<^term>\<open>2 :: int\<close> is a bit shift to the left and
 
     \<^item> Division by \<^term>\<open>2 :: int\<close> is a bit shift to the right.
 
     \<^item> Concerning bounded bit values, iterated shifts to the left
     may result in eliminating all bits by shifting them all
     beyond the boundary.  The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close>
     represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary.
 
     \<^item> The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}.
 
     \<^item> This leads to the most fundamental properties of bit values:
 
       \<^item> Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]}
 
       \<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]}
 
   On top of this, the following generic operations are provided
   after import of theory \<^theory>\<open>HOL-Library.Bit_Operations\<close>:
 
     \<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close>
 
     \<^item> Bit mask upto bit \<^term>\<open>n\<close>: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]}
 
     \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]}
 
     \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]}
 
     \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]}
 
     \<^item> Negation: @{thm [mode=iff] bit_not_iff [where ?'a = int, no_vars]}
 
     \<^item> And: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]}
 
     \<^item> Or: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]}
 
     \<^item> Xor: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]}
 
     \<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>:
         @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]}
 
     \<^item> (Bounded) conversion from and to a list of bits:
         @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 
   Proper word types are introduced in theory \<^theory>\<open>HOL-Word.Word\<close>, with
   the following specific operations:
 
     \<^item> Standard arithmetic:
         @{term \<open>(+) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>uminus :: 'a::len word \<Rightarrow> 'a word\<close>},
         @{term \<open>(-) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>(*) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>0 :: 'a::len word\<close>}, @{term \<open>1 :: 'a::len word\<close>}, numerals etc.
 
     \<^item> Standard bit operations: see above.
 
     \<^item> Conversion with unsigned interpretation of words:
 
         \<^item> @{term [source] \<open>unsigned :: 'a::len word \<Rightarrow> 'b::semiring_1\<close>}
 
         \<^item> Important special cases as abbreviations:
 
             \<^item> @{term [source] \<open>unat :: 'a::len word \<Rightarrow> nat\<close>}
 
             \<^item> @{term [source] \<open>uint :: 'a::len word \<Rightarrow> int\<close>}
 
             \<^item> @{term [source] \<open>ucast :: 'a::len word \<Rightarrow> 'b::len word\<close>}
 
     \<^item> Conversion with signed interpretation of words:
 
         \<^item> @{term [source] \<open>signed :: 'a::len word \<Rightarrow> 'b::ring_1\<close>}
 
         \<^item> Important special cases as abbreviations:
 
             \<^item> @{term [source] \<open>sint :: 'a::len word \<Rightarrow> int\<close>}
 
             \<^item> @{term [source] \<open>scast :: 'a::len word \<Rightarrow> 'b::len word\<close>}
 
     \<^item> Operations with unsigned interpretation of words:
 
         \<^item> @{thm [mode=iff] word_le_nat_alt [no_vars]}
 
         \<^item> @{thm [mode=iff] word_less_nat_alt [no_vars]}
 
         \<^item> @{thm unat_div_distrib [no_vars]}
 
         \<^item> @{thm unat_drop_bit_eq [no_vars]}
 
         \<^item> @{thm unat_mod_distrib [no_vars]}
 
         \<^item> @{thm [mode=iff] udvd_iff_dvd [no_vars]}
 
     \<^item> Operations with with signed interpretation of words:
 
         \<^item> @{thm [mode=iff] word_sle_eq [no_vars]}
 
         \<^item> @{thm [mode=iff] word_sless_alt [no_vars]}
 
         \<^item> @{thm sint_signed_drop_bit_eq [no_vars]}
 
     \<^item> Rotation and reversal:
 
         \<^item> @{term [source] \<open>word_rotl :: nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_rotr :: nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_roti :: int \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_reverse :: 'a::len word \<Rightarrow> 'a word\<close>}
 
     \<^item> Concatenation: @{term [source, display] \<open>word_cat :: 'a::len word \<Rightarrow> 'b::len word \<Rightarrow> 'c::len word\<close>}
 
   For proofs about words the following default strategies are applicable:
 
     \<^item> Using bit extensionality (facts \<^text>\<open>bit_eq_iff\<close>, \<^text>\<open>bit_eqI\<close>).
 
     \<^item> Using the @{method transfer} method.
 \<close>
 
 subsection \<open>More theories\<close>
 
 text \<open>
   Note: currently, the theories listed here are hardly separate
   entites since they import each other in various ways.
   Always inspect them to understand what you pull in if you
   want to import one.
 
     \<^descr>[Syntax]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Hex_Words\<close>]
         Printing word numerals as hexadecimal numerals.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Type_Syntax\<close>]
         Pretty type-sensitive syntax for cast operations.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Syntax\<close>]
         Specific ASCII syntax for prominent bit operations on word.
 
     \<^descr>[Proof tools]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Norm_Words\<close>]
         Rewriting word numerals to normal forms.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Bitwise\<close>]
         Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_EqI\<close>]
         Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.
 
     \<^descr>[Operations]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Lib\<close>]
         Various operations on word, particularly:
 
           \<^item> @{term [source] \<open>(sdiv) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
 
           \<^item> @{term [source] \<open>(smod) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Aligned\<close>] \
 
           \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Next\<close>] \
 
           \<^item> @{thm word_next_unfold [no_vars]}
 
           \<^item> @{thm word_prev_unfold [no_vars]}
 
     \<^descr>[Types]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Signed_Words\<close>]
 
           Formal tagging of word types with a \<^text>\<open>signed\<close> marker;
           currently it is not clear what practical relevance
           this bears.
 
     \<^descr>[Mechanisms]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Enum\<close>]
 
           More on explicit enumeration of word types.
 
     \<^descr>[Lemmas]
 
       Collections of lemmas:
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas\<close>] generic.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas_32\<close>] for 32-bit words.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas_64\<close>] for 64-bit words.
 \<close>
 
 
 subsection \<open>Legacy theories\<close>
 
 text \<open>
   The following theories contain material which has been
   factored out since it is not recommended to use it in
   new applications, mostly because matters can be expressed
   succinctly using already existing operations.
 
   This section gives some indication how to migrate away
   from those theories.  However theorem coverage may still
   be terse in some cases.
 
   \<^descr>[\<^theory>\<open>HOL-Word.Misc_lsb\<close>]
 
     A mere alias: @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]}
 
   \<^descr>[\<^theory>\<open>HOL-Word.Misc_msb\<close>]
 
     An alias for the most significant bit; suggested replacements:
 
       \<^item> @{thm [mode=iff] msb_int_def [of k]}
 
       \<^item> @{thm [mode=iff] word_msb_sint [no_vars]}
 
       \<^item> @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]}
 
       \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]}
 
   \<^descr>[\<^theory>\<open>HOL-Word.Misc_set_bit\<close>]
 
     An alias: @{thm set_bit_eq [no_vars]}
 
   \<^descr>[\<^theory>\<open>HOL-Word.Misc_Typedef\<close>]
 
     An invasive low-level extension to HOL typedef to provide
     conversions along type morphisms.
 
   \<^descr>[\<^theory>\<open>HOL-Word.Traditional_Syntax\<close>]
 
     Clones of existing operations decorated with
     traditional syntax:
 
       \<^item> @{thm test_bit_eq_bit [no_vars]}
 
       \<^item> @{thm shiftl_eq_push_bit [no_vars]}
 
       \<^item> @{thm shiftr_eq_drop_bit [no_vars]}
 
+  \<^descr>[\<^theory>\<open>HOL-Word.Bit_Comprehension\<close>]
+
+    Comprehension syntax for bit values over predicates
+    \<^typ>\<open>nat \<Rightarrow> bool\<close>.  For \<^typ>\<open>'a::len word\<close>, straightforward
+    alternatives exist; difficult to handle for \<^typ>\<open>int\<close>.
+
   \<^descr>[\<^theory>\<open>HOL-Word.Reversed_Bit_Lists\<close>]
 
     Representation of bit values as explicit list in
     \<^emph>\<open>reversed\<close> order.
 
     This should rarely be necessary: the \<^const>\<open>bit\<close> projection
     should be sufficient in most cases.  In case explicit lists
     are needed, existing operations can be used:
 
     @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 \<close>
 
 (*<*)
 end
 (*>*)