author | clasohm |
Wed, 21 Jun 1995 15:47:10 +0200 | |
changeset 1151 | c820b3cc3df0 |
parent 972 | e61b058d58d2 |
child 1476 | 608483c2122a |
permissions | -rw-r--r-- |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: Equiv.thy |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
3 |
Authors: Riccardo Mattolini, Dip. Sistemi e Informatica |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
4 |
Lawrence C Paulson, Cambridge University Computer Laboratory |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
Copyright 1994 Universita' di Firenze |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
Copyright 1993 University of Cambridge |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
Equivalence relations in Higher-Order Set Theory |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
9 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
Equiv = Relation + |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
consts |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
13 |
refl,equiv :: "['a set,('a*'a) set]=>bool" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
14 |
sym :: "('a*'a) set=>bool" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
15 |
"'/" :: "['a set,('a*'a) set]=>'a set set" (infixl 90) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
16 |
(*set of equiv classes*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
17 |
congruent :: "[('a*'a) set,'a=>'b]=>bool" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
19 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
20 |
defs |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
21 |
refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)" |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
22 |
sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
23 |
equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
24 |
quotient_def "A/r == UN x:A. {r^^{x}}" |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
25 |
congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
1151 | 26 |
congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. |
27 |
(y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
end |