21476
|
1 |
(* Title: Pure/morphism.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Abstract morphisms on formal entities.
|
|
6 |
*)
|
|
7 |
|
|
8 |
infix 1 $>
|
|
9 |
|
|
10 |
signature BASIC_MORPHISM =
|
|
11 |
sig
|
|
12 |
type morphism
|
|
13 |
val $> : morphism * morphism -> morphism
|
|
14 |
end
|
|
15 |
|
|
16 |
signature MORPHISM =
|
|
17 |
sig
|
|
18 |
include BASIC_MORPHISM
|
|
19 |
val var: morphism -> string * mixfix -> string * mixfix
|
|
20 |
val name: morphism -> string -> string
|
|
21 |
val typ: morphism -> typ -> typ
|
|
22 |
val term: morphism -> term -> term
|
|
23 |
val thm: morphism -> thm -> thm
|
|
24 |
val morphism:
|
|
25 |
{name: string -> string,
|
|
26 |
var: string * mixfix -> string * mixfix,
|
|
27 |
typ: typ -> typ,
|
|
28 |
term: term -> term,
|
|
29 |
thm: thm -> thm} -> morphism
|
|
30 |
val comp: morphism -> morphism -> morphism
|
|
31 |
val identity: morphism
|
|
32 |
val transfer: theory -> morphism
|
|
33 |
end;
|
|
34 |
|
|
35 |
structure Morphism: MORPHISM =
|
|
36 |
struct
|
|
37 |
|
|
38 |
datatype morphism = Morphism of
|
|
39 |
{name: string -> string,
|
|
40 |
var: string * mixfix -> string * mixfix,
|
|
41 |
typ: typ -> typ,
|
|
42 |
term: term -> term,
|
|
43 |
thm: thm -> thm};
|
|
44 |
|
|
45 |
fun name (Morphism {name, ...}) = name;
|
|
46 |
fun var (Morphism {var, ...}) = var;
|
|
47 |
fun typ (Morphism {typ, ...}) = typ;
|
|
48 |
fun term (Morphism {term, ...}) = term;
|
|
49 |
fun thm (Morphism {thm, ...}) = thm;
|
|
50 |
|
|
51 |
val morphism = Morphism;
|
|
52 |
|
|
53 |
fun comp
|
|
54 |
(Morphism {name = name1, var = var1, typ = typ1, term = term1, thm = thm1})
|
|
55 |
(Morphism {name = name2, var = var2, typ = typ2, term = term2, thm = thm2}) =
|
|
56 |
morphism {name = name1 o name2, var = var1 o var2,
|
|
57 |
typ = typ1 o typ2, term = term1 o term2, thm = thm1 o thm2};
|
|
58 |
|
|
59 |
fun phi1 $> phi2 = comp phi2 phi1;
|
|
60 |
|
|
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;
|
|
66 |
|
|
67 |
structure BasicMorphism: BASIC_MORPHISM = Morphism;
|
|
68 |
open BasicMorphism;
|
|
69 |
|