src/Pure/morphism.ML
changeset 21476 4677b7b84247
child 21492 c73faa8e98aa
equal deleted inserted replaced
21475:ec0d1cf0eb35 21476:4677b7b84247
       
     1 (*  Title:      Pure/morphism.ML
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Abstract morphisms on formal entities.
       
     6 *)
       
     7 
       
     8 infix 1 $>
       
     9 
       
    10 signature BASIC_MORPHISM =
       
    11 sig
       
    12   type morphism
       
    13   val $> : morphism * morphism -> morphism
       
    14 end
       
    15 
       
    16 signature MORPHISM =
       
    17 sig
       
    18   include BASIC_MORPHISM
       
    19   val var: morphism -> string * mixfix -> string * mixfix
       
    20   val name: morphism -> string -> string
       
    21   val typ: morphism -> typ -> typ
       
    22   val term: morphism -> term -> term
       
    23   val thm: morphism -> thm -> thm
       
    24   val morphism:
       
    25    {name: string -> string,
       
    26     var: string * mixfix -> string * mixfix,
       
    27     typ: typ -> typ,
       
    28     term: term -> term,
       
    29     thm: thm -> thm} -> morphism
       
    30   val comp: morphism -> morphism -> morphism
       
    31   val identity: morphism
       
    32   val transfer: theory -> morphism
       
    33 end;
       
    34 
       
    35 structure Morphism: MORPHISM =
       
    36 struct
       
    37 
       
    38 datatype morphism = Morphism of
       
    39  {name: string -> string,
       
    40   var: string * mixfix -> string * mixfix,
       
    41   typ: typ -> typ,
       
    42   term: term -> term,
       
    43   thm: thm -> thm};
       
    44 
       
    45 fun name (Morphism {name, ...}) = name;
       
    46 fun var (Morphism {var, ...}) = var;
       
    47 fun typ (Morphism {typ, ...}) = typ;
       
    48 fun term (Morphism {term, ...}) = term;
       
    49 fun thm (Morphism {thm, ...}) = thm;
       
    50 
       
    51 val morphism = Morphism;
       
    52 
       
    53 fun comp
       
    54     (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1})
       
    55     (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) =
       
    56   morphism {name = name1 o name2, var = var1 o var2,
       
    57     typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2};
       
    58 
       
    59 fun phi1 $> phi2 = comp phi2 phi1;
       
    60 
       
    61 val identity = morphism {name = I, var = I, typ = I, term = I, thm = I};
       
    62 
       
    63 fun transfer thy = morphism {name = I, var = I, typ = I, term = I, thm = Thm.transfer thy};
       
    64 
       
    65 end;
       
    66 
       
    67 structure BasicMorphism: BASIC_MORPHISM = Morphism;
       
    68 open BasicMorphism;
       
    69