Make \sameUpdateLevel the default

[Drodt]

Intended Change

If a rule has an \assumes or \add part, the term in the \find and the other parts should have the same updates applied to them for soundness, at least in most cases. To ensure this, the rules need the \sameUpdateLevel annotation, it is not the default. Recently, we found a number of bugs due to missing \sameUpdateLevel, e.g. #3891 and #3490.

This PR changes the default as discussed in the KaKeY meeting on the 24th of April 2026: By default, any rule with \assumes or \add automatically has the SAME_UPDATE_LEVEL restriction, unless \ignoreUpdateLevel is added.

This makes a number of unsound rules sound (while going over the rules, I saw many where \sameUpdateLevel was missing. It also affects the one step simplifier: Some rule were not handles by OSS because the had the \sameUpdateLevel annotation but no \assumes or \add; that seemed incorrect.

Because this is a breaking syntax change, we should consider it for 3.0.

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

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: Ran the tests.
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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

[unp1]

Thanks a lot! 👍

Two minor issues to discuss:

• the logic printer nows prints for pure rewrite rules (w/o add and assumes) the \ignoreUpdateLevel flag. E.g. swicth on that taclets are shown for inner nodes, apply eqSymm on an equation
• Should we keep the token SAMEUPDATELEVEL and the grammar rule so that existing proofs with included rules do not break

[Drodt]

Both are fixed now. Now the application restrictions still print as \sameUpdateLevel, which was the easier path (and makes it easier to see which rules were missing them).

[unp1]

Thanks!