src/Pure/morphism.ML
author haftmann
Wed Jan 21 16:47:32 2009 +0100 (2009-01-21)
changeset 29581 b3b33e0298eb
parent 28965 1de908189869
child 29605 f2924219125e
permissions -rw-r--r--
binding is alias for Binding.T
     1 (*  Title:      Pure/morphism.ML
     2     Author:     Makarius
     3 
     4 Abstract morphisms on formal entities.
     5 *)
     6 
     7 infix 1 $>
     8 
     9 signature BASIC_MORPHISM =
    10 sig
    11   type morphism
    12   type declaration = morphism -> Context.generic -> Context.generic
    13   val $> : morphism * morphism -> morphism
    14 end
    15 
    16 signature MORPHISM =
    17 sig
    18   include BASIC_MORPHISM
    19   val var: morphism -> binding * mixfix -> binding * mixfix
    20   val binding: morphism -> binding -> binding
    21   val typ: morphism -> typ -> typ
    22   val term: morphism -> term -> term
    23   val fact: morphism -> thm list -> thm list
    24   val thm: morphism -> thm -> thm
    25   val cterm: morphism -> cterm -> cterm
    26   val morphism:
    27    {binding: binding -> binding,
    28     var: binding * mixfix -> binding * mixfix,
    29     typ: typ -> typ,
    30     term: term -> term,
    31     fact: thm list -> thm list} -> morphism
    32   val binding_morphism: (binding -> binding) -> morphism
    33   val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
    34   val typ_morphism: (typ -> typ) -> morphism
    35   val term_morphism: (term -> term) -> morphism
    36   val fact_morphism: (thm list -> thm list) -> morphism
    37   val thm_morphism: (thm -> thm) -> morphism
    38   val identity: morphism
    39   val compose: morphism -> morphism -> morphism
    40   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
    41   val form: (morphism -> 'a) -> 'a
    42 end;
    43 
    44 structure Morphism: MORPHISM =
    45 struct
    46 
    47 datatype morphism = Morphism of
    48  {binding: binding -> binding,
    49   var: binding * mixfix -> binding * mixfix,
    50   typ: typ -> typ,
    51   term: term -> term,
    52   fact: thm list -> thm list};
    53 
    54 type declaration = morphism -> Context.generic -> Context.generic;
    55 
    56 fun binding (Morphism {binding, ...}) = binding;
    57 fun var (Morphism {var, ...}) = var;
    58 fun typ (Morphism {typ, ...}) = typ;
    59 fun term (Morphism {term, ...}) = term;
    60 fun fact (Morphism {fact, ...}) = fact;
    61 val thm = singleton o fact;
    62 val cterm = Drule.cterm_rule o thm;
    63 
    64 val morphism = Morphism;
    65 
    66 fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
    67 fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
    68 fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
    69 fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
    70 fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
    71 fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
    72 
    73 val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
    74 
    75 fun compose
    76     (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
    77     (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
    78   morphism {binding = binding1 o binding2, var = var1 o var2,
    79     typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
    80 
    81 fun phi1 $> phi2 = compose phi2 phi1;
    82 
    83 fun transform phi f = fn psi => f (phi $> psi);
    84 fun form f = f identity;
    85 
    86 end;
    87 
    88 structure BasicMorphism: BASIC_MORPHISM = Morphism;
    89 open BasicMorphism;