25 {name: string -> string, |
25 {name: string -> string, |
26 var: string * mixfix -> string * mixfix, |
26 var: string * mixfix -> string * mixfix, |
27 typ: typ -> typ, |
27 typ: typ -> typ, |
28 term: term -> term, |
28 term: term -> term, |
29 thm: thm -> thm} -> morphism |
29 thm: thm -> thm} -> morphism |
|
30 val name_morphism: (string -> string) -> morphism |
|
31 val var_morphism: (string * mixfix -> string * mixfix) -> morphism |
|
32 val typ_morphism: (typ -> typ) -> morphism |
|
33 val term_morphism: (term -> term) -> morphism |
|
34 val thm_morphism: (thm -> thm) -> morphism |
|
35 val identity: morphism |
30 val comp: morphism -> morphism -> morphism |
36 val comp: morphism -> morphism -> morphism |
31 val identity: morphism |
|
32 val transfer: theory -> morphism |
|
33 end; |
37 end; |
34 |
38 |
35 structure Morphism: MORPHISM = |
39 structure Morphism: MORPHISM = |
36 struct |
40 struct |
37 |
41 |
48 fun term (Morphism {term, ...}) = term; |
52 fun term (Morphism {term, ...}) = term; |
49 fun thm (Morphism {thm, ...}) = thm; |
53 fun thm (Morphism {thm, ...}) = thm; |
50 |
54 |
51 val morphism = Morphism; |
55 val morphism = Morphism; |
52 |
56 |
|
57 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, thm = I}; |
|
58 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, thm = I}; |
|
59 fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, thm = I}; |
|
60 fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, thm = I}; |
|
61 fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, thm = thm}; |
|
62 |
|
63 val identity = morphism {name = I, var = I, typ = I, term = I, thm = I}; |
|
64 |
53 fun comp |
65 fun comp |
54 (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1}) |
66 (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1}) |
55 (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) = |
67 (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) = |
56 morphism {name = name1 o name2, var = var1 o var2, |
68 morphism {name = name1 o name2, var = var1 o var2, |
57 typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2}; |
69 typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2}; |
58 |
70 |
59 fun phi1 $> phi2 = comp phi2 phi1; |
71 fun phi1 $> phi2 = comp phi2 phi1; |
60 |
72 |
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; |
73 end; |
66 |
74 |
67 structure BasicMorphism: BASIC_MORPHISM = Morphism; |
75 structure BasicMorphism: BASIC_MORPHISM = Morphism; |
68 open BasicMorphism; |
76 open BasicMorphism; |
69 |
|