如何使用自定义类型设置（又称“ relator”）？
在isabelle/hol中，我想使用两个自定义typedef s相互构建的 s，并证明它们两个都实例化某些类型类（例如，来自hol.rings。）。在这种情况下，我不明白正确调用setup_lifiting需要哪些定义或事实。此外，我想了解此关键字在声明typedef之后使用的确切目的（目前我只是尝试模仿现有工作的结构）以及所谓的 relators 是在此过程中使用的。 locale 和 typeclass pdf教程都没有详细介绍此命令。
为了显式，请考虑
type_synonym 'v monom_list = "('v × nat)list"
[...]
typedef (overloaded) 'v monom = "Collect (monom_inv :: ...)"
适用不变monom_inv。同一条目继续定义多项式，
type_synonym ('v,'a)poly = "('v monom × 'a)list"
并定义合适的不变Poly_inv。
在'v Monom的键入之后，调用setup_lifting type_definition_monoment作为基础类型的必要 relators （？）似乎没有问题（特别是列表）是标准库的一部分。 （如果这是对实际发生的事情的误解。）
但是，在新的typedef（Overloaded）（'v，'a）polyq =“ collect（poly_inv :: ...）之后>（这不是上面引用的AFP条目的一部分），情况有所不同。现在，调用
setup_lifting type_definition_polyq
会产生一个警告，该警告读取：生成参数化的对应关系失败。原因：找到类型为“多项式”的关系
。 ？如果是，我该如何定义monom类型的关系？
In the Isabelle/HOL, I would like to work with two custom typedefs that build on top of each other, and show that both of them instantiate certain type classes (e.g. from HOL.Rings). I do not understand what definitions or facts are required to properly call setup_lifiting in this case. Moreover, I would like to understand what precise purpose this keyword serves after declaring a typedef (currently I simply try to mimick the structure of existing work) and what the so-called relators are which are used in the process. Neither the locale nor the typeclass PDF tutorials go into much detail on this command.
For explicitness, consider the AFP entry implementing polynomials, which schematically defines monomials as
type_synonym 'v monom_list = "('v × nat)list"
[...]
typedef (overloaded) 'v monom = "Collect (monom_inv :: ...)"
for an adequate invariant monom_inv. The same entry proceeds to define polynomials as
type_synonym ('v,'a)poly = "('v monom × 'a)list"
and also defines a suitable invariant poly_inv.
After the typedef of 'v monom, it appears to be no problem to call setup_lifting type_definition_monom as the necessary relators (?) for the underlying types (in particular lists) are part of the standard library. (Please correct if this is a misunderstanding of what's actually going on.)
However, after a new typedef (overloaded) ('v, 'a) polyq = "Collect (poly_inv :: ...)" (which is not part of the AFP entry cited above), things are different. Now, calling
setup_lifting type_definition_polyq
yields a warning which reads: Generation of a parametrized correspondence relation failed. Reason: No relator for the type "Polynomials.monom" found.
Do I need to address this issue to afterwards call for example instatiation polyq :: (...) comm_semiring_1? If yes, how can I go about defining a relator for the monom type?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
setup_lifting仅在您打算使用升降机和传输框架时才有用，对于可以阅读 Huffman和Kuncar的CPP纸。该框架中的一些最新进展主要与有限的天然函子有关，为此，您可以查看此。提出合适的关系器需要深入了解数据类型。这里
setup_lifting免费为我们提供一些相对简单的关系定理。（从伊莎贝尔Zulip聊天中回答。）
The
setup_liftingis only useful if you intend to use the lifting-and-transfer framework, for the details of which you can read Huffman and Kuncar's CPP paper. Some recent progress in this framework is mostly related to bounded natural functors, for which you can have a look at this paper.Proposing suitable relators requires insight of the data type. Here
setup_liftinggives us some relatively easy relator theorems for free.(Answer from the Isabelle Zulip Chat.)