lib+autocorres: move NatBitwise to AutoCorres

Since most bitwise operations are now available by default for nat,
only word abstraction in AutoCorres depends on NatBitwise.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/HaskellLib_H.thy

@@ -12,7 +12,6 @@
 theory HaskellLib_H
 imports
   Lib
-  NatBitwise
   More_Numeral_Type
   Monads.NonDetMonadVCG
 begin

lib/Lib.thy

@@ -2513,38 +2513,6 @@ lemma option_Some_value_independent:
   "\<lbrakk> f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v' \<rbrakk> \<Longrightarrow> f y = Some v"
   by blast
 
-text \<open>Some int bitwise lemmas. Helpers for proofs about \<^file>\<open>NatBitwise.thy\<close>\<close>
-lemma int_2p_eq_shiftl:
-  "(2::int)^x = 1 << x"
-  by (simp add: shiftl_int_def)
-
-lemma nat_int_mul:
-  "nat (int a * b) = a * nat b"
-  by (simp add: nat_mult_distrib)
-
-lemma int_shiftl_less_cancel:
-  "n \<le> m \<Longrightarrow> ((x :: int) << n < y << m) = (x < y << (m - n))"
-  apply (drule le_Suc_ex)
-  apply (clarsimp simp: shiftl_int_def power_add)
-  done
-
-lemma int_shiftl_lt_2p_bits:
-  "0 \<le> (x::int) \<Longrightarrow> x < 1 << n \<Longrightarrow> \<forall>i \<ge> n. \<not> x !! i"
-  apply (clarsimp simp: shiftl_int_def)
-  by (metis bit_take_bit_iff not_less take_bit_int_eq_self_iff)
-\<comment> \<open>TODO: The converse should be true as well, but seems hard to prove.\<close>
-
-lemmas int_eq_test_bit = bin_eq_iff
-lemmas int_eq_test_bitI = int_eq_test_bit[THEN iffD2, rule_format]
-
-lemma le_nat_shrink_left:
-  "y \<le> z \<Longrightarrow> y = Suc x \<Longrightarrow> x < z"
-  by simp
-
-lemma length_ge_split:
-  "n < length xs \<Longrightarrow> \<exists>x xs'. xs = x # xs' \<and> n \<le> length xs'"
-  by (cases xs) auto
-
 text \<open>Support for defining enumerations on datatypes derived from enumerations\<close>
 lemma distinct_map_enum:
   "\<lbrakk> (\<forall> x y. (F x = F y \<longrightarrow> x = y )) \<rbrakk>

tools/autocorres/NatBitwise.thy

@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-(* Instance of bit ops for nat. Used by HaskellLib and AutoCorres.
- * Lemmas about this instance should also go here. *)
+(* Instance of bit ops for nat.
+   Lemmas about this instance should also go here. *)
 theory NatBitwise
 imports
-  Lib
+  Word_Lib.WordSetup
 begin
 
 instantiation nat :: lsb
@@ -50,10 +50,20 @@ lemma nat_2p_eq_shiftl:
 
 lemmas shiftl_nat_alt_def = shiftl_nat_def
 
+lemma nat_int_mul:
+  "nat (int a * b) = a * nat b"
+  by (simp add: nat_mult_distrib)
+
 lemma shiftl_nat_def:
   "(x::nat) << y = nat (int x << y)"
   by (simp add: nat_int_mul push_bit_eq_mult shiftl_def)
 
+lemma int_shiftl_less_cancel:
+  "n \<le> m \<Longrightarrow> ((x :: int) << n < y << m) = (x < y << (m - n))"
+  apply (drule le_Suc_ex)
+  apply (clarsimp simp: shiftl_int_def power_add)
+  done
+
 lemma nat_shiftl_less_cancel:
   "n \<le> m \<Longrightarrow> ((x :: nat) << n < y << m) = (x < y << (m - n))"
   apply (simp add: nat_int_comparison(2) shiftl_nat_def shiftl_def)
@@ -69,4 +79,16 @@ lemma nat_shiftl_lt_2p_bits:
 lemmas nat_eq_test_bit = bit_eq_iff
 lemmas nat_eq_test_bitI = bit_eq_iff[THEN iffD2, rule_format]
 
+lemma int_2p_eq_shiftl:
+  "(2::int)^x = 1 << x"
+  by (simp add: shiftl_int_def)
+
+lemma int_shiftl_lt_2p_bits:
+  "0 \<le> (x::int) \<Longrightarrow> x < 1 << n \<Longrightarrow> \<forall>i \<ge> n. \<not> x !! i"
+  apply (clarsimp simp: shiftl_int_def)
+  by (metis bit_take_bit_iff not_less take_bit_int_eq_self_iff)
+\<comment> \<open>TODO: The converse should be true as well, but seems hard to prove.\<close>
+
+lemmas int_eq_test_bitI = bin_eq_iff[THEN iffD2, rule_format]
+
 end

tools/autocorres/WordAbstract.thy

@@ -8,7 +8,7 @@ theory WordAbstract
 imports
   L2Defs
   ExecConcrete
-  Lib.NatBitwise
+  NatBitwise
 begin
 
 definition "WORD_MAX x \<equiv> ((2 ^ (len_of x - 1) - 1) :: int)"