src/HOL/Finite.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 6015 d1d5dd2f121c
child 7958 f531589c9fc1
permissions -rw-r--r--
tidying
     1 (*  Title:      HOL/Finite.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson & Tobias Nipkow
     4     Copyright   1995  University of Cambridge & TU Muenchen
     5 
     6 Finite sets, their cardinality, and a fold functional.
     7 *)
     8 
     9 Finite = Divides + Power + Inductive +
    10 
    11 consts Finites :: 'a set set
    12 
    13 inductive "Finites"
    14   intrs
    15     emptyI  "{} : Finites"
    16     insertI "A : Finites ==> insert a A : Finites"
    17 
    18 syntax finite :: 'a set => bool
    19 translations  "finite A"  ==  "A : Finites"
    20 
    21 (* This definition, although traditional, is ugly to work with
    22 constdefs
    23   card :: 'a set => nat
    24   "card A == LEAST n. ? f. A = {f i |i. i<n}"
    25 Therefore we have switched to an inductive one:
    26 *)
    27 
    28 consts cardR :: "('a set * nat) set"
    29 
    30 inductive cardR
    31 intrs
    32   EmptyI  "({},0) : cardR"
    33   InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
    34 
    35 constdefs
    36   card :: 'a set => nat
    37  "card A == @n. (A,n) : cardR"
    38 
    39 (*
    40 A "fold" functional for finite sets.  For n non-negative we have
    41     fold f e {x1,...,xn} = f x1 (... (f xn e))
    42 where f is at least left-commutative.
    43 *)
    44 
    45 consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
    46 
    47 inductive "foldSet f e"
    48   intrs
    49     emptyI   "({}, e) : foldSet f e"
    50 
    51     insertI  "[| x ~: A;  (A,y) : foldSet f e |]
    52 	      ==> (insert x A, f x y) : foldSet f e"
    53 
    54 constdefs
    55    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    56   "fold f e A == @x. (A,x) : foldSet f e"
    57   (* A frequent instance: *)
    58    setsum :: ('a => nat) => 'a set => nat
    59   "setsum f == fold (op+ o f) 0"
    60 
    61 locale LC =
    62   fixes
    63     f    :: ['b,'a] => 'a
    64   assumes
    65     lcomm    "f x (f y z) = f y (f x z)"
    66 
    67 locale ACe =
    68   fixes 
    69     f    :: ['a,'a] => 'a
    70     e    :: 'a
    71   assumes
    72     ident    "f x e = x"
    73     commute  "f x y = f y x"
    74     assoc    "f (f x y) z = f x (f y z)"
    75 
    76 end