Email Gateway (Aug 18 2022 at 09:51): Email Gateway (Aug 18 2022 at 09:51):From: Lawrence Paulson <lp15@cam.ac.uk>
The collapsing of ALL x. P(x) to All(P) is a side-effect of the way
that all binding syntax is handled in Isabelle. Although it can be
annoying, here All(P)-->All(P) tells you that (ALL x. P(x)) and (ALL
y. P(y)) are actually the same formula in Isabelle.
Larry Paulson
Email Gateway (Aug 18 2022 at 09:52):From: Lawrence Paulson <lp15@cam.ac.uk>
Here (ALL x y. P(x, y)) is internally All(%x. All(%y. P x y)), which
can be collapsed to All(%x. All(P x)), so you see (ALL x y. P(x, y)).
The "collapsing" is actually called eta-contraction and it is
performed by the rewriter.
[Note to Isabelle/HOL users: in FOL, P(x,y) is what you would write
as P x y. Thus this example behaves differently in Isabelle/HOL,
where P(x,y) abbreviates P(Pair x y) and the eta-contraction is no
longer possible.]
Larry Paulson
Email Gateway (Aug 18 2022 at 09:52):From: Makarius <makarius@sketis.net>
This looks like you don't have Poly/ML installed properly for your
platform. Since this is ppc-darwin we already provide precompiled
packages for HOL etc. on the Isabelle download site. Try to use these
before attempting to install any operation system packages for Poly/ML,
ProofGeneral etc. that occasionally show up elsewhere.
This should enable you to run plain isabelle tty sessions at the least.
Getting a version of (X)Emacs that works with ProofGeneral is a different
issue.
Makarius
Email Gateway (Aug 18 2022 at 09:57):From: Joao Marcos <jmarcos@dimap.ufrn.br>
Dear ALL x. IsabelleExpert(x):
Sometimes Isabelle returns outputs that I see as somewhat unexpected...
For instance, suppose I want to show that the name of a universally
quantified variable can be changed, and write:
Goalw [iff_def] "(ALL x. P(x)) <-> (ALL y. P(y))";
I would have expected then the output to be a goal such as:
((ALL x. P(x))-->(ALL y. P(y))) & ((ALL y. P(y))-->(ALL x. P(x)))
but Isabelle gives me the following:
Level 0 (1 subgoal)
((ALL x. P(x))<->(ALL y. P(y)))
WHY??
Suppose, moreover, I want to prove that contiguous universal
quantifiers can be exchanged, and write:
Goalw [iff_def] "(ALL x. (ALL y. P(x,y))) <-> (ALL y. (ALL x. P(x,y)))";
Here the output is:
Level 0 (1 subgoal)
(ALL x y. P(x, y)) <-> (ALL y x. P(x, y))
WHY does the system exchange some but not all instances of P(x,y) for
P(x), and uses "All" to write the new goal??
I note that these things only occur when I use Goalw plus a rewrite
rule such as iff_def, but not if I simply use Goal to prove my
theorem. Why?
Thanx in advance for the clarification,
JM
Last updated: May 03 2024 at 08:18 UTC