Email Gateway (Aug 19 2022 at 13:25): Email Gateway (Aug 19 2022 at 13:25):From: Moa Johansson <moa.johansson@chalmers.se>
Hi,
I'm currently porting some functionality from the HipSpec lemma discovery system into Isabelle. I have run into a small problem:
What is the proper way of "lifting" the variables in a theorem to meta-variables?
I.e. when the theorem P x = Q y has been proved, I need to convert all Frees (here let's assume they are x,y) to Vars, getting P ?x = Q ?y.
This happens automatically when performing proofs interactively. Basically, I think I want to have almost the functionality of the function Goal.prove, but as this raises an error when the tactic fails it doesn't quite fit.
Seems like this should be quite simple to do, perhaps this is what Thm.generalize is for? If so, what are its expected arguments? Seems like the first two are lists of all the type-variable and variable names we want to lift, but what is the int?
Grateful for tips!
Moa
Email Gateway (Aug 19 2022 at 13:25):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Moa,
Am 31.01.2014 um 17:11 schrieb Moa Johansson <moa.johansson@chalmers.se>:
I'm currently porting some functionality from the HipSpec lemma discovery system into Isabelle.
Great!
Seems like this should be quite simple to do, perhaps this is what Thm.generalize is for? If so, what are its expected arguments? Seems like the first two are lists of all the type-variable and variable names we want to lift, but what is the int?
You might want to have a look at "Drule.generalize". It provides a slightly higher-level interface, without the mysterious "int".
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 13:25):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t recognise much in the code any more, but you could consider Drule.export_without_context.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:25):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Moa,
an even higher-level interface that also works in a localized setting is
the following:
Proof_Context.export names_ctxt ctxt
Here ctxt is the context in which your theorem lives (in particular the
one that knows about free variables that are not really free but e.g.,
fixed by a locale). The second context (names_ctxt) is the enriched
version of ctxt where the variables to be exported have been declared
(e.g., via names_ctxt = Variable.declare_thm thm ctxt).
Dmitriy
Email Gateway (Aug 19 2022 at 13:25):From: Makarius <makarius@sketis.net>
Not that one again: any of the "without_context" operations are even worse
than the "global" ones. That is anncient legacy.
We have official type Proof.context with various elementary operations to
fix variables and export results since about 1999. The "implementation"
manual explains that in section 6.1 with various examples.
Makarius
Email Gateway (Aug 19 2022 at 13:25):From: Makarius <makarius@sketis.net>
On Fri, 31 Jan 2014, Moa Johansson wrote:
What is the proper way of "lifting" the variables in a theorem to
meta-variables? I.e. when the theorem P x = Q y has been proved, I need
to convert all Frees (here let's assume they are x,y) to Vars, getting P
?x = Q ?y.
Note that "lifting of variables" has a special meaning in Isabelle
terminology, according to Larry. The "implementation" manual section
2.4.2 explains that to some extent, but you won't need that here.
Above, the question is where x and y were coming from. Just using
undeclared Free variables causes lots of headaches -- one needs to
understand both the normal Isabelle context discipline and what happens
without that to get things work.
It is easier to rely on the normal context discipline by default, and
trust that this things work (they had more than a decade to mature).
This happens automatically when performing proofs interactively.
This is because a statement like
lemma "x = x"
has an implicit "eigen context" around it
lemma
fixes x :: 'a
shows "x = x"
So you state something for fixed x :: 'a, and get the result for arbitrary
?x :: ?'a (the type generalization is subject to Hindley-Milner
polymorphism).
Basically, I think I want to have almost the functionality of the
function Goal.prove
See implementation manual section 6.3 on Goal.prove. It allows you to
provide fixes and assumes just like a toplevel statement, but that needs
to be explicit in Isabelle/ML. You can also build up the context
separately, and export proven results from it.
but as this raises an error when the tactic fails it doesn't quite fit.
I don't understand that. It seems to refer implicitly to a particular
approach used here. Do you want to use local variables within a tactic?
Then just fix them, and export whatever you prove, and they become
schematic.
Seems like this should be quite simple to do, perhaps this is what
Thm.generalize is for?
Thm.generalize is a primitive inference, so it is primitive, not simple.
You can ignore that, unless you want to understand the implementation of
the system. Mixing primitive things with the simple high-level things
usually leads to something complicated.
Makarius
Email Gateway (Aug 19 2022 at 13:35):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
I don't know about recent versions of Isabelle, but in Isabelle2005 the
function Drule.standard does this (plus some other useful things).
I see subsequent emails in the thread talk about contexts - again I
don't know about subsequent versions of Isabelle, but in Isabelle 2005
contexts (as I understand the way the word is used nowadays) are not
part of a theorem.
Of course current versions of Isabelle may use different functions to do
this, and possibly it may not be so easy nowadays
Cheers,
Jeremy
Email Gateway (Aug 19 2022 at 13:35):From: Makarius <makarius@sketis.net>
What you call "Isar" above is merely the tactic script emulation, which is
also called "apply-style" occasionally. This is a minimal standard from
around 2002, but your ML scripts follow the one of 1998. Proper Isar
proofs are something else.
In old versions of Isabelle there is even some perl script to help in the
semi-automatic conversion, cf. "isabelle convert" in Isabelle2005, but it
was deleted later since it is long obsolete.
This thread is now once again where it gets since 10 years or so: after 15
years of introducing a new Isabelle theory format, to replace the old
Foo.thy/Foo.ML pair, someone is still using something that hardly anybody
else remembers or cares about.
Makarius
Email Gateway (Aug 19 2022 at 13:38):From: Lars Noschinski <noschinl@in.tum.de>
If your work can at least be put into the form
lemma <name>: <prop>
<proof>
you can always escape to Isabelle/ML by using
apply (tactic {* <some arbitrary ML code> *}
done
-- Lars
Email Gateway (Aug 19 2022 at 13:39):From: Makarius <makarius@sketis.net>
Moa, if you have any further questions, you are wolcome. Maybe just open
another thread, so that the carnival session can continue undisturbed
here. (The original question was not about "lifting variables" anyway.)
Makarius
Email Gateway (Aug 19 2022 at 13:42):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 02/04/2014 02:03 AM, Lars Noschinski wrote:
On 03.02.2014 12:16, Jeremy Dawson wrote:
I've been told similar things on occasions before, and it turns out
not to be true. Unless (in this case), your "minimal standards" means
rewriting everything in Isar. Which, as my previous email pointed
out, is not on, since I'm guessing my latest effort involves three to
four hundred thousand tactic applications.
If your work can at least be put into the formlemma <name>: <prop>
<proof>you can always escape to Isabelle/ML by using
apply (tactic {* <some arbitrary ML code> *}
done-- Lars
Well, is this acceptable for stuff submitted to the AFP?
Is the person in charge of it reading this thread? Who is in charge of it?
Is Isar-2005 code acceptable or does it have to be Isar-2014? If the
latter,
are there conversion guides between consecutive versions, which the AFP
maintainers used?
What are the minimal standards referred to by Makarius in his earlier post?
Jeremy
>
>
Email Gateway (Aug 19 2022 at 13:42):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 04.02.2014, at 10:27 am, Jeremy Dawson <Jeremy.Dawson@anu.edu.au> wrote:
On 02/04/2014 02:03 AM, Lars Noschinski wrote:
On 03.02.2014 12:16, Jeremy Dawson wrote:
I've been told similar things on occasions before, and it turns out
not to be true. Unless (in this case), your "minimal standards" means
rewriting everything in Isar. Which, as my previous email pointed
out, is not on, since I'm guessing my latest effort involves three to
four hundred thousand tactic applications.
If your work can at least be put into the formlemma <name>: <prop>
<proof>you can always escape to Isabelle/ML by using
apply (tactic {* <some arbitrary ML code> *}
done-- Lars
Well, is this acceptable for stuff submitted to the AFP?
In exceptional situations yes. Otherwise, we prefer structured Isar over apply style, but do not mandate it. Currently about 3% of the files in the AFP are ML (50 out of 1663, 6 files use ML embedded in .thy).
Is the person in charge of it reading this thread? Who is in charge of it?
Google "archive of formal proofs editors":
"The editors of the archive are
• Gerwin Klein, National ICT Australia
• Tobias Nipkow, Technische Universität München
• Larry Paulson, University of Cambridge"
Is Isar-2005 code acceptable or does it have to be Isar-2014? If the latter,
are there conversion guides between consecutive versions, which the AFP
maintainers used?
Submissions must work with the current Isabelle release version (currently 2013-2).
In exceptional circumstances (e.g. just before the next Isabelle release or similar), submissions for the current development version may be accepted, but they will not be listed on the front page until that Isabelle release comes out.
Older Isabelle versions are not accepted.
The rationale is that users should be able to download any AFP entry with the current Isabelle release and have everything work out of box. Entries are maintained to stay current over time.
What are the minimal standards referred to by Makarius in his earlier post?
For the AFP: http://afp.sourceforge.net/submitting.shtml
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 13:42):From: Makarius <makarius@sketis.net>
No, Isabelle2005 has the same notion of global background context (type
"theory") and local proof context (type "Proof.context"), it also has
locales and other applications of local context routinely available. The
thing that is part of the thm is merely a certificate of the background
theory, not a proper context. (It is merely a historical accident that
the certificate also contains the full background theory content, not just
its identification stamp.)
Drule.standard was already disruptive to local situations in Isabelle2005,
but many more tools were not properly localized, so it did not stand out
particularly.
Starting with Isabelle2007, old things were systematically removed under
the label of "localization". That is a long story and still not finished,
but the system is continously converging to a fully local context
displiciple for all proof tools and definitional packages.
The jump from Isabelle2005 to Isabelle2007 (with 25 months distance) also
marks the point where really ancient things from the 1990-ies were
removed. This is the deeper reason why you are yourself still stuck with
it, since it is possible to pretend that it is Isabelle98.
Consequently we have every few months a thread on this mailing list to
uncover features of historic Isabelle versions that hardly anybody
remembers anymore.
Makarius
Email Gateway (Aug 19 2022 at 13:44):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
Although you say "No", you seem to be agreeing with me that a theorem in
Isabelle2005 is associated with a global background context (type
"theory") and not a local proof context (type "Proof.context") (I take
it that this is the same thing as a "proper context").
More importantly you seem to regard things from the 1990-ies as really
ancient. While that may be so in the context of computer hardware, it's
not so in the context of mathematical proofs. The pen and paper
mathematical proofs I did in the 1970s are still 100% useful today, and
that's the way I want it to be.
Jeremy
Email Gateway (Aug 19 2022 at 13:46):From: Makarius <makarius@sketis.net>
On Sun, 2 Feb 2014, Jeremy Dawson wrote:
Although you say "No", you seem to be agreeing with me that a theorem in
Isabelle2005 is associated with a global background context (type "theory")
and not a local proof context (type "Proof.context") (I take it that this is
the same thing as a "proper context").
Yes, type thm has a back-reference to some background theory. This is its
certificate in the sense of the LCF kernel. It is not a proper context.
(Better forget functions like "the_context" that might still be in one of
your ancient Isabelle versions.)
In contrast, a proper context has type Proof.context, and is separate from
type thm. When you work with formal entities (typ, term, thm) in
Isabelle/ML, they implicitly "belong" to a ctxt: Proof.context. The
context is required for all non-trivial operations: parsing, printing,
advanced proof tools.
If you don't have a proper context, that's bad, but there is no problem to
get one. Just make your ML function depend on ctxt: Proof.context, and
propagate the context you get from the Isabelle framework, e.g. in
commands like 'method_setup'.
(As usual I am speaking here of current Isabelle versions, lets say 5
years back in time, but not 15 or 20.)
More importantly you seem to regard things from the 1990-ies as really
ancient. While that may be so in the context of computer hardware, it's
not so in the context of mathematical proofs. The pen and paper
mathematical proofs I did in the 1970s are still 100% useful today, and
that's the way I want it to be.
So how about your Isabelle98-style ML tactic scripts in Isabelle2005 in
this respect? Are they really proofs in any sense of the word? Can
anybody read them today, lets say without struggling days or weeks to make
Isabelle2005 run on current systems?
The Proof.context was introduced shortly after Isabelle98 in order to
support structured proofs in Isar. Later it turned out as generally
useful concept, so after 2000 or so, more and more tools became
context-aware. That made a big difference: before there was unsure
tinkering with free and schematic variables by hand, never being sure if
they could clash with other variables from the environment; afterwards
things actually started working reliably.
Makarius
Email Gateway (Aug 19 2022 at 13:47):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
On 02/02/2014 05:27 AM, Makarius wrote:
On Sun, 2 Feb 2014, Jeremy Dawson wrote:
Although you say "No", you seem to be agreeing with me that a theorem
in Isabelle2005 is associated with a global background context (type
"theory") and not a local proof context (type "Proof.context") (I
take it that this is the same thing as a "proper context").Yes, type thm has a back-reference to some background theory. This is
its certificate in the sense of the LCF kernel. It is not a proper
context. (Better forget functions like "the_context" that might still
be in one of your ancient Isabelle versions.)In contrast, a proper context has type Proof.context, and is separate
from type thm. When you work with formal entities (typ, term, thm) in
Isabelle/ML, they implicitly "belong" to a ctxt: Proof.context. The
context is required for all non-trivial operations: parsing, printing,
advanced proof tools.If you don't have a proper context, that's bad, but there is no
problem to get one. Just make your ML function depend on ctxt:
Proof.context, and propagate the context you get from the Isabelle
framework, e.g. in commands like 'method_setup'.(As usual I am speaking here of current Isabelle versions, lets say 5
years back in time, but not 15 or 20.)More importantly you seem to regard things from the 1990-ies as
really ancient. While that may be so in the context of computer
hardware, it's not so in the context of mathematical proofs. The pen
and paper mathematical proofs I did in the 1970s are still 100%
useful today, and that's the way I want it to be.So how about your Isabelle98-style ML tactic scripts in Isabelle2005
in this respect? Are they really proofs in any sense of the word?
Can anybody read them today, lets say without struggling days or weeks
to make Isabelle2005 run on current systems?Hi Makarius,
Whether they are proofs is a question which others might debate, and
have done so, at least since the proof of the four-colour theorem, if
not before. Whether they can be read today (without running them on an
Isabelle system) - with only the greatest of difficulty. They're to be
run on an appropriate system. Reading their source is more difficult
than a document in LaTex or HTML, easier than a document in PostScript
or PDF. And I can read (on the computer) documents dating from 2005 in
all of these formats without "struggling days or weeks to make [the 2005
versions of interpreters of those languages] run on current systems".
My whole point is that it should NOT be difficult for anyone to run
proofs today which were written in 2005 (or, indeed, much earlier).
And of course if I were to write out _all_ the steps of the proofs I've
done recently, whether in Isar, or any other language without (eg)
TRYALL (EVERY' [ ....]) there would be hundreds of thousands of lines of
code, so no-one would read it anyway, so I don't actually see what your
point is in asking whether anyone can read my proofs. Isar proofs
wouldn't (and, within reason, couldn't) be read either.
The Proof.context was introduced shortly after Isabelle98 in order to
support structured proofs in Isar. Later it turned out as generally
useful concept, so after 2000 or so, more and more tools became
context-aware. That made a big difference: before there was unsure
tinkering with free and schematic variables by hand, never being sure
if they could clash with other variables from the environment;
afterwards things actually started working reliably.I'm not clear what the problem is that you are describing but it doesn't
sound like anything I have issues with in my work.
Jeremy
Makarius
Email Gateway (Aug 19 2022 at 13:48):From: Makarius <makarius@sketis.net>
On Mon, 3 Feb 2014, Jeremy Dawson wrote:
My whole point is that it should NOT be difficult for anyone to run
proofs today which were written in 2005 (or, indeed, much earlier).
That problem is de-facto solved since 2004: Isabelle/AFP http://afp.sf.net
You merely need to put your material into shape (according to minimal
standards that are routine today) and submit it to the editors of the
archive. Afterwards it is usually maintained "automagically" to work with
current Isabelle versions, but in extreme cases the editors might ask for
you for assistance.
Thus you can see old Isabelle applications from the late 1990-ies fresh
and running on Isabelle2013-2, e.g. see the 2004 edition where the
archive was started by importing material from previous years.
The Proof.context was introduced shortly after Isabelle98 in order to
support structured proofs in Isar. Later it turned out as generally
useful concept, so after 2000 or so, more and more tools became
context-aware. That made a big difference: before there was unsure
tinkering with free and schematic variables by hand, never being sure
if they could clash with other variables from the environment;
afterwards things actually started working reliably.I'm not clear what the problem is that you are describing but it doesn't
sound like anything I have issues with in my work.
That was merely an attempt to close the circle on this thread. It started
out about proper treatment of fixed and schematic variables in Isabelle
today, using a proper Proof.context. That is quite different from the
all-global nothing-local situation in Isabelle98, which we should better
forget here.
Makarius
Email Gateway (Aug 19 2022 at 13:50):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
I've been told similar things on occasions before, and it turns out not
to be true. Unless (in this case), your "minimal standards" means
rewriting everything in Isar. Which, as my previous email pointed out,
is not on, since I'm guessing my latest effort involves three to four
hundred thousand tactic applications.
If I'm wrong about this, please clarify
Cheers,
Jeremy
Last updated: Apr 25 2024 at 12:23 UTC