diff --git a/thys/Word_Lib/ROOT b/thys/Word_Lib/ROOT --- a/thys/Word_Lib/ROOT +++ b/thys/Word_Lib/ROOT @@ -1,34 +1,35 @@ chapter AFP session Word_Lib (AFP) = HOL + options [timeout = 300] sessions "HOL-Library" "HOL-Eisbach" theories [document = false] \ \Attempt to just generated word-specific document material\ Enumeration Even_More_List Legacy_Aliases More_Arithmetic More_Divides More_Misc More_Sublist Strict_part_mono theories Bits_Int Bit_Comprehension More_Word Bit_Shifts_Infix_Syntax Next_and_Prev Signed_Division_Word theories [document = false] Many_More Singleton_Bit_Shifts Typedef_Morphisms theories Bitwise Guide theories [document = false] Examples document_files "root.tex" + "root.bib" diff --git a/thys/Word_Lib/Signed_Division_Word.thy b/thys/Word_Lib/Signed_Division_Word.thy --- a/thys/Word_Lib/Signed_Division_Word.thy +++ b/thys/Word_Lib/Signed_Division_Word.thy @@ -1,251 +1,257 @@ (* * Copyright Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section \Signed division on word\ theory Signed_Division_Word imports "HOL-Library.Signed_Division" "HOL-Library.Word" begin +text \ + The following specification of division follows ISO C99, which in turn adopted the typical + behavior of hardware modern in the beginning of the 1990ies. + The underlying integer division is named ``T-division'' in \cite{leijen01}. +\ + instantiation word :: (len) signed_division begin lift_definition signed_divide_word :: \'a::len word \ 'a word \ 'a word\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k sdiv signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) lift_definition signed_modulo_word :: \'a::len word \ 'a word \ 'a word\ is \\k l. signed_take_bit (LENGTH('a) - Suc 0) k smod signed_take_bit (LENGTH('a) - Suc 0) l\ by (simp flip: signed_take_bit_decr_length_iff) lemma sdiv_word_def [code]: \v sdiv w = word_of_int (sint v sdiv sint w)\ for v w :: \'a::len word\ by transfer simp lemma smod_word_def [code]: \v smod w = word_of_int (sint v smod sint w)\ for v w :: \'a::len word\ by transfer simp instance proof fix v w :: \'a word\ have \sint v sdiv sint w * sint w + sint v smod sint w = sint v\ by (fact sdiv_mult_smod_eq) then have \word_of_int (sint v sdiv sint w * sint w + sint v smod sint w) = (word_of_int (sint v) :: 'a word)\ by simp then show \v sdiv w * w + v smod w = v\ by (simp add: sdiv_word_def smod_word_def) qed end lemma sdiv_smod_id: \(a sdiv b) * b + (a smod b) = a\ for a b :: \'a::len word\ by (fact sdiv_mult_smod_eq) lemma signed_div_arith: "sint ((a::('a::len) word) sdiv b) = signed_take_bit (LENGTH('a) - 1) (sint a sdiv sint b)" apply transfer apply simp done lemma signed_mod_arith: "sint ((a::('a::len) word) smod b) = signed_take_bit (LENGTH('a) - 1) (sint a smod sint b)" apply transfer apply simp done lemma word_sdiv_div0 [simp]: "(a :: ('a::len) word) sdiv 0 = 0" apply (auto simp: sdiv_word_def signed_divide_int_def sgn_if) done lemma smod_word_zero [simp]: \w smod 0 = w\ for w :: \'a::len word\ by transfer (simp add: take_bit_signed_take_bit) lemma word_sdiv_div1 [simp]: "(a :: ('a::len) word) sdiv 1 = a" apply (cases \LENGTH('a)\) apply simp_all apply transfer apply simp apply (case_tac nat) apply simp_all apply (simp add: take_bit_signed_take_bit) done lemma smod_word_one [simp]: \w smod 1 = 0\ for w :: \'a::len word\ by (simp add: smod_word_def signed_modulo_int_def) lemma word_sdiv_div_minus1 [simp]: "(a :: ('a::len) word) sdiv -1 = -a" apply (auto simp: sdiv_word_def signed_divide_int_def sgn_if) apply transfer apply simp apply (metis Suc_pred len_gt_0 signed_take_bit_eq_iff_take_bit_eq signed_take_bit_of_0 take_bit_of_0) done lemma smod_word_minus_one [simp]: \w smod - 1 = 0\ for w :: \'a::len word\ by (simp add: smod_word_def signed_modulo_int_def) lemma one_sdiv_word_eq [simp]: \1 sdiv w = of_bool (w = 1 \ w = - 1) * w\ for w :: \'a::len word\ proof (cases \1 < \sint w\\) case True then show ?thesis by (auto simp add: sdiv_word_def signed_divide_int_def split: if_splits) next case False then have \\sint w\ \ 1\ by simp then have \sint w \ {- 1, 0, 1}\ by auto then have \(word_of_int (sint w) :: 'a::len word) \ word_of_int ` {- 1, 0, 1}\ by blast then have \w \ {- 1, 0, 1}\ by simp then show ?thesis by auto qed lemma one_smod_word_eq [simp]: \1 smod w = 1 - of_bool (w = 1 \ w = - 1)\ for w :: \'a::len word\ using sdiv_smod_id [of 1 w] by auto lemma minus_one_sdiv_word_eq [simp]: \- 1 sdiv w = - (1 sdiv w)\ for w :: \'a::len word\ apply (auto simp add: sdiv_word_def signed_divide_int_def) apply transfer apply simp done lemma minus_one_smod_word_eq [simp]: \- 1 smod w = - (1 smod w)\ for w :: \'a::len word\ using sdiv_smod_id [of \- 1\ w] by auto lemma smod_word_alt_def: "(a :: ('a::len) word) smod b = a - (a sdiv b) * b" by (simp add: minus_sdiv_mult_eq_smod) lemmas sdiv_word_numeral_numeral [simp] = sdiv_word_def [of \numeral a\ \numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sdiv_word_minus_numeral_numeral [simp] = sdiv_word_def [of \- numeral a\ \numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sdiv_word_numeral_minus_numeral [simp] = sdiv_word_def [of \numeral a\ \- numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sdiv_word_minus_numeral_minus_numeral [simp] = sdiv_word_def [of \- numeral a\ \- numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas smod_word_numeral_numeral [simp] = smod_word_def [of \numeral a\ \numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas smod_word_minus_numeral_numeral [simp] = smod_word_def [of \- numeral a\ \numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas smod_word_numeral_minus_numeral [simp] = smod_word_def [of \numeral a\ \- numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas smod_word_minus_numeral_minus_numeral [simp] = smod_word_def [of \- numeral a\ \- numeral b\, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas word_sdiv_0 = word_sdiv_div0 lemma sdiv_word_min: "- (2 ^ (size a - 1)) \ sint (a :: ('a::len) word) sdiv sint (b :: ('a::len) word)" using sdiv_int_range [where a="sint a" and b="sint b"] apply auto apply (cases \LENGTH('a)\) apply simp_all apply transfer apply simp apply (rule order_trans) defer apply assumption apply simp apply (metis abs_le_iff add.inverse_inverse le_cases le_minus_iff not_le signed_take_bit_int_eq_self_iff signed_take_bit_minus) done lemma sdiv_word_max: \sint a sdiv sint b \ 2 ^ (size a - Suc 0)\ for a b :: \'a::len word\ proof (cases \sint a = 0 \ sint b = 0 \ sgn (sint a) \ sgn (sint b)\) case True then show ?thesis apply (auto simp add: sgn_if not_less signed_divide_int_def split: if_splits) apply (smt (z3) pos_imp_zdiv_neg_iff zero_le_power) apply (smt (z3) not_exp_less_eq_0_int pos_imp_zdiv_neg_iff) done next case False then have \\sint a\ div \sint b\ \ \sint a\\ by (subst nat_le_eq_zle [symmetric]) (simp_all add: div_abs_eq_div_nat) also have \\sint a\ \ 2 ^ (size a - Suc 0)\ using sint_range_size [of a] by auto finally show ?thesis using False by (simp add: signed_divide_int_def) qed lemmas word_sdiv_numerals_lhs = sdiv_word_def[where v="numeral x" for x] sdiv_word_def[where v=0] sdiv_word_def[where v=1] lemmas word_sdiv_numerals = word_sdiv_numerals_lhs[where w="numeral y" for y] word_sdiv_numerals_lhs[where w=0] word_sdiv_numerals_lhs[where w=1] lemma smod_word_mod_0: "x smod (0 :: ('a::len) word) = x" by (fact smod_word_zero) lemma smod_word_0_mod [simp]: "0 smod (x :: ('a::len) word) = 0" by (clarsimp simp: smod_word_def) lemma smod_word_max: "sint (a::'a word) smod sint (b::'a word) < 2 ^ (LENGTH('a::len) - Suc 0)" apply (cases \sint b = 0\) apply (simp_all add: sint_less) apply (cases \LENGTH('a)\) apply simp_all using smod_int_range [where a="sint a" and b="sint b"] apply auto apply (rule less_le_trans) apply assumption apply (auto simp add: abs_le_iff) apply (metis diff_Suc_1 le_cases linorder_not_le sint_lt) apply (metis add.inverse_inverse diff_Suc_1 linorder_not_less neg_less_iff_less sint_ge) done lemma smod_word_min: "- (2 ^ (LENGTH('a::len) - Suc 0)) \ sint (a::'a word) smod sint (b::'a word)" apply (cases \LENGTH('a)\) apply simp_all apply (cases \sint b = 0\) apply simp_all apply (metis diff_Suc_1 sint_ge) using smod_int_range [where a="sint a" and b="sint b"] apply auto apply (rule order_trans) defer apply assumption apply (auto simp add: algebra_simps abs_le_iff) apply (metis abs_zero add.left_neutral add_mono_thms_linordered_semiring(1) diff_Suc_1 le_cases linorder_not_less sint_lt zabs_less_one_iff) apply (metis abs_zero add.inverse_inverse add.left_neutral add_mono_thms_linordered_semiring(1) diff_Suc_1 le_cases le_minus_iff linorder_not_less sint_ge zabs_less_one_iff) done lemmas word_smod_numerals_lhs = smod_word_def[where v="numeral x" for x] smod_word_def[where v=0] smod_word_def[where v=1] lemmas word_smod_numerals = word_smod_numerals_lhs[where w="numeral y" for y] word_smod_numerals_lhs[where w=0] word_smod_numerals_lhs[where w=1] end diff --git a/thys/Word_Lib/document/root.bib b/thys/Word_Lib/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Word_Lib/document/root.bib @@ -0,0 +1,5 @@ +@article{leijen01, + author = {Leijen, Daan}, + title = {Division and Modulus for Computer Scientists}, + year = 2001, + url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}} diff --git a/thys/Word_Lib/document/root.tex b/thys/Word_Lib/document/root.tex --- a/thys/Word_Lib/document/root.tex +++ b/thys/Word_Lib/document/root.tex @@ -1,52 +1,56 @@ % % Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) % % SPDX-License-Identifier: CC-BY-SA-4.0 % \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{tt} \begin{document} \title{Finite Machine Word Library} -\author{Joel Beeren, Sascha Böhme, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski,\\ - Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell} +\author{Joel Beeren, Sascha Böhme, Matthew Fernandez, Xin Gao,\\ + Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis,\\ + Daniel Matichuk, Thomas Sewell} \maketitle \begin{abstract} This entry contains an extension to the Isabelle library for fixed-width machine words. In particular, the entry adds printing as hexadecimals, additional operations, reasoning about alignment, signed words, enumerations of words, normalisation of word numerals, and an extensive library of properties about generic fixed-width words, as well as an instantiation of many of these to the commonly used 32 and 64-bit bases. In addition to the listed authors, the entry contains contributions by Nelson Billing, Andrew Boyton, Matthew Brecknell, Cornelius Diekmann, Peter Gammie, Gianpaolo Gioiosa, David Greenaway, Lars Noschinski, Sean Seefried, and Simon Winwood. \end{abstract} \tableofcontents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} +\bibliographystyle{abbrv} +\bibliography{root} + \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: