15 end |
14 end |
16 |
15 |
17 signature MORPHISM = |
16 signature MORPHISM = |
18 sig |
17 sig |
19 include BASIC_MORPHISM |
18 include BASIC_MORPHISM |
20 val var: morphism -> Name.binding * mixfix -> Name.binding * mixfix |
19 val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix |
21 val name: morphism -> Name.binding -> Name.binding |
20 val binding: morphism -> Binding.T -> Binding.T |
22 val typ: morphism -> typ -> typ |
21 val typ: morphism -> typ -> typ |
23 val term: morphism -> term -> term |
22 val term: morphism -> term -> term |
24 val fact: morphism -> thm list -> thm list |
23 val fact: morphism -> thm list -> thm list |
25 val thm: morphism -> thm -> thm |
24 val thm: morphism -> thm -> thm |
26 val cterm: morphism -> cterm -> cterm |
25 val cterm: morphism -> cterm -> cterm |
27 val morphism: |
26 val morphism: |
28 {name: Name.binding -> Name.binding, |
27 {binding: Binding.T -> Binding.T, |
29 var: Name.binding * mixfix -> Name.binding * mixfix, |
28 var: Binding.T * mixfix -> Binding.T * mixfix, |
30 typ: typ -> typ, |
29 typ: typ -> typ, |
31 term: term -> term, |
30 term: term -> term, |
32 fact: thm list -> thm list} -> morphism |
31 fact: thm list -> thm list} -> morphism |
33 val name_morphism: (Name.binding -> Name.binding) -> morphism |
32 val binding_morphism: (Binding.T -> Binding.T) -> morphism |
34 val var_morphism: (Name.binding * mixfix -> Name.binding * mixfix) -> morphism |
33 val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism |
35 val typ_morphism: (typ -> typ) -> morphism |
34 val typ_morphism: (typ -> typ) -> morphism |
36 val term_morphism: (term -> term) -> morphism |
35 val term_morphism: (term -> term) -> morphism |
37 val fact_morphism: (thm list -> thm list) -> morphism |
36 val fact_morphism: (thm list -> thm list) -> morphism |
38 val thm_morphism: (thm -> thm) -> morphism |
37 val thm_morphism: (thm -> thm) -> morphism |
39 val identity: morphism |
38 val identity: morphism |
44 |
43 |
45 structure Morphism: MORPHISM = |
44 structure Morphism: MORPHISM = |
46 struct |
45 struct |
47 |
46 |
48 datatype morphism = Morphism of |
47 datatype morphism = Morphism of |
49 {name: Name.binding -> Name.binding, |
48 {binding: Binding.T -> Binding.T, |
50 var: Name.binding * mixfix -> Name.binding * mixfix, |
49 var: Binding.T * mixfix -> Binding.T * mixfix, |
51 typ: typ -> typ, |
50 typ: typ -> typ, |
52 term: term -> term, |
51 term: term -> term, |
53 fact: thm list -> thm list}; |
52 fact: thm list -> thm list}; |
54 |
53 |
55 type declaration = morphism -> Context.generic -> Context.generic; |
54 type declaration = morphism -> Context.generic -> Context.generic; |
56 |
55 |
57 fun name (Morphism {name, ...}) = name; |
56 fun binding (Morphism {binding, ...}) = binding; |
58 fun var (Morphism {var, ...}) = var; |
57 fun var (Morphism {var, ...}) = var; |
59 fun typ (Morphism {typ, ...}) = typ; |
58 fun typ (Morphism {typ, ...}) = typ; |
60 fun term (Morphism {term, ...}) = term; |
59 fun term (Morphism {term, ...}) = term; |
61 fun fact (Morphism {fact, ...}) = fact; |
60 fun fact (Morphism {fact, ...}) = fact; |
62 val thm = singleton o fact; |
61 val thm = singleton o fact; |
63 val cterm = Drule.cterm_rule o thm; |
62 val cterm = Drule.cterm_rule o thm; |
64 |
63 |
65 val morphism = Morphism; |
64 val morphism = Morphism; |
66 |
65 |
67 fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I}; |
66 fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I}; |
68 fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I}; |
67 fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I}; |
69 fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I}; |
68 fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I}; |
70 fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I}; |
69 fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I}; |
71 fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact}; |
70 fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact}; |
72 fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm}; |
71 fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm}; |
73 |
72 |
74 val identity = morphism {name = I, var = I, typ = I, term = I, fact = I}; |
73 val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I}; |
75 |
74 |
76 fun compose |
75 fun compose |
77 (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1}) |
76 (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1}) |
78 (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) = |
77 (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) = |
79 morphism {name = name1 o name2, var = var1 o var2, |
78 morphism {binding = binding1 o binding2, var = var1 o var2, |
80 typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2}; |
79 typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2}; |
81 |
80 |
82 fun phi1 $> phi2 = compose phi2 phi1; |
81 fun phi1 $> phi2 = compose phi2 phi1; |
83 |
82 |
84 fun transform phi f = fn psi => f (phi $> psi); |
83 fun transform phi f = fn psi => f (phi $> psi); |