isabelle: src/HOL/Finite.thy@25b2a895f864 (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
1556 2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	18	constdefs
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	19
1556 2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	20	finite :: 'a set => bool
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	21	"finite A == A : Fin(UNIV)"
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	22
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	23	card :: 'a set => nat
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	24	"card A == LEAST n. ? f. A = {f i \|i. i<n}"
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	25
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	26	end

author	wenzelm
	Fri, 25 Apr 1997 17:50:55 +0200
changeset 3061	25b2a895f864
parent 1556	2fd82cec17d4
child 3367	832c245d967c
permissions	-rw-r--r--