equal
deleted
inserted
replaced
10 constdefs |
10 constdefs |
11 equiv :: "['a set, ('a*'a) set] => bool" |
11 equiv :: "['a set, ('a*'a) set] => bool" |
12 "equiv A r == refl A r & sym(r) & trans(r)" |
12 "equiv A r == refl A r & sym(r) & trans(r)" |
13 |
13 |
14 quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) |
14 quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) |
15 "A//r == UN x:A. {r^^{x}}" (*set of equiv classes*) |
15 "A//r == UN x:A. {r```{x}}" (*set of equiv classes*) |
16 |
16 |
17 congruent :: "[('a*'a) set, 'a=>'b] => bool" |
17 congruent :: "[('a*'a) set, 'a=>'b] => bool" |
18 "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
18 "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
19 |
19 |
20 congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool" |
20 congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool" |