src/HOL/Finite.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9087 12db178a78df
child 11092 69c1abb9a129
permissions -rw-r--r--
improved theory reference in comment
     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 + SetInterval +
    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 axclass	finite<term
    22   finite "finite UNIV"
    23 
    24 (* This definition, although traditional, is ugly to work with
    25 constdefs
    26   card :: 'a set => nat
    27   "card A == LEAST n. ? f. A = {f i |i. i<n}"
    28 Therefore we have switched to an inductive one:
    29 *)
    30 
    31 consts cardR :: "('a set * nat) set"
    32 
    33 inductive cardR
    34 intrs
    35   EmptyI  "({},0) : cardR"
    36   InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
    37 
    38 constdefs
    39   card :: 'a set => nat
    40  "card A == @n. (A,n) : cardR"
    41 
    42 (*
    43 A "fold" functional for finite sets.  For n non-negative we have
    44     fold f e {x1,...,xn} = f x1 (... (f xn e))
    45 where f is at least left-commutative.
    46 *)
    47 
    48 consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
    49 
    50 inductive "foldSet f e"
    51   intrs
    52     emptyI   "({}, e) : foldSet f e"
    53 
    54     insertI  "[| x ~: A;  (A,y) : foldSet f e |]
    55 	      ==> (insert x A, f x y) : foldSet f e"
    56 
    57 constdefs
    58    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
    59   "fold f e A == @x. (A,x) : foldSet f e"
    60 
    61    setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
    62   "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
    63 
    64 locale LC =
    65   fixes
    66     f    :: ['b,'a] => 'a
    67   assumes
    68     lcomm    "f x (f y z) = f y (f x z)"
    69 
    70 locale ACe =
    71   fixes 
    72     f    :: ['a,'a] => 'a
    73     e    :: 'a
    74   assumes
    75     ident    "f x e = x"
    76     commute  "f x y = f y x"
    77     assoc    "f (f x y) z = f x (f y z)"
    78 
    79 end