src/HOL/Finite.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8962 633e1682455c
child 9087 12db178a78df
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1370
diff changeset
     1
(*  Title:      HOL/Finite.thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1475
diff changeset
     3
    Author:     Lawrence C Paulson & Tobias Nipkow
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1475
diff changeset
     4
    Copyright   1995  University of Cambridge & TU Muenchen
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
5616
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
     6
Finite sets, their cardinality, and a fold functional.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
8962
633e1682455c setsum is now overloaded on plus_ac0
paulson
parents: 7958
diff changeset
     9
Finite = Divides + Power + Inductive + SetInterval +
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1475
diff changeset
    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
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3389
diff changeset
    13
inductive "Finites"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    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
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
7958
f531589c9fc1 added various little lemmas
oheimb
parents: 6015
diff changeset
    21
axclass	finite<term
f531589c9fc1 added various little lemmas
oheimb
parents: 6015
diff changeset
    22
  finite "finite UNIV"
f531589c9fc1 added various little lemmas
oheimb
parents: 6015
diff changeset
    23
5626
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    24
(* This definition, although traditional, is ugly to work with
1556
2fd82cec17d4 added constdefs section
clasohm
parents: 1531
diff changeset
    25
constdefs
2fd82cec17d4 added constdefs section
clasohm
parents: 1531
diff changeset
    26
  card :: 'a set => nat
2fd82cec17d4 added constdefs section
clasohm
parents: 1531
diff changeset
    27
  "card A == LEAST n. ? f. A = {f i |i. i<n}"
5626
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    28
Therefore we have switched to an inductive one:
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    29
*)
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    30
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    31
consts cardR :: "('a set * nat) set"
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    32
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    33
inductive cardR
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    34
intrs
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    35
  EmptyI  "({},0) : cardR"
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    36
  InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    37
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    38
constdefs
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    39
  card :: 'a set => nat
f67c34721486 New inductive definition of `card'
nipkow
parents: 5616
diff changeset
    40
 "card A == @n. (A,n) : cardR"
1531
e5eb247ad13c Added a constant UNIV == {x.True}
nipkow
parents: 1475
diff changeset
    41
5616
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    42
(*
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    43
A "fold" functional for finite sets.  For n non-negative we have
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    44
    fold f e {x1,...,xn} = f x1 (... (f xn e))
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    45
where f is at least left-commutative.
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    46
*)
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    47
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    48
consts foldSet :: "[['b,'a] => 'a, 'a] => ('b set * 'a) set"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    49
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    50
inductive "foldSet f e"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    51
  intrs
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    52
    emptyI   "({}, e) : foldSet f e"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    53
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    54
    insertI  "[| x ~: A;  (A,y) : foldSet f e |]
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    55
	      ==> (insert x A, f x y) : foldSet f e"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    56
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    57
constdefs
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    58
   fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    59
  "fold f e A == @x. (A,x) : foldSet f e"
8962
633e1682455c setsum is now overloaded on plus_ac0
paulson
parents: 7958
diff changeset
    60
633e1682455c setsum is now overloaded on plus_ac0
paulson
parents: 7958
diff changeset
    61
   setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)"
5616
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    62
  "setsum f == fold (op+ o f) 0"
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    63
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    64
locale LC =
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    65
  fixes
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    66
    f    :: ['b,'a] => 'a
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    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
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    69
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    70
locale ACe =
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    71
  fixes 
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    72
    f    :: ['a,'a] => 'a
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    73
    e    :: 'a
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    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
497eeeace3fc Merges FoldSet into Finite
nipkow
parents: 5101
diff changeset
    78
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
end