Re: [isabelle] Using abbreviations with case expressions



Hi Brian,

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 don't think this is so easy. Abbreviations are unfolded only after type inference (being typed is one of their main advantage over old translations). Translating case expressions later would mean that the representation that exists before that is typable in some way. This is probably not impossible, but requires some non-trivial rethinking of how the translation works.

In your particular example, could you just use "notation"?

Alex





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