--- a/src/HOL/Finite.thy Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Finite.thy Mon Mar 04 14:37:33 1996 +0100
@@ -1,12 +1,13 @@
(* Title: HOL/Finite.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
+ Author: Lawrence C Paulson & Tobias Nipkow
+ Copyright 1995 University of Cambridge & TU Muenchen
-Finite powerset operator
+Finite sets and their cardinality
*)
-Finite = Lfp +
+Finite = Arith +
+
consts Fin :: 'a set => 'a set set
inductive "Fin(A)"
@@ -14,4 +15,10 @@
emptyI "{} : Fin(A)"
insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)"
+consts finite :: 'a set => bool
+defs finite_def "finite A == A : Fin(UNIV)"
+
+consts card :: 'a set => nat
+defs card_def "card A == LEAST n. ? f. A = {f i |i. i<n}"
+
end