| author | wenzelm |
| Tue, 24 Aug 1999 11:50:58 +0200 | |
| changeset 7333 | 6cb15c6f1d9f |
| parent 3842 | b55686a7b22c |
| permissions | -rw-r--r-- |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
1 |
(* Title: HOL/Quot/HQUOT.thy |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
3 |
Author: Oscar Slotosch |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
5 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
6 |
quotient constructor for higher order quotients |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
7 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
8 |
*) |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
9 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
10 |
HQUOT = PER + |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
11 |
|
| 3842 | 12 |
typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
|
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
13 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
14 |
(* constants for equivalence classes *) |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
15 |
consts |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
16 |
peclass :: "'a::per => 'a quot" |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
17 |
any_in :: "'a::per quot => 'a" |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
18 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
19 |
syntax "@ecl" :: "'a::per => 'a quot" ("<[ _ ]>")
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
20 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
21 |
translations "<[x]>" == "peclass x" |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
22 |
|
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
23 |
defs |
| 3842 | 24 |
peclass_def "<[x]> == Abs_quot {y. y===x}"
|
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
25 |
any_in_def "any_in f == @x.<[x]>=f" |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
26 |
end |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
27 |