author | lcp |
Fri, 12 Aug 1994 12:51:34 +0200 | |
changeset 516 | 1957113f0d7d |
child 534 | cd8bec47e175 |
permissions | -rw-r--r-- |
516 | 1 |
(* Title: ZF/Finite.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Finite powerset operator |
|
7 |
*) |
|
8 |
||
9 |
Finite = Arith + |
|
10 |
consts Fin :: "i=>i" |
|
11 |
inductive |
|
12 |
domains "Fin(A)" <= "Pow(A)" |
|
13 |
intrs |
|
14 |
emptyI "0 : Fin(A)" |
|
15 |
consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" |
|
16 |
type_intrs "[empty_subsetI, cons_subsetI, PowI]" |
|
17 |
type_elims "[make_elim PowD]" |
|
18 |
end |