【发布时间】：2015-10-27 18:43:26
【问题描述】：
我最近开始与 Isabelle 合作，我一直在尝试探索它的不同部分。是否有可能在 Isabelle 中证明整合是可能的？如[0,1]、dx之间的积分x。如果可能，请您指导我访问相关的 Isabelle .thy 文件，甚至是简短的教程。
我试过环顾四周，但没有成功。
谢谢。
【问题讨论】：
-
我会重新表述你的问题，因为不是每个人都精通科学文献的出版。
标签： isabelle
【发布时间】：2015-10-27 18:43:26
【问题描述】：
还有来自https://github.com/avigad/isabelle/blob/master/Analysis/Interval_Integral.thy 的IntervalIntegral.thy。这具有丰富的测度理论背景的优势，并且很快将被合并到 Isabelle 的测度理论库中。如果你想证明从某处到某处的积分等于某个项，你通常使用微积分基本定理 (interval_integral_FTC_finite) 来证明你有一个不定积分，然后用它来计算定积分。也可以通过替换集成，例如interval_integral_substitution_finite.
【讨论】：
相关理论在HOL-Multivariate_Analysis，特别是理论Integration及以下。
免责声明：我根本没有使用过这些定义，只是知道它们的存在。
【讨论】：