`card`関数の発見

Question

設定された基数を決定する関数がどこにあるのか混乱しています。私がをCardinality.thyに見ると、何も見つかりませんが、cardの略語が見つかるはずです（cardの定義はありません）MainをインポートするPhantom_Typeがインポートされます。

Answer 1

だけイザベル/ jEditの中の用語「カードの上でCtrlキーを押しながらクリックすると、それは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のカーディナリティです。