Email Gateway (Aug 18 2022 at 14:37): Email Gateway (Aug 18 2022 at 14:37):From: Brian Huffman <brianh@cs.pdx.edu>
I agree that the old Integral should be kept somewhere, like in HOL/ex.
Johannes and Robert: I thought your plan was just to remove it from
the Isabelle/HOL image (which I fully approve of), but now it is
completely gone!
It is probably best to handle little-used libraries in a more
conservative way, like first moving them to a different directory,
rather than just deleting them completely. Libraries may have value
even if nobody imports them: I think Integral.thy is a fairly readable
exposition of gauge integrals (especially when compared to
Multivariate_Analysis!), and would be a useful object of study for
someone trying to learn the subject. I'll take responsibility for
maintaining the theory, if maintenance is a concern.
Email Gateway (Aug 18 2022 at 14:37):From: Tobias Nipkow <nipkow@in.tum.de>
I sympathize with Brian's sentiments. But when you put the theory into
HOL/ex
include a comment that states clearly that this is of
historical/expository interest only and that HOL's proper integration
theory is found elsewhere.
Remove extraneous stuff, in this case the lemmas beyond FCT1.
Tobias
Brian Huffman schrieb:
Email Gateway (Aug 18 2022 at 14:37):From: Johannes Hölzl <hoelzl@in.tum.de>
Readded the old Integration theory to HOL examples.
It would be of course nice if someone could cleanup the proofs in this
theory and rewrite them in nice Isar-style.
Email Gateway (Aug 18 2022 at 14:44):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Isabelle Users,
Robert Himmelmann is currently porting the Multivariate Analysis from
HOL-light to Isabelle/HOL. This contains a definition of the Gauge
Integral. However a one-dimensional version of this is already in
src/HOL/Integration.
To avoid a duplication of maintenance we plan to remove the current
one-dimensional Integral definition and replace it by a definition based
on Multivariate Analysis. Therefore users of the old Integral need to
adjust their proofs and import the HOL-Multivariate_Analysis image in
the future.
Is there anyone using the old Integral? There is no usage in Isabelle or
the AFP. Are there any objections or comments?
Best Regards,
PS: Also Armin Heller and I currently port the Probability theory from
HOL4, which contains the Lebegues integration (based again on
afp/thy/Integration). Hence in the future will be at least two integrals
in Isabelle/HOL anyway. Hopefully we can show the equivalence of both
integrals when the function if Gauge and Lebegues integrable.
Email Gateway (Aug 18 2022 at 14:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Sounds reasonable to me. Perhaps the old Integral could go to a theory
in ex/?
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC