src/ZF/Finite.thy
changeset 534 cd8bec47e175
parent 516 1957113f0d7d
child 578 efc648d29dd0
     1.1 --- a/src/ZF/Finite.thy	Tue Aug 16 19:01:26 1994 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Aug 16 19:03:45 1994 +0200
     1.3 @@ -7,7 +7,10 @@
     1.4  *)
     1.5  
     1.6  Finite = Arith + 
     1.7 -consts Fin :: "i=>i"
     1.8 +consts
     1.9 +  Fin 	    :: "i=>i"
    1.10 +  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
    1.11 +
    1.12  inductive
    1.13    domains   "Fin(A)" <= "Pow(A)"
    1.14    intrs
    1.15 @@ -15,4 +18,12 @@
    1.16      consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
    1.17    type_intrs "[empty_subsetI, cons_subsetI, PowI]"
    1.18    type_elims "[make_elim PowD]"
    1.19 +
    1.20 +inductive
    1.21 +  domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    1.22 +  intrs
    1.23 +    emptyI  "0 : A -||> B"
    1.24 +    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
    1.25 +\	     |] ==> cons(<a,b>,h) : A -||> B"
    1.26 +  type_intrs "Fin.intrs"
    1.27  end