author | haftmann |
Mon, 15 Dec 2008 09:58:45 +0100 | |
changeset 29105 | 8f38bf68d42e |
parent 28965 | 1de908189869 |
child 29581 | b3b33e0298eb |
permissions | -rw-r--r-- |
21476 | 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 |
|
24031 | 12 |
type declaration = morphism -> Context.generic -> Context.generic |
21476 | 13 |
val $> : morphism * morphism -> morphism |
14 |
end |
|
15 |
||
16 |
signature MORPHISM = |
|
17 |
sig |
|
18 |
include BASIC_MORPHISM |
|
28965 | 19 |
val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix |
20 |
val binding: morphism -> Binding.T -> Binding.T |
|
21476 | 21 |
val typ: morphism -> typ -> typ |
22 |
val term: morphism -> term -> term |
|
21521 | 23 |
val fact: morphism -> thm list -> thm list |
21476 | 24 |
val thm: morphism -> thm -> thm |
22235 | 25 |
val cterm: morphism -> cterm -> cterm |
21476 | 26 |
val morphism: |
28965 | 27 |
{binding: Binding.T -> Binding.T, |
28 |
var: Binding.T * mixfix -> Binding.T * mixfix, |
|
21476 | 29 |
typ: typ -> typ, |
30 |
term: term -> term, |
|
21521 | 31 |
fact: thm list -> thm list} -> morphism |
28965 | 32 |
val binding_morphism: (Binding.T -> Binding.T) -> morphism |
33 |
val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism |
|
21492 | 34 |
val typ_morphism: (typ -> typ) -> morphism |
35 |
val term_morphism: (term -> term) -> morphism |
|
21521 | 36 |
val fact_morphism: (thm list -> thm list) -> morphism |
21492 | 37 |
val thm_morphism: (thm -> thm) -> morphism |
21476 | 38 |
val identity: morphism |
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
39 |
val compose: morphism -> morphism -> morphism |
22670
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
40 |
val transform: morphism -> (morphism -> 'a) -> morphism -> 'a |
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
41 |
val form: (morphism -> 'a) -> 'a |
21476 | 42 |
end; |
43 |
||
44 |
structure Morphism: MORPHISM = |
|
45 |
struct |
|
46 |
||
47 |
datatype morphism = Morphism of |
|
28965 | 48 |
{binding: Binding.T -> Binding.T, |
49 |
var: Binding.T * mixfix -> Binding.T * mixfix, |
|
21476 | 50 |
typ: typ -> typ, |
51 |
term: term -> term, |
|
21521 | 52 |
fact: thm list -> thm list}; |
21476 | 53 |
|
24031 | 54 |
type declaration = morphism -> Context.generic -> Context.generic; |
55 |
||
28965 | 56 |
fun binding (Morphism {binding, ...}) = binding; |
21476 | 57 |
fun var (Morphism {var, ...}) = var; |
58 |
fun typ (Morphism {typ, ...}) = typ; |
|
59 |
fun term (Morphism {term, ...}) = term; |
|
21521 | 60 |
fun fact (Morphism {fact, ...}) = fact; |
61 |
val thm = singleton o fact; |
|
22235 | 62 |
val cterm = Drule.cterm_rule o thm; |
21476 | 63 |
|
64 |
val morphism = Morphism; |
|
65 |
||
28965 | 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}; |
|
21492 | 72 |
|
28965 | 73 |
val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I}; |
21492 | 74 |
|
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
75 |
fun compose |
28965 | 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, |
|
21521 | 79 |
typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2}; |
21476 | 80 |
|
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
81 |
fun phi1 $> phi2 = compose phi2 phi1; |
21476 | 82 |
|
22670
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
83 |
fun transform phi f = fn psi => f (phi $> psi); |
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
84 |
fun form f = f identity; |
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
85 |
|
21476 | 86 |
end; |
87 |
||
88 |
structure BasicMorphism: BASIC_MORPHISM = Morphism; |
|
89 |
open BasicMorphism; |