diff --git a/ROOTS b/ROOTS index 3599f648b..6b9290a52 100644 --- a/ROOTS +++ b/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 diff --git a/lib/Basics/CLib.thy b/lib/Basics/CLib.thy index 67d0bc42f..3a10ae9bf 100644 --- a/lib/Basics/CLib.thy +++ b/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: diff --git a/lib/Basics/README.md b/lib/Basics/README.md index 6b952d50b..dc98a2779 100644 --- a/lib/Basics/README.md +++ b/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/ diff --git a/lib/Basics/ROOT b/lib/Basics/ROOT index add4bd49b..1b4b5d2f2 100644 --- a/lib/Basics/ROOT +++ b/lib/Basics/ROOT @@ -6,7 +6,7 @@ chapter Lib -session Basics (lib) = Word_Lib + +session Basics (lib) = Word_Lib_l4v + theories CLib \ No newline at end of file diff --git a/lib/Lib.thy b/lib/Lib.thy index 1374020d1..221f44f0c 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -22,7 +22,7 @@ imports Monads.Monad_Lib Basics.CLib NICTATools - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" begin (* FIXME: eliminate *) diff --git a/lib/More_Numeral_Type.thy b/lib/More_Numeral_Type.thy index fa5cb4a0f..62d152aed 100644 --- a/lib/More_Numeral_Type.thy +++ b/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 diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 7d0272dda..b8fe341bf 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/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 diff --git a/lib/ROOT b/lib/ROOT index 5a2970e13..6dfbf19e0 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -6,7 +6,7 @@ chapter Lib -session Lib (lib) = Word_Lib + +session Lib (lib) = Word_Lib_l4v + sessions "HOL-Library" Basics diff --git a/lib/Word_Lib/AARCH64/WordSetup.thy b/lib/Word_Lib_l4v/AARCH64/WordSetup.thy similarity index 96% rename from lib/Word_Lib/AARCH64/WordSetup.thy rename to lib/Word_Lib_l4v/AARCH64/WordSetup.thy index 75b7adb20..7e71e78ae 100644 --- a/lib/Word_Lib/AARCH64/WordSetup.thy +++ b/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 diff --git a/lib/Word_Lib/ARM/WordSetup.thy b/lib/Word_Lib_l4v/ARM/WordSetup.thy similarity index 96% rename from lib/Word_Lib/ARM/WordSetup.thy rename to lib/Word_Lib_l4v/ARM/WordSetup.thy index 96f166580..506254919 100644 --- a/lib/Word_Lib/ARM/WordSetup.thy +++ b/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 diff --git a/lib/Word_Lib/ARM_HYP/WordSetup.thy b/lib/Word_Lib_l4v/ARM_HYP/WordSetup.thy similarity index 96% rename from lib/Word_Lib/ARM_HYP/WordSetup.thy rename to lib/Word_Lib_l4v/ARM_HYP/WordSetup.thy index 96f166580..506254919 100644 --- a/lib/Word_Lib/ARM_HYP/WordSetup.thy +++ b/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 diff --git a/lib/Word_Lib/Aligned.thy b/lib/Word_Lib_l4v/Aligned.thy similarity index 100% rename from lib/Word_Lib/Aligned.thy rename to lib/Word_Lib_l4v/Aligned.thy diff --git a/lib/Word_Lib/Bit_Comprehension.thy b/lib/Word_Lib_l4v/Bit_Comprehension.thy similarity index 100% rename from lib/Word_Lib/Bit_Comprehension.thy rename to lib/Word_Lib_l4v/Bit_Comprehension.thy diff --git a/lib/Word_Lib/Bit_Comprehension_Int.thy b/lib/Word_Lib_l4v/Bit_Comprehension_Int.thy similarity index 100% rename from lib/Word_Lib/Bit_Comprehension_Int.thy rename to lib/Word_Lib_l4v/Bit_Comprehension_Int.thy diff --git a/lib/Word_Lib/Bit_Shifts_Infix_Syntax.thy b/lib/Word_Lib_l4v/Bit_Shifts_Infix_Syntax.thy similarity index 100% rename from lib/Word_Lib/Bit_Shifts_Infix_Syntax.thy rename to lib/Word_Lib_l4v/Bit_Shifts_Infix_Syntax.thy diff --git a/lib/Word_Lib/Bits_Int.thy b/lib/Word_Lib_l4v/Bits_Int.thy similarity index 99% rename from lib/Word_Lib/Bits_Int.thy rename to lib/Word_Lib_l4v/Bits_Int.thy index 2587cfbf7..b5f3f921b 100644 --- a/lib/Word_Lib/Bits_Int.thy +++ b/lib/Word_Lib_l4v/Bits_Int.thy @@ -8,10 +8,10 @@ section \Bitwise Operations on integers\ theory Bits_Int imports - "Word_Lib.Most_significant_bit" - "Word_Lib.Least_significant_bit" - "Word_Lib.Generic_set_bit" - "Word_Lib.Bit_Comprehension" + "Word_Lib_l4v.Most_significant_bit" + "Word_Lib_l4v.Least_significant_bit" + "Word_Lib_l4v.Generic_set_bit" + "Word_Lib_l4v.Bit_Comprehension" begin subsection \Implicit bit representation of \<^typ>\int\\ diff --git a/lib/Word_Lib/Bitwise.thy b/lib/Word_Lib_l4v/Bitwise.thy similarity index 100% rename from lib/Word_Lib/Bitwise.thy rename to lib/Word_Lib_l4v/Bitwise.thy diff --git a/lib/Word_Lib/Bitwise_Signed.thy b/lib/Word_Lib_l4v/Bitwise_Signed.thy similarity index 100% rename from lib/Word_Lib/Bitwise_Signed.thy rename to lib/Word_Lib_l4v/Bitwise_Signed.thy diff --git a/lib/Word_Lib/Boolean_Inequalities.thy b/lib/Word_Lib_l4v/Boolean_Inequalities.thy similarity index 100% rename from lib/Word_Lib/Boolean_Inequalities.thy rename to lib/Word_Lib_l4v/Boolean_Inequalities.thy diff --git a/lib/Word_Lib/Distinct_Prop.thy b/lib/Word_Lib_l4v/Distinct_Prop.thy similarity index 99% rename from lib/Word_Lib/Distinct_Prop.thy rename to lib/Word_Lib_l4v/Distinct_Prop.thy index 00ad10481..1dc84fd56 100644 --- a/lib/Word_Lib/Distinct_Prop.thy +++ b/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" diff --git a/lib/Word_Lib/Enumeration.thy b/lib/Word_Lib_l4v/Enumeration.thy similarity index 100% rename from lib/Word_Lib/Enumeration.thy rename to lib/Word_Lib_l4v/Enumeration.thy diff --git a/lib/Word_Lib/Enumeration_Word.thy b/lib/Word_Lib_l4v/Enumeration_Word.thy similarity index 100% rename from lib/Word_Lib/Enumeration_Word.thy rename to lib/Word_Lib_l4v/Enumeration_Word.thy diff --git a/lib/Word_Lib/Even_More_List.thy b/lib/Word_Lib_l4v/Even_More_List.thy similarity index 100% rename from lib/Word_Lib/Even_More_List.thy rename to lib/Word_Lib_l4v/Even_More_List.thy diff --git a/lib/Word_Lib/Examples.thy b/lib/Word_Lib_l4v/Examples.thy similarity index 100% rename from lib/Word_Lib/Examples.thy rename to lib/Word_Lib_l4v/Examples.thy diff --git a/lib/Word_Lib/Generic_set_bit.thy b/lib/Word_Lib_l4v/Generic_set_bit.thy similarity index 100% rename from lib/Word_Lib/Generic_set_bit.thy rename to lib/Word_Lib_l4v/Generic_set_bit.thy diff --git a/lib/Word_Lib/Guide.thy b/lib/Word_Lib_l4v/Guide.thy similarity index 82% rename from lib/Word_Lib/Guide.thy rename to lib/Word_Lib_l4v/Guide.thy index f87ee74e7..84da6b9b4 100644 --- a/lib/Word_Lib/Guide.thy +++ b/lib/Word_Lib_l4v/Guide.thy @@ -198,35 +198,35 @@ text \ \<^descr>[Syntax] - \<^descr>[\<^theory>\Word_Lib.Syntax_Bundles\] + \<^descr>[\<^theory>\Word_Lib_l4v.Syntax_Bundles\] Bundles to provide alternative syntax for various bit operations. - \<^descr>[\<^theory>\Word_Lib.Hex_Words\] + \<^descr>[\<^theory>\Word_Lib_l4v.Hex_Words\] Printing word numerals as hexadecimal numerals. - \<^descr>[\<^theory>\Word_Lib.Type_Syntax\] + \<^descr>[\<^theory>\Word_Lib_l4v.Type_Syntax\] Pretty type-sensitive syntax for cast operations. - \<^descr>[\<^theory>\Word_Lib.Word_Syntax\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_Syntax\] Specific ASCII syntax for prominent bit operations on word. \<^descr>[Proof tools] - \<^descr>[\<^theory>\Word_Lib.Norm_Words\] + \<^descr>[\<^theory>\Word_Lib_l4v.Norm_Words\] Rewriting word numerals to normal forms. - \<^descr>[\<^theory>\Word_Lib.Bitwise\] + \<^descr>[\<^theory>\Word_Lib_l4v.Bitwise\] Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions. - \<^descr>[\<^theory>\Word_Lib.Bitwise_Signed\] + \<^descr>[\<^theory>\Word_Lib_l4v.Bitwise_Signed\] Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions. - \<^descr>[\<^theory>\Word_Lib.Word_EqI\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_EqI\] Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions. \<^descr>[Operations] - \<^descr>[\<^theory>\Word_Lib.Signed_Division_Word\] + \<^descr>[\<^theory>\Word_Lib_l4v.Signed_Division_Word\] Signed division on word: @@ -234,16 +234,16 @@ text \ \<^item> @{term [source] \(smod) :: 'a::len word \ 'a word \ 'a word\} - \<^descr>[\<^theory>\Word_Lib.Aligned\] \ + \<^descr>[\<^theory>\Word_Lib_l4v.Aligned\] \ \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]} - \<^descr>[\<^theory>\Word_Lib.Least_significant_bit\] + \<^descr>[\<^theory>\Word_Lib_l4v.Least_significant_bit\] The least significant bit as an alias: @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]} - \<^descr>[\<^theory>\Word_Lib.Most_significant_bit\] + \<^descr>[\<^theory>\Word_Lib_l4v.Most_significant_bit\] The most significant bit: @@ -255,7 +255,7 @@ text \ \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]} - \<^descr>[\<^theory>\Word_Lib.Bit_Shifts_Infix_Syntax\] + \<^descr>[\<^theory>\Word_Lib_l4v.Bit_Shifts_Infix_Syntax\] Bit shifts decorated with infix syntax: @@ -265,57 +265,57 @@ text \ \<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]} - \<^descr>[\<^theory>\Word_Lib.Next_and_Prev\] \ + \<^descr>[\<^theory>\Word_Lib_l4v.Next_and_Prev\] \ \<^item> @{thm word_next_unfold [no_vars]} \<^item> @{thm word_prev_unfold [no_vars]} - \<^descr>[\<^theory>\Word_Lib.Enumeration_Word\] + \<^descr>[\<^theory>\Word_Lib_l4v.Enumeration_Word\] More on explicit enumeration of word types. - \<^descr>[\<^theory>\Word_Lib.More_Word_Operations\] + \<^descr>[\<^theory>\Word_Lib_l4v.More_Word_Operations\] Even more operations on word. \<^descr>[Types] - \<^descr>[\<^theory>\Word_Lib.Signed_Words\] + \<^descr>[\<^theory>\Word_Lib_l4v.Signed_Words\] Formal tagging of word types with a \<^text>\signed\ marker. \<^descr>[Lemmas] - \<^descr>[\<^theory>\Word_Lib.More_Word\] + \<^descr>[\<^theory>\Word_Lib_l4v.More_Word\] More lemmas on words. - \<^descr>[\<^theory>\Word_Lib.Word_Lemmas\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_Lemmas\] More lemmas on words, covering many other theories mentioned here. \<^descr>[Words of popular lengths]. - \<^descr>[\<^theory>\Word_Lib.Word_8\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_8\] for 8-bit words. - \<^descr>[\<^theory>\Word_Lib.Word_16\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_16\] for 16-bit words. - \<^descr>[\<^theory>\Word_Lib.Word_32\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_32\] for 32-bit words. - \<^descr>[\<^theory>\Word_Lib.Word_64\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_64\] for 64-bit words. This theory is not part of \<^text>\Word_Lib_Sumo\, because it shadows - names from \<^theory>\Word_Lib.Word_32\. They can be used together, but then will have + names from \<^theory>\Word_Lib_l4v.Word_32\. They can be used together, but then will have to use qualified names in applications. - \<^descr>[\<^theory>\Word_Lib.Machine_Word_32\ and \<^theory>\Word_Lib.Machine_Word_64\] + \<^descr>[\<^theory>\Word_Lib_l4v.Machine_Word_32\ and \<^theory>\Word_Lib_l4v.Machine_Word_64\] 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 \ from those theories. However theorem coverage may still be terse in some cases. - \<^descr>[\<^theory>\Word_Lib.Word_Lib_Sumo\] + \<^descr>[\<^theory>\Word_Lib_l4v.Word_Lib_Sumo\] 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>\Word_Lib.Word_64\ separately. + \<^theory>\Word_Lib_l4v.Word_64\ separately. - \<^descr>[\<^theory>\Word_Lib.Generic_set_bit\] + \<^descr>[\<^theory>\Word_Lib_l4v.Generic_set_bit\] Kind of an alias: @{thm set_bit_eq [no_vars]} - \<^descr>[\<^theory>\Word_Lib.Typedef_Morphisms\] + \<^descr>[\<^theory>\Word_Lib_l4v.Typedef_Morphisms\] 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>\Word_Lib.Bit_Comprehension\] + \<^descr>[\<^theory>\Word_Lib_l4v.Bit_Comprehension\] Comprehension syntax for bit values over predicates \<^typ>\nat \ bool\, for \<^typ>\'a::len word\; straightforward alternatives exist. - \<^descr>[\<^theory>\Word_Lib.Bit_Comprehension_Int\] + \<^descr>[\<^theory>\Word_Lib_l4v.Bit_Comprehension_Int\] Comprehension syntax for bit values over predicates \<^typ>\nat \ bool\, for \<^typ>\int\; inherently non-computational. - \<^descr>[\<^theory>\Word_Lib.Reversed_Bit_Lists\] + \<^descr>[\<^theory>\Word_Lib_l4v.Reversed_Bit_Lists\] Representation of bit values as explicit list in \<^emph>\reversed\ order. @@ -383,11 +383,11 @@ text \ @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} - \<^descr>[\<^theory>\Word_Lib.Many_More\] + \<^descr>[\<^theory>\Word_Lib_l4v.Many_More\] Collection of operations and theorems which are kept for backward - compatibility and not used in other theories in session \<^text>\Word_Lib\. - They are used in applications of \<^text>\Word_Lib\, but should be migrated to there. + compatibility and not used in other theories in session \<^text>\Word_Lib_l4v\. + They are used in applications of \<^text>\Word_Lib_l4v\, but should be migrated to there. \ section \Changelog\ @@ -395,31 +395,31 @@ section \Changelog\ text \ \<^descr>[Changes since AFP 2022] ~ - \<^item> Theory \<^text>\Word_Lib.Ancient_Numeral\ has been removed from session. + \<^item> Theory \<^text>\Word_Lib_l4v.Ancient_Numeral\ has been removed from session. \<^item> Bit comprehension syntax for \<^typ>\int\ moved to separate theory - \<^theory>\Word_Lib.Bit_Comprehension_Int\. + \<^theory>\Word_Lib_l4v.Bit_Comprehension_Int\. \<^descr>[Changes since AFP 2021] ~ - \<^item> Theory \<^text>\Word_Lib.Ancient_Numeral\ is not part of \<^theory>\Word_Lib.Word_Lib_Sumo\ + \<^item> Theory \<^text>\Word_Lib_l4v.Ancient_Numeral\ is not part of \<^theory>\Word_Lib_l4v.Word_Lib_Sumo\ any longer. \<^item> Infix syntax for \<^term>\(AND)\, \<^term>\(OR)\, \<^term>\(XOR)\ organized in syntax bundle \<^bundle>\bit_operations_syntax\. \<^item> Abbreviation \<^abbrev>\max_word\ moved from distribution into theory - \<^theory>\Word_Lib.Legacy_Aliases\. + \<^theory>\Word_Lib_l4v.Legacy_Aliases\. \<^item> Operation \<^const>\test_bit\ replaced by input abbreviation \<^abbrev>\test_bit\. \<^item> Abbreviations \<^abbrev>\bin_nth\, \<^abbrev>\bin_last\, \<^abbrev>\bin_rest\, \<^abbrev>\bintrunc\, \<^abbrev>\sbintrunc\, \<^abbrev>\norm_sint\, - \<^abbrev>\bin_cat\ moved into theory \<^theory>\Word_Lib.Legacy_Aliases\. + \<^abbrev>\bin_cat\ moved into theory \<^theory>\Word_Lib_l4v.Legacy_Aliases\. \<^item> Operations \<^abbrev>\bshiftr1\, \<^abbrev>\setBit\, \<^abbrev>\clearBit\ moved from distribution into theory - \<^theory>\Word_Lib.Legacy_Aliases\ and replaced by input abbreviations. + \<^theory>\Word_Lib_l4v.Legacy_Aliases\ and replaced by input abbreviations. \<^item> Operations \<^const>\shiftl1\, \<^const>\shiftr1\, \<^const>\sshiftr1\ moved here from distribution. diff --git a/lib/Word_Lib/Hex_Words.thy b/lib/Word_Lib_l4v/Hex_Words.thy similarity index 100% rename from lib/Word_Lib/Hex_Words.thy rename to lib/Word_Lib_l4v/Hex_Words.thy diff --git a/lib/Word_Lib/Least_significant_bit.thy b/lib/Word_Lib_l4v/Least_significant_bit.thy similarity index 100% rename from lib/Word_Lib/Least_significant_bit.thy rename to lib/Word_Lib_l4v/Least_significant_bit.thy diff --git a/lib/Word_Lib/Legacy_Aliases.thy b/lib/Word_Lib_l4v/Legacy_Aliases.thy similarity index 100% rename from lib/Word_Lib/Legacy_Aliases.thy rename to lib/Word_Lib_l4v/Legacy_Aliases.thy diff --git a/lib/Word_Lib/Machine_Word_32.thy b/lib/Word_Lib_l4v/Machine_Word_32.thy similarity index 100% rename from lib/Word_Lib/Machine_Word_32.thy rename to lib/Word_Lib_l4v/Machine_Word_32.thy diff --git a/lib/Word_Lib/Machine_Word_32_Basics.thy b/lib/Word_Lib_l4v/Machine_Word_32_Basics.thy similarity index 100% rename from lib/Word_Lib/Machine_Word_32_Basics.thy rename to lib/Word_Lib_l4v/Machine_Word_32_Basics.thy diff --git a/lib/Word_Lib/Machine_Word_64.thy b/lib/Word_Lib_l4v/Machine_Word_64.thy similarity index 100% rename from lib/Word_Lib/Machine_Word_64.thy rename to lib/Word_Lib_l4v/Machine_Word_64.thy diff --git a/lib/Word_Lib/Machine_Word_64_Basics.thy b/lib/Word_Lib_l4v/Machine_Word_64_Basics.thy similarity index 100% rename from lib/Word_Lib/Machine_Word_64_Basics.thy rename to lib/Word_Lib_l4v/Machine_Word_64_Basics.thy diff --git a/lib/Word_Lib/Many_More.thy b/lib/Word_Lib_l4v/Many_More.thy similarity index 100% rename from lib/Word_Lib/Many_More.thy rename to lib/Word_Lib_l4v/Many_More.thy diff --git a/lib/Word_Lib/More_Arithmetic.thy b/lib/Word_Lib_l4v/More_Arithmetic.thy similarity index 100% rename from lib/Word_Lib/More_Arithmetic.thy rename to lib/Word_Lib_l4v/More_Arithmetic.thy diff --git a/lib/Word_Lib/More_Bit_Ring.thy b/lib/Word_Lib_l4v/More_Bit_Ring.thy similarity index 100% rename from lib/Word_Lib/More_Bit_Ring.thy rename to lib/Word_Lib_l4v/More_Bit_Ring.thy diff --git a/lib/Word_Lib/More_Divides.thy b/lib/Word_Lib_l4v/More_Divides.thy similarity index 100% rename from lib/Word_Lib/More_Divides.thy rename to lib/Word_Lib_l4v/More_Divides.thy diff --git a/lib/Word_Lib/More_Misc.thy b/lib/Word_Lib_l4v/More_Misc.thy similarity index 100% rename from lib/Word_Lib/More_Misc.thy rename to lib/Word_Lib_l4v/More_Misc.thy diff --git a/lib/Word_Lib/More_Sublist.thy b/lib/Word_Lib_l4v/More_Sublist.thy similarity index 100% rename from lib/Word_Lib/More_Sublist.thy rename to lib/Word_Lib_l4v/More_Sublist.thy diff --git a/lib/Word_Lib/More_Word.thy b/lib/Word_Lib_l4v/More_Word.thy similarity index 100% rename from lib/Word_Lib/More_Word.thy rename to lib/Word_Lib_l4v/More_Word.thy diff --git a/lib/Word_Lib/More_Word_Operations.thy b/lib/Word_Lib_l4v/More_Word_Operations.thy similarity index 100% rename from lib/Word_Lib/More_Word_Operations.thy rename to lib/Word_Lib_l4v/More_Word_Operations.thy diff --git a/lib/Word_Lib/Most_significant_bit.thy b/lib/Word_Lib_l4v/Most_significant_bit.thy similarity index 100% rename from lib/Word_Lib/Most_significant_bit.thy rename to lib/Word_Lib_l4v/Most_significant_bit.thy diff --git a/lib/Word_Lib/Next_and_Prev.thy b/lib/Word_Lib_l4v/Next_and_Prev.thy similarity index 100% rename from lib/Word_Lib/Next_and_Prev.thy rename to lib/Word_Lib_l4v/Next_and_Prev.thy diff --git a/lib/Word_Lib/Norm_Words.thy b/lib/Word_Lib_l4v/Norm_Words.thy similarity index 100% rename from lib/Word_Lib/Norm_Words.thy rename to lib/Word_Lib_l4v/Norm_Words.thy diff --git a/lib/Word_Lib/X64/WordSetup.thy b/lib/Word_Lib_l4v/RISCV64/WordSetup.thy similarity index 96% rename from lib/Word_Lib/X64/WordSetup.thy rename to lib/Word_Lib_l4v/RISCV64/WordSetup.thy index 75b7adb20..7e71e78ae 100644 --- a/lib/Word_Lib/X64/WordSetup.thy +++ b/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 diff --git a/lib/Word_Lib/ROOT b/lib/Word_Lib_l4v/ROOT similarity index 86% rename from lib/Word_Lib/ROOT rename to lib/Word_Lib_l4v/ROOT index 5a2b12301..aee9f1f88 100644 --- a/lib/Word_Lib/ROOT +++ b/lib/Word_Lib_l4v/ROOT @@ -6,8 +6,8 @@ chapter Lib -session Word_Lib (lib) = HOL + - options [timeout = 300, document=pdf] +session Word_Lib_l4v (lib) = HOL + + options [timeout = 900, document=pdf] sessions "HOL-Library" "HOL-Eisbach" diff --git a/lib/Word_Lib/Reversed_Bit_Lists.thy b/lib/Word_Lib_l4v/Reversed_Bit_Lists.thy similarity index 100% rename from lib/Word_Lib/Reversed_Bit_Lists.thy rename to lib/Word_Lib_l4v/Reversed_Bit_Lists.thy diff --git a/lib/Word_Lib/Rsplit.thy b/lib/Word_Lib_l4v/Rsplit.thy similarity index 100% rename from lib/Word_Lib/Rsplit.thy rename to lib/Word_Lib_l4v/Rsplit.thy diff --git a/lib/Word_Lib/Sgn_Abs.thy b/lib/Word_Lib_l4v/Sgn_Abs.thy similarity index 100% rename from lib/Word_Lib/Sgn_Abs.thy rename to lib/Word_Lib_l4v/Sgn_Abs.thy diff --git a/lib/Word_Lib/Signed_Division_Word.thy b/lib/Word_Lib_l4v/Signed_Division_Word.thy similarity index 100% rename from lib/Word_Lib/Signed_Division_Word.thy rename to lib/Word_Lib_l4v/Signed_Division_Word.thy diff --git a/lib/Word_Lib/Signed_Words.thy b/lib/Word_Lib_l4v/Signed_Words.thy similarity index 100% rename from lib/Word_Lib/Signed_Words.thy rename to lib/Word_Lib_l4v/Signed_Words.thy diff --git a/lib/Word_Lib/Singleton_Bit_Shifts.thy b/lib/Word_Lib_l4v/Singleton_Bit_Shifts.thy similarity index 100% rename from lib/Word_Lib/Singleton_Bit_Shifts.thy rename to lib/Word_Lib_l4v/Singleton_Bit_Shifts.thy diff --git a/lib/Word_Lib/Strict_part_mono.thy b/lib/Word_Lib_l4v/Strict_part_mono.thy similarity index 100% rename from lib/Word_Lib/Strict_part_mono.thy rename to lib/Word_Lib_l4v/Strict_part_mono.thy diff --git a/lib/Word_Lib/Syntax_Bundles.thy b/lib/Word_Lib_l4v/Syntax_Bundles.thy similarity index 100% rename from lib/Word_Lib/Syntax_Bundles.thy rename to lib/Word_Lib_l4v/Syntax_Bundles.thy diff --git a/lib/Word_Lib/Type_Syntax.thy b/lib/Word_Lib_l4v/Type_Syntax.thy similarity index 100% rename from lib/Word_Lib/Type_Syntax.thy rename to lib/Word_Lib_l4v/Type_Syntax.thy diff --git a/lib/Word_Lib/Typedef_Morphisms.thy b/lib/Word_Lib_l4v/Typedef_Morphisms.thy similarity index 100% rename from lib/Word_Lib/Typedef_Morphisms.thy rename to lib/Word_Lib_l4v/Typedef_Morphisms.thy diff --git a/lib/Word_Lib/Word_16.thy b/lib/Word_Lib_l4v/Word_16.thy similarity index 100% rename from lib/Word_Lib/Word_16.thy rename to lib/Word_Lib_l4v/Word_16.thy diff --git a/lib/Word_Lib/Word_32.thy b/lib/Word_Lib_l4v/Word_32.thy similarity index 100% rename from lib/Word_Lib/Word_32.thy rename to lib/Word_Lib_l4v/Word_32.thy diff --git a/lib/Word_Lib/Word_64.thy b/lib/Word_Lib_l4v/Word_64.thy similarity index 100% rename from lib/Word_Lib/Word_64.thy rename to lib/Word_Lib_l4v/Word_64.thy diff --git a/lib/Word_Lib/Word_8.thy b/lib/Word_Lib_l4v/Word_8.thy similarity index 100% rename from lib/Word_Lib/Word_8.thy rename to lib/Word_Lib_l4v/Word_8.thy diff --git a/lib/Word_Lib/Word_EqI.thy b/lib/Word_Lib_l4v/Word_EqI.thy similarity index 100% rename from lib/Word_Lib/Word_EqI.thy rename to lib/Word_Lib_l4v/Word_EqI.thy diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib_l4v/Word_Lemmas.thy similarity index 100% rename from lib/Word_Lib/Word_Lemmas.thy rename to lib/Word_Lib_l4v/Word_Lemmas.thy diff --git a/lib/Word_Lib/Word_Lemmas_32_Internal.thy b/lib/Word_Lib_l4v/Word_Lemmas_32_Internal.thy similarity index 100% rename from lib/Word_Lib/Word_Lemmas_32_Internal.thy rename to lib/Word_Lib_l4v/Word_Lemmas_32_Internal.thy diff --git a/lib/Word_Lib/Word_Lemmas_64_Internal.thy b/lib/Word_Lib_l4v/Word_Lemmas_64_Internal.thy similarity index 100% rename from lib/Word_Lib/Word_Lemmas_64_Internal.thy rename to lib/Word_Lib_l4v/Word_Lemmas_64_Internal.thy diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib_l4v/Word_Lemmas_Internal.thy similarity index 99% rename from lib/Word_Lib/Word_Lemmas_Internal.thy rename to lib/Word_Lib_l4v/Word_Lemmas_Internal.thy index 643786b46..7c330d3d0 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib_l4v/Word_Lemmas_Internal.thy @@ -48,12 +48,12 @@ lemma signed_ge_zero_scast_eq_ucast: "0 <=s x \ 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: "(\ P \ Q) \ P \ 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 \ d \ a - (b - c) \ (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: "\ x && mask n = y && mask n; x >> n = y >> n \ \ x = y" diff --git a/lib/Word_Lib/Word_Lemmas_Prefix.thy b/lib/Word_Lib_l4v/Word_Lemmas_Prefix.thy similarity index 100% rename from lib/Word_Lib/Word_Lemmas_Prefix.thy rename to lib/Word_Lib_l4v/Word_Lemmas_Prefix.thy diff --git a/lib/Word_Lib/Word_Lib_Sumo.thy b/lib/Word_Lib_l4v/Word_Lib_Sumo.thy similarity index 100% rename from lib/Word_Lib/Word_Lib_Sumo.thy rename to lib/Word_Lib_l4v/Word_Lib_Sumo.thy diff --git a/lib/Word_Lib/Word_Names.thy b/lib/Word_Lib_l4v/Word_Names.thy similarity index 100% rename from lib/Word_Lib/Word_Names.thy rename to lib/Word_Lib_l4v/Word_Names.thy diff --git a/lib/Word_Lib/Word_Syntax.thy b/lib/Word_Lib_l4v/Word_Syntax.thy similarity index 100% rename from lib/Word_Lib/Word_Syntax.thy rename to lib/Word_Lib_l4v/Word_Syntax.thy diff --git a/lib/Word_Lib/RISCV64/WordSetup.thy b/lib/Word_Lib_l4v/X64/WordSetup.thy similarity index 96% rename from lib/Word_Lib/RISCV64/WordSetup.thy rename to lib/Word_Lib_l4v/X64/WordSetup.thy index 75b7adb20..7e71e78ae 100644 --- a/lib/Word_Lib/RISCV64/WordSetup.thy +++ b/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 diff --git a/lib/Word_Lib/document/root.tex b/lib/Word_Lib_l4v/document/root.tex similarity index 100% rename from lib/Word_Lib/document/root.tex rename to lib/Word_Lib_l4v/document/root.tex diff --git a/lib/sep_algebra/ROOT b/lib/sep_algebra/ROOT index 7aa4d7353..5b8cdca6a 100644 --- a/lib/sep_algebra/ROOT +++ b/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" diff --git a/misc/regression/tests.xml b/misc/regression/tests.xml index 34b9ef841..139fbad91 100644 --- a/misc/regression/tests.xml +++ b/misc/regression/tests.xml @@ -53,7 +53,7 @@ - isabelle/bin/isabelle build -d . -vb Word_Lib + isabelle/bin/isabelle build -d . -vb Word_Lib_l4v diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy index 530b503eb..8f4729aaf 100644 --- a/proof/crefine/ARM_HYP/ArchMove_C.thy +++ b/proof/crefine/ARM_HYP/ArchMove_C.thy @@ -250,7 +250,7 @@ lemma is_aligned_ptrFromPAddr_pageBitsForSize: "is_aligned p (pageBitsForSize sz) \ 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 \ 2 ^ asid_high_bits - 1 \ (x::word32) << asid_low_bits \ 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) \ mask asid_bits \ (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: "\ (asid :: word32) \ mask asid_bits; asid >> asid_low_bits = 0 \ \ (asid && mask asid_low_bits = 0) = (asid = 0)" diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index 3db339c08..34012d829 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -174,7 +174,7 @@ lemma to_bool_if: "(if w \ 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) \ LENGTH('b::len)" shows "UCAST('a \ 'b) (w >> n) = UCAST('a \ '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) \ 0 <=s UCAST('a \ '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 \ 'c) (UCAST('a \ 'b) w) = UCAST('a \ '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: "\ unat x < n ; n \ Suc 0 \ \ ucast x = 0" by (simp add: le_Suc_eq unsigned_eq_0_iff) diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy index 55ef038c6..ed7e84c1d 100644 --- a/proof/drefine/Intent_DR.thy +++ b/proof/drefine/Intent_DR.thy @@ -1456,7 +1456,7 @@ lemma mask_inj_if: "\a && mask n = a; b && mask n = b; a && mask n = b && mask n\\ a = b" by (rule box_equals) -(* FIXME: move to Word_Lib, generalise *) +(* FIXME: move to Word_Lib_l4v, generalise *) lemma bound_preserve_mask: "\ is_aligned (x::word32) n; x\ mask k; (z::word32)\ mask n; n < 32; k < 32; n \ k \ \ x+z \ mask k" diff --git a/proof/infoflow/refine/ARM/Example_Valid_StateH.thy b/proof/infoflow/refine/ARM/Example_Valid_StateH.thy index e4e181837..6170a8907 100644 --- a/proof/infoflow/refine/ARM/Example_Valid_StateH.thy +++ b/proof/infoflow/refine/ARM/Example_Valid_StateH.thy @@ -526,7 +526,7 @@ lemma pt_offs_range_correct: "x \ pt_offs_range High_pt_ptr \ \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 \ (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 \ (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 \ (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 \ k < len_of TYPE('a) \ (of_bl x :: 'a :: len word) \ 2 ^ k - 1" by (simp add: of_bl_length_less) @@ -606,11 +606,11 @@ lemma cnode_offs_in_range: "length x = 10 \ Silc_cnode_ptr + of_bl x * 0x10 \ 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 \ 2 ^ n - 1 \ 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 "\0 < c; a \ b * c \ \ a div c \ b" diff --git a/proof/invariant-abstract/VSpacePre_AI.thy b/proof/invariant-abstract/VSpacePre_AI.thy index a368c89bf..d3c5d2caf 100644 --- a/proof/invariant-abstract/VSpacePre_AI.thy +++ b/proof/invariant-abstract/VSpacePre_AI.thy @@ -64,7 +64,7 @@ lemma invs_valid_irq_states[elim!]: "invs s \ 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) \ 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 diff --git a/spec/ROOT b/spec/ROOT index f05baca97..baa968f64 100644 --- a/spec/ROOT +++ b/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" diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index 54b9b7ce4..41d9331a7 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -24,7 +24,7 @@ theory Intents_D imports - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" "ASpec.CapRights_A" begin diff --git a/spec/cspec/KernelState_C.thy b/spec/cspec/KernelState_C.thy index 0bd87b4af..5930f48c9 100644 --- a/spec/cspec/KernelState_C.thy +++ b/spec/cspec/KernelState_C.thy @@ -6,7 +6,7 @@ theory KernelState_C imports - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" "CLib.BitFieldProofsLib" "Substitute" begin diff --git a/spec/cspec/c/gen-config-thy.py b/spec/cspec/c/gen-config-thy.py index 730489b7a..02981f80d 100755 --- a/spec/cspec/c/gen-config-thy.py +++ b/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 (* diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy index 98c96196f..937e7c5fb 100644 --- a/spec/design/m-skel/AARCH64/MachineTypes.thy +++ b/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 diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index 6455feb8a..5f6d86d04 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/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 diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy index 7e895ec27..b57e15946 100644 --- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy +++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy @@ -8,7 +8,7 @@ chapter \ARM\_HYP Machine Types\ theory MachineTypes imports - Word_Lib.WordSetup + Word_Lib_l4v.WordSetup Monads.Nondet_Empty_Fail Monads.Nondet_No_Fail Monads.Reader_Option_ND diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy index 234e80542..c75a6efe7 100644 --- a/spec/design/m-skel/RISCV64/MachineTypes.thy +++ b/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 diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy index e8465d4e1..696648953 100644 --- a/spec/design/m-skel/X64/MachineTypes.thy +++ b/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 diff --git a/spec/design/skel/AARCH64/ArchInvocationLabels_H.thy b/spec/design/skel/AARCH64/ArchInvocationLabels_H.thy index 4b7e93575..616ce7b26 100644 --- a/spec/design/skel/AARCH64/ArchInvocationLabels_H.thy +++ b/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 diff --git a/spec/design/skel/ARM/ArchInvocationLabels_H.thy b/spec/design/skel/ARM/ArchInvocationLabels_H.thy index f09d72dc5..a135ecace 100644 --- a/spec/design/skel/ARM/ArchInvocationLabels_H.thy +++ b/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 diff --git a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy index bbfce9692..2569abb59 100644 --- a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy +++ b/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 diff --git a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy index bae9fc2b0..8a2be2fc6 100644 --- a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy +++ b/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 diff --git a/spec/design/skel/X64/ArchInvocationLabels_H.thy b/spec/design/skel/X64/ArchInvocationLabels_H.thy index c967f7f16..49518e5e5 100644 --- a/spec/design/skel/X64/ArchInvocationLabels_H.thy +++ b/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 diff --git a/spec/machine/AARCH64/MachineOps.thy b/spec/machine/AARCH64/MachineOps.thy index cdef617ec..6f5eceba9 100644 --- a/spec/machine/AARCH64/MachineOps.thy +++ b/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 diff --git a/spec/machine/AARCH64/Platform.thy b/spec/machine/AARCH64/Platform.thy index 6d6c5c712..f8b636e4d 100644 --- a/spec/machine/AARCH64/Platform.thy +++ b/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 diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy index 91abe6940..f55793d09 100644 --- a/spec/machine/ARM/Platform.thy +++ b/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 diff --git a/spec/machine/ARM_HYP/Platform.thy b/spec/machine/ARM_HYP/Platform.thy index 6c121747c..66af4543d 100644 --- a/spec/machine/ARM_HYP/Platform.thy +++ b/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 diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy index a8d52be68..b13a344f8 100644 --- a/spec/machine/RISCV64/MachineOps.thy +++ b/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 diff --git a/spec/machine/RISCV64/Platform.thy b/spec/machine/RISCV64/Platform.thy index 1443ed182..4814a88b1 100644 --- a/spec/machine/RISCV64/Platform.thy +++ b/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 diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index 6ec113cc0..f7efafeef 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/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 diff --git a/spec/machine/X64/Platform.thy b/spec/machine/X64/Platform.thy index d6b16038d..77549836e 100644 --- a/spec/machine/X64/Platform.thy +++ b/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 diff --git a/spec/take-grant/System_S.thy b/spec/take-grant/System_S.thy index 8fa7dfece..22c6daecb 100644 --- a/spec/take-grant/System_S.thy +++ b/spec/take-grant/System_S.thy @@ -16,7 +16,7 @@ *) theory System_S -imports "Word_Lib.WordSetup" +imports "Word_Lib_l4v.WordSetup" begin (* System entities: Definition of entities that constitute the system diff --git a/tools/asmrefine/GraphLang.thy b/tools/asmrefine/GraphLang.thy index 12daf6cd7..94010f948 100644 --- a/tools/asmrefine/GraphLang.thy +++ b/tools/asmrefine/GraphLang.thy @@ -512,7 +512,7 @@ fun parse_n p (n :: ss) = let in funpow_yield n p ss end | parse_n _ [] = raise PARSEGRAPH ["parse_n: empty"] -fun mk_binT sz = Word_Lib.mk_wordT sz |> dest_Type |> snd |> hd +fun mk_binT sz = Word_Lib_l4v.mk_wordT sz |> dest_Type |> snd |> hd val ptr_size_str = case @{typ machine_word} of @@ -521,7 +521,7 @@ val ptr_size_str = fun parse_typ ("Word" :: n :: ss) = let val n = parse_int n - in (Word_Lib.mk_wordT n, ss) end + in (Word_Lib_l4v.mk_wordT n, ss) end | parse_typ ("Bool" :: ss) = (@{typ bool}, ss) | parse_typ ("Mem" :: ss) = (@{typ "machine_word \ word8"}, ss) | parse_typ ("Dom" :: ss) = (@{typ "machine_word set"}, ss) diff --git a/tools/asmrefine/ROOT b/tools/asmrefine/ROOT index 228aed43c..2986b3b2e 100644 --- a/tools/asmrefine/ROOT +++ b/tools/asmrefine/ROOT @@ -8,7 +8,7 @@ chapter "Tools" session AsmRefine = CParser + sessions - Word_Lib + Word_Lib_l4v Lib CLib directories diff --git a/tools/asmrefine/TailrecPre.thy b/tools/asmrefine/TailrecPre.thy index d2d55e96c..9aca00106 100644 --- a/tools/asmrefine/TailrecPre.thy +++ b/tools/asmrefine/TailrecPre.thy @@ -6,7 +6,7 @@ theory TailrecPre imports - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" "Lib.Lib" begin diff --git a/tools/autocorres/AbstractArrays.thy b/tools/autocorres/AbstractArrays.thy index 4d6279f20..85e7acbe8 100644 --- a/tools/autocorres/AbstractArrays.thy +++ b/tools/autocorres/AbstractArrays.thy @@ -7,7 +7,7 @@ theory AbstractArrays imports "CParser.TypHeapLib" - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" begin (* diff --git a/tools/autocorres/HeapLift.thy b/tools/autocorres/HeapLift.thy index e45ccf6f0..d84fe0a20 100644 --- a/tools/autocorres/HeapLift.thy +++ b/tools/autocorres/HeapLift.thy @@ -1134,7 +1134,7 @@ lemma abs_spec_modify_global[heap_abs]: (* Signed words are stored on the heap as unsigned words. *) -(* FIXME: move to Word_Lib *) +(* FIXME: move to Word_Lib_l4v *) lemma uint_scast: "uint (scast x :: 'a word) = uint (x :: 'a::len signed word)" by (metis len_signed scast_nop2 uint_word_of_int_eq word_uint.Rep_inverse) diff --git a/tools/autocorres/NatBitwise.thy b/tools/autocorres/NatBitwise.thy index 7de19e00f..aadcfc138 100644 --- a/tools/autocorres/NatBitwise.thy +++ b/tools/autocorres/NatBitwise.thy @@ -8,7 +8,7 @@ Lemmas about this instance should also go here. *) theory NatBitwise imports - Word_Lib.WordSetup + Word_Lib_l4v.WordSetup begin instantiation nat :: lsb diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy index 3b54035ca..49c233cd9 100644 --- a/tools/autocorres/NonDetMonadEx.thy +++ b/tools/autocorres/NonDetMonadEx.thy @@ -10,7 +10,7 @@ theory NonDetMonadEx imports - "Word_Lib.WordSetup" + "Word_Lib_l4v.WordSetup" "Monads.Nondet_VCG" "Monads.Nondet_Monad_Equations" "Monads.Nondet_More_VCG" diff --git a/tools/autocorres/WordAbstract.thy b/tools/autocorres/WordAbstract.thy index e2ebd0f0c..6db209676 100644 --- a/tools/autocorres/WordAbstract.thy +++ b/tools/autocorres/WordAbstract.thy @@ -171,18 +171,18 @@ lemma unat_abstract_binops: by (auto simp: unat_plus_if' unat_div unat_mod UWORD_MAX_def le_to_less_plus_one WordAbstract.unat_mult_simple word_bits_def unat_sub word_le_nat_alt) -(* FIXME: move to Word_Lib *) +(* FIXME: move to Word_Lib_l4v *) lemma unat_of_int: "\i \ 0; i < 2 ^ LENGTH('a)\ \ unat (of_int i :: 'a::len word) = nat i" by (metis nat_less_numeral_power_cancel_iff of_nat_nat unat_of_nat_len) -(* FIXME: move to Word_Lib *) +(* FIXME: move to Word_Lib_l4v *) (* FIXME generalises Word_Lemmas_32.unat_of_int_32 *) lemma unat_of_int_signed: "\i \ 0; i < 2 ^ LENGTH('a)\ \ unat (of_int i :: 'a::len signed word) = nat i" by (simp add: unat_of_int) -(* FIXME: move to Word_Lib *) +(* FIXME: move to Word_Lib_l4v *) lemma nat_sint: "0 <=s (x :: 'a::len signed word) \ nat (sint x) = unat x" apply (subst unat_of_int_signed[where 'a='a, symmetric]) diff --git a/tools/autocorres/tools/release.py b/tools/autocorres/tools/release.py index 7acfbcb06..61b0cd8e8 100755 --- a/tools/autocorres/tools/release.py +++ b/tools/autocorres/tools/release.py @@ -200,7 +200,7 @@ with TempDir(cleanup=(not args.no_cleanup)) as base_dir: shutil.copyfile(f_src, f_dest) # Copy various other files. - for session in ['Basics', 'Eisbach_Tools', 'ML_Utils', 'Monads', 'Word_Lib']: + for session in ['Basics', 'Eisbach_Tools', 'ML_Utils', 'Monads', 'Word_Lib_l4v']: shutil.copyfile( os.path.join(args.repository, 'lib', session, 'ROOT'), os.path.join(target_dir, 'lib', session, 'ROOT')) diff --git a/tools/autocorres/tools/release_files/ROOTS.base_dir b/tools/autocorres/tools/release_files/ROOTS.base_dir index caf4ca837..27bd9a02e 100644 --- a/tools/autocorres/tools/release_files/ROOTS.base_dir +++ b/tools/autocorres/tools/release_files/ROOTS.base_dir @@ -2,6 +2,6 @@ lib/Basics lib/Eisbach_Tools lib/ML_Utils lib/Monads -lib/Word_Lib +lib/Word_Lib_l4v c-parser autocorres diff --git a/tools/c-parser/ROOT b/tools/c-parser/ROOT index cf43f0868..01ea8876b 100644 --- a/tools/c-parser/ROOT +++ b/tools/c-parser/ROOT @@ -6,7 +6,7 @@ chapter "C-Parser" -session "Simpl-VCG" in Simpl = Word_Lib + +session "Simpl-VCG" in Simpl = Word_Lib_l4v + sessions "HOL-Statespace" theories diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index 97afbdddd..8bcaea200 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -109,13 +109,14 @@ do done # other misc files +<<<<<<< HEAD cp -v lib/Word_Lib/ROOT "$outputdir/src/lib/Word_Lib/" cp -v lib/Basics/ROOT "$outputdir/src/lib/Basics/" cp -v lib/ML_Utils/ROOT "$outputdir/src/lib/ML_Utils/" echo "Creating ROOTS file" cat >"$outputdir/src/ROOTS" <