src/ZF/Finite.thy
author paulson
Tue Aug 01 15:28:21 2000 +0200 (2000-08-01)
changeset 9491 1a36151ee2fc
parent 6053 8a1059aa01f0
child 12175 5cf58a1799a7
permissions -rw-r--r--
natify, a coercion to reduce the number of type constraints in arithmetic
     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 + Nat +
    10 
    11 setup setup_datatypes
    12 
    13 (*The natural numbers as a datatype*)
    14 rep_datatype 
    15   elim		natE
    16   induct	nat_induct
    17   case_eqns	nat_case_0, nat_case_succ
    18   recursor_eqns recursor_0, recursor_succ
    19 
    20 
    21 consts
    22   Fin       :: i=>i
    23   FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)
    24 
    25 inductive
    26   domains   "Fin(A)" <= "Pow(A)"
    27   intrs
    28     emptyI  "0 : Fin(A)"
    29     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    30   type_intrs empty_subsetI, cons_subsetI, PowI
    31   type_elims "[make_elim PowD]"
    32 
    33 inductive
    34   domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    35   intrs
    36     emptyI  "0 : A -||> B"
    37     consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
    38              |] ==> cons(<a,b>,h) : A -||> B"
    39   type_intrs "Fin.intrs"
    40 end