Get all (incl. -t1 tests) up to src/boss building w/tight-equality

Get core HOL to build with new definition of "by"

Progress with github issue #407

patternMatchesLib: implement flattening

Also implement general (non boolean) lifting and extending the input as
necessary auxiliary functionality.

patternMatchesLib: further cleanups

- restructure some proofs in patternMatchesTheory
- provide additional selftest
- minor improvements to nchotomy computation
- provide equality version of PMATCH_IS_EXHAUSTIVE_FULL_CONSEQ_CHECK
- rename PMATCH_IS_EXHAUSTIVE_FULL_CONSEQ_CHECK ->
PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK
- remove patternMatchesExamples.ML, since it got replaced by
selftest.sml and proper documentation is nearly ready

patternMatches: remove dead code

Remove old version of definitions and lemmata accidentilly left by
6c1bd42517e3224fca860aabc5bf040af7cc455e in patternMatchesScript.

patternMatchesLib: improve lifting

The lifting of pmatch case-expressions to the next boolean level was not
implemented well. It was rather slow, there was poor support for rows
with overlapping patterns and variable names were not chosen nicely.

This commit reimplements PMATCH_LIFT_BOOL_CONV and PMATCH_TO_TOP_RULE.
As part of this reimplementation, checking for exhaustiveness got
improved. In this process PMATCH_IS_EXHAUSTIVE_CONSEQ_CONV got renamed
to PMATCH_IS_EXHAUSTIVE_FULL_CONSEQ_CHECK (since it is no consequence
conversion). However, usually the new PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK
should be used instead.

Fix pre-boss theories in light of pat_assum renaming

Start on Absyn-level approach to PMATCH-parsing

Code for new style pattern-match parsing

Syntax as described in github issue #286 parses.

Examples:

> ``case x of 0 => 3 | SUC n when n < 10 => n + 1``;
val it =
``PMATCH x
[PMATCH_ROW (λ_. 0) (K T) (λ_. 3);
PMATCH_ROW (λn. SUC n) (λn. n < 10) (λn. n + 1)]``:
term
> Datatype `tree = Lf | Nd tree 'a tree`;
<<HOL message: Defined type: "tree">>
val it = (): unit
> ``case t of Lf => 0 | Nd t1 x t2 => x + f t1``;
val it =
``PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,x,t2). Nd t1 x t2) (K T) (λ(t1,x,t2). x + f t1)]``:
term
> ``x + case t of Lf => 0 | x .| Nd t1 x t2 => f t1``;
<<HOL message: inventing new type variable names: 'a>>
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λx. Nd t1 x t2) (K T) (λx. f t1)]``:
term
> ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 => f t1``;
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (K T) (λ(t1,t2). f t1)]``:
term
> ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 when g t2 > 6 => f t1``;
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (λ(t1,t2). g t2 > 6)
(λ(t1,t2). f t1)]``:
term

I think we do still need a separate notation to indicate no variables
are to be bound, as

| .| pat => rhs

won't work when .| is an infix. Maybe

| ..| pat => rhs

This would be needed in a situation where all of the variables in pat
have to be read as free (referring to variables occurring in a wider
context).

patternMatches turns on pmatch, adds .| infix

patternMatches: remove unicode in src

pattern_matches: add support for computeLib

move "pattern_matches" examples to "src"