diff --git a/thys/X86_Semantics/BitByte.thy b/thys/X86_Semantics/BitByte.thy
--- a/thys/X86_Semantics/BitByte.thy
+++ b/thys/X86_Semantics/BitByte.thy
@@ -1,246 +1,253 @@
 (*  Title:       X86 instruction semantics and basic block symbolic execution
     Authors:     Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
     Year:        2020
     Maintainer:  Freek Verbeek (freek@vt.edu)
 *)
 
 section "Bit and byte-level theorems"
 
 theory BitByte
-  imports Main Word_Lib.Bitwise
+  imports Main "Word_Lib.Syntax_Bundles" "Word_Lib.Bit_Shifts_Infix_Syntax" "Word_Lib.Bitwise"
 begin
 
+subsection \<open>Basics\<close>
+
+unbundle bit_operations_syntax
+unbundle bit_projection_infix_syntax
 
 definition take_bits :: "nat \<Rightarrow> nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word" ("\<langle>_,_\<rangle>_" 51) \<comment> \<open>little-endian\<close>
   where "take_bits l h w \<equiv> (w >> l) AND mask (h-l)"
 
 text \<open>
   @{term "take_bits l h w"} takes a subset of bits from word @{term w}, from low (inclusive) to high (exclusive).
   For example, @{term [show_types] "take_bits 2 5 (28::8word) = 7"}.
 \<close>
 
 definition take_byte :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 8word" \<comment> \<open>little-endian\<close>
   where "take_byte n w \<equiv> ucast (\<langle>n*8,n*8+8\<rangle>w)"
 
 text \<open>
   @{term "take_byte n w"} takes the nth byte from word @{term w}.
   For example, @{term [show_types] "take_byte 1 (42 << 8::16word) = 42"}.
 \<close>
 
 definition overwrite :: "nat \<Rightarrow> nat \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word \<Rightarrow> 'a::len word"
   where "overwrite l h w0 w1 \<equiv> ((\<langle>h,LENGTH('a)\<rangle>w0) << h) OR ((\<langle>l,h\<rangle>w1) << l) OR (\<langle>0,l\<rangle>w0)"
 
 text \<open>
   @{term "overwrite l h w0 w1"} overwrites low (inclusive) to high (exclusive) bits in
   word @{term w0} with bits from word @{term w1}.
   For example, @{term [show_types] "(overwrite 2 4 28 227 :: 8word) = 16"}.
 \<close>
 
 
 text \<open>We prove some theorems about taking the nth bit/byte of an operation. These are useful to prove
       equaltiy between different words, by first applying rule @{thm word_eqI}.\<close>
 
+lemma bit_take_bits_iff [bit_simps]:
+  \<open>(\<langle>l,h\<rangle>w) !! n \<longleftrightarrow> n < LENGTH('a) \<and> n < h - l \<and> w !! (n + l)\<close> for w :: \<open>'a::len word\<close>
+  by (simp add: take_bits_def bit_simps ac_simps)
+
+lemma bit_take_byte_iff [bit_simps]:
+  \<open>take_byte m w !! n \<longleftrightarrow> n < LENGTH('a) \<and> n < 8 \<and> w !! (n + m * 8)\<close> for w :: \<open>'a::len word\<close>
+  by (auto simp add: take_byte_def bit_simps)
+
+lemma bit_overwrite_iff [bit_simps]:
+  \<open>overwrite l h w0 w1 !! n \<longleftrightarrow> n < LENGTH('a) \<and>
+    (if l \<le> n \<and> n < h then w1 else w0) !! n\<close>
+    for w0 w1 :: \<open>'a::len word\<close>
+  by (auto simp add: overwrite_def bit_simps)
+
 lemma nth_takebits:
   fixes w :: "'a::len word"
   shows "(\<langle>l,h\<rangle>w) !! n = (if n < LENGTH('a) \<and> n < h - l then w !! (n + l) else False)"
-  by (auto simp add: take_bits_def word_ao_nth word_size nth_shiftr)
+  by (auto simp add: bit_simps)
 
 lemma nth_takebyte:
   fixes w :: "'a::len word"
   shows "take_byte (n div 8) w !! (n mod 8) = (if n mod 8 < LENGTH('a) then w!!n else False )"
-  by (auto simp add: take_byte_def nth_ucast nth_takebits split: if_split_asm)
+  by (simp add: bit_simps)
 
 lemma nth_take_byte_overwrite:
   fixes v v' :: "'a::len word"
   shows "take_byte n (overwrite l h v v') !! i = (if i + n * 8 < l \<or> i + n * 8 \<ge> h then take_byte n v !! i else take_byte n v' !! i)"
-  by (auto simp add: take_byte_def overwrite_def nth_ucast nth_takebits word_ao_nth nth_shiftl)
-     (metis test_bit_bin)+
+  by (auto simp add: bit_simps dest: bit_imp_le_length)
 
 lemma nth_bitNOT:
   fixes a :: "'a::len word"
   shows "(NOT a) !! n \<longleftrightarrow> (if n < LENGTH('a)  then \<not>(a !! n) else False)"
-  apply (auto simp add: word_ops_nth_size word_size)
-  by (simp add: bin_nth_uint word_test_bit_def)
+  by (simp add: bit_simps)
 
 
 text \<open>Various simplification rules\<close>
 
 lemma ucast_take_bits:
   fixes w :: "'a::len word"
   assumes "h = LENGTH('b)"
       and "LENGTH('b) \<le> LENGTH('a)"
-  shows "ucast (\<langle>0,h\<rangle>w) = (ucast w ::'b :: len word)"
-  apply (rule word_eqI)
+    shows "ucast (\<langle>0,h\<rangle>w) = (ucast w ::'b :: len word)"
+  apply (rule bit_word_eqI)
   using assms
-  by (auto simp add: word_size nth_ucast nth_takebits)
+  apply (simp add: bit_simps)
+  done
 
 lemma take_bits_ucast:
   fixes w :: "'b::len word"
   assumes "h = LENGTH('b)"
   shows "(\<langle>0,h\<rangle> (ucast w ::'a :: len word)) = (ucast w ::'a :: len word)"
-  apply (rule word_eqI)
-  by (metis Traditional_Infix_Syntax.nth_ucast add.right_neutral assms(1) diff_zero nth_takebits test_bit_size word_size)
+  apply (rule bit_word_eqI)
+  using assms
+  apply (auto simp add: bit_simps dest: bit_imp_le_length)
+  done
 
 lemma take_bits_take_bits:
   fixes w :: "'a::len word"
   shows "(\<langle>l,h\<rangle>(\<langle>l',h'\<rangle>w)) = (if min LENGTH('a) h \<ge> h' - l' then \<langle>l+l',h'\<rangle>w else (\<langle>l+l',l'+min LENGTH('a) h\<rangle>w))"
-  apply (rule word_eqI)
-  by (auto simp add: word_size nth_takebits word_ao_nth nth_shiftl min_def)
-     (metis semiring_normalization_rules(25))+
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps ac_simps)
+  apply auto
+  done
 
 lemma take_bits_overwrite:
   shows "\<langle>l,h\<rangle>(overwrite l h w0 w1) = \<langle>l,h\<rangle>w1"
-  apply (auto simp add: overwrite_def)
-  apply (rule word_eqI)
-  by (auto simp add: word_size nth_takebits word_ao_nth nth_shiftl)
-     (simp add: bin_nth_uint_imp word_test_bit_def)
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps ac_simps)
+  apply (auto dest: bit_imp_le_length)
+  done
 
 lemma overwrite_0_take_bits_0:
   shows "overwrite 0 h (\<langle>0,h\<rangle>w0) w1 = \<langle>0,h\<rangle>w1"
-  apply (auto simp add: overwrite_def)
-  apply (rule word_eqI)
-  by (auto simp add: word_size nth_takebits word_ao_nth nth_shiftl)
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps ac_simps)
+  done
 
 lemma take_byte_shiftlr_256:
-fixes v :: "256 word"
+  fixes v :: "256 word"
   assumes "m \<le> n"
   shows "take_byte n (v << m*8) = (if (n+1)*8 \<le> 256 then take_byte (n-m) v else 0)"
-  apply (rule word_eqI)
+  apply (rule bit_word_eqI)
   using assms
-  by (auto simp add: take_byte_def nth_ucast nth_takebits word_size nth_shiftl diff_mult_distrib)
-
+  apply (simp add: bit_simps)
+  apply (simp add: algebra_simps)
+  done
 
 
 subsection \<open> Take\_Bits and arithmetic\<close>
 
 text \<open>This definition is based on @{thm to_bl_plus_carry}, which formulates addition as bitwise operations using @{term xor3} and @{term carry}.\<close>
 
 definition bitwise_add :: "(bool \<times> bool) list \<Rightarrow> bool \<Rightarrow> bool list"
   where "bitwise_add x c \<equiv> foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) x (\<lambda>_. []) c"
 
 lemma length_foldr_bitwise_add:
   shows "length (bitwise_add x c) = length x"
   unfolding bitwise_add_def
   by(induct x arbitrary: c) auto
 
 text \<open>This is the "heart" of the proof: bitwise addition of two appended zipped lists can be expressed as
       two consecutive bitwise additions.
       Here, I need to make the assumption that the final carry is False.
  \<close>
 lemma bitwise_add_append:
   assumes "x = [] \<or> \<not>carry (fst (last x)) (snd (last x)) True"
   shows "bitwise_add (x @ y) (x\<noteq>[] \<and> c) = bitwise_add x (x\<noteq>[] \<and> c) @ bitwise_add y False"
   using assms
   unfolding bitwise_add_def
   by(induct x arbitrary: c) (auto simp add: case_prod_unfold xor3_def carry_def split: if_split_asm)
 
 lemma bitwise_add_take_append:
   shows "take (length x) (bitwise_add (x @ y) c) = bitwise_add x c"
   unfolding bitwise_add_def
   by(induct x arbitrary: c) (auto simp add: case_prod_unfold xor3_def carry_def split: if_split_asm)
 
 lemma bitwise_add_zero:
   shows "bitwise_add (replicate n (False, False)) False = replicate n False "
   unfolding bitwise_add_def
   by(induct n) (auto simp add: xor3_def carry_def)
 
 lemma bitwise_add_take:
   shows "take n (bitwise_add x c) = bitwise_add (take n x) c"
   unfolding bitwise_add_def
   by (induct n arbitrary: x c,auto)
      (metis append_take_drop_id bitwise_add_def bitwise_add_take_append diff_is_0_eq' length_foldr_bitwise_add length_take nat_le_linear rev_min_pm1 take_all)
 
 
 lemma fst_hd_drop_zip:
   assumes "n < length x"
       and "length x = length y"
   shows "fst (hd (drop n (zip x y))) = hd (drop n x)"
   using assms
   by (induct x arbitrary: n y,auto)
      (metis (no_types, lifting) Cons_nth_drop_Suc drop_zip fst_conv length_Cons list.sel(1) zip_Cons_Cons)
 
 lemma snd_hd_drop_zip:
   assumes "n < length x"
       and "length x = length y"
   shows "snd (hd (drop n (zip x y))) = hd (drop n y)"
   using assms
   by (induct x arbitrary: n y,auto)
      (metis (no_types, lifting) Cons_nth_drop_Suc drop_zip snd_conv length_Cons list.sel(1) zip_Cons_Cons)
 
 text \<open>
   Ucasting of @{term "a+b"} can be rewritten to taking bits of @{term a} and @{term b}.
 \<close>
 
 lemma ucast_plus:
   fixes a b :: "'a::len word"
   assumes "LENGTH('a) > LENGTH('b)"
   shows "(ucast (a + b) ::'b::len word) = (ucast a + ucast b::'b::len word)"
 proof-
   have "to_bl (ucast (a + b) ::'b::len word) = to_bl (ucast a + ucast b::'b::len word)"
     using assms
     apply (auto simp add: to_bl_ucast to_bl_plus_carry word_rep_drop length_foldr_bitwise_add drop_zip[symmetric] rev_drop bitwise_add_def simp del: foldr_replicate foldr_append)
     apply (simp only: bitwise_add_def[symmetric] length_foldr_bitwise_add)
     by (auto simp add: drop_take bitwise_add_take[symmetric] rev_take length_foldr_bitwise_add)
   thus ?thesis
     using word_bl.Rep_eqD
     by blast
 qed
 
 lemma ucast_uminus:
   fixes a b :: "'a::len word"
 assumes "LENGTH('a) > LENGTH('b)"
   shows "ucast (- a) = (- ucast a :: 'b::len word)"
   apply (subst twos_complement)+
   apply (subst word_succ_p1)+
   apply (subst ucast_plus)
   apply (rule assms)
    apply simp
    apply (rule word_eqI)
    apply (auto simp add: word_size nth_ucast nth_bitNOT)
    using assms order.strict_trans
    by blast
 
 lemma ucast_minus:
   fixes a b :: "'a::len word"
   assumes "LENGTH('a) > LENGTH('b)"
   shows "(ucast (a - b) ::'b::len word) = (ucast a - ucast b::'b::len word)"
   using ucast_plus[OF assms,of a "-b"] ucast_uminus[OF assms,of b]
   by auto
 
-
-
 lemma to_bl_takebits:
   fixes a :: "'a::len word"
   shows "to_bl (\<langle>0,h\<rangle>a) = replicate (LENGTH('a) - h) False @ drop (LENGTH('a) - h) (to_bl a)"
   apply (auto simp add: take_bits_def bl_word_and to_bl_mask)
   apply (rule nth_equalityI)
   by (auto simp add: min_def nth_append)
 
+
 text \<open> All simplification rules that are used during symbolic execution.\<close>
 lemmas BitByte_simps = ucast_plus ucast_minus ucast_uminus take_bits_overwrite take_bits_take_bits
-  ucast_take_bits overwrite_0_take_bits_0 mask_eq
+  ucast_take_bits overwrite_0_take_bits_0 mask_eq_exp_minus_1
   ucast_down_ucast_id is_down take_bits_ucast ucast_up_ucast_id is_up
 
-
-
-
 text \<open>Simplification for immediate (numeral) values.\<close>
 lemmas take_bits_numeral[simp] = take_bits_def[of _ _ "numeral n"] for n
 lemmas take_bits_num0[simp] = take_bits_def[of _ _ "0"] for n
 lemmas take_bits_num1[simp] = take_bits_def[of _ _ "1"] for n
 lemmas overwrite_numeral_numeral[simp] = overwrite_def[of _ _ "numeral n" "numeral m"] for n m
 lemmas overwrite_num0_numeral[simp] = overwrite_def[of _ _ 0 "numeral m"] for n m
 lemmas overwrite_numeral_num0[simp] = overwrite_def[of _ _ "numeral m" 0] for n m
 lemmas overwrite_numeral_00[simp] = overwrite_def[of _ _ 0 0]
 
-lemmas shiftr_def_numeral[simp] = shiftr_def[of "- numeral n" "numeral m"] for n m
-lemmas shiftr1_def_numeral[simp] = shiftr1_eq[of "- numeral n"] for n
-lemmas bintrunc_numeral_minus_1[simp] = bintrunc_numeral[of k "-1"] for k
-
-lemmas word_less_minus_numeral_numeral [simp] = word_less_def [of "- numeral a" "numeral b"] for a b
-
-lemmas ucast_minus_numeral[simp] = ucast_eq[of "- numeral w"] for w
-lemmas mask_numeral[simp] = mask_eq[of "numeral w"] for w
-
-
 end
\ No newline at end of file
diff --git a/thys/X86_Semantics/Memory.thy b/thys/X86_Semantics/Memory.thy
--- a/thys/X86_Semantics/Memory.thy
+++ b/thys/X86_Semantics/Memory.thy
@@ -1,358 +1,358 @@
 (*  Title:       X86 instruction semantics and basic block symbolic execution
     Authors:     Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
     Year:        2020
     Maintainer:  Freek Verbeek (freek@vt.edu)
 *)
 
 section "Memory-related theorems"
 
 theory Memory
   imports BitByte
 begin
 
 context
   fixes dummy_type :: "'a::len"
 begin
 
 primrec read_bytes :: "('a word \<Rightarrow> 8 word) \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> 8word list"
   where "read_bytes m a 0   = []"
   | "read_bytes m a (Suc n) = m (a + of_nat n) # read_bytes m a n"
 
 text \<open>Read bytes from memory. Memory is represented by a term of @{typ "64 word \<Rightarrow> 8 word"}.
       Given an address @{term [show_types] "a::64 word"} and a size @{term n}, retrieve the bytes in
       the order they are stored in memory.\<close>
 
 definition region_addresses :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word set"
   where "region_addresses a si \<equiv> {a' . \<exists> i < si . a' = a + of_nat (si - i - 1)}"
 
 text \<open>The set of addresses belonging to a region starting at address @{term "a::64 word"} of @{term si} bytes.\<close>
 
 definition region_overflow :: "'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "region_overflow a si \<equiv> unat a + si \<ge> 2^LENGTH('a)"
 
 text \<open>An overflow occurs if the address plus the size is greater equal @{term "2^64"}\<close>
 
 definition enclosed :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "enclosed a' si' a si \<equiv> unat a + si < 2^LENGTH('a) \<and> unat a \<le> unat a' \<and> unat a' + si' \<le> unat a + si"
 
 text \<open>A region is enclosed in another if its @{const region_addresses} is a subset of the other.\<close>
 
 definition separate :: "'a word \<Rightarrow> nat \<Rightarrow> 'a word \<Rightarrow> nat \<Rightarrow> bool"
   where "separate a si a' si' \<equiv> si \<noteq>0 \<and> si' \<noteq> 0 \<and> region_addresses a si \<inter> region_addresses a' si' = {}"
 
 text \<open>A region is separate from another if they do not overlap.\<close>
 
 
 
 lemma region_addresses_iff: "a' \<in> region_addresses a si \<longleftrightarrow> unat (a' - a) < si"
-  apply (auto simp add: region_addresses_def)
+  apply (auto simp add: region_addresses_def unsigned_of_nat)
    apply (metis diff_Suc_less le_less_trans less_imp_Suc_add take_bit_nat_less_eq_self zero_less_Suc)
   by (smt (z3) add.commute add_Suc_right add_diff_cancel_left' diff_add_cancel less_add_Suc2 less_imp_Suc_add word_unat.Rep_inverse)
 
 lemma notin_region_addresses:
   assumes "x \<notin> region_addresses a si"
   shows "unat x < unat a \<or> unat a + si \<le> unat x"
   by (metis assms add.commute less_diff_conv2 not_le_imp_less region_addresses_iff unat_sub_if')
 
 lemma notin_region_addresses_sub:
   assumes "x \<notin> region_addresses a si"
   shows "unat (x - a') < unat (a - a') \<or> unat (a - a') + si \<le> unat (x - a')"
   using assms notin_region_addresses region_addresses_iff by auto
 
 lemma region_addresses_eq_empty_iff: "region_addresses a si = {} \<longleftrightarrow> si = 0"
   by (metis region_addresses_iff add_diff_cancel_left' ex_in_conv neq0_conv not_less0 unsigned_0)
 
 lemma length_read_bytes:
   shows "length (read_bytes m a si) = si"
   by (induct si,auto)
 
 lemma nth_read_bytes:
 assumes "n < si"
 shows "read_bytes m a si ! n = m (a + of_nat (si - 1 - n))"
   using assms
   apply (induct si arbitrary: n,auto)
   subgoal for si n
     by(cases n,auto)
   done
 
 text \<open>Writing to memory occurs via function @{const override_on}.
       In case of enclosure, reading bytes from memory overridden on a set of region addresses can
       be simplified to reading bytes from the overwritten memory only.
       In case of separation, reading bytes from overridden memory can be simplified to reading
       from the original memory.\<close>
 
 lemma read_bytes_override_on_enclosed:
 assumes "offset' \<le> offset"
     and "si' \<le> si"
     and "unat offset + si' \<le> si + unat offset'"
   shows "read_bytes (override_on m m' (region_addresses (a - offset) si)) (a - offset') si' = read_bytes m' (a - offset') si'"
 proof-
   {
     fix i
     assume 1: "i < si'"
     let ?i = "(si + i + unat offset') - unat offset - si'"
 
     have "i + unat offset' < si' + unat offset"
       using 1 assms(1)
       by unat_arith
     hence 2: "si + i + unat offset' - (unat offset + si') < si"
       using diff_less[of "(si' + unat offset - i) - unat offset'" si] assms(3)
       by auto
     moreover
     have "of_nat (si' - Suc i) - offset' = of_nat (si - Suc ?i) - offset"
       using assms 1 2 by (auto simp add: of_nat_diff)
     ultimately
     have "\<exists> i' < si. of_nat (si' - Suc i) - offset' = of_nat (si - Suc i') - offset"
       by auto
   }
   note 1 = this
   show ?thesis
     apply (rule nth_equalityI)
     using 1
     by (auto simp add: length_read_bytes nth_read_bytes override_on_def region_addresses_def)
 qed
 
 lemmas read_bytes_override_on = read_bytes_override_on_enclosed[where offset=0 and offset'=0,simplified]
 
 lemma read_bytes_override_on_enclosed_plus:
   assumes "unat offset + si' \<le> si"
       and "si \<le> 2^LENGTH('a)"
   shows "read_bytes (override_on m m' (region_addresses a si)) (offset+a) si' = read_bytes m' (offset+a) si'"
 proof-
   {
     fix i
     have "i < si' \<Longrightarrow> \<exists> i' < si. offset + (of_nat (si' - Suc i)::'a word) = of_nat (si - Suc i')"
       apply (rule exI[of _"si - si' + i - unat offset"])
       using assms by (auto simp add: of_nat_diff)
   }
   note 1 = this
   show ?thesis
     apply (rule nth_equalityI)
     using assms 1
     by (auto simp add: override_on_def length_read_bytes nth_read_bytes region_addresses_def)
 qed
 
 
 lemma read_bytes_override_on_separate:
 assumes "separate a si a' si'"
   shows "read_bytes (override_on m m' (region_addresses a si)) a' si' = read_bytes m a' si'"
   apply (rule nth_equalityI)
   using assms
   by (auto simp add: length_read_bytes nth_read_bytes override_on_def separate_def region_addresses_def)
 
 
 text\<open>Bytes are are written to memory one-by-one, then read by @{const read_bytes} producing a list of bytes.
     That list is concatenated again using @{const word_rcat}. Writing @{term si} bytes of word @{term w} into
     memory, reading the byte-list and concatenating again produces @{term si} bytes of the original word.\<close>
 
 
 lemma word_rcat_read_bytes_enclosed:
   fixes w :: "'b::len word"
   assumes "LENGTH('b) \<le> 2^LENGTH('a)"
     and "unat offset + si \<le> 2^LENGTH('a)"
   shows "word_rcat (read_bytes (\<lambda>a'. take_byte (unat (a' - a)) w) (a + offset) si) = \<langle>unat offset * 8,(unat offset + si) * 8\<rangle>w"
   apply (rule word_eqI)
   using assms
   apply (auto simp add: test_bit_rcat word_size length_read_bytes rev_nth nth_read_bytes unat_of_nat nth_takebyte unat_word_ariths )
     apply (auto simp add: take_byte_def nth_ucast nth_takebits take_bit_eq_mod split: if_split_asm)[1]
    apply (auto simp add: nth_takebits split: if_split_asm)[1]
   apply (auto simp add: take_byte_def nth_ucast nth_takebits split: if_split_asm)[1]
   by (auto simp add: rev_nth length_read_bytes take_byte_def nth_ucast nth_takebits nth_read_bytes unat_word_ariths unat_of_nat take_bit_eq_mod split: if_split_asm)
 
 lemmas word_rcat_read_bytes = word_rcat_read_bytes_enclosed[where offset=0,simplified]
 
 
 
 text \<open>The following theorems allow reasoning over enclosure and separation, for example as linear arithmetic.\<close>
 
 lemma enclosed_spec:
   assumes enclosed: "enclosed a' si' a si"
       and x_in: "x \<in> region_addresses a' si'"
     shows "x \<in> region_addresses a si"
 proof -
   from x_in have "unat (x - a') < si'"
     using region_addresses_iff by blast
   with enclosed have "unat (x - a) < si"
     unfolding enclosed_def by (auto simp add: unat_sub_if' split: if_split_asm)
   then show ?thesis
     using region_addresses_iff by blast
 qed
 
 lemma address_in_enclosed_region_as_linarith:
   assumes "enclosed a' si' a si"
       and "x \<in> region_addresses a' si'"
     shows "a \<le> x \<and> a' \<le> x \<and> x < a' + of_nat si' \<and> x < a + of_nat si"
   using assms
   by (auto simp add: enclosed_def region_addresses_def word_le_nat_alt word_less_nat_alt unat_of_nat unat_word_ariths unat_sub_if' take_bit_eq_mod)
 
 
 lemma address_of_enclosed_region_ge:
   assumes "enclosed a' si' a si"
     shows "a' \<ge> a"
   using assms word_le_nat_alt
   by (auto simp add: enclosed_def)
 
 lemma address_in_enclosed_region:
   assumes "enclosed a' si' a si"
       and "x \<in> region_addresses a' si'"
     shows "unat (x - a) \<ge> unat (a' - a) \<and> unat (a' - a) + si' > unat (x - a) \<and> unat (x - a) < si"
   by (smt (z3) address_in_enclosed_region_as_linarith add_diff_cancel_left' address_of_enclosed_region_ge assms(1) assms(2) diff_diff_add enclosed_spec le_iff_add nat_add_left_cancel_less region_addresses_iff unat_sub_if' word_le_minus_mono_left word_unat.Rep_inverse word_unat_less_le)
 
 lemma enclosed_minus_minus:
   fixes a :: "'a word"
   assumes "offset \<ge> offset'"
       and "unat offset - si \<le> unat offset' - si'"
       and "unat offset' \<ge> si'"
       and "unat offset \<ge> si"
       and "a \<ge> offset"
     shows "enclosed (a - offset') si' (a - offset) si"
 proof-
   have "unat offset' \<le> unat a"
     using assms(1,5)
     by unat_arith
   thus ?thesis
     using assms
     apply (auto simp add: enclosed_def unat_sub_if_size word_size)
     apply unat_arith
     using diff_le_mono2[of "unat offset - si" "unat offset' - si'" "unat a"]
     apply (auto simp add: enclosed_def unat_sub_if_size word_size)
      by unat_arith+
 qed
 
 lemma enclosed_plus:
   fixes a :: "'a word"
   assumes "si' < si"
       and "unat a + si < 2^LENGTH('a)"
     shows "enclosed a si' a si"
   using assms
   by (auto simp add: enclosed_def)
 
 lemma separate_symm: "separate a si a' si' = separate a' si' a si"
   by (metis inf.commute separate_def)
 
 lemma separate_iff: "separate a si a' si' \<longleftrightarrow> si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
 proof
   assume assm: "separate a si a' si'"
   have "unat (a' - a) \<ge> si" if "separate a si a' si'" for a si a' si'
   proof (rule ccontr)
     assume "\<not> unat (a' - a) \<ge> si"
     then have "a' \<in> region_addresses a si"
       by (simp add: region_addresses_iff)
     moreover from that have "a' \<in> region_addresses a' si'"
       using region_addresses_iff separate_def by auto
     ultimately have "\<not>separate a si a' si'"
       by (meson disjoint_iff separate_def)
     with that show False
       by blast
   qed
   with assm have "unat (a' - a) \<ge> si" and "unat (a - a') \<ge> si'"
     using separate_symm by auto
   with assm show "si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
     using separate_def by auto
 next
   assume assm: "si > 0 \<and> si' > 0 \<and> unat (a' - a) \<ge> si \<and> unat (a - a') \<ge> si'"
   then have "unat (x - a') \<ge> si'" if "unat (x - a) < si" for x
     using that apply (auto simp add: unat_sub_if' split: if_split_asm)
      apply (meson Nat.le_diff_conv2 add_increasing le_less_trans less_imp_le_nat unsigned_greater_eq unsigned_less)
     by (smt (z3) Nat.le_diff_conv2 add_leD2 le_less_trans linorder_not_less nat_le_linear unat_lt2p)
   then have "region_addresses a si \<inter> region_addresses a' si' = {}"
     by (simp add: region_addresses_iff disjoint_iff leD)
   with assm show "separate a si a' si'"
     by (simp add: separate_def)
 qed
 
 lemma separate_as_linarith:
 assumes "\<not>region_overflow a si"
     and "\<not>region_overflow a' si'"
   shows "separate a si a' si' \<longleftrightarrow> 0 < si \<and> 0 < si' \<and> (a + of_nat si \<le> a' \<or> a' + of_nat si' \<le> a)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs then show ?rhs
    by (meson separate_iff le_less le_plus not_le_imp_less word_of_nat_le)
 next
   have *: "separate a si a' si'"
     if "si > 0" and "si' > 0" and "a + of_nat si \<le> a'"
       and "\<not>region_overflow a si" and "\<not>region_overflow a' si'"
     for a si a' si'
   proof -
     from that have "unat a + si < 2^LENGTH('a)" and "unat a' + si' < 2^LENGTH('a)"
       by (meson not_le region_overflow_def)+
     have "x < a + of_nat si" if "x \<in> region_addresses a si" for x
       by (smt (z3) Abs_fnat_hom_add \<open>unat a + si < 2 ^ LENGTH('a)\<close> add.commute dual_order.trans le_add1 less_diff_conv2 not_less region_addresses_iff that unat_of_nat_len unat_sub_if' word_less_iff_unsigned word_unat.Rep_inverse)
     moreover have "x \<ge> a'" if "x \<in> region_addresses a' si'" for x
       using address_in_enclosed_region_as_linarith enclosed_def \<open>unat a' + si' < 2 ^ LENGTH('a)\<close> that by blast
     ultimately show ?thesis
       using separate_def that by fastforce
   qed
   assume ?rhs then show ?lhs
     by (meson "*" assms separate_symm)
 qed
 
 text \<open>Compute separation in case the addresses and sizes are immediate values.\<close>
 lemmas separate_as_linarith_numeral [simp] =
   separate_as_linarith [of "numeral a::'a word" "numeral si" "numeral a'::'a word" "numeral si'"] for a si a' si'
 lemmas separate_as_linarith_numeral_1 [simp] =
   separate_as_linarith [of "numeral a::'a word" "numeral si" "numeral a'::'a word" "Suc 0"] for a si a'
 lemmas separate_as_linarith_numeral1_ [simp] =
   separate_as_linarith [of "numeral a::'a word" "Suc 0" "numeral a'::'a word" "numeral si'"] for a a' si'
 lemmas separate_as_linarith_numeral11 [simp] =
   separate_as_linarith [of "numeral a::'a word" "Suc 0" "numeral a'::'a word" "Suc 0"] for a a'
 lemmas region_overflow_numeral[simp] =
   region_overflow_def [of "numeral a::'a word" "numeral si"] for a si
 lemmas region_overflow_numeral1[simp] =
   region_overflow_def [of "numeral a::'a word" "Suc 0"] for a
 
 
 lemma separate_plus_none:
   assumes "si' \<le> unat offset"
       and "0 < si"
       and "0 < si'"
       and "unat offset + si \<le> 2^LENGTH('a)"
     shows "separate (offset + a) si a si'"
   using assms apply (auto simp add: separate_iff)
   by (smt (z3) Nat.diff_diff_right add.commute add_leD1 diff_0 diff_is_0_eq diff_zero not_gr_zero unat_sub_if' unsigned_0)
 
 lemmas unat_minus = unat_sub_if'[of 0,simplified]
 
 lemma separate_minus_minus':
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "unat offset' \<ge> si'"
       and "unat offset - si \<ge> unat offset'"
     shows "separate (a - offset) si (a - offset') si'"
   using assms apply (auto simp add: separate_iff)
    apply (metis Nat.le_diff_conv2 add.commute add_leD2 unat_sub_if')
   by (smt (z3) add.commute add_diff_cancel_right' diff_add_cancel diff_le_self diff_less less_le_trans nat_le_linear not_le unat_sub_if')
 
 lemma separate_minus_minus:
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "unat offset' \<ge> si'"
       and "unat offset - si \<ge> unat offset' \<or> unat offset' - si' \<ge> unat offset"
     shows "separate (a - offset) si (a - offset') si'"
   by (meson assms separate_minus_minus' separate_symm)
 
 lemma separate_minus_none:
   assumes "si \<noteq> 0"
       and "si' \<noteq> 0"
       and "unat offset \<ge> si"
       and "si' \<le> 2^LENGTH('a) - unat offset"
     shows "separate (a - offset) si a si'"
 proof -
   have "0 < si" and "0 < si'"
     using assms(1,2) by blast+
   moreover have "\<not> offset \<le> 0"
     using assms(1) assms(3) by fastforce
   ultimately show ?thesis
     by (smt (z3) add_diff_cancel_left' assms(3,4) diff_diff_eq2 diff_zero le_add_diff_inverse less_or_eq_imp_le separate_iff unat_sub_if' unsigned_0 unsigned_less word_less_eq_iff_unsigned)
 qed
 
 
 text \<open>The following theorems are used during symbolic execution to determine whether two regions are separate.\<close>
 
 lemmas separate_simps = separate_plus_none separate_minus_none separate_minus_minus
 
 end
 end
\ No newline at end of file