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