isabelle: src/ZF/Finite.thy@20c42415c07d (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Finite.thy
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	5
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	6	Finite powerset operator
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	7	*)
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	8
806 6330ca0a3ac5 removed quotes around "Inductive" lcp parents: 578 diff changeset	9	Finite = Arith + Inductive +
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	10	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	11	Fin :: i=>i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	12	FiniteFun :: [i,i]=>i ("(_ -\|\|>/ _)" [61, 60] 60)
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	13
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	14	inductive
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	15	domains "Fin(A)" <= "Pow(A)"
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	16	intrs
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	17	emptyI "0 : Fin(A)"
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	18	consI "[\| a: A; b: Fin(A) \|] ==> cons(a,b) : Fin(A)"
6053 8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 1478 diff changeset	19	type_intrs empty_subsetI, cons_subsetI, PowI
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	20	type_elims "[make_elim PowD]"
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	21
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	22	inductive
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	23	domains "FiniteFun(A,B)" <= "Fin(A*B)"
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	24	intrs
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	25	emptyI "0 : A -\|\|> B"
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 806 diff changeset	26	consI "[\| a: A; b: B; h: A -\|\|> B; a ~: domain(h)
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	27	\|] ==> cons(<a,b>,h) : A -\|\|> B"
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	28	type_intrs "Fin.intrs"
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	29	end

author	wenzelm
	Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717	20c42415c07d
parent 6053	8a1059aa01f0
child 9491	1a36151ee2fc
permissions	-rw-r--r--