src/ZF/Finite.thy
author wenzelm
Thu Nov 15 18:37:34 2001 +0100 (2001-11-15)
changeset 12214 f368821d9c68
parent 12175 5cf58a1799a7
child 13194 812b00ed1c03
permissions -rw-r--r--
depends on Epsilon!
     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 = Inductive + Epsilon + Nat +
    10 
    11 (*The natural numbers as a datatype*)
    12 rep_datatype 
    13   elim		natE
    14   induct	nat_induct
    15   case_eqns	nat_case_0, nat_case_succ
    16   recursor_eqns recursor_0, recursor_succ
    17 
    18 
    19 consts
    20   Fin       :: i=>i
    21   FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)
    22 
    23 inductive
    24   domains   "Fin(A)" <= "Pow(A)"
    25   intrs
    26     emptyI  "0 : Fin(A)"
    27     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    28   type_intrs empty_subsetI, cons_subsetI, PowI
    29   type_elims "[make_elim PowD]"
    30 
    31 inductive
    32   domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    33   intrs
    34     emptyI  "0 : A -||> B"
    35     consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
    36              |] ==> cons(<a,b>,h) : A -||> B"
    37   type_intrs "Fin.intrs"
    38 end