[isabelle] Using abbreviations with case expressions



Is it unreasonable to expect this to work?

theory Scratch imports Main begin

abbreviation (input) emptystring :: string ("ε")
  where "ε ≡ []"

term "case s of ε ⇒ True | c # cs ⇒ False"

*** Error in case expression:
*** Not a datatype constructor: Scratch.emptystring
*** In clause
*** emptystring ⇒ True
*** Failed to parse term
*** At command "term"

Apparently the parse translation for case expressions happens after
processing notation (e.g. "[]" -> "List.Nil" or "c # cs" -> "List.Cons
c cs") but before processing abbreviations (e.g. "emptystring" ->
"List.Nil :: string"). Could this be changed so that abbreviations are
expanded earlier?

I suppose I could work around this problem by using something like this:

syntax emptystring :: logic ("ε")
translations "emptystring" == "CONST Nil :: string"

but the "syntax" and "translations" commands seem to be considered a
bit "old-style" nowadays, or at least a bit too low-level to be
considered best practice.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.