author | wenzelm |
Wed, 31 Jul 2019 19:50:38 +0200 | |
changeset 70451 | 550a5a822edb |
parent 70310 | c82f59c47aaf |
child 74220 | c49134ee16c1 |
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 |
|
54740 | 19 |
exception MORPHISM of string * exn |
67650 | 20 |
val morphism: string -> |
21 |
{binding: (binding -> binding) list, |
|
22 |
typ: (typ -> typ) list, |
|
23 |
term: (term -> term) list, |
|
24 |
fact: (thm list -> thm list) list} -> morphism |
|
54740 | 25 |
val pretty: morphism -> Pretty.T |
29581 | 26 |
val binding: morphism -> binding -> binding |
69062 | 27 |
val binding_prefix: morphism -> (string * bool) list |
21476 | 28 |
val typ: morphism -> typ -> typ |
29 |
val term: morphism -> term -> term |
|
21521 | 30 |
val fact: morphism -> thm list -> thm list |
21476 | 31 |
val thm: morphism -> thm -> thm |
22235 | 32 |
val cterm: morphism -> cterm -> cterm |
67650 | 33 |
val identity: morphism |
34 |
val compose: morphism -> morphism -> morphism |
|
35 |
val transform: morphism -> (morphism -> 'a) -> morphism -> 'a |
|
36 |
val form: (morphism -> 'a) -> 'a |
|
54740 | 37 |
val binding_morphism: string -> (binding -> binding) -> morphism |
38 |
val typ_morphism: string -> (typ -> typ) -> morphism |
|
39 |
val term_morphism: string -> (term -> term) -> morphism |
|
40 |
val fact_morphism: string -> (thm list -> thm list) -> morphism |
|
41 |
val thm_morphism: string -> (thm -> thm) -> morphism |
|
53087 | 42 |
val transfer_morphism: theory -> morphism |
67664 | 43 |
val transfer_morphism': Proof.context -> morphism |
44 |
val transfer_morphism'': Context.generic -> morphism |
|
61064 | 45 |
val trim_context_morphism: morphism |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
46 |
val instantiate_frees_morphism: |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
47 |
((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism |
67651
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
48 |
val instantiate_morphism: |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
49 |
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism |
21476 | 50 |
end; |
51 |
||
52 |
structure Morphism: MORPHISM = |
|
53 |
struct |
|
54 |
||
54740 | 55 |
(* named functions *) |
56 |
||
57 |
type 'a funs = (string * ('a -> 'a)) list; |
|
58 |
||
59 |
exception MORPHISM of string * exn; |
|
60 |
||
61 |
fun app (name, f) x = f x |
|
62505 | 62 |
handle exn => |
63 |
if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn); |
|
54740 | 64 |
|
65 |
fun apply fs = fold_rev app fs; |
|
66 |
||
67 |
||
68 |
(* type morphism *) |
|
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
69 |
|
21476 | 70 |
datatype morphism = Morphism of |
54740 | 71 |
{names: string list, |
72 |
binding: binding funs, |
|
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
73 |
typ: typ funs, |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
74 |
term: term funs, |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
75 |
fact: thm list funs}; |
21476 | 76 |
|
24031 | 77 |
type declaration = morphism -> Context.generic -> Context.generic; |
78 |
||
67650 | 79 |
fun morphism a {binding, typ, term, fact} = |
80 |
Morphism { |
|
81 |
names = if a = "" then [] else [a], |
|
82 |
binding = map (pair a) binding, |
|
83 |
typ = map (pair a) typ, |
|
84 |
term = map (pair a) term, |
|
85 |
fact = map (pair a) fact}; |
|
86 |
||
54740 | 87 |
fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names)); |
88 |
||
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset
|
89 |
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); |
62663 | 90 |
|
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
91 |
fun binding (Morphism {binding, ...}) = apply binding; |
69062 | 92 |
fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of; |
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
93 |
fun typ (Morphism {typ, ...}) = apply typ; |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
94 |
fun term (Morphism {term, ...}) = apply term; |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
95 |
fun fact (Morphism {fact, ...}) = apply fact; |
21521 | 96 |
val thm = singleton o fact; |
22235 | 97 |
val cterm = Drule.cterm_rule o thm; |
21476 | 98 |
|
54740 | 99 |
|
67650 | 100 |
(* morphism combinators *) |
21492 | 101 |
|
54740 | 102 |
val identity = morphism "" {binding = [], typ = [], term = [], fact = []}; |
103 |
||
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
104 |
fun compose |
54740 | 105 |
(Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1}) |
106 |
(Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) = |
|
107 |
Morphism { |
|
108 |
names = names1 @ names2, |
|
109 |
binding = binding1 @ binding2, |
|
110 |
typ = typ1 @ typ2, |
|
111 |
term = term1 @ term2, |
|
112 |
fact = fact1 @ fact2}; |
|
21476 | 113 |
|
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
114 |
fun phi1 $> phi2 = compose phi2 phi1; |
21476 | 115 |
|
22670
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
116 |
fun transform phi f = fn psi => f (phi $> psi); |
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
117 |
fun form f = f identity; |
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
118 |
|
67650 | 119 |
|
120 |
(* concrete morphisms *) |
|
121 |
||
122 |
fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []}; |
|
123 |
fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []}; |
|
124 |
fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []}; |
|
125 |
fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]}; |
|
126 |
fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]}; |
|
127 |
||
70310
c82f59c47aaf
clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
wenzelm
parents:
69062
diff
changeset
|
128 |
val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer; |
67664 | 129 |
val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; |
130 |
val transfer_morphism'' = transfer_morphism o Context.theory_of; |
|
131 |
||
67650 | 132 |
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; |
133 |
||
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
134 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
135 |
(* instantiate *) |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
136 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
137 |
fun instantiate_frees_morphism ([], []) = identity |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
138 |
| instantiate_frees_morphism (cinstT, cinst) = |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
139 |
let |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
140 |
val instT = map (apsnd Thm.typ_of) cinstT; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
141 |
val inst = map (apsnd Thm.term_of) cinst; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
142 |
in |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
143 |
morphism "instantiate_frees" |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
144 |
{binding = [], |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
145 |
typ = if null instT then [] else [Term_Subst.instantiateT_frees instT], |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
146 |
term = [Term_Subst.instantiate_frees (instT, inst)], |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
147 |
fact = [map (Thm.instantiate_frees (cinstT, cinst))]} |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
148 |
end; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
149 |
|
67651
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
150 |
fun instantiate_morphism ([], []) = identity |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
151 |
| instantiate_morphism (cinstT, cinst) = |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
152 |
let |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
153 |
val instT = map (apsnd Thm.typ_of) cinstT; |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
154 |
val inst = map (apsnd Thm.term_of) cinst; |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
155 |
in |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
156 |
morphism "instantiate" |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
157 |
{binding = [], |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
158 |
typ = if null instT then [] else [Term_Subst.instantiateT instT], |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
159 |
term = [Term_Subst.instantiate (instT, inst)], |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
160 |
fact = [map (Thm.instantiate (cinstT, cinst))]} |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
161 |
end; |
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
162 |
|
21476 | 163 |
end; |
164 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
29605
diff
changeset
|
165 |
structure Basic_Morphism: BASIC_MORPHISM = Morphism; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
29605
diff
changeset
|
166 |
open Basic_Morphism; |