It allows one to declare a relation well-founded without need to prove it

As a side-effect, it does not require to import `relations.WellFounded`

See issue #626

Update oracles

Add elimination also in Alt-Ergo >= 2.4.0 and Z3 >= 4.4.0

- added break and continue
- added range with one, two or three argument(s)
- added slice (`list[i1:i2]`)
- added negative index (`list[n], with -len(list) ≤ n < len(list)`)
- added lists methods:
  - `list.append(n)`
  - `list.pop()`
  - `list.clear()`
  - `list.sort()`
  - `list.reverse()`
- added `is_permutation(list1, list2)` predicate
- added assignment operators `+=`, `-=`, `*=`, `//=`, `%=`
- functions can now return `bool` and `list`

fix pre-condition on signed division

give values for constants in each clone

Makes both signed and unsigned operations, which have
slightly different pre-conditions.

Further improvement needed: overflow checks are still
using functions `to_int` or `to_uint`, which are not
suitable for SMT solvers with bit-vector support.

This avoids proof differences in examples later on.

fix also isabelle realization checksums, both for 2018 and 2019 versions

Suitable for SMT solvers with BV support, but not for others: need to add definitional axioms and realize them in Coq and Isabelle

When defined as a `val function` the postcondition of the program function
`make` is just `result = make n v`, referring to the logical function `make`.
But the equality cannot be proven because array equality is not defined.

To facilitate proofs about results of the program functions `make`, this
commit separates the definitions of the logical function from the program
function `make`, so that the postconditions of the program function `make`
refer to the properties of the resulting arrey.

Yannick Moy authored Aug 24, 2020 and Benedikt Becker committed Sep 08, 2020

This entails creating the modules for conversions between these and smaller
bitvectors, as well as to the larger (and newly created) 256-bit bitvector
for verifying absence of overflows on operations over 128-bit bitvectors.

Change-Id: I6089b63b7c37c6cc6b00ab13795e2edeb8b048df

was missing a precondition because the contract was written *after*
the function body, not before