src/HOL/Finite.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1556 2fd82cec17d4
child 3367 832c245d967c
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
clasohm@1475
     1
(*  Title:      HOL/Finite.thy
clasohm@923
     2
    ID:         $Id$
nipkow@1531
     3
    Author:     Lawrence C Paulson & Tobias Nipkow
nipkow@1531
     4
    Copyright   1995  University of Cambridge & TU Muenchen
clasohm@923
     5
nipkow@1531
     6
Finite sets and their cardinality
clasohm@923
     7
*)
clasohm@923
     8
nipkow@1531
     9
Finite = Arith +
nipkow@1531
    10
clasohm@1370
    11
consts Fin :: 'a set => 'a set set
clasohm@923
    12
clasohm@923
    13
inductive "Fin(A)"
clasohm@923
    14
  intrs
clasohm@923
    15
    emptyI  "{} : Fin(A)"
clasohm@923
    16
    insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
clasohm@923
    17
clasohm@1556
    18
constdefs
nipkow@1531
    19
clasohm@1556
    20
  finite :: 'a set => bool
clasohm@1556
    21
  "finite A == A : Fin(UNIV)"
clasohm@1556
    22
clasohm@1556
    23
  card :: 'a set => nat
clasohm@1556
    24
  "card A == LEAST n. ? f. A = {f i |i. i<n}"
nipkow@1531
    25
clasohm@923
    26
end