Basic Theory of Sets

[WolframPfeifer]

This PR adds a basic theory of (polymorphic) sets with cardinality to KeY. The rules are taken from the LocSet rules with the obvious adaptations (removal of Object/Field in favor of the generic sort T). However, I tried to keep the rule base minimal (20 rules at the moment), the rules are selected pragmatically (what was needed for a recent example) without any further thoughts about completeness.

In its current state, this PR partially solves #3690: At the moment, polymorphic sorts cannot be used in JML.
I don't really have an idea what the syntax should be on JML level, and think that we should discuss this before I try to implement anything.

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base

Ensuring quality

• I added new test case(s) for new functionality: Small (auto-)provable lemma added to RunAllProofs (setExample.key)

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[wadoon]

Is it possible to define type alias? typealias locset = Set<[Tuple<[any,field]>]>?