isabelle: src/HOL/Finite.thy@f886dbd91ee5 (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
3389 3150eba724a1 New theorem about the cardinality of the powerset (uses exponentiation) paulson parents: 3367 diff changeset	9	Finite = Divides + Power +
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	10
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	11	consts Finites :: 'a set set
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	13	inductive "Finites"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	intrs
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	15	emptyI "{} : Finites"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	16	insertI "A : Finites ==> insert a A : Finites"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	17
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	18	syntax finite :: 'a set => bool
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	19	translations "finite A" == "A : Finites"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	20
1556 2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	21	constdefs
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	22	card :: 'a set => nat
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	23	"card A == LEAST n. ? f. A = {f i \|i. i<n}"
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	24
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	25	end

author	paulson
	Wed, 23 Jul 1997 11:52:22 +0200
changeset 3564	f886dbd91ee5
parent 3413	c1f63cc3a768
child 5101	52e7c75acfe6
permissions	-rw-r--r--