Re: [isabelle] Happy New Year with Free/Bound Variables
On 01/02/2013 01:54 PM, Gottfried Barrow wrote:
just a remark: I think what Andrej Bauer is writing about is different
from what is usually discussed on the Isabelle mailing lists. I don't
think that anybody ever thought or claimed that Isabelle logically
equates a formula with its universal closure. The discussions are
usually about: what is the exact meaning if I write something like
On 12/30/2012 7:50 AM, Alfio Martini wrote:
Anyway, I finish this e-mail by posting the link from a post by Andrej
Bauer on the role
of free and bound variables. This topic seems to be the one which was
topics most discussed in the list during this year.
"Free variables are not "implicitly universally quantified"!
lemma "P x"
where "P" is some formula with the free variable "x". In this context, a
helpful answer is that free variables are implicitly universally
quantified. A more cautious answer would be something like:
When writing a top-level lemma statement like 'lemma "P x"' Isabelle
behaves as if the free variable "x" was universally quantified at the
meta-level for almost all purposes ;)
An answer to what question? What algorithm do you mean? And how do you
relate this article to the topic of "free/bound variables"?
(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:
That I didn't learn about it from those other
group of people is a bad mark against them.
What is that supposed to mean?
happy new year,
This archive was generated by a fusion of
Pipermail (Mailman edition) and