diff --git a/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy b/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
--- a/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
+++ b/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
@@ -1,397 +1,397 @@
 theory Impl_Uv_Set
-imports 
-  "../../Iterator/Iterator" 
-  "../Intf/Intf_Set" 
+imports
+  "../../Iterator/Iterator"
+  "../Intf/Intf_Set"
   Native_Word.Uint
 begin
 
   subsection \<open>Bit-Vectors as Lists of Words\<close>
 
   subsubsection \<open>Lookup\<close>
 
   primrec lookup :: "nat \<Rightarrow> ('a::len) word list \<Rightarrow> bool" where
     "lookup _ [] \<longleftrightarrow> False"
-  | "lookup n (w#ws) 
+  | "lookup n (w#ws)
       \<longleftrightarrow> (if n<LENGTH('a) then test_bit w n else lookup (n-LENGTH('a)) ws)"
 
-  lemma lookup_append[simp]: "lookup n (w1@w2 :: 'a::len word list) 
+  lemma lookup_append[simp]: "lookup n (w1@w2 :: 'a::len word list)
     \<longleftrightarrow> (
-      if n < LENGTH('a) * length w1 then 
-        lookup n w1 
+      if n < LENGTH('a) * length w1 then
+        lookup n w1
       else lookup (n - LENGTH('a) * length w1) w2)"
     by (induction w1 arbitrary: n) auto
 
   lemma lookup_zeroes[simp]: "lookup i (replicate n (0::'a::len word)) = False"
     by (induction n arbitrary: i) auto
 
-  lemma lookup_out_of_bound: 
+  lemma lookup_out_of_bound:
     fixes uv :: "'a::len word list"
-    assumes "\<not> i < LENGTH('a::len) * length uv" 
+    assumes "\<not> i < LENGTH('a::len) * length uv"
     shows "\<not> lookup i uv"
     using assms
     by (induction uv arbitrary: i) auto
 
 
   subsubsection \<open>Empty\<close>
 
   definition empty :: "'a::len word list" where "empty = []"
 
   subsubsection \<open>Set and Reset Bit\<close>
 
-  function single_bit :: "nat \<Rightarrow> ('a::len) word list" 
+  function single_bit :: "nat \<Rightarrow> ('a::len) word list"
     where "single_bit n = (
-      if (n<LENGTH('a)) then 
-        [set_bit 0 n True] 
+      if (n<LENGTH('a)) then
+        [set_bit 0 n True]
       else 0#single_bit (n-LENGTH('a)))"
     by pat_completeness auto
   termination
     apply (relation "measure id")
     apply simp
     apply (simp add: not_less less_diff_conv2)
     done
 
   declare single_bit.simps[simp del]
 
   lemma lookup_single_bit[simp]: "lookup i ((single_bit n)::'a::len word list) \<longleftrightarrow> i = n"
     apply (induction n arbitrary: i rule: single_bit.induct)
     apply (subst single_bit.simps)
     apply (auto simp: bin_nth_sc_gen)
     done
 
   primrec set_bit :: "nat \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list" where
     "set_bit i [] = single_bit i"
   | "set_bit i (w#ws) = (
-      if i<LENGTH('a) then 
+      if i<LENGTH('a) then
         Bit_Operations.set_bit i w # ws
-      else 
+      else
         w # set_bit (i - LENGTH('a)) ws)"
-  
+
   lemma set_bit_lookup[simp]: "lookup i (set_bit j ws) \<longleftrightarrow> (lookup i ws \<or> i=j)"
     apply (induction ws arbitrary: i j)
-     apply (auto simp add: test_bit_eq_bit word_size bit_set_bit_iff exp_eq_zero_iff)
+     apply (auto simp add: test_bit_eq_bit word_size ring_bit_operations_class.bit_set_bit_iff)
     done
 
   primrec reset_bit :: "nat \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list" where
     "reset_bit i [] = []"
   | "reset_bit i (w#ws) = (
-      if i<LENGTH('a) then 
+      if i<LENGTH('a) then
         unset_bit i w # ws
-      else 
+      else
         w # reset_bit (i - LENGTH('a)) ws)"
-  
+
   lemma reset_bit_lookup[simp]: "lookup i (reset_bit j ws) \<longleftrightarrow> (lookup i ws \<and> i\<noteq>j)"
     apply (induction ws arbitrary: i j)
     apply (auto simp: test_bit_eq_bit word_size bit_unset_bit_iff)
     done
 
   subsubsection \<open>Binary Operations\<close>
 
-  definition 
-    is_bin_op_impl 
+  definition
+    is_bin_op_impl
     :: "(bool\<Rightarrow>bool\<Rightarrow>bool) \<Rightarrow> ('a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word) \<Rightarrow> bool"
-    where "is_bin_op_impl f g \<equiv> 
+    where "is_bin_op_impl f g \<equiv>
     (\<forall>w v.  \<forall>i<LENGTH('a). test_bit (g w v) i \<longleftrightarrow> f (test_bit w i) (test_bit v i))"
 
   definition "is_strict_bin_op_impl f g \<equiv> is_bin_op_impl f g \<and> f False False = False"
 
-  fun binary :: "('a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word) 
+  fun binary :: "('a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word)
     \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list"
-    where 
+    where
     "binary f [] [] = []"
   | "binary f [] (w#ws) = f 0 w # binary f [] ws"
   | "binary f (v#vs) [] = f v 0 # binary f vs []"
   | "binary f (v#vs) (w#ws) = f v w # binary f vs ws"
 
   lemma binary_lookup:
     assumes "is_strict_bin_op_impl f g"
     shows "lookup i (binary g ws vs) \<longleftrightarrow> f (lookup i ws) (lookup i vs)"
     using assms
     apply (induction g ws vs arbitrary: i rule: binary.induct)
     apply (auto simp: is_strict_bin_op_impl_def is_bin_op_impl_def)
     done
 
   subsection \<open>Abstraction to Sets of Naturals\<close>
 
   definition "\<alpha> uv \<equiv> {n. lookup n uv}"
-  
+
   lemma memb_correct: "lookup i ws \<longleftrightarrow> i\<in>\<alpha> ws"
     by (auto simp: \<alpha>_def)
 
   lemma empty_correct: "\<alpha> empty = {}"
     by (simp add: \<alpha>_def empty_def)
 
   lemma single_bit_correct: "\<alpha> (single_bit n) = {n}"
     by (simp add: \<alpha>_def)
 
   lemma insert_correct: "\<alpha> (set_bit i ws) = Set.insert i (\<alpha> ws)"
     by (auto simp add: \<alpha>_def)
 
   lemma delete_correct: "\<alpha> (reset_bit i ws) = (\<alpha> ws) - {i}"
     by (auto simp add: \<alpha>_def)
 
   lemma binary_correct:
     assumes "is_strict_bin_op_impl f g"
     shows "\<alpha> (binary g ws vs) = { i . f (i\<in>\<alpha> ws) (i\<in>\<alpha> vs) }"
     unfolding \<alpha>_def
     by (auto simp add: binary_lookup[OF assms])
 
   fun union :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list"
-    where 
+    where
     "union [] ws = ws"
   | "union vs [] = vs"
   | "union (v#vs) (w#ws) = (v OR w) # union vs ws"
 
   lemma union_lookup[simp]:
-    fixes vs :: "'a::len word list" 
+    fixes vs :: "'a::len word list"
     shows "lookup i (union vs ws) \<longleftrightarrow> lookup i vs \<or> lookup i ws"
     apply (induction vs ws arbitrary: i rule: union.induct)
     apply (auto simp: word_ao_nth)
     done
 
   lemma union_correct: "\<alpha> (union ws vs) = \<alpha> ws \<union> \<alpha> vs"
     by (auto simp add: \<alpha>_def)
 
   fun inter :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list"
-    where 
+    where
     "inter [] ws = []"
   | "inter vs [] = []"
   | "inter (v#vs) (w#ws) = (v AND w) # inter vs ws"
 
   lemma inter_lookup[simp]:
-    fixes vs :: "'a::len word list" 
+    fixes vs :: "'a::len word list"
     shows "lookup i (inter vs ws) \<longleftrightarrow> lookup i vs \<and> lookup i ws"
     apply (induction vs ws arbitrary: i rule: inter.induct)
     apply (auto simp: word_ao_nth)
     done
 
   lemma inter_correct: "\<alpha> (inter ws vs) = \<alpha> ws \<inter> \<alpha> vs"
     by (auto simp add: \<alpha>_def)
 
 
   fun diff :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> 'a::len word list"
-    where 
+    where
     "diff [] ws = []"
   | "diff vs [] = vs"
   | "diff (v#vs) (w#ws) = (v AND NOT w) # diff vs ws"
 
   lemma diff_lookup[simp]:
-    fixes vs :: "'a::len word list" 
+    fixes vs :: "'a::len word list"
     shows "lookup i (diff vs ws) \<longleftrightarrow> lookup i vs - lookup i ws"
     apply (induction vs ws arbitrary: i rule: diff.induct)
     apply (auto simp: word_ops_nth_size word_size)
     done
 
   lemma diff_correct: "\<alpha> (diff ws vs) = \<alpha> ws - \<alpha> vs"
     by (auto simp add: \<alpha>_def)
-   
+
   fun zeroes :: "'a::len word list \<Rightarrow> bool" where
     "zeroes [] \<longleftrightarrow> True"
   | "zeroes (w#ws) \<longleftrightarrow> w=0 \<and> zeroes ws"
 
   lemma zeroes_lookup: "zeroes ws \<longleftrightarrow> (\<forall>i. \<not>lookup i ws)"
     apply (induction ws)
     apply (auto simp: word_eq_iff)
     by (metis diff_add_inverse2 not_add_less2)
 
   lemma isEmpty_correct: "zeroes ws \<longleftrightarrow> \<alpha> ws = {}"
     by (auto simp: zeroes_lookup \<alpha>_def)
 
   fun equal :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> bool" where
     "equal [] [] \<longleftrightarrow> True"
   | "equal [] ws \<longleftrightarrow> zeroes ws"
   | "equal vs [] \<longleftrightarrow> zeroes vs"
   | "equal (v#vs) (w#ws) \<longleftrightarrow> v=w \<and> equal vs ws"
 
-  lemma equal_lookup: 
+  lemma equal_lookup:
     fixes vs ws :: "'a::len word list"
     shows "equal vs ws \<longleftrightarrow> (\<forall>i. lookup i vs = lookup i ws)"
   proof (induction vs ws rule: equal.induct)
     fix v w and vs ws :: "'a::len word list"
     assume IH: "equal vs ws = (\<forall>i. lookup i vs = lookup i ws)"
     show "equal (v # vs) (w # ws) = (\<forall>i. lookup i (v # vs) = lookup i (w # ws))"
     proof (rule iffI, rule allI)
       fix i
       assume "equal (v#vs) (w#ws)"
       thus "lookup i (v # vs) = lookup i (w # ws)"
         by (auto simp: IH)
     next
       assume "\<forall>i. lookup i (v # vs) = lookup i (w # ws)"
       thus "equal (v # vs) (w # ws)"
         apply (auto simp: word_eq_iff IH)
         apply metis
         apply metis
         apply (drule_tac x="i + LENGTH('a)" in spec)
         apply auto []
         apply (drule_tac x="i + LENGTH('a)" in spec)
         apply auto []
         done
     qed
   qed (auto simp: zeroes_lookup)
-    
+
   lemma equal_correct: "equal vs ws \<longleftrightarrow> \<alpha> vs = \<alpha> ws"
     by (auto simp: \<alpha>_def equal_lookup)
-  
+
   fun subseteq :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> bool" where
     "subseteq [] ws \<longleftrightarrow> True"
   | "subseteq vs [] \<longleftrightarrow> zeroes vs"
   | "subseteq (v#vs) (w#ws) \<longleftrightarrow> (v AND NOT w = 0) \<and> subseteq vs ws"
 
-  
-  lemma subseteq_lookup: 
+
+  lemma subseteq_lookup:
     fixes vs ws :: "'a::len word list"
     shows "subseteq vs ws \<longleftrightarrow> (\<forall>i. lookup i vs \<longrightarrow> lookup i ws)"
     apply (induction vs ws rule: subseteq.induct)
     apply simp
     apply (auto simp: zeroes_lookup) []
     apply (auto simp: word_ops_nth_size word_size word_eq_iff)
     by (metis diff_add_inverse2 not_add_less2)
 
   lemma subseteq_correct: "subseteq vs ws \<longleftrightarrow> \<alpha> vs \<subseteq> \<alpha> ws"
     by (auto simp: \<alpha>_def subseteq_lookup)
 
 
   fun subset :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> bool" where
     "subset [] ws \<longleftrightarrow> \<not>zeroes ws"
   | "subset vs [] \<longleftrightarrow> False"
   | "subset (v#vs) (w#ws) \<longleftrightarrow> (if v=w then subset vs ws else subseteq (v#vs) (w#ws))"
 
-  lemma subset_lookup: 
+  lemma subset_lookup:
     fixes vs ws :: "'a::len word list"
-    shows "subset vs ws \<longleftrightarrow> ((\<forall>i. lookup i vs \<longrightarrow> lookup i ws) 
+    shows "subset vs ws \<longleftrightarrow> ((\<forall>i. lookup i vs \<longrightarrow> lookup i ws)
       \<and> (\<exists>i. \<not>lookup i vs \<and> lookup i ws))"
     apply (induction vs ws rule: subset.induct)
     apply (simp add: zeroes_lookup)
     apply (simp add: zeroes_lookup) []
     apply (simp del: subseteq_correct add: subseteq_lookup)
     apply safe
     apply simp_all
     apply (auto simp: word_ops_nth_size word_size word_eq_iff)
     done
 
   lemma subset_correct: "subset vs ws \<longleftrightarrow> \<alpha> vs \<subset> \<alpha> ws"
     by (auto simp: \<alpha>_def subset_lookup)
 
-  
+
   fun disjoint :: "'a::len word list \<Rightarrow> 'a::len word list \<Rightarrow> bool" where
     "disjoint [] ws \<longleftrightarrow> True"
   | "disjoint vs [] \<longleftrightarrow> True"
   | "disjoint (v#vs) (w#ws) \<longleftrightarrow> (v AND w = 0) \<and> disjoint vs ws"
 
-  lemma disjoint_lookup: 
+  lemma disjoint_lookup:
     fixes vs ws :: "'a::len word list"
     shows "disjoint vs ws \<longleftrightarrow> (\<forall>i. \<not>(lookup i vs \<and> lookup i ws))"
     apply (induction vs ws rule: disjoint.induct)
     apply simp
     apply simp
     apply (auto simp: word_ops_nth_size word_size word_eq_iff)
     by (metis diff_add_inverse2 not_add_less2)
 
   lemma disjoint_correct: "disjoint vs ws \<longleftrightarrow> \<alpha> vs \<inter> \<alpha> ws = {}"
     by (auto simp: \<alpha>_def disjoint_lookup)
 
-  
+
 subsection \<open>Lifting to Uint\<close>
   type_synonym uint_vector = "uint list"
 
   lift_definition uv_\<alpha> :: "uint_vector \<Rightarrow> nat set" is \<alpha> .
   lift_definition uv_lookup :: "nat \<Rightarrow> uint_vector \<Rightarrow> bool" is lookup .
   lift_definition uv_empty :: "uint_vector" is empty .
   lift_definition uv_single_bit :: "nat \<Rightarrow> uint_vector" is single_bit .
   lift_definition uv_set_bit :: "nat \<Rightarrow> uint_vector \<Rightarrow> uint_vector" is set_bit .
   lift_definition uv_reset_bit :: "nat \<Rightarrow> uint_vector \<Rightarrow> uint_vector" is reset_bit .
   lift_definition uv_union :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> uint_vector" is union .
   lift_definition uv_inter :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> uint_vector" is inter .
   lift_definition uv_diff :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> uint_vector" is diff .
   lift_definition uv_zeroes :: "uint_vector \<Rightarrow> bool" is zeroes .
   lift_definition uv_equal :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> bool" is equal .
   lift_definition uv_subseteq :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> bool" is subseteq .
   lift_definition uv_subset :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> bool" is subset .
   lift_definition uv_disjoint :: "uint_vector \<Rightarrow> uint_vector \<Rightarrow> bool" is disjoint .
 
   lemmas uv_memb_correct = memb_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_empty_correct = empty_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_single_bit_correct = single_bit_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_insert_correct = insert_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_delete_correct = delete_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_union_correct = union_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_inter_correct = inter_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_diff_correct = diff_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_isEmpty_correct = isEmpty_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_equal_correct = equal_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_subseteq_correct = subseteq_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_subset_correct = subset_correct[where 'a=dflt_size, Transfer.transferred]
   lemmas uv_disjoint_correct = disjoint_correct[where 'a=dflt_size, Transfer.transferred]
 
 
 
-  lemmas [where 'a=dflt_size, Transfer.transferred, code] = 
-    lookup.simps 
+  lemmas [where 'a=dflt_size, Transfer.transferred, code] =
+    lookup.simps
     empty_def
-    single_bit.simps 
-    set_bit.simps 
-    reset_bit.simps 
-    union.simps 
-    inter.simps 
-    diff.simps 
-    zeroes.simps 
-    equal.simps 
-    subseteq.simps 
-    subset.simps 
-    disjoint.simps 
-    
+    single_bit.simps
+    set_bit.simps
+    reset_bit.simps
+    union.simps
+    inter.simps
+    diff.simps
+    zeroes.simps
+    equal.simps
+    subseteq.simps
+    subset.simps
+    disjoint.simps
 
-  hide_const (open) \<alpha> lookup empty single_bit set_bit reset_bit union inter diff zeroes 
+
+  hide_const (open) \<alpha> lookup empty single_bit set_bit reset_bit union inter diff zeroes
     equal subseteq subset disjoint
 
 
 subsection \<open>Autoref Setup\<close>
 
-  definition uv_set_rel_def_internal: 
-    "uv_set_rel Rk \<equiv> 
+  definition uv_set_rel_def_internal:
+    "uv_set_rel Rk \<equiv>
       if Rk=nat_rel then br uv_\<alpha> (\<lambda>_. True) else {}"
-  lemma uv_set_rel_def: 
-    "\<langle>nat_rel\<rangle>uv_set_rel \<equiv> br uv_\<alpha> (\<lambda>_. True)" 
+  lemma uv_set_rel_def:
+    "\<langle>nat_rel\<rangle>uv_set_rel \<equiv> br uv_\<alpha> (\<lambda>_. True)"
     unfolding uv_set_rel_def_internal relAPP_def by simp
 
   lemmas [autoref_rel_intf] = REL_INTFI[of "uv_set_rel" i_set]
 
   lemma uv_set_rel_sv[relator_props]: "single_valued (\<langle>nat_rel\<rangle>uv_set_rel)"
     unfolding uv_set_rel_def by auto
 
   lemma uv_autoref[autoref_rules,param]:
     "(uv_lookup,(\<in>)) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
     "(uv_empty,{}) \<in> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_set_bit,insert) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_reset_bit,op_set_delete) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_union,(\<union>)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_inter,(\<inter>)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_diff,(-)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel"
     "(uv_zeroes,op_set_isEmpty) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
     "(uv_equal,(=)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
     "(uv_subseteq,(\<subseteq>)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
     "(uv_subset,(\<subset>)) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
     "(uv_disjoint,op_set_disjoint) \<in> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> \<langle>nat_rel\<rangle>uv_set_rel \<rightarrow> bool_rel"
-    by (auto 
+    by (auto
       simp: uv_set_rel_def br_def
       simp: uv_memb_correct uv_empty_correct uv_insert_correct uv_delete_correct
       simp: uv_union_correct uv_inter_correct uv_diff_correct uv_isEmpty_correct
       simp: uv_equal_correct uv_subseteq_correct uv_subset_correct uv_disjoint_correct)
 
 
-  export_code 
-    uv_lookup 
+  export_code
+    uv_lookup
     uv_empty
-    uv_single_bit 
-    uv_set_bit 
-    uv_reset_bit 
-    uv_union 
-    uv_inter 
-    uv_diff 
-    uv_zeroes 
-    uv_equal 
-    uv_subseteq 
-    uv_subset 
-    uv_disjoint 
+    uv_single_bit
+    uv_set_bit
+    uv_reset_bit
+    uv_union
+    uv_inter
+    uv_diff
+    uv_zeroes
+    uv_equal
+    uv_subseteq
+    uv_subset
+    uv_disjoint
   checking SML Scala Haskell? OCaml?
 
 end
diff --git a/thys/Native_Word/Bits_Integer.thy b/thys/Native_Word/Bits_Integer.thy
--- a/thys/Native_Word/Bits_Integer.thy
+++ b/thys/Native_Word/Bits_Integer.thy
@@ -1,688 +1,688 @@
 (*  Title:      Bits_Integer.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Bit operations for target language integers\<close>
 
 theory Bits_Integer imports
   More_Bits_Int
   Code_Symbolic_Bits_Int
 begin
 
 lemmas [transfer_rule] =
   identity_quotient
   fun_quotient
   Quotient_integer[folded integer.pcr_cr_eq]
 
 lemma undefined_transfer:
   assumes "Quotient R Abs Rep T"
   shows "T (Rep undefined) undefined"
 using assms unfolding Quotient_alt_def by blast
 
 bundle undefined_transfer = undefined_transfer[transfer_rule]
 
 section \<open>More lemmas about @{typ integer}s\<close>
 
 context
 includes integer.lifting
 begin
 
 lemma bitval_integer_transfer [transfer_rule]:
   "(rel_fun (=) pcr_integer) of_bool of_bool"
 by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def)
 
 lemma integer_of_nat_less_0_conv [simp]: "\<not> integer_of_nat n < 0"
 by(transfer) simp
 
 lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n"
 by(induct n) simp_all
 
 lemma pow_integer_transfer [transfer_rule]:
   "(rel_fun pcr_integer (rel_fun (=) pcr_integer)) (^) (^)"
 by(auto 4 3 simp add: integer.pcr_cr_eq cr_integer_def int_of_integer_pow)
 
 lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0 \<longleftrightarrow> False"
 by(cases n)(simp_all add: Code_Numeral.sub_code)
 
 lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n"
 by transfer simp
 
 lemma nat_of_integer_sub1_conv_pred_numeral [simp]:
   "nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n"
 by(cases n)(simp_all add: Code_Numeral.sub_code)
 
 lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1"
 by transfer simp
 
 lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2"
 by transfer simp
 
 
 section \<open>Bit operations on @{typ integer}\<close>
 
 text \<open>Bit operations on @{typ integer} are the same as on @{typ int}\<close>
 
 lift_definition bin_rest_integer :: "integer \<Rightarrow> integer" is bin_rest .
 lift_definition bin_last_integer :: "integer \<Rightarrow> bool" is bin_last .
 lift_definition Bit_integer :: "integer \<Rightarrow> bool \<Rightarrow> integer" is \<open>\<lambda>k b. of_bool b + 2 * k\<close> .
 
 end
 
 instance integer :: semiring_bit_syntax ..
 
-context 
+context
   includes lifting_syntax integer.lifting
 begin
 
 lemma test_bit_integer_transfer [transfer_rule]:
   \<open>(pcr_integer ===> (=)) bit (!!)\<close>
   unfolding test_bit_eq_bit by transfer_prover
 
 lemma shiftl_integer_transfer [transfer_rule]:
   \<open>(pcr_integer ===> (=) ===> pcr_integer) (\<lambda>k n. push_bit n k) (<<)\<close>
   unfolding shiftl_eq_push_bit by transfer_prover
 
 lemma shiftr_integer_transfer [transfer_rule]:
   \<open>(pcr_integer ===> (=) ===> pcr_integer) (\<lambda>k n. drop_bit n k) (>>)\<close>
   unfolding shiftr_eq_drop_bit by transfer_prover
 
 end
 
 instantiation integer :: lsb begin
 context includes integer.lifting begin
 
 lift_definition lsb_integer :: "integer \<Rightarrow> bool" is lsb .
 
 instance
   by (standard; transfer) (fact lsb_odd)
 
 end
 end
 
 instantiation integer :: msb begin
 context includes integer.lifting begin
 
 lift_definition msb_integer :: "integer \<Rightarrow> bool" is msb .
 
 instance ..
 
 end
 end
 
 instantiation integer :: set_bit begin
 context includes integer.lifting begin
 
 lift_definition set_bit_integer :: "integer \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> integer" is set_bit .
 
 instance
   apply standard
   apply transfer
   apply (simp add: bit_simps)
   done
 
 end
 end
 
 abbreviation (input) wf_set_bits_integer
 where "wf_set_bits_integer \<equiv> wf_set_bits_int"
 
 
 section \<open>Target language implementations\<close>
 
 text \<open>
   Unfortunately, this is not straightforward,
   because these API functions have different signatures and preconditions on the parameters:
 
   \begin{description}
   \item[Standard ML] Shifts in IntInf are given as word, but not IntInf.
   \item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer.
   \end{description}
 
   Additional constants take only parameters of type @{typ integer} rather than @{typ nat}
   and check the preconditions as far as possible (e.g., being non-negative) in a portable way.
-  Manual implementations inside code\_printing perform the remaining range checks and convert 
+  Manual implementations inside code\_printing perform the remaining range checks and convert
   these @{typ integer}s into the right type.
 
   For normalisation by evaluation, we derive custom code equations, because NBE
   does not know these code\_printing serialisations and would otherwise loop.
 \<close>
 
 code_identifier code_module Bits_Integer \<rightharpoonup>
   (SML) Bits_Int and (OCaml) Bits_Int and (Haskell) Bits_Int and (Scala) Bits_Int
 
 code_printing code_module Bits_Integer \<rightharpoonup> (SML)
 \<open>structure Bits_Integer : sig
   val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
   val shiftl : IntInf.int -> IntInf.int -> IntInf.int
   val shiftr : IntInf.int -> IntInf.int -> IntInf.int
   val test_bit : IntInf.int -> IntInf.int -> bool
 end = struct
 
 val maxWord = IntInf.pow (2, Word.wordSize);
 
 fun set_bit x n b =
   if n < maxWord 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 raise (Fail ("Bit index too large: " ^ IntInf.toString n));
 
 fun shiftl x n =
   if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
   else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));
 
 fun shiftr x n =
   if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
   else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));
 
 fun test_bit x n =
   if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
   else raise (Fail ("Bit index too large: " ^ IntInf.toString n));
 
 end; (*struct Bits_Integer*)\<close>
 code_reserved SML Bits_Integer
 
 code_printing code_module Bits_Integer \<rightharpoonup> (OCaml)
 \<open>module Bits_Integer : sig
   val shiftl : Z.t -> Z.t -> Z.t
   val shiftr : Z.t -> Z.t -> Z.t
   val test_bit : Z.t -> Z.t -> bool
 end = struct
 
 (* We do not need an explicit range checks here,
-   because Big_int.int_of_big_int raises Failure 
+   because Big_int.int_of_big_int raises Failure
    if the argument does not fit into an int. *)
 let shiftl x n = Z.shift_left x (Z.to_int n);;
 
 let shiftr x n = Z.shift_right x (Z.to_int n);;
 
 let test_bit x n =  Z.testbit x (Z.to_int n);;
 
 end;; (*struct Bits_Integer*)\<close>
 code_reserved OCaml Bits_Integer
 
 code_printing code_module Data_Bits \<rightharpoonup> (Haskell)
 \<open>
 module Data_Bits where {
 
 import qualified Data.Bits;
 
 {-
-  The ...Bounded functions assume that the Integer argument for the shift 
+  The ...Bounded functions assume that the Integer argument for the shift
   or bit index fits into an Int, is non-negative and (for types of fixed bit width)
   less than bitSize
 -}
 
 infixl 7 .&.;
 infixl 6 `xor`;
 infixl 5 .|.;
 
 (.&.) :: Data.Bits.Bits a => a -> a -> a;
 (.&.) = (Data.Bits..&.);
 
 xor :: Data.Bits.Bits a => a -> a -> a;
 xor = Data.Bits.xor;
 
 (.|.) :: Data.Bits.Bits a => a -> a -> a;
 (.|.) = (Data.Bits..|.);
 
 complement :: Data.Bits.Bits a => a -> a;
 complement = Data.Bits.complement;
 
 testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool;
 testBitUnbounded x b
   | b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b)
   | otherwise = error ("Bit index too large: " ++ show b)
 ;
 
 testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool;
 testBitBounded x b = Data.Bits.testBit x (fromInteger b);
 
 setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
 setBitUnbounded x n b
-  | n <= toInteger (Prelude.maxBound :: Int) = 
+  | n <= toInteger (Prelude.maxBound :: Int) =
     if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n)
   | otherwise = error ("Bit index too large: " ++ show n)
 ;
 
 setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
 setBitBounded x n True = Data.Bits.setBit x (fromInteger n);
 setBitBounded x n False = Data.Bits.clearBit x (fromInteger n);
 
 shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
-shiftlUnbounded x n 
+shiftlUnbounded x n
   | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n)
   | otherwise = error ("Shift operand too large: " ++ show n)
 ;
 
 shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a;
 shiftlBounded x n = Data.Bits.shiftL x (fromInteger n);
 
 shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
-shiftrUnbounded x n 
+shiftrUnbounded x n
   | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n)
   | otherwise = error ("Shift operand too large: " ++ show n)
 ;
 
 shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a;
 shiftrBounded x n = Data.Bits.shiftR x (fromInteger n);
 
 }\<close>
 
-  and \<comment> \<open>@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to 
+  and \<comment> \<open>@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to
             Haskell's Prelude.Int type instead of Integer. For compatibility
-            with the Haskell target, we nevertheless provide bounded and 
+            with the Haskell target, we nevertheless provide bounded and
             unbounded functions.\<close>
   (Haskell_Quickcheck)
 \<open>
 module Data_Bits where {
 
 import qualified Data.Bits;
 
 {-
-  The functions assume that the Int argument for the shift or bit index is 
+  The functions assume that the Int argument for the shift or bit index is
   non-negative and (for types of fixed bit width) less than bitSize
 -}
 
 infixl 7 .&.;
 infixl 6 `xor`;
 infixl 5 .|.;
 
 (.&.) :: Data.Bits.Bits a => a -> a -> a;
 (.&.) = (Data.Bits..&.);
 
 xor :: Data.Bits.Bits a => a -> a -> a;
 xor = Data.Bits.xor;
 
 (.|.) :: Data.Bits.Bits a => a -> a -> a;
 (.|.) = (Data.Bits..|.);
 
 complement :: Data.Bits.Bits a => a -> a;
 complement = Data.Bits.complement;
 
 testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
 testBitUnbounded = Data.Bits.testBit;
 
 testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
 testBitBounded = Data.Bits.testBit;
 
 setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
 setBitUnbounded x n True = Data.Bits.setBit x n;
 setBitUnbounded x n False = Data.Bits.clearBit x n;
 
 setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
 setBitBounded x n True = Data.Bits.setBit x n;
 setBitBounded x n False = Data.Bits.clearBit x n;
 
 shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftlUnbounded = Data.Bits.shiftL;
 
 shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftlBounded = Data.Bits.shiftL;
 
 shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftrUnbounded = Data.Bits.shiftR;
 
 shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a;
 shiftrBounded = Data.Bits.shiftR;
 
 }\<close>
 code_reserved Haskell Data_Bits
 
 code_printing code_module Bits_Integer \<rightharpoonup> (Scala)
 \<open>object Bits_Integer {
 
 def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt =
   if (n.isValidInt)
     if (b)
       x.setBit(n.toInt)
     else
       x.clearBit(n.toInt)
   else
     sys.error("Bit index too large: " + n.toString)
 
 def shiftl(x: BigInt, n: BigInt) : BigInt =
   if (n.isValidInt)
     x << n.toInt
   else
     sys.error("Shift index too large: " + n.toString)
 
 def shiftr(x: BigInt, n: BigInt) : BigInt =
   if (n.isValidInt)
     x << n.toInt
   else
     sys.error("Shift index too large: " + n.toString)
 
 def testBit(x: BigInt, n: BigInt) : Boolean =
   if (n.isValidInt)
-    x.testBit(n.toInt) 
+    x.testBit(n.toInt)
   else
     sys.error("Bit index too large: " + n.toString)
 
 } /* object Bits_Integer */\<close>
 
 code_printing
   constant "(AND) :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.andb ((_),/ (_))" and
   (OCaml) "Z.logand" and
   (Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.orb ((_),/ (_))" and
   (OCaml) "Z.logor" and
   (Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.xorb ((_),/ (_))" and
   (OCaml) "Z.logxor" and
   (Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 2 "^"
 | constant "NOT :: integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.notb" and
   (OCaml) "Z.lognot" and
   (Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and
   (Scala) "_.unary'_~"
 
 code_printing constant bin_rest_integer \<rightharpoonup>
   (SML) "IntInf.div ((_), 2)" and
   (OCaml) "Z.shift'_right/ _/ 1" and
   (Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and
   (Scala) "_ >> 1"
 
 context
 includes integer.lifting
 begin
 
 lemma bitNOT_integer_code [code]:
   fixes i :: integer shows
   "NOT i = - i - 1"
 by transfer(simp add: int_not_def)
 
 lemma bin_rest_integer_code [code nbe]:
   "bin_rest_integer i = i div 2"
   by transfer rule
 
 lemma bin_last_integer_code [code]:
   "bin_last_integer i \<longleftrightarrow> i AND 1 \<noteq> 0"
   by transfer (rule bin_last_conv_AND)
 
 lemma bin_last_integer_nbe [code nbe]:
   "bin_last_integer i \<longleftrightarrow> i mod 2 \<noteq> 0"
 by transfer(simp add: bin_last_def)
 
 lemma bitval_bin_last_integer [code_unfold]:
   "of_bool (bin_last_integer i) = i AND 1"
 by transfer(rule bitval_bin_last)
 
 end
 
 definition integer_test_bit :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))"
 
 declare [[code drop: \<open>bit :: integer \<Rightarrow> nat \<Rightarrow> bool\<close>]]
 
 lemma bit_integer_code [code]:
   "bit x n \<longleftrightarrow> integer_test_bit x (integer_of_nat n)"
   by (simp add: integer_test_bit_def)
 
 lemma integer_test_bit_code [code]:
   "integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_test_bit 0 0 = False"
   "integer_test_bit 0 (Code_Numeral.Pos n) = False"
   "integer_test_bit (Code_Numeral.Pos num.One)      0 = True"
   "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False"
   "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True"
   "integer_test_bit (Code_Numeral.Pos num.One)      (Code_Numeral.Pos n') = False"
   "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Neg num.One)      0 = True"
   "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False"
   "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True"
   "integer_test_bit (Code_Numeral.Neg num.One)      (Code_Numeral.Pos n') = True"
   "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)"
                 apply (simp_all add: integer_test_bit_def bit_integer_def)
-  using bin_nth_numeral_simps(5) apply simp
-  done
+  using bin_nth_numeral_simps bit_numeral_int_simps(6)
+  by presburger
 
 code_printing constant integer_test_bit \<rightharpoonup>
   (SML) "Bits'_Integer.test'_bit" and
   (OCaml) "Bits'_Integer.test'_bit" and
   (Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and
   (Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and
   (Scala) "Bits'_Integer.testBit"
 
 context
 includes integer.lifting
 begin
 
 lemma lsb_integer_code [code]:
   fixes x :: integer shows
   "lsb x = bit x 0"
 by transfer(simp add: lsb_int_def)
 
 definition integer_set_bit :: "integer \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> integer"
 where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_integer_code [code]:
   "set_bit x i b = integer_set_bit x (integer_of_nat i) b"
 by(simp add: integer_set_bit_def)
 
-lemma set_bit_integer_conv_masks: 
+lemma set_bit_integer_conv_masks:
   fixes x :: integer shows
   "set_bit x i b = (if b then x OR (1 << i) else x AND NOT (1 << i))"
-  by transfer (simp add: int_set_bit_False_conv_NAND int_set_bit_True_conv_OR shiftl_eq_push_bit) 
+  by transfer (simp add: int_set_bit_False_conv_NAND int_set_bit_True_conv_OR shiftl_eq_push_bit)
 
 end
 
 code_printing constant integer_set_bit \<rightharpoonup>
   (SML) "Bits'_Integer.set'_bit" and
   (Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and
   (Scala) "Bits'_Integer.setBit"
 
 text \<open>
   OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks.
   We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR.
 \<close>
 lemma integer_set_bit_code [code]:
   "integer_set_bit x n b =
   (if n < 0 then undefined x n b else
    if b then x OR (push_bit (nat_of_integer n) 1)
    else x AND NOT (push_bit (nat_of_integer n) 1))"
   by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def)
 
 definition integer_shiftl :: "integer \<Rightarrow> integer \<Rightarrow> integer"
 where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)"
 
 declare [[code drop: \<open>push_bit :: nat \<Rightarrow> integer \<Rightarrow> integer\<close>]]
 
-lemma shiftl_integer_code [code]: 
+lemma shiftl_integer_code [code]:
   fixes x :: integer shows
   "push_bit n x = integer_shiftl x (integer_of_nat n)"
 by(auto simp add: integer_shiftl_def)
 
 context
 includes integer.lifting
 begin
 
 lemma shiftl_integer_conv_mult_pow2:
   fixes x :: integer shows
   "x << n = x * 2 ^ n"
   by (simp add: push_bit_eq_mult shiftl_eq_push_bit)
 
 lemma integer_shiftl_code [code]:
   "integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_shiftl x 0 = x"
   "integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)"
   "integer_shiftl 0 (Code_Numeral.Pos n) = 0"
      apply (simp_all add: integer_shiftl_def numeral_eq_Suc)
   apply transfer
   apply (simp add: ac_simps)
   done
 
 end
 
 code_printing constant integer_shiftl \<rightharpoonup>
   (SML) "Bits'_Integer.shiftl" and
   (OCaml) "Bits'_Integer.shiftl" and
   (Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) "Bits'_Integer.shiftl"
 
 definition integer_shiftr :: "integer \<Rightarrow> integer \<Rightarrow> integer"
 where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)"
 
 declare [[code drop: \<open>drop_bit :: nat \<Rightarrow> integer \<Rightarrow> integer\<close>]]
 
-lemma shiftr_integer_conv_div_pow2: 
+lemma shiftr_integer_conv_div_pow2:
   includes integer.lifting fixes x :: integer shows
   "x >> n = x div 2 ^ n"
   by (simp add: drop_bit_eq_div shiftr_eq_drop_bit)
 
 lemma shiftr_integer_code [code]:
   fixes x :: integer shows
   "drop_bit n x = integer_shiftr x (integer_of_nat n)"
 by(auto simp add: integer_shiftr_def)
 
 code_printing constant integer_shiftr \<rightharpoonup>
   (SML) "Bits'_Integer.shiftr" and
   (OCaml) "Bits'_Integer.shiftr" and
   (Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) "Bits'_Integer.shiftr"
 
 lemma integer_shiftr_code [code]:
   includes integer.lifting
   shows
   "integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_shiftr x 0 = x"
   "integer_shiftr 0 (Code_Numeral.Pos n) = 0"
   "integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0"
-  "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) = 
+  "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
-  "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) = 
+  "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
   "integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1"
-  "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) = 
+  "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)"
-  "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) = 
+  "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)"
           apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc)
     apply transfer apply simp
    apply transfer apply simp
   apply transfer apply (simp add: add_One)
   done
 
 context
 includes integer.lifting
 begin
 
 lemma Bit_integer_code [code]:
   "Bit_integer i False = push_bit 1 i"
   "Bit_integer i True = (push_bit 1 i) + 1"
   by (transfer; simp add: shiftl_int_def)+
 
 lemma msb_integer_code [code]:
   "msb (x :: integer) \<longleftrightarrow> x < 0"
 by transfer(simp add: msb_int_def)
 
 end
 
 context
 includes integer.lifting natural.lifting
 begin
 
 lemma bitAND_integer_unfold [code]:
   "x AND y =
    (if x = 0 then 0
     else if x = - 1 then y
     else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x \<and> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       and_int_rec [of _ \<open>_ * 2\<close>] and_int_rec [of \<open>_ * 2\<close>] and_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 lemma bitOR_integer_unfold [code]:
   "x OR y =
    (if x = 0 then y
     else if x = - 1 then - 1
     else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x \<or> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       or_int_rec [of _ \<open>_ * 2\<close>] or_int_rec [of _ \<open>1 + _ * 2\<close>] or_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 lemma bitXOR_integer_unfold [code]:
   "x XOR y =
    (if x = 0 then y
     else if x = - 1 then NOT y
     else Bit_integer (bin_rest_integer x XOR bin_rest_integer y)
       (\<not> bin_last_integer x \<longleftrightarrow> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       xor_int_rec [of _ \<open>_ * 2\<close>] xor_int_rec [of \<open>_ * 2\<close>] xor_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 end
 
 
 section \<open>Test code generator setup\<close>
 
 definition bit_integer_test :: "bool" where
   "bit_integer_test =
   (([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5)
     , -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5)
     , NOT 1, NOT (- 3)
     , -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3)
     , set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False
     , 1 << 2, -1 << 3
     , 100 >> 3, -100 >> 3] :: integer list)
   = [ 3, 1, 1, -7
     , -3, -3, 7, -1
     , -2, 2
     , -4, -4, 6, 6
     , 21, -1, 4, -7
     , 4, -8
     , 12, -13] \<and>
     [ (5 :: integer) !! 4, (5 :: integer) !! 2, (-5 :: integer) !! 4, (-5 :: integer) !! 2
-    , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer), 
+    , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer),
       msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)]
   = [ False, True, True, False,
       True, False, True, False,
       False, False, True, True])"
 
 export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala
 
 notepad begin
 have bit_integer_test by eval
 have bit_integer_test by normalization
 have bit_integer_test by code_simp
 end
 ML_val \<open>val true = @{code bit_integer_test}\<close>
 
 lemma "x AND y = x OR (y :: integer)"
 quickcheck[random, expect=counterexample]
 quickcheck[exhaustive, expect=counterexample]
 oops
 
 lemma "(x :: integer) AND x = x OR x"
 quickcheck[narrowing, expect=no_counterexample]
 oops
 
 lemma "(f :: integer \<Rightarrow> unit) = g"
 quickcheck[narrowing, size=3, expect=no_counterexample]
 by(simp add: fun_eq_iff)
 
 hide_const bit_integer_test
 hide_fact bit_integer_test_def
 
 end