Email Gateway (Aug 19 2022 at 11:23): Email Gateway (Aug 19 2022 at 11:23):From: René Neumann <rene.neumann@in.tum.de>
Dear all,
I've used COMP so far in the following manner:
lemma lift_foo:
assumes "asm ==> concl"
shows "asm ==> concl'"
proof - ... qed
lemmas foo1_impl = foo1[COMP lift_foo]
lemmas foo2_impl = foo2[COMP lift_foo]
lemmas foo3_impl = foo3[COMP lift_foo]
...
Now I'm porting to Isabelle2013, where COMP has been removed.
Unfortunately, THEN is no sufficient replacement as the resulting
foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.
Is there some nice way of replacing the use of COMP here? Spelling out
the whole proofs (i.e. proving "asm ==> concl'" directly, for each
concl') is no real option here, as concl and concl' are usually quite
large properties which I do not intend to duplicate (maintainability and
such...)
Thanks a lot,
René
smime.p7s
Email Gateway (Aug 19 2022 at 11:24):From: Makarius <makarius@sketis.net>
On Mon, 29 Jul 2013, René Neumann wrote:
Now I'm porting to Isabelle2013, where COMP has been removed.
In such situations, the NEWS file is the first place to look. It says:
Unfortunately, THEN is no sufficient replacement as the resulting
foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.
The usual game is to write statements and proofs in a way that one does
not have to disobey the nice structure of rules provided by Larry Paulson
in 1989. There are many ways to do that, but from the given example it is
hard to guess what is right.
Makarius
Email Gateway (Aug 19 2022 at 11:24):From: René Neumann <rene.neumann@in.tum.de>
Am 29.07.2013 22:39, schrieb Makarius:
On Mon, 29 Jul 2013, René Neumann wrote:
Now I'm porting to Isabelle2013, where COMP has been removed.
In such situations, the NEWS file is the first place to look. It says:
I had a look there. That's how I noted it was gone ...
- Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN",
Can't make it work (that's why I asked here on the list).
or explicit proof structure instead.
Don't want it that way.
Note that Isabelle/ML provides a variety of
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.
I don't know Isabelle/ML in a way to make it work.
Unfortunately, THEN is no sufficient replacement as the resulting
foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.The usual game is to write statements and proofs in a way that one does
not have to disobey the nice structure of rules provided by Larry
Paulson in 1989. There are many ways to do that, but from the given
example it is hard to guess what is right.
Could you, nevertheless, provide some pointers here, please? Because
currently, I'm unsure how I'd have to refine my example to make my
intention more visible.
Email Gateway (Aug 19 2022 at 11:24):From: Tobias Nipkow <nipkow@in.tum.de>
Can you give a concrete example where the use of COMP leads to something the
Isabelle user needs to be protected from?
Tobias
Email Gateway (Aug 19 2022 at 11:24):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear René,
You will have to restructure your lemmas or proofs unless you want to define your own COMP
attribute, there's no way to do it as before with THEN/OF. Here are a few ideas.
lemma lift_foo:
assumes "asm ==> concl"
shows "asm ==> concl'"
proof - ... qedlemmas foo1_impl = foo1[COMP lift_foo]
lemmas foo2_impl = foo2[COMP lift_foo]
lemmas foo3_impl = foo3[COMP lift_foo]
...
I suspect that foo1 has the form "asm ==> concl", right?
lemma lift_foo:
assumes "asm --> concl"
shows "asm --> concl'"
proof ... qed
lemmas foo1_impl = foo1[THEN lift_foo]
Note that "asm" as a premise in the assumes is redundant in lift_foo. The following
lemma is equivalent:
lift_foo': "[| concl; asm |] ==> concl"
If you now do rule composition with THEN, you get "[| asm; asm |] ==> concl'"
instead of "[| asm ==> asm; asm |] ==> concl'". I don't know if that's better.
If you can prove "concl ==> concl'" without the assumption asm, then that works perfectly.
context assumes asm begin
lemma lift_foo: "concl ==> concl'"
proof - ... qed
lemma foo1: "concl"
lemmas foo1_impl = foo1[THEN lift_foo]
end
lemma remove_trivial_assumption: "((PROP A ==> PROP A) ==> PROP B) == PROP B"
by(rule equal_intr_rule)
lemmas foo1_impl = foo1[THEN lift_foo, unfolded remove_trivial_assumption]
lemma remove_double_assumption: "(PROP A ==> PROP A ==> PROP B) == (PROP A ==> PROP B)"
by(rule equal_intr_rule)
lemmas foo1_impl = foo[THEN lift_foo', unfolded remove_double_assumption]
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:24):From: Makarius <makarius@sketis.net>
Even after reading the answers by Andreas, I don't understand the purpose
of lift_foo.
Just technically, you can produce a compact form in the sense of (1) above
on the spot, as a variations of the tricks that were shown already:
thm lift_foo [unfolded atomize_all atomize_imp]
Can you explain the application behind all this?
Makarius
Email Gateway (Aug 19 2022 at 11:24):From: René Neumann <rene.neumann@in.tum.de>
I have a ton of theorems about some function foo. Now I have some
refinement foo_impl, where most of the properties of foo also hold.
For usability reasons I'd like to lift the appropriate theorems from foo
to foo_impl (so I don't have to do it everytime I need a lemma about
foo_impl), but I'd also like to avoid duplication (i.e. stating the
properties over and over again, as it then becomes quite tedious to do
smaller refactoring).
So in the end, it is more of academic use (hah!) and could easily be
solved by copy'n'paste,
but I hate copying boilerplate.
Email Gateway (Aug 19 2022 at 11:25):From: Makarius <makarius@sketis.net>
COMP is conceptually outside the Isabelle/Pure framework (Paulson 1989)
and the Isabelle/Isar proof language (Wenzel 1999). It violates certain
assumptions about the structure of rules.
We've had a recent isabelle-users thread on COMP in May, with the typical
situation that someone does not understand the purpose of !! and ==> yet,
is surprised about its behaviour in rule composition, and wants to bypass
it without understanding the consequences.
Before everything is repeated, see especially this explanation by Larry:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-May/msg00016.html
Even in its internal use COMP came out of use in recent years -- the
"INCR" variants are more frequent now, but none of that is for regular
use, it is just too complicated.
We've had a few breakdowns on the isabelle-dev mailing list this year
already, coming on us from distant past. This resulted in Thm.bicompose
in 8 variants (one function with 3 funny flags), where INCR_COMP and
COMP_INCR are just the tip of the iceberg. Just formally, such diversity
cannot be part of a public programming API in Isabelle/ML. I am even
myself never quite sure which of the many COMP variants need to be used
when building certain system infrastructure.
For Isabelle/Isar the Isabelle2013/NEWS claims that it is really obsolete,
based on empirical information from AFP as usual. So far this thread did
not show a counterexample yet, but it might still come. (If all fails
users may always define their own Isar attributes as explained in the
isar-ref manual, but I don't think this will be required.)
Makarius
Email Gateway (Aug 19 2022 at 11:25):From: Makarius <makarius@sketis.net>
In this generic way, it sounds like an application of locale +
interpretation.
Makarius
Email Gateway (Aug 19 2022 at 11:25):From: René Neumann <rene.neumann@in.tum.de>
We already have to deal with way too much locales here, adding one more
layer would only complicate things.
So for the moment, I'll stick with proving it explicitly.
Thanks for the hints though (also @Andreas -- unfortunately, I couldn't
use on of those proposals to make it 'feel right', it always felt kind
of hackish).
Email Gateway (Aug 19 2022 at 11:25):From: René Neumann <rene.neumann@in.tum.de>
I'm with Tobias (as he stated in the thread you mentioned) to have an OF
and/or THEN variant which allows to instantiate the premise without
handling ==> and !! in a special way, because it is sometimes extremely
helpful.
And COMP is this THEN variant, is it not?
Btw: Reading the implementation manual on Drule.compose. It should read
"The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ), shouldn't it?
Email Gateway (Aug 19 2022 at 11:25):From: Makarius <makarius@sketis.net>
Looking here again, this note by Andreas seems important.
Makarius
Email Gateway (Aug 19 2022 at 11:25):From: Makarius <makarius@sketis.net>
On Wed, 31 Jul 2013, René Neumann wrote:
And COMP is this THEN variant, is it not?
Not at all. It is just one big misunderstanding. Every time I see
remaining occurrences COMP in the Isabelle sources, I need to check
several times to convince myself that it is probably right, and not better
INCR_COMP or COMP_INCR, or one of the new 8 uniform varieties of the
thing that are probably in the next release (for internal use only).
If you want to use Isabelle professionally, you should forget about COMP
and do it by more standard means.
Btw: Reading the implementation manual on Drule.compose. It should read
"The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ), shouldn't
it?
Which implementation manual are you reading excactly? I don't see this in
http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf
Makarius
Email Gateway (Aug 19 2022 at 11:26):From: Makarius <makarius@sketis.net>
Tools that really need that (which was not yet proven here) are doing that
via the "prop" protective marker, and protectI, protectD rules etc.
together with plain resolution of Pure.
This is how all the second-generation locale infrastructure was made in
the early/mid 2000-nds (COMP is from the early 1990-ies).
Makarius
Email Gateway (Aug 19 2022 at 11:26):From: Makarius <makarius@sketis.net>
The above "Drule.compose" (instead of "compose") is probably from some
arbitrary repository version after the Isabelle2013, but I had already
dropped the subscript "i" last November when refurbishing really ancient
material by Larry, so it is not there in the official release.
In the next release, the old "ref" manual will no longer exist, and its
remaining material fully absorbed into the isar-ref and implementation
manuals -- after 5 years of working on that.
Makarius
Email Gateway (Aug 19 2022 at 11:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
(the thread is a little but fringed already, I answer at an arbitrary point)
in the next Isabelle release, there will be interpretation within
bounded contexts which is maybe helpful in your scenario.
context
fixes …
assumes …
begin
…
interpretation … -- {* + *}
…
end -- {* here all facts stemming from + disappear again *}
This construction appears to me at another powerful means to organize
abstract specifications and interpretations since it avoid the ancient
»can bin problem« that you can either interpret a whole locale or nothing.
Would this fit your scenario? For me this is indeed hard to judge
without a look at your theories.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:36):From: René Neumann <rene.neumann@in.tum.de>
Thanks for the hint (such a thing is good to know). Unfortunately, it
does not fit my usecase without a larger rewrite. And also I'd like to
avoid introducing new locales (I have several dozens here already that
are already too confusing).
I now used one of the proposals of Andreas, namely an unnamed context.
This worked out pretty well as it turned out to not just be a
workaround but a really useful tool here (a large bunch of lemmas with
the same assumption). (Now all that remains to remember is the
existence of this context when looking at the theory again in a later
point in time :))
Thanks to all,
René
smime.p7s
Email Gateway (Aug 19 2022 at 11:38):From: René Neumann <rene.neumann@in.tum.de>
Am 31.07.2013 23:48, schrieb Makarius:
On Wed, 31 Jul 2013, Makarius wrote:
Btw: Reading the implementation manual on Drule.compose. It should
read "The unique s that unifies ψ and φ_i" (i.e. φ_i and not φ),
shouldn't it?Which implementation manual are you reading excactly? I don't see
this in
http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdfThe above "Drule.compose" (instead of "compose") is probably from some
arbitrary repository version after the Isabelle2013, but I had already
dropped the subscript "i" last November when refurbishing really ancient
material by Larry, so it is not there in the official release.
Yes. In the release version it is just named "compose" without the
Drule. But the rest of text is the same (page 89 near the bottom).
Still wondering: Was dropping the subscript intentional? Or is my
understanding completely off and it is indeed correct without the i?
In the next release, the old "ref" manual will no longer exist, and its
remaining material fully absorbed into the isar-ref and implementation
manuals -- after 5 years of working on that.
I don't get the context (from the rest of the mail/thread), but
congratulation.
Email Gateway (Aug 19 2022 at 11:39):From: René Neumann <rene.neumann@in.tum.de>
I'd like to point out though, that I do not use Isabelle/ML and hence
the point (as I understand you), that using it in ML without thought
might deal some harm, does not apply here. Or could it really deal some
damage in the high-level view I'm using?
I do trust you that there are good reasons to remove COMP. Still my wish
to have those THEN/OF variants remains :)
Email Gateway (Aug 19 2022 at 11:40):From: René Neumann <rene.neumann@in.tum.de>
I'm not an Isabelle-Dev. I'm not interested in writing tools, I just
want to prove theorems.
smime.p7s
Email Gateway (Aug 19 2022 at 11:41):From: Makarius <makarius@sketis.net>
No, I merely dropped the old-style Latex @i of Larry when updating the
manual last November. This "painting" of informal text is not
machine-checked, so it can occasionally break down.
Makarius
Email Gateway (Aug 19 2022 at 11:42):From: Makarius <makarius@sketis.net>
On Thu, 1 Aug 2013, René Neumann wrote:
I'd like to point out though, that I do not use Isabelle/ML and hence
the point (as I understand you), that using it in ML without thought
might deal some harm, does not apply here. Or could it really deal some
damage in the high-level view I'm using?
We did not get very far so far, the thread is going backwards in circles.
Andreas Lochbihler made several constructive attempts to guess what you
are trying to do and propose some alternatives. Maybe you can show more
of the actual application, so that it can be sorted out the proper way.
I do trust you that there are good reasons to remove COMP.
Just normal garbage collection on the sources: it was no longer used and
in conflict with certain concepts, causing occasional breakdown in
unexpected situations, so it was deleted. This time it was not about
"old-fashioned" or "legacy" features, but obsolete things as the NEWS
explained that. If it would have been non-obsolete, I would have had to
sit down and think about getting 8 variants of COMP into Isar source
language.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC