Stream: General

Topic: Single rule expected in cases proof

Gergely Buday (Nov 17 2023 at 11:19):

I have the datatype definition

datatype 'a maybe = Nothing | Just 'a

and when I ask for its case rule:

thm maybe.case

I get

  (case Nothing of Nothing ⇒ ?f1.0 | Just x ⇒ ?f2.0 x) = ?f1.0
  (case Just ?x2.0 of Nothing ⇒ ?f1.0 | Just x ⇒ ?f2.0 x) = ?f2.0 ?x2.0

and when I try to use it as a case rule:

proof (cases a rule: maybe.case)

I get the error message

Single rule expected

How can I do a case distinction proof for this datatype?

Simon Roßkopf (Nov 17 2023 at 11:30):

IIrc the rule is (somewhat confusingly) called maybe.exhaust. The cases method should be able to figure out the correct rule without you providing a rule as well (proof (cases a)).

Simon Roßkopf (Nov 17 2023 at 11:32):

(Also if your datatype is not just an example, consider using theoption type from the library)

Wolfgang Jeltsch (Nov 17 2023 at 15:25):

Let me add that the rule called maybe.cases is actually a split rule, which you can use for the split: parameter of the simplifier.

Last updated: Nov 16 2025 at 20:22 UTC