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