word_lib: re-sync with AFP; fix broken document

Also switched on document generation so we don't miss these in the future.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

word_lib: sync from AFP

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

Word_Lib: add from_bool_eqI

word-lib: strengthen ucast_less_ucast

word-lib: add upward cast monotonicity lemmata

word_lib: avoid shadowing existing lemma

word_lib: add new material from l4v to AFP; cleanup

word_lib: shorter, more automatic proofs

word_lib: word_eqI and word_eqI_solve methods

Improvements on initial version by Thomas Sewell

lib: add word lemma

Add of_nat_unat_le_mask_ucast: equality of words where one is wrapped with
of_nat (unat _).

cleanup: collect word lemmas

lib: add helper lemmas

Word_Lib: add ucast_shiftl_eq_0

Word_Lib: add masking lemmas from RISCV64 lookup proofs

lib: sync Word_Lib with AFP

lib: speed up word8_exhaust

Word_Lib: sync with AFP

Word_Lib: consolidate LemmaBucket and Lib lemmas into Word_Lib

lib/Word_Lib: import merge fixup from AFP

This commit keeps Word_Lib in sync with the AFP

lib/Word_Lib: sync with AFP

Isabelle2018 lib: Word_Lib

x64 crefine: prove several lemmas in Retype_C

To prove that retyping a TCB establishes the state relation for TCBs,
it is necessary to prove that the C FPU null state is always equal to
the Haskell FPU null state. This commit therefore includes some
machinery for maintaining the state relation for the FPU null state,
and repairs many proofs.

lib: add some word lemmas about sless, word_bits

lib: miscellaneous word lemmas

x64: clear some sorry proofs from CSpace_C

Also update some Haskell and abstract specs relating to IO ports.

lib: Word_Lemmas: sign_extended addition and ~~mask lemmas

lib: add generic lemmas from SELFOUR-584 updates

Mainly concerning word_ctz and enumeration_both.

lib: a more intuitive definition of sign_extend for words

Also includes some supporting lemmas useful in bitfield proofs.

word-lib: add some lemmas about sign extension

lib: generic/word/monad/hoare lemmas from SELFOUR-242 verification

Notably useful is hoare_vcg_lift_imp' which generates an implication
rather than a disjunction.

Monadic rewrite rules should be modified to preserve bound variable
names, as demonstrated by monadic_rewrite_symb_exec_l'_preserve_names.
Addressing this more comprehensively is left as a TODO item for the
future (see VER-554).

Expand eval_bool; add a method word_eqI_solve.

A number of proofs begin with word_eqI followed by some similar steps,
suggesting a 'word_eqI_solve' proof method, which is implemented here.

Many of these steps are standard, however a tricky part is that constants of
type 'nat' which encode a particular number of bits must often be unfolded.
This was done by expanding the eval_bool machinery to add eval_int_nat, which
tries to evaluate ints and nats.

Testing eval_int_nat revealed the need to improve the code generator setup
somewhat. The Arch locale contains many of the relevant constants, and they are
given global names via requalify_const, but the code generator doesn't know
about them. Some tweaks make them available. I *think* this is safe for
arch_split, as long as the proofs that derive from them are true in each
architecture.

Isabelle2017: update Word_Lib for RC0

* Various equalities from underlying HOL-Word have been reoriented.

* word_eqI is no longer rule_format.

* zdiff_zmod_* were renamed to mod_diff_*_eq.

lib: move some lemmas from bitfield proofs to word-lib

Removes all trailing whitespaces

Word_Lib: miscellaneous conditional injectivity rules

Word_Lib: add le_mask_shiftl_le_mask

lib: word and misc lemmas from SELFOUR-242 proofs

These precipitated out during cleanup.

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2016-1: update Word_Lib

Word_Lib now looks more like the current AFP entry, though there are
still some local modifications.

Word_Lib: lemmas about high bits w.r.t. mask operations

Revert SELFOUR-242: invert bitfield scheduler and optimise fast path

This reverts:
- a67b443ca5a1e4a8f4d4a7fe0757861e2a7898b5
"SELFOUR-242: update goal number based indentation in Fastpath_C"
- f704cf04044209df996ef6c22bc8ea52122a2c1e
"SELFOUR-242: invert bitfield scheduler and optimise fast path"

Verification confirmed functional correctness and refinement of the
system in this case. However, guarantees on thread scheduling and
fairness are not modeled in the current verification. Once this issue is
addressed, SELFOUR-242 will be re-examined.

SELFOUR-242: invert bitfield scheduler and optimise fast path

* Reverse the level 2 of the bitmap scheduler to move the highest priority
threads' level 2 entries into the same cache line as the level 1.
* Use the bitfield scheduler to make the fast path a more common occurrence.
* Change possibleSwitchTo to not invoke scheduler when the fast path would not
invoke it either (using implicit assumptions about the current thread being
the highest priority schedulable thread)

Word_Lib: lemmas comparing different word sizes

Word_Lemmas: NOT_mask_shifted_lenword

[rebased from https://github.com/seL4/l4v/pull/10]

word_lib: move unrelated lemmas out of Word_Lib into Lib

word_lib: AFP document setup

word_lib: run isabelle update_then for new style and fun

word_lib: use cartouches

lib: move Distinct_Prop out of Word_Lib

word_lib: Distinct_Prop cleanup

word_lib: move out unused HOL_Lemmas

manual levity into Word_Lemmas

word_lib: adjust theory dependencies

lib: closure for Word_Lib and own session

word_lib: AFP naming conventions