src/HOL/Finite.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1556 2fd82cec17d4
child 3367 832c245d967c
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Finite.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson & Tobias Nipkow
     4     Copyright   1995  University of Cambridge & TU Muenchen
     5 
     6 Finite sets and their cardinality
     7 *)
     8 
     9 Finite = Arith +
    10 
    11 consts Fin :: 'a set => 'a set set
    12 
    13 inductive "Fin(A)"
    14   intrs
    15     emptyI  "{} : Fin(A)"
    16     insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
    17 
    18 constdefs
    19 
    20   finite :: 'a set => bool
    21   "finite A == A : Fin(UNIV)"
    22 
    23   card :: 'a set => nat
    24   "card A == LEAST n. ? f. A = {f i |i. i<n}"
    25 
    26 end