src/HOL/Finite.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6015 d1d5dd2f121c
child 7958 f531589c9fc1
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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
berghofe@5101
     9
Finite = Divides + Power + Inductive +
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
nipkow@5626
    21
(* This definition, although traditional, is ugly to work with
clasohm@1556
    22
constdefs
clasohm@1556
    23
  card :: 'a set => nat
clasohm@1556
    24
  "card A == LEAST n. ? f. A = {f i |i. i<n}"
nipkow@5626
    25
Therefore we have switched to an inductive one:
nipkow@5626
    26
*)
nipkow@5626
    27
nipkow@5626
    28
consts cardR :: "('a set * nat) set"
nipkow@5626
    29
nipkow@5626
    30
inductive cardR
nipkow@5626
    31
intrs
nipkow@5626
    32
  EmptyI  "({},0) : cardR"
nipkow@5626
    33
  InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
nipkow@5626
    34
nipkow@5626
    35
constdefs
nipkow@5626
    36
  card :: 'a set => nat
nipkow@5626
    37
 "card A == @n. (A,n) : cardR"
nipkow@1531
    38
nipkow@5616
    39
(*
nipkow@5616
    40
A "fold" functional for finite sets.  For n non-negative we have
nipkow@5616
    41
    fold f e {x1,...,xn} = f x1 (... (f xn e))
nipkow@5616
    42
where f is at least left-commutative.
nipkow@5616
    43
*)
nipkow@5616
    44
nipkow@5616
    45
consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
nipkow@5616
    46
nipkow@5616
    47
inductive "foldSet f e"
nipkow@5616
    48
  intrs
nipkow@5616
    49
    emptyI   "({}, e) : foldSet f e"
nipkow@5616
    50
nipkow@5616
    51
    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
nipkow@5616
    52
	      ==> (insert x A, f x y) : foldSet f e"
nipkow@5616
    53
nipkow@5616
    54
constdefs
nipkow@5616
    55
   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
nipkow@5616
    56
  "fold f e A == @x. (A,x) : foldSet f e"
nipkow@5616
    57
  (* A frequent instance: *)
nipkow@5616
    58
   setsum :: ('a => nat) => 'a set => nat
nipkow@5616
    59
  "setsum f == fold (op+ o f) 0"
nipkow@5616
    60
nipkow@5616
    61
locale LC =
nipkow@5616
    62
  fixes
nipkow@5616
    63
    f    :: ['b,'a] => 'a
nipkow@5616
    64
  assumes
paulson@5782
    65
    lcomm    "f x (f y z) = f y (f x z)"
nipkow@5616
    66
nipkow@5616
    67
locale ACe =
nipkow@5616
    68
  fixes 
nipkow@5616
    69
    f    :: ['a,'a] => 'a
nipkow@5616
    70
    e    :: 'a
nipkow@5616
    71
  assumes
paulson@5782
    72
    ident    "f x e = x"
paulson@5782
    73
    commute  "f x y = f y x"
paulson@5782
    74
    assoc    "f (f x y) z = f x (f y z)"
nipkow@5616
    75
clasohm@923
    76
end