Re: [isabelle] Using abbreviations with case expressions



On Wed, Jan 5, 2011 at 12:17 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> 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.

Ok, I had a feeling that this would be tricky to implement. I don't
have any critical need for this feature or anything, I just tried it
on a whim and was a bit surprised by the error message I got.

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

No, notation won't work in this particular example, because the
abbreviation "emptystring" has a more specific type than the constant
"Nil" that it stands for.

It seems that "syntax" + "translations" is the right way to go for
this kind of thing.

Using those commands seems a bit weird though, simply because they use
old-style input syntax (similar to "consts" or "defs") instead of the
new-style (like "notation"). Modernizing the input syntax of the
"syntax" and "translations" commands would make me feel more confident
that these will continue to be fully supported as user-level commands
in the future.

- Brian





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