Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

被引：0

作者：

Hoelzl, Johannes ^{[1
]}

Immler, Fabian ^{[1
]}

Huffman, Brian ^{[2
]}

机构：

[1] Tech Univ Munich, Inst Informat, Munich, Germany

[2] Galois Inc, Portland, OR USA

来源：

INTERACTIVE THEOREM PROVING, ITP 2013 | 2013年 / 7998卷

关键词：

Type classes; Filters; Mathematical analysis; Topology; Limits; Euclidean vector spaces; Isabelle/HOL;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: R, C and R-n. Isabelle's new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.

引用

页码：279 / 294

页数：16

共 10 条

[1] FLEURIOT J, 2000, LMS J COMPUT MATH, V3, P140
[2] Haftmann F, 2007, LECT NOTES COMPUT SC, V4502, P160
[3] Haftmann F, 2009, LECT NOTES COMPUT SC, V5497, P153, DOI 10.1007/978-3-642-02444-3_10
[4] Harrison J, 2005, LECT NOTES COMPUT SC, V3603, P114
[5] Holzl Johannes, 2011, Interactive Theorem Proving. Proceedings Second International Conference, ITP 2011, P135, DOI 10.1007/978-3-642-22863-6_12
[6] Immler Fabian, 2012, Interactive Theorem Proving. Proceedings of the Third International Conference, ITP 2012, P377, DOI 10.1007/978-3-642-32347-8_26
[7] Immler F, 2012, THESIS
[8] Joshi K.D., 1983, Introduction to general topology
[9] Lester D.R., 2007, 2 WORKSHOP AUTOMATED, P11
[10] Type classes for mathematics in type theory
Spitters, Bas
Van der Weegen, Eelis
[J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2011, 21 (04) : 795 - 825

← 1 →