Bob Rubbens (Feb 23 2025 at 07:51): Bob Rubbens (Feb 23 2025 at 07:51):Isabelle doesn't seem to have a simplification rule for:
(i :: nat) < j ⟹ Max {i..<j} = j - 1
Is this rule missing? Do you think it could/should/shouldn't be added to Isabelle? It's not a difficult fact to prove but it's useful to have, especially in combination with upt. There also doesn't seem to be a rule for the combination of Max and upto.
Last updated: Mar 09 2025 at 12:28 UTC