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
     1 (*  Title:      HOL/Quot/HQUOT.thy
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 quotient constructor for higher order quotients
     7 
     8 *)
     9 
    10 HQUOT = PER +      
    11 
    12 typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
    13 
    14 (* constants for equivalence classes *)
    15 consts
    16         peclass         :: "'a::per => 'a quot"
    17         any_in          :: "'a::per quot => 'a"
    18 
    19 syntax          "@ecl"  :: "'a::per => 'a quot" ("<[ _ ]>")
    20 
    21 translations    "<[x]>" == "peclass x"
    22 
    23 defs
    24         peclass_def     "<[x]> == Abs_quot {y. y===x}"
    25         any_in_def      "any_in f == @x.<[x]>=f"
    26 end
    27