isabelle: src/ZF/Finite.thy@436019ca97d7 (annotated)

516 1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	1	(* Title: ZF/Finite.thy
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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
578 efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without lcp parents: 534 diff changeset	9	Finite = Arith + "Inductive" +
534 cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	10	consts
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	11	Fin :: "i=>i"
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	12	FiniteFun :: "[i,i]=>i" ("(_ -\|\|>/ _)" [61, 60] 60)
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)"
1957113f0d7d installation of new inductive/datatype sections lcp parents: diff changeset	19	type_intrs "[empty_subsetI, cons_subsetI, PowI]"
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"
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	26	consI "[\| a: A; b: B; h: A -\|\|> B; a ~: domain(h) \
cd8bec47e175 ZF/Finite: added the finite function space, A-\|\|>B lcp parents: 516 diff changeset	27	\ \|] ==> cons(<a,b>,h) : A -\|\|> B"
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	lcp
	Thu, 24 Nov 1994 10:23:41 +0100
changeset 737	436019ca97d7
parent 578	efc648d29dd0
child 806	6330ca0a3ac5
permissions	-rw-r--r--