src/Pure/morphism.ML
changeset 22670 c803b2696ada
parent 22571 3f00e937d1c9
child 24031 e94e541346d7
equal deleted inserted replaced
22669:62857ad97cca 22670:c803b2696ada
    35   val term_morphism: (term -> term) -> morphism
    35   val term_morphism: (term -> term) -> morphism
    36   val fact_morphism: (thm list -> thm list) -> morphism
    36   val fact_morphism: (thm list -> thm list) -> morphism
    37   val thm_morphism: (thm -> thm) -> morphism
    37   val thm_morphism: (thm -> thm) -> morphism
    38   val identity: morphism
    38   val identity: morphism
    39   val compose: morphism -> morphism -> morphism
    39   val compose: morphism -> morphism -> morphism
       
    40   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
       
    41   val form: (morphism -> 'a) -> 'a
    40 end;
    42 end;
    41 
    43 
    42 structure Morphism: MORPHISM =
    44 structure Morphism: MORPHISM =
    43 struct
    45 struct
    44 
    46 
    74   morphism {name = name1 o name2, var = var1 o var2,
    76   morphism {name = name1 o name2, var = var1 o var2,
    75     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
    77     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
    76 
    78 
    77 fun phi1 $> phi2 = compose phi2 phi1;
    79 fun phi1 $> phi2 = compose phi2 phi1;
    78 
    80 
       
    81 fun transform phi f = fn psi => f (phi $> psi);
       
    82 fun form f = f identity;
       
    83 
    79 end;
    84 end;
    80 
    85 
    81 structure BasicMorphism: BASIC_MORPHISM = Morphism;
    86 structure BasicMorphism: BASIC_MORPHISM = Morphism;
    82 open BasicMorphism;
    87 open BasicMorphism;