lib: avoid internal index names

The lemma set `exception_set_finite` contained the members
`exception_set_finite_1` and `exception_set_finite_2`. The `_1`/`_2`
suffix clashes with the internal `(1)` suffix for lemma set references,
which in some code paths is internally represented as `_1`, leading to
an error message.

Curiously this error message only occurs when the proof is run
single-threaded, so it has gone unnoticed for quite some time.

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

lib: Isabelle2020 update

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

lib: add lemmas from RISCV64 theories

Some improved ccorres lemmas, dealing with throw and catch, and usual
assortment of misc list/set/map lemmas.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

lib: add ML_goal command

Sometimes we want to prove a fact, but the fact is painful or
error-prone to type out manually. In these cases, we'd like to construct
the goal fact using ML and then immediately enter a proof block.

Previously, we could achieve something like this through careful use of
`Thm.trivial` and `schematic_goal`, but this would clutter up the ML
namespace and wouln't handle meta conjuncts (`&&&`). The new `ML_goal`
command addresses both of these issues.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>

lib: remove eq_restrict_map_None from the simp set

Hotfix for a7ed68e75db, which moved some lemmas from X64 Move_C.thy into
Lib. `eq_restrict_map_None` being in the simp set caused several
breakages across other arches.

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>

x64 crefine/lib: move word lemmas out of Move_C into Word_Lemmas_64_Internal

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>

licenses: convert license tags to SPDX

Collect abstract lemmas in Refine

Create ArchMove_R.thy for transporting arch specific lemmas (and generic
lemmas that are used somewhat specifically by one architecture) to theory
files before Refine.

Create Move_R.thy as an arch generic Refine theory file for transporting
generic lemmas to theory files before Refine.

Also delete some lemmas that have existed earlier already or are not
needed.

Rename Move.thy in CRefine to Move_C.thy for consistency.

lib: migrate distinct_map_enum into Lib

lib: add helper lemmas

lib: add graph_of_SomeD

lib: move up library lemmas from RISCV64 and X64

lib: add option_Some_value_independent

lib: move int bitwise lemmas from NatBitwise to Lib

NB: this now imports HOL-Word into Lib and Lib in turn
into NatBitwise.

global: isabelle update_cartouches

lib: update for Isabelle 2019

lib: move "tl_nat_list_simp" up.

lib + sysinit: whitespace cleanup; renamed lookup_obj

Word_Lib: consolidate LemmaBucket and Lib lemmas into Word_Lib

Isabelle2018: Lib update

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

lib: some simple rules about rtrancl/rtranclp.

These generalise trancl_id from HOL to cover rtrancl and rtranclp.

Also improve one minor proof.

lib: Replace subseq->match abbreviation.

The subseq_abbreviation mechanism was a useful way of quoting some of a
definition or term, specialised to the case of left-associated sequences.

Lambda abstractions are now handled better.

The previous subseq mechanism required some generalisations. It is now replaced
by match_abbreviation, which is a more general approach.

The match mechanism picks a term, can select a matching subterm, and can
rewrite the selected term based on pattern matching also. The new mechanism
can cover all the cases of the previous one, as shown in examples.

lib: Subseq_Abbreviation, quote subsequence terms.

It's annoying that, given automatic definitions (such as we have
with the Haskell translator and C parser), there's no way to capture
a few lines of them.

This mechanism allows you to add an abbreviation for some subsequence of
elements, found somewhere in a theorem, where a sequence is defined by its
constructor and the start and end points are matched by pattern matching.

lib: add methods for extracting conjuncts from the conclusion

Isabelle2017: update lib for RC0

* ML Proof_Context.fact_alias renamed to alias_fact.

* Named_Target.init removed redundant parameter.

* Simplified Greatest, removed GreatestM.

* Introduced thm_node type in proofterm.ML.

Isabelle2017: remove String_Compare

This was a workaround for an Isabelle2016-1 performace regression, and
is no longer required.

Add some methods to trym.

Add "Try Methods" mechanism trym.

Like try0/try but extensible by new methods. Methods must currently
be single tokens, however Eisbach makes it easy to install such
abbreviations.

remove most tab characters

Add command/keyword 'value_abbreviation'.

This computes a value (like the existing value keyword) and also saves
the result of that computation as an abbreviation.

This will be useful in CRefine etc to give names to magic numbers that
derive from configuration variables/constants.

Removes all trailing whitespaces

x64: ArchVSpaceLookup_AI: prove vs_lookup_pages1_wellformed_order

Show that there is a measure on vs_refs, on which vs_lookup_pages1 is
strictly monotonically increasing.

We also prove various lemmas relating vs_lookup and vs_lookup_pages, and
valid_arch_objs.

There are many things previously proved in ArchRetype_AI and
ArchDetype_AI that are now broken because Xin's work overwrote some
things I also proved in ArchVSpace_AI. I'm not fixing them here.

Isabelle2016-1: configure c-parser with faster string comparisons

Isabelle2016-1: fix proofs involving UNION

SUPREMUM changed from a definition to an abbreviation.

A number of proofs that previously used blast, fastforce or auto to
solve goals involving UNION, now either fail or loop. This commit
includes various ad-hoc workarounds.

Isabelle2016-1: update references to renamed constants and facts

lib: include NICTA_Tools in Lib (ASpec image and friends)

(VER-587)

lib: make CCorres_Rewrite available in CRefine and friends

word_lib: move unrelated lemmas out of Word_Lib into Lib

word_lib: Distinct_Prop cleanup

word_lib: move out unused HOL_Lemmas

word_lib: adjust theory dependencies

lib: remove duplicate definition of `find`

lib: closure for Word_Lib and own session

lib: start disentangling spaghetti word dependencies

Isabelle2016-RC0 up to WordLemmaBucket modulo Eisbach

fewer warnings

remove warnings

ported lib/* theories to Isabelle2014-RC0

Port AutoCorres to Isabelle 2014-RC0

Import release snapshot.