author | paulson |
Fri, 29 Nov 1996 18:03:21 +0100 | |
changeset 2284 | 80ebd1a213fd |
parent 1556 | 2fd82cec17d4 |
child 3367 | 832c245d967c |
permissions | -rw-r--r-- |
(* Title: HOL/Finite.thy ID: $Id$ Author: Lawrence C Paulson & Tobias Nipkow Copyright 1995 University of Cambridge & TU Muenchen Finite sets and their cardinality *) Finite = Arith + consts Fin :: 'a set => 'a set set inductive "Fin(A)" intrs emptyI "{} : Fin(A)" insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)" constdefs finite :: 'a set => bool "finite A == A : Fin(UNIV)" card :: 'a set => nat "card A == LEAST n. ? f. A = {f i |i. i<n}" end