查找`card`函数

Question

我对确定集合基数的函数的确切位置感到困惑。如果我在Cardinality.thy中查找，什么也找不到，但是导入了Phantom_Type，这又导入了Main，其中至少可以找到card的缩写(尽管不是card本身的定义)。

Answer 1

只需按住ctrl键并单击Isabelle/jEdit中的术语‘card’，就会直接转到Finite_Set.thy中的定义

text ‹
  The traditional definition
  @{prop "card A ≡ LEAST n. ∃f. A = {f i |i. i < n}"}
  is ugly to work with.
  But now that we have @{const fold} things are easy:
›

global_interpretation card: folding "λ_. Suc" 0
  defines card = "folding.F (λ_. Suc) 0"
  by standard rule

这使用了folding语言环境，它提供了对有限集的元素进行折叠(即迭代)的操作。

我不知道你在想什么缩写。如果你指的是CARD('a)，那只是card (UNIV :: 'a set)的一些语法，也就是'a类型的基数。