Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning



Am 22/03/2013 08:15, schrieb C. Diekmann:
> Hi,
> 
> I found a very counterintuitive problem with tuples in set notation.
> 
> I want to define some sort of reflexive closure.
> When I write {(v, v). v ∈ {''a'', ''b''}} I hope to get {(''a'',
> ''a''), (''b'', ''b'')}. However, I found that
> lemma "(''a'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)
> and even
> lemma "(''xyz'', ''b'') ∈ {(v, v). v ∈ {''a'', ''b''}}" by(simp)
> 
> With `declare[[show_types]]`, I traced the problem and found:
> lemma "{(v, v). v ∈ {''a'', ''b''}} = {(x, y). y∈{''a'', ''b''}}" by simp
> My set is actually translated into {(va∷'a, v∷char list). v ∈ {''a'', ''b''}}

As Christian already said, this is the explanation. Just like in functional
programming, patterns must be linear. Unlike in FP, Isabelle silently translates
your non-linear pattern into a linear one (for set comprehensions only). It
should of course be rejected but at the time I was too lazy to implement this
(it would have meant going to the ML level). Of course these days the philosophy
is still to accept it but use the right interface to warn the user that what he
typed is not what he got and he better beware ;-)

Tobias

> Why does this happen?
> Why wasn't there even some warning that a new variable `va` was introduced?
> 
> 
> Regards
>   Cornelius
> 




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