18 include BASIC_MORPHISM |
18 include BASIC_MORPHISM |
19 val var: morphism -> string * mixfix -> string * mixfix |
19 val var: morphism -> string * mixfix -> string * mixfix |
20 val name: morphism -> string -> string |
20 val name: morphism -> string -> string |
21 val typ: morphism -> typ -> typ |
21 val typ: morphism -> typ -> typ |
22 val term: morphism -> term -> term |
22 val term: morphism -> term -> term |
|
23 val fact: morphism -> thm list -> thm list |
23 val thm: morphism -> thm -> thm |
24 val thm: morphism -> thm -> thm |
24 val morphism: |
25 val morphism: |
25 {name: string -> string, |
26 {name: string -> string, |
26 var: string * mixfix -> string * mixfix, |
27 var: string * mixfix -> string * mixfix, |
27 typ: typ -> typ, |
28 typ: typ -> typ, |
28 term: term -> term, |
29 term: term -> term, |
29 thm: thm -> thm} -> morphism |
30 fact: thm list -> thm list} -> morphism |
30 val name_morphism: (string -> string) -> morphism |
31 val name_morphism: (string -> string) -> morphism |
31 val var_morphism: (string * mixfix -> string * mixfix) -> morphism |
32 val var_morphism: (string * mixfix -> string * mixfix) -> morphism |
32 val typ_morphism: (typ -> typ) -> morphism |
33 val typ_morphism: (typ -> typ) -> morphism |
33 val term_morphism: (term -> term) -> morphism |
34 val term_morphism: (term -> term) -> morphism |
|
35 val fact_morphism: (thm list -> thm list) -> morphism |
34 val thm_morphism: (thm -> thm) -> morphism |
36 val thm_morphism: (thm -> thm) -> morphism |
35 val identity: morphism |
37 val identity: morphism |
36 val comp: morphism -> morphism -> morphism |
38 val comp: morphism -> morphism -> morphism |
37 end; |
39 end; |
38 |
40 |
42 datatype morphism = Morphism of |
44 datatype morphism = Morphism of |
43 {name: string -> string, |
45 {name: string -> string, |
44 var: string * mixfix -> string * mixfix, |
46 var: string * mixfix -> string * mixfix, |
45 typ: typ -> typ, |
47 typ: typ -> typ, |
46 term: term -> term, |
48 term: term -> term, |
47 thm: thm -> thm}; |
49 fact: thm list -> thm list}; |
48 |
50 |
49 fun name (Morphism {name, ...}) = name; |
51 fun name (Morphism {name, ...}) = name; |
50 fun var (Morphism {var, ...}) = var; |
52 fun var (Morphism {var, ...}) = var; |
51 fun typ (Morphism {typ, ...}) = typ; |
53 fun typ (Morphism {typ, ...}) = typ; |
52 fun term (Morphism {term, ...}) = term; |
54 fun term (Morphism {term, ...}) = term; |
53 fun thm (Morphism {thm, ...}) = thm; |
55 fun fact (Morphism {fact, ...}) = fact; |
|
56 val thm = singleton o fact; |
54 |
57 |
55 val morphism = Morphism; |
58 val morphism = Morphism; |
56 |
59 |
57 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, thm = I}; |
60 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I}; |
58 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, thm = I}; |
61 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I}; |
59 fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, thm = I}; |
62 fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I}; |
60 fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, thm = I}; |
63 fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I}; |
61 fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, thm = thm}; |
64 fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact}; |
|
65 fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm}; |
62 |
66 |
63 val identity = morphism {name = I, var = I, typ = I, term = I, thm = I}; |
67 val identity = morphism {name = I, var = I, typ = I, term = I, fact = I}; |
64 |
68 |
65 fun comp |
69 fun comp |
66 (Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1}) |
70 (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1}) |
67 (Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) = |
71 (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) = |
68 morphism {name = name1 o name2, var = var1 o var2, |
72 morphism {name = name1 o name2, var = var1 o var2, |
69 typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2}; |
73 typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2}; |
70 |
74 |
71 fun phi1 $> phi2 = comp phi2 phi1; |
75 fun phi1 $> phi2 = comp phi2 phi1; |
72 |
76 |
73 end; |
77 end; |
74 |
78 |