Il-to-Il: General otherwise elimination [archival branch]

[nomeata]

This is an IL pass that eliminates general uses of otherwise; general in the sense that it can handle overlapping LHS like

relation Step: expr -> expr

rule Step_is_null1:
  (is_null 0) -> True
rule Step_is_null2:
  (is_null n) -> False
  -- otherwise

or rules referring to predicates:

relation Even : Even expr
rule Even_0:
  Even 0
rule Even_SS:
  Even (S (S n))
  -- Even n

rule Step_is_even1:
  (is_even n) -> True
  -- Even n
rule Step_is_even2:
  (is_even n) -> False
  -- otherwise

It uses the apartness check (#16) to clean up the generated rules a bit. It could do more systematic clean up to introduce negated boolean premises in the restricted case, but doesn’t do this yet.

This PR is not for merging, but merely for archival reasons, as Andreas says we actively don’t want to support otherwise in the general form, and don’t want the necessary IL changes (a general form of negated premise).

Instead, I understand he envisions a check in the IL checker to enforce the necessary invariants (“all rules before otherwise have either syntactically equal or obviously apart LHS, and those that have equal LHS only have boolean premises”), and then a IL-to-IL pass that handles precisely those cases.

[nomeata]

So, is it worth reviving this approach?