我想 缩写 为类型类名称创建同义词。这是我现在的做法：
class fooC = linordered_idom
instance int :: fooC
proof qed
definition foof :: "'a::fooC ⇒ 'a" where
"foof x = x"
term "foof (x::int)"
value "foof (x::int)"
如果没有更好的方法，这样做会很好。缺点是我必须实例化int，并且该class命令需要花费一些时间来实现自身。
此更新是为了向Makarius阐明我的需要，解释我想要的目的，并提供我熟悉的用于创建符号，缩写和同义词的命令列表，但是我无法获得这些命令为我想要的工作。
我想“同义词”会是一个更好的词，但是我选择了“缩写”，因为它描述了我想要的东西，即能够为类型类创建一个较短的名称，例如重命名linordered_semidom为losdC。尽管Isarabbreviation具有的某些属性definition，但它也只定义了语法。因此，因为“缩写”描述了我想要的内容，并且abbreviation仅定义了语法，所以我选择了“缩写”而不是“同义词”或“别名”。
“别名”将描述我想要的。关于句子“如果您只想保存在编辑器中的键入，可以在其中使用一些缩写”，这是我尝试过尝试重新命名的命令linordered_idom，但是我无法让它们为我工作：
type_notationtype_synonymnotationabbreviationsyntax我只列出它们，而不是解释我曾经尝试过的事情，并试图记住我曾尝试过的事情。我在“ class”上进行了搜索，仅找到了Isar命令class和classes。我认为也许区域设置命令可能适用，但是我什么也没找到。
我想要的很简单，例如如何type_synonym用于定义类型的同义词。
我通常希望缩短类型类的名称，例如linordered_idom，因为最终，我计划广泛使用代数类型类。
但是，还有第二个原因，那就是重命名某些东西linordered_semidom，使其成为三种类型的命名方案的一部分。
对于任何代数类型类，例如linordered_semidom，我都可以将该类型类与一起使用quotient_type，以创建我称之为数字系统的类型，例如用于如何nat定义int。
Int.thy作为模板，我使用进行了此操作linordered_semidom，然后将其实例化为comm_ring_1，这是我最近有空的时间。
另外，使用typedef，对于具有zero和one（以及其他依赖项）的任何代数类型类ord，我可以定义所有大于或等于零的元素的类型，为所有大于零的元素定义一个类型。我这样做是为了linordered_idom，但后来我发现我实际上需要走这quotient_type条路，才能得到模型化的东西rat。
这是很长的解释。最终，我将开始处理众多代数类型类，并且从一个类型类中，我还将获得另外两个。如果我对20个类型类都这样做，并且也使用它们，那么冗长的描述性名称将不起作用，而重命名类型类将帮助我了解哪些类型类可以一起使用。
这是针对的方案linordered_semidom，在我能够尝试全部操作之前，我不知道它的实际效果：
linordered_semidom是基类。我将其重命名为losdC。这三种类型的数字均大于或等于零。losdQ是losdC使用定义的quotient_type。它给了我负数，并且使我能够强迫losdC自己losdQ。losd1是使用定义的typedef，并且是大于零的数字。我需要一个统一的命名模式，以保持它的所有直：losdC，losdQ，和losd1。
我还没有完全工作，以为事情了（我甚至接近），但类似，这一切都与实施，为代数类型类之间的基本关系nat，int以及rat，其中real可能最终开始发挥作用。另外，这是从这些类型中获取非负或正成员的类型，如果默认情况下不存在这些成员。
有nat用于int和int用于rat。
随着nat使用int，我们得到默认情况下，这是一个非负整数nat。
随着int使用rat，我们没有得到的非负成员rat，我们得到的分数。（再次，我说的是一种非负数和正数，而不是一组非负数和正数。）
所以，如果我使用linordered_idom和quotient_type定义分数的话，我必须使用typedef两次获得非负和那些分数，这意味着我将有4种类型的积极成员保持，跟踪liodC，liodQ，liod0，和liod1。
如果有一个简单的重命名类型类的解决方案，那么我不必要地讲了大约600个单词。
定义不是缩写，它引入了逻辑上相等的单独术语。这适用于术语常量。
类型类在语义上是类型的谓词，因此连接到某些谓词（术语常量），但是实际上，您很少访问该谓词。那么“缩写类型类”的确切含义是什么？
例如，您可能希望操纵类名称空间以为其获取别名，这在原则上是可能的。但是目的是什么？
如果只想在编辑器中保存键入内容，则可以在其中使用一些缩写。
在正式系统中，另一种可能性是在名称空间中引入真正的别名。Isabelle为此提供了一些设施，这些设施并没有被广为宣传，因为如果名称更改过多，确实存在使图书馆晦涩难懂并阻止其他任何人理解它们的危险。
在理论来源中使用一些友好的Isabelle / ML就是这样工作的：
class foobar = ord + fixes foobar :: 'a
setup {* Sign.class_alias @{binding f} @{class foobar} *}
typ "'a::f"
instantiation nat :: f
begin
definition foobar_nat :: nat where "foobar_nat = 0"
instance ..
end
注意，Sign.class_alias仅在狭义上指代类型类名称空间。一个同时class有很多东西：语言环境，const（谓词），类型类。您可以在以下示例中看到该示例，其中该类用作本地定义和定理的“目标”：
definition (in foobar) "fuzz = foobar"
theorem (in foobar) "fuzz = foobar" by (simp add: fuzz_def)
从技术上讲，上面使用的语言环境名称空间也可以支持别名，但是并不能做到这一点。只有基本Sign.class_alias，Sign.type_alias，Sign.const_alias暴露了不寻常的情况下，与传统图书馆地址问题。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句