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

author	nipkow
	Mon, 06 Aug 2001 13:43:24 +0200
changeset 11464	ddea204de5bc
parent 9491	1a36151ee2fc
child 12175	5cf58a1799a7
permissions	-rw-r--r--