Email Gateway (Aug 18 2022 at 19:29): Email Gateway (Aug 18 2022 at 19:29):From: Giuliano Losa <giuliano.losa@epfl.ch>
Hello,
the following definition is interpreted in a confusing way:
def ident :: "'a set => ('a \times 'a) set"
where "ident S = {(x,x) . x \in S}"
the command "thm ident_def" yields
ident ?S \<equiv> {(xa, x). x \<in> ?S}
Should this be considered as a bug?
Giuliano
Email Gateway (Aug 18 2022 at 19:29):From: Tobias Nipkow <nipkow@in.tum.de>
No, a feature. Patterns may not contain repeated variables.
Tobias
Email Gateway (Aug 18 2022 at 19:29):From: Ramana Kumar <rk436@cam.ac.uk>
In case it's not obvious, you probably want something like "ident S =
{(x,y). x \in S \and (x = y)}".
Email Gateway (Aug 18 2022 at 19:29):From: Brian Huffman <huffman@in.tum.de>
I think what you really want is "ident S = {(x, x) | x. x \<in> S}".
(This is actually a syntactic abbreviation for "{y. \<exists>x. y =
(x, x) \<and> x \<in> S}".)
Email Gateway (Aug 18 2022 at 19:29):From: Jonas Wagner <jonas.wagner@epfl.ch>
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
Email Gateway (Aug 18 2022 at 19:29):From: Brian Huffman <huffman@in.tum.de>
+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.
(ghci)
Prelude> :t \x -> \x -> x
\x -> \x -> x :: t -> t1 -> t1
(polyml)
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)
(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.)
Email Gateway (Aug 18 2022 at 19:30):From: Tjark Weber <webertj@in.tum.de>
On Thu, 2012-04-05 at 11:25 +0200, Brian Huffman wrote:
Isabelle's treatment of bound variables is perfectly consistent with
mainstream functional programming languages like Haskell or ML:
Function abstractions may shadow existing names.(ghci)
Prelude> :t \x -> \x -> x
\x -> \x -> x :: t -> t1 -> t1(polyml)
fn x => fn x => x
val it = fn: 'a -> 'b -> 'b
True, but the original example was "ident S = {(x,x) . x \in S}". Hence
I believe the following behavior to be more relevant:
(polyml)
fn (x,x) => x;
Error-x has already been bound in this match Found near fn (x, x) => x
Static Errors
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 19:30):From: Makarius <makarius@sketis.net>
This thread got split over two isabelle mailing lists for unknown reasons,
so I repeat my answer from isabelle-dev here once more:
Things like %x x x x. x and fix x fix x fix x have "x = x" are perfectly
legal and behave quite uniformly for many years, i.e. with little
surprise to people who have got acquainted with Isabelle scoping rules.
To make things even more simple for beginners, the Prover IDE markup
protocol already indicates the internal scopes in the source text. E.g.
when using CONTROL/COMMAND with mouse clicks, one can explore the
internal bindings. It is only a small addition to the display engine to
make variable scopes immediately visible in the source text, like
Netbeans would do for Java for example when the user moves or hovers
over the text.
In contrast, lots of warning messages are old-school TTY technology, and
in Proof General the channel for that gets easily overloaded so that the
user is switching into SPAM mode.
Jonas, since you are from EPFL you are probably familier with the Scala
scoping, which is often more harsh in forbidding plain nesting of scopes
that would be just fine in the ML, HOL, Haskell tradition. I find the
Scala behaviour quite confusing at times.
Anyway the IDE solution sketched above will make things easier for
beginners without having to reconsider traditions that are established for
decades in certain communities.
Makarius
Email Gateway (Aug 18 2022 at 19:30):From: Brian Huffman <huffman@in.tum.de>
Good point.
So while "Collect (split (%x x. x \<in> S))" is clearly valid input,
the status of the equivalent-according-to-the-parser "{(x, x). x \<in>
S}" is not so clear.
It might be possible to set up an ML parse translation for tuple
abstractions (see section "Tuple syntax" in Product_Type.thy for how
things are implemented now). The parse translation could produce a
syntax error if any variable names are repeated.
I'm not sure whether it would be worth the trouble to implement it,
though, unless more people ask for it.
Email Gateway (Aug 18 2022 at 19:30):From: Makarius <makarius@sketis.net>
Changing ML parse translations is always a very delicate process, and
actually ongoing for several years. Instead of added new features, there
is presently an attempt to make case syntax conceptually sound, possibly
also list comprehensions.
This is motivated again by the IDE markup, because that reveals tiny
conceptual mishaps in the existing syntax.
Makarius
Email Gateway (Aug 18 2022 at 19:30):From: Makarius <makarius@sketis.net>
Just some more fun with patterns in ML.
This is nothing special beyond infixes and symbolic names:
fun * * = + *
Here are separate scopes for function vs. arguments:
fun x x = x
It actually makes some sense here:
fun foo {foo, bar} = foo
fun bar {foo, bar} = bar
Makarius
Last updated: Apr 26 2024 at 04:17 UTC