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