Re: [isabelle] Confusing behavior of a paired set comprehension

+1 vote for "feature".

Isabelle's treatment of bound variables is perfectly consistent with
mainstream functional programming languages like Haskell or ML:
Function abstractions may shadow existing names.

Prelude> :t \x -> \x -> x
\x -> \x -> x :: t -> t1 -> t1

fn x => fn x => x
val it = fn: 'a -> 'b -> 'b

Isabelle's pretty printer renames such repeated bound variable names
on the fly. This is a nice feature to improve readability:

term "%x x. x"
"%x xa. xa" :: "'a => 'b => 'b"

And it also prevents ambiguity, for example:

lemma "!!x. P x ==> ALL x. Q x"
apply (rule allI)

1. "!!x xa. P x ==> Q xa"

(In this case, "!!x x. P x ==> Q x" would simply be wrong, so it is a
very good thing that the renaming happens in this situation.)

- Brian

On Wed, Apr 4, 2012 at 12:43 PM, Jonas Wagner <jonas.wagner at> wrote:
>> No, a feature. Patterns may not contain repeated variables.
> +1 vote for "bug".
> The fact that Patterns may not contain repeated variables is perfectly fine.
> The fact that the first occurrence of a repeated variable is silently
> replaced by another variables is not fine.
> But that's just the option of an Isabelle Newbie who got his proof wrong due
> to a surprising feature ;)
> Best,
> Jonas

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