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.)
On Wed, Apr 4, 2012 at 12:43 PM, Jonas Wagner <jonas.wagner at epfl.ch> 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 ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and