Email Gateway (Aug 18 2022 at 09:52): Email Gateway (Aug 18 2022 at 09:52):From: Clemens Ballarin <ballarin@in.tum.de>
On 3 Nov 2006, at 0:37, Dr. Brendan Patrick Mahony wrote:
Is there a forum where changes to Isabelle are being discussed with
users of Isabelle? Very little is appearing in this mailing list. Am I
really expected to maintain 50kloc of Isabelle code against a nightly
rebuild of the development version in order to know what changes are
being made?
This should probably be commented on by the main Isabelle developers.
Clearly there has to be a balance between progress and backwards
compatibility.
Well the simple example is:
locale carrier =
fixes X::"'a set"
assumes nempty: "X \<noteq> {}"...
interpretation prod_carrier: carrier ["A \<times> B"]
This all makes sense to me, but my question now would be in what
context lemmas about the product are going to be used. Or are you just
interested in having a library of those lemmas?
Actually, it occurs to me now that there is a third way, but it really
twists the locale framework in my opinion.
Your observation that interpretations in locales are meant to express
conditional interpretations is correct. A natural representation of
your example would be along the following lines:
Define a context for products:
locale carrier2 =
fixes A and B
assumes "A~={}" and "B~={}"
Map theorems from carrier into this context:
interpretation carrier2 < carrier "A <*> B"
Unfortunately, this is not currently possible. You may, as you
observe, use defines to replace the substitution and say:
locale carrier2 =
fixes A and B and P
assumes "A~={}" and "B~={}"
defines "X == A <*> B"
interpretation carrier2 < carrier X
BTW Does anyone know why my original posts are not appearing in the
list, but the replies are?
Well, this one wasn't posted to Isabelle Users.
Clemens
Email Gateway (Aug 18 2022 at 09:52):From: Makarius <makarius@sketis.net>
The user relevant changed are explained in the NEWS file of any official
Isabelle distribution.
The development snapshots are not intendeded for users, and their
corresponding NEWS might contain internal notes that will change/disappear
eventually. For really keeping track of the internal development process
you need to check the ChangeLog of the devel download site as well.
Makarius
Email Gateway (Aug 18 2022 at 09:57):From: "Dr. Brendan Patrick Mahony" <Brendan.Mahony@dsto.defence.gov.au>
Suppose I can prove
lemma f_locI: "p x ==> loc (f x)"
Is there any way to parley that into an interpretation?
Something like:
interpretation fl:
assumes "p x"
interprets loc ["f x"],
where fl.result is of the form "p x ==> R (f x)" for result (in loc)
of the form "R y".
In a proof I can do
lemma
assumes a1: "p x"
shows "Q x"
proof -
from f_locI [OF a1] interpret fl: loc ["f x"]
...
qed
but the first form would be preferable.
Also, is there anyway the interpretation could leave its top goal as
"loc (f x)"?
Automatically applying the intro_classes analog is pretty annoying
for locales (it might be more acceptable for
axclasses!). It seems natural to me to do proofs about the locale
predicate (sub-algebras, homomorphic images etc) and this convention
makes unnecessarily awkward to use such results.
It would also be nice if the intro_locales method actually fully
unwound all of the locale axioms for you, so that interpretation
proofs were more like instance proofs.
Brendan
Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
Email Gateway (Aug 18 2022 at 09:57):From: Clemens Ballarin <ballarin@in.tum.de>
Forgot to post this answer to the list. C.
Begin forwarded message:
From: Clemens Ballarin <ballarin@in.tum.de>
Date: 2 November 2006 10:59:51 GMT+01:00
To: "Dr. Brendan Patrick Mahony" <Brendan.Mahony@dsto.defence.gov.au>
Subject: Re: [isabelle] Conditional interpretations?
On 2 Nov 2006, at 4:56, Dr. Brendan Patrick Mahony wrote:
Suppose I can prove
lemma f_locI: "p x ==> loc (f x)"
Is there any way to parley that into an interpretation?
No. It would be interesting to see a scenario where this is useful.
Normally, attributes under such an interpretation are no longer useful
since theorems have additional premises.
Also, is there anyway the interpretation could leave its top goal as
"loc (f x)"?
This has been implemented a while ago.
It would also be nice if the intro_locales method actually fully
unwound all of the locale axioms for you, so that interpretation
proofs were more like instance proofs.
If you have intro_locales, you should also have the change above. To
unfold all predicates use unfold_locales.
Clemens
Last updated: May 03 2024 at 08:18 UTC