`card` 함수 찾기

Question

세트 카디널리티를 결정하는 함수가 어디에 위치하는지 혼란 스럽습니다. 내가 을 Cardinality.thy으로 보면, 찾을 수있는 것이 없지만 적어도 card이라는 약어가있는 곳에서 Main을 가져 오는 Phantom_Type을 가져옵니다 (비록 card의 정의는 아니지만).

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 유형의 카디널리티입니다.