isabelle: src/ZF/Finite.thy@073116d65bb9 (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
12214 f368821d9c68 depends on Epsilon! wenzelm parents: 12175 diff changeset	9	Finite = Inductive + Epsilon + Nat +
9491 1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	10
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	11	(The natural numbers as a datatype)
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	12	rep_datatype
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	13	elim natE
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	14	induct nat_induct
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	15	case_eqns nat_case_0, nat_case_succ
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	16	recursor_eqns recursor_0, recursor_succ
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	17
1a36151ee2fc natify, a coercion to reduce the number of type constraints in arithmetic paulson parents: 6053 diff changeset	18
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	19	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	Fin :: i=>i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	21	FiniteFun :: [i,i]=>i ("(_ -\|\|>/ _)" [61, 60] 60)
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	22
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	23	inductive
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	24	domains "Fin(A)" <= "Pow(A)"
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	25	intrs
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	26	emptyI "0 : Fin(A)"
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	27	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	28	type_intrs empty_subsetI, cons_subsetI, PowI
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	29	type_elims "[make_elim PowD]"
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	30
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	31	inductive
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	32	domains "FiniteFun(A,B)" <= "Fin(A*B)"
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	33	intrs
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	34	emptyI "0 : A -\|\|> B"
1155 928a16e02f9f removed \...\ inside strings clasohm parents: 806 diff changeset	35	consI "[\| a: A; b: B; h: A -\|\|> B; a ~: domain(h)
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	36	\|] ==> cons(<a,b>,h) : A -\|\|> B"
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	37	type_intrs "Fin.intrs"
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	38	end

author	berghofe
	Mon, 21 Jan 2002 14:43:38 +0100
changeset 12822	073116d65bb9
parent 12214	f368821d9c68
child 13194	812b00ed1c03
permissions	-rw-r--r--