author  nipkow 
Mon, 04 Mar 1996 14:37:33 +0100  
changeset 1531  e5eb247ad13c 
parent 1475  7f5a4cd08209 
child 1556  2fd82cec17d4 
permissions  rwrr 
1475  1 
(* Title: HOL/Finite.thy 
923  2 
ID: $Id$ 
1531  3 
Author: Lawrence C Paulson & Tobias Nipkow 
4 
Copyright 1995 University of Cambridge & TU Muenchen 

923  5 

1531  6 
Finite sets and their cardinality 
923  7 
*) 
8 

1531  9 
Finite = Arith + 
10 

1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
923
diff
changeset

11 
consts Fin :: 'a set => 'a set set 
923  12 

13 
inductive "Fin(A)" 

14 
intrs 

15 
emptyI "{} : Fin(A)" 

16 
insertI "[ a: A; b: Fin(A) ] ==> insert a b : Fin(A)" 

17 

1531  18 
consts finite :: 'a set => bool 
19 
defs finite_def "finite A == A : Fin(UNIV)" 

20 

21 
consts card :: 'a set => nat 

22 
defs card_def "card A == LEAST n. ? f. A = {f i i. i<n}" 

23 

923  24 
end 