Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name.

Signed-off-by: Achim D. Brucker <adbrucker@0x5f.org>

ROOTS

@@ -11,7 +11,7 @@ lib/Basics
 lib/Eisbach_Tools
 lib/ML_Utils
 lib/Monads
-lib/Word_Lib
+lib/Word_Lib_l4v
 lib/sep_algebra
 lib/EVTutorial
 docs

lib/Basics/CLib.thy

@@ -6,7 +6,7 @@
  *)
 
 theory CLib
-  imports Word_Lib.Many_More
+  imports Word_Lib_l4v.Many_More
 begin
 
 lemma nat_diff_less:

lib/Basics/README.md

@@ -9,7 +9,7 @@ This session contains basic library theories that are needed in other sessions
 of this repository, such as [Monads] or [CParser], but that we do not want to
 put into these sessions to avoid circular session dependencies.
 
-Dependencies on `Word_Lib` and the Isabelle distribution (e.g. `HOL-Libary`) are
+Dependencies on `Word_Lib_l4v` and the Isabelle distribution (e.g. `HOL-Libary`) are
 fine, but avoid introducing any further session dependencies.
 
 [Monads]: ../Monads/

lib/Basics/ROOT

@@ -6,7 +6,7 @@
 
 chapter Lib
 
-session Basics (lib) = Word_Lib +
+session Basics (lib) = Word_Lib_l4v +
 
   theories
     CLib

lib/Lib.thy

@@ -22,7 +22,7 @@ imports
   Monads.Monad_Lib
   Basics.CLib
   NICTATools
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
 begin
 
 (* FIXME: eliminate *)

lib/More_Numeral_Type.thy

@@ -5,7 +5,7 @@
  *)
 
 theory More_Numeral_Type
-  imports "Word_Lib.WordSetup"
+  imports "Word_Lib_l4v.WordSetup"
 begin
 
 (* This theory provides additional setup for numeral types, which should probably go into

lib/NonDetMonadLemmaBucket.thy

@@ -18,7 +18,7 @@ imports
   Oblivious
   Injection_Handler
   Monads.Nondet_While_Loop_Rules_Completeness
-  "Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
+  "Word_Lib_l4v.Distinct_Prop" (* for distinct_tuple_helper *)
   Monads.Reader_Option_VCG
 begin
 

lib/ROOT

@@ -6,7 +6,7 @@
 
 chapter Lib
 
-session Lib (lib) = Word_Lib +
+session Lib (lib) = Word_Lib_l4v +
   sessions
     "HOL-Library"
     Basics

lib/Word_Lib_l4v/AARCH64/WordSetup.thy

@@ -5,7 +5,7 @@
  *)
 
 
-theory WordSetup (* part of non-AFP Word_Lib *)
+theory WordSetup (* part of non-AFP Word_Lib_l4v *)
 imports
   Word_Lemmas_64_Internal
   Distinct_Prop

lib/Word_Lib_l4v/ARM/WordSetup.thy

@@ -5,7 +5,7 @@
  *)
 
 
-theory WordSetup (* part of non-AFP Word_Lib *)
+theory WordSetup (* part of non-AFP Word_Lib_l4v *)
 imports
   Word_Lemmas_32_Internal
   Distinct_Prop

lib/Word_Lib_l4v/ARM_HYP/WordSetup.thy

@@ -5,7 +5,7 @@
  *)
 
 
-theory WordSetup (* part of non-AFP Word_Lib *)
+theory WordSetup (* part of non-AFP Word_Lib_l4v *)
 imports
   Word_Lemmas_32_Internal
   Distinct_Prop

lib/Word_Lib_l4v/Bits_Int.thy

@@ -8,10 +8,10 @@ section \<open>Bitwise Operations on integers\<close>
 
 theory Bits_Int
   imports
-    "Word_Lib.Most_significant_bit"
+    "Word_Lib_l4v.Most_significant_bit"
-    "Word_Lib.Least_significant_bit"
+    "Word_Lib_l4v.Least_significant_bit"
-    "Word_Lib.Generic_set_bit"
+    "Word_Lib_l4v.Generic_set_bit"
-    "Word_Lib.Bit_Comprehension"
+    "Word_Lib_l4v.Bit_Comprehension"
 begin
 
 subsection \<open>Implicit bit representation of \<^typ>\<open>int\<close>\<close>

lib/Word_Lib_l4v/Distinct_Prop.thy

@@ -6,7 +6,7 @@
 
 section "Distinct Proposition"
 
-theory Distinct_Prop  (* part of non-AFP Word_Lib *)
+theory Distinct_Prop  (* part of non-AFP Word_Lib_l4v *)
 imports
   Many_More
   "HOL-Library.Prefix_Order"

lib/Word_Lib_l4v/Guide.thy

@@ -198,35 +198,35 @@ text \<open>
 
     \<^descr>[Syntax]
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Syntax_Bundles\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Syntax_Bundles\<close>]
         Bundles to provide alternative syntax for various bit operations.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Hex_Words\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Hex_Words\<close>]
         Printing word numerals as hexadecimal numerals.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Type_Syntax\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Type_Syntax\<close>]
         Pretty type-sensitive syntax for cast operations.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_Syntax\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Syntax\<close>]
         Specific ASCII syntax for prominent bit operations on word.
 
     \<^descr>[Proof tools]
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Norm_Words\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Norm_Words\<close>]
         Rewriting word numerals to normal forms.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Bitwise\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Bitwise\<close>]
         Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Bitwise_Signed\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Bitwise_Signed\<close>]
         Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_EqI\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_EqI\<close>]
         Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.
 
     \<^descr>[Operations]
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Signed_Division_Word\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Signed_Division_Word\<close>]
 
         Signed division on word:
 
@@ -234,16 +234,16 @@ text \<open>
 
           \<^item> @{term [source] \<open>(smod) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Aligned\<close>] \
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Aligned\<close>] \
 
           \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Least_significant_bit\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Least_significant_bit\<close>]
 
         The least significant bit as an alias:
         @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Most_significant_bit\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Most_significant_bit\<close>]
 
         The most significant bit:
 
@@ -255,7 +255,7 @@ text \<open>
 
           \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Bit_Shifts_Infix_Syntax\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Bit_Shifts_Infix_Syntax\<close>]
 
         Bit shifts decorated with infix syntax:
 
@@ -265,57 +265,57 @@ text \<open>
 
           \<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Next_and_Prev\<close>] \
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Next_and_Prev\<close>] \
 
           \<^item> @{thm word_next_unfold [no_vars]}
 
           \<^item> @{thm word_prev_unfold [no_vars]}
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Enumeration_Word\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Enumeration_Word\<close>]
 
         More on explicit enumeration of word types.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.More_Word_Operations\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.More_Word_Operations\<close>]
 
         Even more operations on word.
 
     \<^descr>[Types]
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Signed_Words\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Signed_Words\<close>]
 
           Formal tagging of word types with a \<^text>\<open>signed\<close> marker.
 
     \<^descr>[Lemmas]
 
-      \<^descr>[\<^theory>\<open>Word_Lib.More_Word\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.More_Word\<close>]
 
           More lemmas on words.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Lemmas\<close>]
 
           More lemmas on words, covering many other theories mentioned here.
 
     \<^descr>[Words of popular lengths].
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_8\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_8\<close>]
 
           for 8-bit words.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_16\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_16\<close>]
 
           for 16-bit words.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_32\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_32\<close>]
 
           for 32-bit words.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Word_64\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_64\<close>]
 
           for 64-bit words. This theory is not part of  \<^text>\<open>Word_Lib_Sumo\<close>, because it shadows
-          names from \<^theory>\<open>Word_Lib.Word_32\<close>. They can be used together, but then will have
+          names from \<^theory>\<open>Word_Lib_l4v.Word_32\<close>. They can be used together, but then will have
           to use qualified names in applications.
 
-      \<^descr>[\<^theory>\<open>Word_Lib.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib.Machine_Word_64\<close>]
+      \<^descr>[\<^theory>\<open>Word_Lib_l4v.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib_l4v.Machine_Word_64\<close>]
 
           provide lemmas for 32-bit words and 64-bit words under the same name,
           which can help to organize applications relying on some form
@@ -343,36 +343,36 @@ text \<open>
   from those theories.  However theorem coverage may still
   be terse in some cases.
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Lib_Sumo\<close>]
 
     An entry point importing any relevant theory in that session.  Intended
     for backward compatibility: start importing this theory when
     migrating applications to Isabelle2021, and later sort out
     what you really need. You may need to include
-   \<^theory>\<open>Word_Lib.Word_64\<close> separately.
+   \<^theory>\<open>Word_Lib_l4v.Word_64\<close> separately.
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Generic_set_bit\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Generic_set_bit\<close>]
 
     Kind of an alias: @{thm set_bit_eq [no_vars]}
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Typedef_Morphisms\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Typedef_Morphisms\<close>]
 
     A low-level extension to HOL typedef providing
     conversions along type morphisms.  The @{method transfer} method
     seems to be sufficient for most applications though.
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.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.
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Bit_Comprehension_Int\<close>]
 
     Comprehension syntax for bit values over predicates
     \<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>int\<close>; inherently non-computational.
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Reversed_Bit_Lists\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Reversed_Bit_Lists\<close>]
 
     Representation of bit values as explicit list in
     \<^emph>\<open>reversed\<close> order.
@@ -383,11 +383,11 @@ text \<open>
 
     @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 
-  \<^descr>[\<^theory>\<open>Word_Lib.Many_More\<close>]
+  \<^descr>[\<^theory>\<open>Word_Lib_l4v.Many_More\<close>]
 
     Collection of operations and theorems which are kept for backward
-    compatibility and not used in other theories in session \<^text>\<open>Word_Lib\<close>.
+    compatibility and not used in other theories in session \<^text>\<open>Word_Lib_l4v\<close>.
-    They are used in applications of \<^text>\<open>Word_Lib\<close>, but should be migrated to there.
+    They are used in applications of \<^text>\<open>Word_Lib_l4v\<close>, but should be migrated to there.
 \<close>
 
 section \<open>Changelog\<close>
@@ -395,31 +395,31 @@ section \<open>Changelog\<close>
 text \<open>
   \<^descr>[Changes since AFP 2022] ~
 
-    \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> has been removed from session.
+    \<^item> Theory \<^text>\<open>Word_Lib_l4v.Ancient_Numeral\<close> has been removed from session.
 
     \<^item> Bit comprehension syntax for \<^typ>\<open>int\<close> moved to separate theory
-      \<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>.
+      \<^theory>\<open>Word_Lib_l4v.Bit_Comprehension_Int\<close>.
 
   \<^descr>[Changes since AFP 2021] ~
 
-    \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
+    \<^item> Theory \<^text>\<open>Word_Lib_l4v.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib_l4v.Word_Lib_Sumo\<close>
       any longer.
 
     \<^item> Infix syntax for \<^term>\<open>(AND)\<close>, \<^term>\<open>(OR)\<close>, \<^term>\<open>(XOR)\<close> organized in
       syntax bundle \<^bundle>\<open>bit_operations_syntax\<close>.
 
     \<^item> Abbreviation \<^abbrev>\<open>max_word\<close> moved from distribution into theory
-      \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
+      \<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close>.
 
     \<^item> Operation \<^const>\<open>test_bit\<close> replaced by input abbreviation \<^abbrev>\<open>test_bit\<close>.
 
     \<^item> Abbreviations \<^abbrev>\<open>bin_nth\<close>, \<^abbrev>\<open>bin_last\<close>, \<^abbrev>\<open>bin_rest\<close>,
       \<^abbrev>\<open>bintrunc\<close>, \<^abbrev>\<open>sbintrunc\<close>, \<^abbrev>\<open>norm_sint\<close>,
-      \<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
+      \<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close>.
 
     \<^item> Operations \<^abbrev>\<open>bshiftr1\<close>,
       \<^abbrev>\<open>setBit\<close>, \<^abbrev>\<open>clearBit\<close> moved from distribution into theory
-      \<^theory>\<open>Word_Lib.Legacy_Aliases\<close> and replaced by input abbreviations.
+      \<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close> and replaced by input abbreviations.
 
     \<^item> Operations \<^const>\<open>shiftl1\<close>, \<^const>\<open>shiftr1\<close>, \<^const>\<open>sshiftr1\<close>
       moved here from distribution.

lib/Word_Lib_l4v/RISCV64/WordSetup.thy

@@ -5,7 +5,7 @@
  *)
 
 
-theory WordSetup (* part of non-AFP Word_Lib *)
+theory WordSetup (* part of non-AFP Word_Lib_l4v *)
 imports
   Word_Lemmas_64_Internal
   Distinct_Prop

lib/Word_Lib_l4v/ROOT

@@ -6,8 +6,8 @@
 
 chapter Lib
 
-session Word_Lib (lib) = HOL +
+session Word_Lib_l4v (lib) = HOL +
-  options [timeout = 300, document=pdf]
+  options [timeout = 900, document=pdf]
   sessions
     "HOL-Library"
     "HOL-Eisbach"

lib/Word_Lib_l4v/Word_Lemmas_Internal.thy

@@ -48,12 +48,12 @@ lemma signed_ge_zero_scast_eq_ucast:
  "0 <=s x \<Longrightarrow> scast x = ucast x"
   by (simp add: scast_eq_ucast word_sle_msb_le)
 
-(* FIXME: move out of Word_Lib *)
+(* FIXME: move out of Word_Lib_l4v *)
 lemma disjCI2:
   "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q"
   by blast
 
-(* FIXME: move out of Word_Lib *)
+(* FIXME: move out of Word_Lib_l4v *)
 lemma nat_diff_diff_le_lhs:
   "a + c - b \<le> d \<Longrightarrow> a - (b - c) \<le> (d :: nat)"
   by arith
@@ -664,7 +664,7 @@ lemma FF_eq_minus_1:
 lemmas shiftl_t2n' = shiftl_eq_mult[where x="w::'a::len word" for w]
 
 
-(* candidates for moving to AFP Word_Lib: *)
+(* candidates for moving to AFP Word_Lib_l4v: *)
 
 lemma word_mask_shift_eqI:
   "\<lbrakk> x && mask n = y && mask n; x >> n = y >> n \<rbrakk> \<Longrightarrow> x = y"

lib/Word_Lib_l4v/X64/WordSetup.thy

@@ -5,7 +5,7 @@
  *)
 
 
-theory WordSetup (* part of non-AFP Word_Lib *)
+theory WordSetup (* part of non-AFP Word_Lib_l4v *)
 imports
   Word_Lemmas_64_Internal
   Distinct_Prop

lib/sep_algebra/ROOT

@@ -6,7 +6,7 @@
 
 chapter Lib
 
-session Sep_Algebra (lib) = Word_Lib +
+session Sep_Algebra (lib) = Word_Lib_l4v +
   sessions
     "HOL-Eisbach"
     "HOL-Hoare"

misc/regression/tests.xml

@@ -53,7 +53,7 @@
 
   <!-- Build Isabelle and common theories (Pure, HOL, Word). -->
   <sequence>
-    <test name="isabelle" cwd="../.." cpu-timeout="3600">isabelle/bin/isabelle build -d . -vb Word_Lib</test>
+    <test name="isabelle" cwd="../.." cpu-timeout="3600">isabelle/bin/isabelle build -d . -vb Word_Lib_l4v</test>
   </sequence>
 
     <!-- Ensure that all of our XML files are strictly correct. -->

proof/crefine/ARM_HYP/ArchMove_C.thy

@@ -250,7 +250,7 @@ lemma is_aligned_ptrFromPAddr_pageBitsForSize:
   "is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (ptrFromPAddr p) (pageBitsForSize sz)"
   by (cases sz ; simp add: is_aligned_ptrFromPAddr_n pageBits_def)
 
-(* FIXME: generalise, move to Word_Lib, and/or rewrite using
+(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using
    'leq_high_bits_shiftr_low_bits_leq_bits' *)
 lemma le_mask_asid_bits_helper:
   "x \<le> 2 ^ asid_high_bits - 1 \<Longrightarrow> (x::word32) << asid_low_bits \<le> mask asid_bits"
@@ -271,7 +271,7 @@ lemma is_aligned_pageBitsForSize_minimum:
   apply (erule is_aligned_weaken, simp)+
   done
 
-(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'shift_then_mask_eq_shift_low_bits' *)
+(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using 'shift_then_mask_eq_shift_low_bits' *)
 lemma shiftr_asid_low_bits_mask_asid_high_bits:
   "(asid :: word32) \<le> mask asid_bits
       \<Longrightarrow> (asid >> asid_low_bits) && mask asid_high_bits = asid >> asid_low_bits"
@@ -288,7 +288,7 @@ lemma ucast_asid_high_bits_is_shift:
   unfolding asid_bits_def asid_low_bits_def asid_high_bits_of_def
   by (rule ucast_ucast_eq_mask_shift, simp)
 
-(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'leq_low_bits_iff_zero' *)
+(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using 'leq_low_bits_iff_zero' *)
 lemma shiftr_asid_low_bits_mask_eq_0:
   "\<lbrakk> (asid :: word32) \<le> mask asid_bits; asid >> asid_low_bits = 0 \<rbrakk>
         \<Longrightarrow> (asid && mask asid_low_bits = 0) = (asid = 0)"

proof/crefine/Move_C.thy

@@ -174,7 +174,7 @@ lemma to_bool_if:
   "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
   by (auto simp: to_bool_def)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma word_upcast_shiftr:
   assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
   shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
@@ -187,12 +187,12 @@ lemma word_upcast_neg_msb:
   unfolding ucast_def msb_word_of_int
   by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma word_upcast_0_sle:
   "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
   by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma scast_ucast_up_eq_ucast:
   assumes "LENGTH('a::len) < LENGTH('b::len)"
   shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
@@ -361,7 +361,7 @@ lemma shiftr_and_eq_shiftl:
     thus ?thesis using word_eq_iff by blast
   qed
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma sign_extend_0[simp]:
   "sign_extend a 0 = 0"
   by (simp add: sign_extend_def)
@@ -382,7 +382,7 @@ lemma name_seq_bound_helper:
   apply (rule ccontr, simp add: linorder_not_le)
   done
 
-(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib? *)
+(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib_l4v? *)
 lemma reset_name_seq_bound_helper:
   fixes sz
   fixes v :: "('a :: len) word"
@@ -1318,7 +1318,7 @@ lemma word_ctz_0[simp]:
   "word_ctz (0::64 word) = 64"
   by (clarsimp simp: word_ctz_def to_bl_def)+
 
-(* FIXME move to Word_Lib *)
+(* FIXME move to Word_Lib_l4v *)
 lemma unat_trans_ucast_helper:
   "\<lbrakk> unat x < n ; n \<le> Suc 0 \<rbrakk> \<Longrightarrow> ucast x = 0"
   by (simp add: le_Suc_eq unsigned_eq_0_iff)

proof/drefine/Intent_DR.thy

@@ -1456,7 +1456,7 @@ lemma mask_inj_if:
   "\<lbrakk>a && mask n = a; b && mask n = b; a && mask n = b && mask n\<rbrakk>\<Longrightarrow> a = b"
   by (rule box_equals)
 
-(* FIXME: move to Word_Lib, generalise *)
+(* FIXME: move to Word_Lib_l4v, generalise *)
 lemma bound_preserve_mask:
   "\<lbrakk> is_aligned (x::word32) n; x\<le> mask k; (z::word32)\<le> mask n; n < 32; k < 32; n \<le> k \<rbrakk> \<Longrightarrow>
    x+z \<le> mask k"

proof/infoflow/refine/ARM/Example_Valid_StateH.thy

@@ -526,7 +526,7 @@ lemma pt_offs_range_correct:
   "x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> \<exists>y. x = High_pt_ptr + (ucast (y:: 8 word) << 2)"
   by (simp_all add: pt_offs_range_correct' s0_ptrs_aligned)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma bl_to_bin_le2p_aux:
   "bl_to_bin_aux bs w \<le> (w + 1) * (2 ^ length bs) - 1"
   apply (induct bs arbitrary: w)
@@ -536,7 +536,7 @@ lemma bl_to_bin_le2p_aux:
   apply (drule meta_spec, erule xtr8 [rotated], simp)+
   done
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma bl_to_bin_le2p: "bl_to_bin bs \<le> (2 ^ length bs) - 1"
   apply (unfold bl_to_bin_def)
   apply (rule xtr3)
@@ -545,7 +545,7 @@ lemma bl_to_bin_le2p: "bl_to_bin bs \<le> (2 ^ length bs) - 1"
   apply simp
   done
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma of_bl_length_le:
   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) \<le> 2 ^ k - 1"
   by (simp add: of_bl_length_less)
@@ -606,11 +606,11 @@ lemma cnode_offs_in_range:
   "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<in> cnode_offs_range Silc_cnode_ptr"
   by (simp_all add: cnode_offs_in_range' s0_ptrs_aligned)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma le_mask_eq: "x \<le> 2 ^ n - 1 \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
   by (metis and_mask_eq_iff_le_mask mask_2pm1)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma word_div_mult':
   fixes c :: "'a::len word"
   shows "\<lbrakk>0 < c; a \<le> b * c \<rbrakk> \<Longrightarrow> a div c \<le> b"

proof/invariant-abstract/VSpacePre_AI.thy

@@ -64,7 +64,7 @@ lemma invs_valid_irq_states[elim!]:
   "invs s \<Longrightarrow> valid_irq_states s"
   by(auto simp: invs_def valid_state_def)
 
-(* FIXME: move to Word_Lib *)
+(* FIXME: move to Word_Lib_l4v *)
 lemma uint_ucast:
   "(x :: 'a :: len word) < 2 ^ LENGTH('b) \<Longrightarrow> uint (ucast x :: 'b :: len word) = uint x"
   by (metis Word.of_nat_unat mod_less of_nat_numeral semiring_1_class.of_nat_power unat_less_helper

spec/ROOT

@@ -27,7 +27,7 @@ chapter "Specifications"
  *)
 
 (* Session on which most other sessions build. *)
-session ASpec in "abstract" = Word_Lib +
+session ASpec in "abstract" = Word_Lib_l4v +
   options [document=pdf]
   sessions
     "HOL-Library"
@@ -61,7 +61,7 @@ session ASpec in "abstract" = Word_Lib +
  * Executable/Design Specification
  *)
 
-session ExecSpec in "design" = Word_Lib +
+session ExecSpec in "design" = Word_Lib_l4v +
   options [document = false]
   sessions
     Lib
@@ -106,7 +106,7 @@ session CKernel in "cspec/$L4V_ARCH" = CParser +
  * CapDL
  *)
 
-session DSpec in capDL = Word_Lib +
+session DSpec in capDL = Word_Lib_l4v +
   sessions
     ExecSpec
     ASpec
@@ -119,7 +119,7 @@ session DSpec in capDL = Word_Lib +
  * Take-Grant.
  *)
 
-session TakeGrant in "take-grant" = Word_Lib +
+session TakeGrant in "take-grant" = Word_Lib_l4v +
   theories
     "System_S"
     "Isolation_S"

spec/capDL/Intents_D.thy

@@ -24,7 +24,7 @@
 
 theory Intents_D
 imports
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "ASpec.CapRights_A"
 begin
 

spec/cspec/KernelState_C.thy

@@ -6,7 +6,7 @@
 
 theory KernelState_C
 imports
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "CLib.BitFieldProofsLib"
   "Substitute"
 begin

spec/cspec/c/gen-config-thy.py

@@ -246,7 +246,7 @@ theory_header = """(*
 chapter "Kernel Configuration"
 
 theory Kernel_Config
-imports Word_Lib.WordSetup
+imports Word_Lib_l4v.WordSetup
 begin
 
 (*

spec/design/m-skel/AARCH64/MachineTypes.thy

@@ -7,6 +7,7 @@ chapter "AARCH64 Machine Types"
 
 theory MachineTypes
 imports
+  Word_Lib_l4v.WordSetup
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_No_Fail

spec/design/m-skel/ARM/MachineTypes.thy

@@ -8,6 +8,7 @@ chapter "ARM Machine Types"
 
 theory MachineTypes
 imports
+  Word_Lib_l4v.WordSetup
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_No_Fail

spec/design/m-skel/ARM_HYP/MachineTypes.thy

@@ -8,7 +8,7 @@ chapter \<open>ARM\_HYP Machine Types\<close>
 
 theory MachineTypes
 imports
-  Word_Lib.WordSetup
+  Word_Lib_l4v.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_No_Fail
   Monads.Reader_Option_ND

spec/design/m-skel/RISCV64/MachineTypes.thy

@@ -8,7 +8,7 @@ chapter "RISCV 64bit Machine Types"
 
 theory MachineTypes
 imports
-  Word_Lib.WordSetup
+  Word_Lib_l4v.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_No_Fail
   Monads.Reader_Option_ND

spec/design/m-skel/X64/MachineTypes.thy

@@ -8,6 +8,7 @@ chapter "x86-64bit Machine Types"
 
 theory MachineTypes
 imports
+  Word_Lib_l4v.WordSetup
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_No_Fail

spec/design/skel/AARCH64/ArchInvocationLabels_H.thy

@@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
 imports
-  "Word_Lib.Enumeration"
+  "Word_Lib_l4v.Enumeration"
   Setup_Locale
 begin
 context Arch begin global_naming AARCH64_H

spec/design/skel/ARM/ArchInvocationLabels_H.thy

@@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
 imports
-    "Word_Lib.Enumeration"
+    "Word_Lib_l4v.Enumeration"
     Setup_Locale
 begin
 context Arch begin global_naming ARM_H

spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy

@@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
 imports
-    "Word_Lib.Enumeration"
+    "Word_Lib_l4v.Enumeration"
     Setup_Locale
 begin
 context Arch begin global_naming ARM_HYP_H

spec/design/skel/RISCV64/ArchInvocationLabels_H.thy

@@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
 imports
-  "Word_Lib.Enumeration"
+  "Word_Lib_l4v.Enumeration"
   Setup_Locale
 begin
 context Arch begin global_naming RISCV64_H

spec/design/skel/X64/ArchInvocationLabels_H.thy

@@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
 
 theory ArchInvocationLabels_H
 imports
-  "Word_Lib.Enumeration"
+  "Word_Lib_l4v.Enumeration"
   Setup_Locale
 begin
 context Arch begin global_naming X64_H

spec/machine/AARCH64/MachineOps.thy

@@ -9,6 +9,7 @@ chapter "Machine Operations"
 
 theory MachineOps
 imports
+  Word_Lib_l4v.WordSetup
   Word_Lib.WordSetup
   Monads.Nondet_Monad
   MachineMonad

spec/machine/AARCH64/Platform.thy

@@ -9,7 +9,7 @@ chapter "Platform Definitions"
 theory Platform
 imports
   "Lib.Lib"
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "Lib.Defs"
   Setup_Locale
   Kernel_Config

spec/machine/ARM/Platform.thy

@@ -10,7 +10,7 @@ theory Platform
 imports
   "Lib.Defs"
   "Lib.Lib"
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   Setup_Locale
   Kernel_Config
 begin

spec/machine/ARM_HYP/Platform.thy

@@ -10,7 +10,7 @@ theory Platform
 imports
   "Lib.Defs"
   "Lib.Lib"
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   Setup_Locale
   Kernel_Config
 begin

spec/machine/RISCV64/MachineOps.thy

@@ -8,7 +8,7 @@ chapter "Machine Operations"
 
 theory MachineOps
 imports
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "Monads.Nondet_Monad"
   MachineMonad
 begin

spec/machine/RISCV64/Platform.thy

@@ -9,7 +9,7 @@ chapter "Platform Definitions"
 theory Platform
 imports
   "Lib.Lib"
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "Lib.Defs"
   Setup_Locale
   Kernel_Config

spec/machine/X64/MachineOps.thy

@@ -8,7 +8,7 @@ chapter "Machine Operations"
 
 theory MachineOps
 imports
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "Monads.Nondet_Monad"
   MachineMonad
 begin

spec/machine/X64/Platform.thy

@@ -9,7 +9,7 @@ chapter "Platform Definitions"
 theory Platform
 imports
   "Lib.Lib"
-  "Word_Lib.WordSetup"
+  "Word_Lib_l4v.WordSetup"
   "Lib.Defs"
   Setup_Locale
   Kernel_Config