src/HOL/Finite.thy

match_bind(_i): 'as' patterns;
assume, theorem, show etc.: propp;
tuned qed msg;

(*  Title:      HOL/Finite.thy
    ID:         $Id$
    Author:     Lawrence C Paulson & Tobias Nipkow
    Copyright   1995  University of Cambridge & TU Muenchen

Finite sets, their cardinality, and a fold functional.
*)

Finite = Divides + Power + Inductive +

consts Finites :: 'a set set

inductive "Finites"
  intrs
    emptyI  "{} : Finites"
    insertI "A : Finites ==> insert a A : Finites"

syntax finite :: 'a set => bool
translations  "finite A"  ==  "A : Finites"

(* This definition, although traditional, is ugly to work with
constdefs
  card :: 'a set => nat
  "card A == LEAST n. ? f. A = {f i |i. i<n}"
Therefore we have switched to an inductive one:
*)

consts cardR :: "('a set * nat) set"

inductive cardR
intrs
  EmptyI  "({},0) : cardR"
  InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"

constdefs
  card :: 'a set => nat
 "card A == @n. (A,n) : cardR"

(*
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.
*)

consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"

inductive "foldSet f e"
  intrs
    emptyI   "({}, e) : foldSet f e"

    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
	      ==> (insert x A, f x y) : foldSet f e"

constdefs
   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
  "fold f e A == @x. (A,x) : foldSet f e"
  (* A frequent instance: *)
   setsum :: ('a => nat) => 'a set => nat
  "setsum f == fold (op+ o f) 0"

locale LC =
  fixes
    f    :: ['b,'a] => 'a
  assumes
    lcomm    "f x (f y z) = f y (f x z)"
  defines
    (*nothing*)

locale ACe =
  fixes 
    f    :: ['a,'a] => 'a
    e    :: 'a
  assumes
    ident    "f x e = x"
    commute  "f x y = f y x"
    assoc    "f (f x y) z = f x (f y z)"
  defines

end