Identify and implement relevant proof rules

[mattulbrich]

For a usable tools, there must be a set of sensible proof rules present.

That here is more an umbrella issue for a lot of smaller items.

That would include:

• a cut rule
• a replacewith rule
• quantifier instantiation and
• quantifier skolemisation
• integer expression simplification
• heap expression simplification
• a working integrated lemma mechanism

The simplification rules must not be atomic steps but sequences of individual rewritings.

[sgrebing]

Instead of cut: better add Hypothesis, case distinction, cut direct, induction?

[JonasKlamroth]

• working lemmas introduced with 153fb12
• quantifier instantiation for forall quantifier, addHypothesis and case distinction added in 055ee81
• @mattulbrich what do mean by integer expression simplification? things like a + 0 == 0 or a more sophiticated rule which is able to simplify arbitrary terms?

[mattulbrich]

@JonasKlamroth. Actually: both. Anything which helps. I do not really know if some "normalisation" technique would help tremendously or if a handful of eager rules will do the trick. I believe that x + (-1)*x + 0*y should automatically be simplified to 0.

[JonasKlamroth]

basic integersimplification added in 5ec4265

[JonasKlamroth]

skolemization rule added in 30734d5