Manuel Eberl (Feb 10 2021 at 12:38): Manuel Eberl (Feb 10 2021 at 12:38):There's a Haskell extention that allows multiway ifs:
if | x < 3 -> "small"
| x < 7 -> "medium"
| otherwise -> "large"
It might be nice to have something like that in Isabelle to avoid some of those clunky nested if then else constructs.
Not sure if it's really worth it but one could try?
Mathias Fleury (Feb 10 2021 at 12:43):I tend to use case for that, even if it has a slightly different semantics…
case (x < 3, x < 7) of
(True, _) => "small"
| (_, True) => "medium"
| _ => "large"
Possible solution:
syntax
"_multiway_if" :: "multiway_if ⇒ 'a" ("if {//(2 _)//}" [12] 62)
"_multiway_if_clause" :: "bool ⇒ 'a ⇒ multiway_if_clause" ("(2_ ⇒/ _)" 13)
"_multiway_if_cons" :: "multiway_if_clause ⇒ multiway_if ⇒ multiway_if" ("_;//_" [13, 12] 12)
"_multiway_if_final" :: "'a ⇒ multiway_if" ("otherwise ⇒ _")
translations
"_multiway_if (_multiway_if_cons (_multiway_if_clause b x) y)" == "CONST If b x (_multiway_if y)"
"_multiway_if (_multiway_if_final x)" => "x"
term "if {p ⇒ y; q ⇒ z; r ⇒ u; otherwise ⇒ x}"
Possible other syntax:
f x = if {x ≥ 0 ⇒ 1; x ≤ 0 ⇒ -1; otherwise ⇒ 0}
f x = (if x ≥ 0 ⇒ 1 | x ≤ 0 ⇒ -1 | otherwise ⇒ 0)
f x = (1 if x ≥ 0; -1 if x ≤ 0; 0 otherwise)
One could also replace if with case or drop it entirely, or replace otherwise with else, replace parentheses with bracets, semicolon with "|" etc.
Not sure how to make the translations work for output as well.
Manuel Eberl (Feb 10 2021 at 14:32):Okay this works for output as well, but it has the disadvantage of also printing if b then x else y as if {b ⇒ x; otherwise ⇒ y}. One would have to tweak it a bit more to prevent that.
nonterminal if_clauses and if_clause
syntax
"_if_block" :: "if_clauses ⇒ 'a" ("if {//(2 _)//}" [12] 62)
"_if_clause" :: "bool ⇒ 'a ⇒ if_clause" ("(2_ ⇒/ _)" 13)
"_if_final" :: "'a ⇒ if_clauses" ("otherwise ⇒ _")
"_if_cons" :: "[if_clause, if_clauses] ⇒ if_clauses" ("_;//_" [13, 12] 12)
syntax (ASCII)
"_if_clause" :: "[pttrn, 'a] ⇒ if_clause" ("(2_ =>/ _)" 13)
translations
"_if_block (_if_cons (_if_clause b t) (_if_final e))"
⇌ "CONST If b t e"
"_if_block (_if_cons b (_if_cons c cs))"
⇌ "_if_block (_if_cons b (_if_final (_if_block (_if_cons c cs))))"
"_if_block (_if_final e)" ⇀ "e"
term "if {P ⇒ x; Q ⇒ y; R ⇒ z; otherwise ⇒ bla}"
Last updated: Nov 07 2025 at 16:23 UTC