Handle Switch in Taclets w/o Transformer

[Drodt]

Intended Change

Instead of relying on the switch-to-if transformer, which may have some bugs, this PR attempts to handle switch statements purely in taclets.

The general approach is to mark the branch currently executed as the active-case.

Effect on Proofs

Name	Nodes (main)	Nodes (match-switch)	Nodes Diff	Branches (main)	Branches (match-switch)	Branches Diff
examples/standard_key/java_dl/switch/empty_switch_array_out_of_bounds_catch.key	275	250	-25	149	143	-6
examples/standard_key/java_dl/switch/large_switch.key	4410	3642	-768	2682	2478	-204
examples/standard_key/java_dl/switch/switch_in_switch.key	5215	2031	-3184	4376	1583	-2793
examples/standard_key/java_dl/switch/empty_switch_null_catch.key	308	275	-33	106	92	-14
examples/standard_key/java_dl/switch/empty_switch_array_out_of_bounds.key	398	372	-26	179	172	-7
examples/standard_key/java_dl/switch/while_and_switch.key	1237	1261	24	831	884	53
examples/standard_key/java_dl/switch/empty_switch_null.key	237	204	-33	79	65	-14
examples/standard_key/java_dl/switch/empty_switch.key	8	3	-5	9	4	-5
examples/standard_key/java_dl/switch/labeled_case.key	194	153	-41	86	82	-4

Plan

• Finish implementation

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml

Additional information and contact(s)

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