isabelle: src/HOL/Finite.thy@e5eb247ad13c (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	1	(* Title: HOL/Finite.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	3	Author: Lawrence C Paulson & Tobias Nipkow
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	4	Copyright 1995 University of Cambridge & TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	6	Finite sets and their cardinality
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	9	Finite = Arith +
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	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 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	inductive "Fin(A)"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	intrs
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	15	emptyI "{} : Fin(A)"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	16	insertI "[\| a: A; b: Fin(A) \|] ==> insert a b : Fin(A)"
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	17
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	18	consts finite :: 'a set => bool
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	19	defs finite_def "finite A == A : Fin(UNIV)"
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	20
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	21	consts card :: 'a set => nat
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	22	defs card_def "card A == LEAST n. ? f. A = {f i \|i. i<n}"
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	23
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	24	end

author	nipkow
	Mon, 04 Mar 1996 14:37:33 +0100
changeset 1531	e5eb247ad13c
parent 1475	7f5a4cd08209
child 1556	2fd82cec17d4
permissions	-rw-r--r--