src/ZF/Finite.thy
 changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 6053 8a1059aa01f0
equal inserted replaced
1477:4c51ab632cda 1478:2b8c2a7547ab
`     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`
`     6 Finite powerset operator`
`     7 *)`
`     7 *)`
`     8 `
`     8 `
`     9 Finite = Arith + Inductive +`
`     9 Finite = Arith + Inductive +`
`    10 consts`
`    10 consts`
`    11   Fin 	    :: i=>i`
`    11   Fin       :: i=>i`
`    12   FiniteFun :: [i,i]=>i		("(_ -||>/ _)" [61, 60] 60)`
`    12   FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)`
`    13 `
`    13 `
`    14 inductive`
`    14 inductive`
`    15   domains   "Fin(A)" <= "Pow(A)"`
`    15   domains   "Fin(A)" <= "Pow(A)"`
`    16   intrs`
`    16   intrs`
`    17     emptyI  "0 : Fin(A)"`
`    17     emptyI  "0 : Fin(A)"`
`    22 inductive`
`    22 inductive`
`    23   domains   "FiniteFun(A,B)" <= "Fin(A*B)"`
`    23   domains   "FiniteFun(A,B)" <= "Fin(A*B)"`
`    24   intrs`
`    24   intrs`
`    25     emptyI  "0 : A -||> B"`
`    25     emptyI  "0 : A -||> B"`
`    26     consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   `
`    26     consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   `
`    27 	     |] ==> cons(<a,b>,h) : A -||> B"`
`    27              |] ==> cons(<a,b>,h) : A -||> B"`
`    28   type_intrs "Fin.intrs"`
`    28   type_intrs "Fin.intrs"`
`    29 end`
`    29 end`