src/ZF/Induct/FoldSet.thy
author paulson
Tue, 21 May 2002 13:06:36 +0200
changeset 13168 afcbca3498b0
parent 12860 7fc3fbfed8ef
child 13194 812b00ed1c03
permissions -rw-r--r--
converted domrange to Isar and merged with equalities

(*  Title:      ZF/Induct/FoldSet.thy
    ID:         $Id$
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory


A "fold" functional for finite sets.  For n non-negative we have
fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
least left-commutative.  
*)

FoldSet =  Main +

consts fold_set :: "[i, i, [i,i]=>i, i] => i"

inductive
  domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
  intrs
  emptyI   "e:B ==> <0, e>:fold_set(A, B, f,e)"
  consI  "[| x:A; x ~:C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
              ==>  <cons(x,C), f(x,y)>:fold_set(A, B, f, e)"
   type_intrs "Fin.intrs"
  
constdefs
  
  fold :: "[i, [i,i]=>i, i, i] => i"  ("fold[_]'(_,_,_')")
  "fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)"

   setsum :: "[i=>i, i] => i"
  "setsum(g, C) == if Finite(C) then
                    fold[int](%x y. g(x) $+ y, #0, C) else #0"
end