author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8962  633e1682455c 
child 9087  12db178a78df 
permissions  rwrr 
1475  1 
(* Title: HOL/Finite.thy 
923  2 
ID: $Id$ 
1531  3 
Author: Lawrence C Paulson & Tobias Nipkow 
4 
Copyright 1995 University of Cambridge & TU Muenchen 

923  5 

5616  6 
Finite sets, their cardinality, and a fold functional. 
923  7 
*) 
8 

8962  9 
Finite = Divides + Power + Inductive + SetInterval + 
1531  10 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

11 
consts Finites :: 'a set set 
923  12 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

13 
inductive "Finites" 
923  14 
intrs 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

15 
emptyI "{} : Finites" 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

16 
insertI "A : Finites ==> insert a A : Finites" 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

17 

c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

18 
syntax finite :: 'a set => bool 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
3389
diff
changeset

19 
translations "finite A" == "A : Finites" 
923  20 

7958  21 
axclass finite<term 
22 
finite "finite UNIV" 

23 

5626  24 
(* This definition, although traditional, is ugly to work with 
1556  25 
constdefs 
26 
card :: 'a set => nat 

27 
"card A == LEAST n. ? f. A = {f i i. i<n}" 

5626  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" 

1531  41 

5616  42 
(* 
43 
A "fold" functional for finite sets. For n nonnegative we have 

44 
fold f e {x1,...,xn} = f x1 (... (f xn e)) 

45 
where f is at least leftcommutative. 

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" 

8962  60 

61 
setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)" 

5616  62 
"setsum f == fold (op+ o f) 0" 
63 

64 
locale LC = 

65 
fixes 

66 
f :: ['b,'a] => 'a 

67 
assumes 

5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

68 
lcomm "f x (f y z) = f y (f x z)" 
5616  69 

70 
locale ACe = 

71 
fixes 

72 
f :: ['a,'a] => 'a 

73 
e :: 'a 

74 
assumes 

5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

75 
ident "f x e = x" 
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

76 
commute "f x y = f y x" 
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5626
diff
changeset

77 
assoc "f (f x y) z = f x (f y z)" 
5616  78 

923  79 
end 