equal
deleted
inserted
replaced
1 (* Title: ZF/Finite.thy |
1 (* Title: ZF/Finite.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Finite powerset operator; finite function space |
|
7 |
|
8 prove X:Fin(A) ==> |X| < nat |
6 prove X:Fin(A) ==> |X| < nat |
9 |
7 |
10 prove: b: Fin(A) ==> inj(b,b) <= surj(b,b) |
8 prove: b: Fin(A) ==> inj(b,b) <= surj(b,b) |
11 *) |
9 *) |
|
10 |
|
11 header{*Finite Powerset Operator and Finite Function Space*} |
12 |
12 |
13 theory Finite = Inductive + Epsilon + Nat: |
13 theory Finite = Inductive + Epsilon + Nat: |
14 |
14 |
15 (*The natural numbers as a datatype*) |
15 (*The natural numbers as a datatype*) |
16 rep_datatype |
16 rep_datatype |