author | wenzelm |
Thu, 06 Jun 2024 12:42:42 +0200 | |
changeset 80267 | ea908185a597 |
parent 78759 | 461e924cc825 |
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 |
|
12 |
val $> : morphism * morphism -> morphism |
|
13 |
end |
|
14 |
||
15 |
signature MORPHISM = |
|
16 |
sig |
|
17 |
include BASIC_MORPHISM |
|
54740 | 18 |
exception MORPHISM of string * exn |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
19 |
val the_theory: theory option -> theory |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
20 |
val set_context: theory -> morphism -> morphism |
78063 | 21 |
val set_context': Proof.context -> morphism -> morphism |
22 |
val set_context'': Context.generic -> morphism -> morphism |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
23 |
val reset_context: morphism -> morphism |
67650 | 24 |
val morphism: string -> |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
25 |
{binding: (theory option -> binding -> binding) list, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
26 |
typ: (theory option -> typ -> typ) list, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
27 |
term: (theory option -> term -> term) list, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
28 |
fact: (theory option -> thm list -> thm list) list} -> morphism |
77902 | 29 |
val is_identity: morphism -> bool |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
30 |
val is_empty: morphism -> bool |
54740 | 31 |
val pretty: morphism -> Pretty.T |
29581 | 32 |
val binding: morphism -> binding -> binding |
69062 | 33 |
val binding_prefix: morphism -> (string * bool) list |
21476 | 34 |
val typ: morphism -> typ -> typ |
35 |
val term: morphism -> term -> term |
|
21521 | 36 |
val fact: morphism -> thm list -> thm list |
21476 | 37 |
val thm: morphism -> thm -> thm |
22235 | 38 |
val cterm: morphism -> cterm -> cterm |
67650 | 39 |
val identity: morphism |
78060 | 40 |
val default: morphism option -> morphism |
67650 | 41 |
val compose: morphism -> morphism -> morphism |
78072 | 42 |
type 'a entity |
43 |
val entity: (morphism -> 'a) -> 'a entity |
|
78075
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
44 |
val entity_reset_context: 'a entity -> 'a entity |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
45 |
val entity_set_context: theory -> 'a entity -> 'a entity |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
46 |
val entity_set_context': Proof.context -> 'a entity -> 'a entity |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
47 |
val entity_set_context'': Context.generic -> 'a entity -> 'a entity |
78072 | 48 |
val transform: morphism -> 'a entity -> 'a entity |
78078 | 49 |
val transform_reset_context: morphism -> 'a entity -> 'a entity |
78072 | 50 |
val form: 'a entity -> 'a |
51 |
val form_entity: (morphism -> 'a) -> 'a |
|
78112 | 52 |
val form_context: theory -> (theory -> 'a) entity -> 'a |
53 |
val form_context': Proof.context -> (Proof.context -> 'a) entity -> 'a |
|
54 |
val form_context'': Context.generic -> (Context.generic -> 'a) entity -> 'a |
|
78085 | 55 |
type declaration = morphism -> Context.generic -> Context.generic |
56 |
type declaration_entity = (Context.generic -> Context.generic) entity |
|
54740 | 57 |
val binding_morphism: string -> (binding -> binding) -> morphism |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
58 |
val typ_morphism': string -> (theory -> typ -> typ) -> morphism |
54740 | 59 |
val typ_morphism: string -> (typ -> typ) -> morphism |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
60 |
val term_morphism': string -> (theory -> term -> term) -> morphism |
54740 | 61 |
val term_morphism: string -> (term -> term) -> morphism |
78081 | 62 |
val fact_morphism': string -> (theory -> thm list -> thm list) -> morphism |
54740 | 63 |
val fact_morphism: string -> (thm list -> thm list) -> morphism |
78081 | 64 |
val thm_morphism': string -> (theory -> thm -> thm) -> morphism |
54740 | 65 |
val thm_morphism: string -> (thm -> thm) -> morphism |
53087 | 66 |
val transfer_morphism: theory -> morphism |
67664 | 67 |
val transfer_morphism': Proof.context -> morphism |
68 |
val transfer_morphism'': Context.generic -> morphism |
|
61064 | 69 |
val trim_context_morphism: morphism |
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
70 |
val set_trim_context: theory -> morphism -> morphism |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
71 |
val set_trim_context': Proof.context -> morphism -> morphism |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
72 |
val set_trim_context'': Context.generic -> morphism -> morphism |
74282 | 73 |
val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism |
74 |
val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism |
|
21476 | 75 |
end; |
76 |
||
77 |
structure Morphism: MORPHISM = |
|
78 |
struct |
|
79 |
||
54740 | 80 |
(* named functions *) |
81 |
||
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
82 |
type 'a funs = (string * (theory option -> 'a -> 'a)) list; |
54740 | 83 |
|
84 |
exception MORPHISM of string * exn; |
|
85 |
||
78759 | 86 |
fun app context (name, f) x = |
87 |
Isabelle_Thread.try_catch (fn () => f context x) |
|
88 |
(fn exn => raise MORPHISM (name, exn)); |
|
54740 | 89 |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
90 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
91 |
(* optional context *) |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
92 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
93 |
fun the_theory (SOME thy) = thy |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
94 |
| the_theory NONE = raise Fail "Morphism lacks theory context"; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
95 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
96 |
fun join_transfer (SOME thy) = Thm.join_transfer thy |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
97 |
| join_transfer NONE = I; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
98 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
99 |
val join_context = join_options Context.join_certificate_theory; |
54740 | 100 |
|
101 |
||
102 |
(* type morphism *) |
|
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
103 |
|
21476 | 104 |
datatype morphism = Morphism of |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
105 |
{context: theory option, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
106 |
names: string list, |
54740 | 107 |
binding: binding funs, |
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
108 |
typ: typ funs, |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
109 |
term: term funs, |
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
37216
diff
changeset
|
110 |
fact: thm list funs}; |
21476 | 111 |
|
78057 | 112 |
fun rep (Morphism args) = args; |
113 |
||
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
114 |
fun apply which phi = |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
115 |
let val args = rep phi |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
116 |
in fold_rev (app (#context args)) (which args) end; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
117 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
118 |
fun put_context context (Morphism {context = _, names, binding, typ, term, fact}) = |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
119 |
Morphism {context = context, names = names, binding = binding, typ = typ, term = term, fact = fact}; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
120 |
|
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
121 |
val set_context = put_context o SOME; |
78063 | 122 |
val set_context' = set_context o Proof_Context.theory_of; |
123 |
val set_context'' = set_context o Context.theory_of; |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
124 |
val reset_context = put_context NONE; |
24031 | 125 |
|
67650 | 126 |
fun morphism a {binding, typ, term, fact} = |
127 |
Morphism { |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
128 |
context = NONE, |
67650 | 129 |
names = if a = "" then [] else [a], |
130 |
binding = map (pair a) binding, |
|
131 |
typ = map (pair a) typ, |
|
132 |
term = map (pair a) term, |
|
133 |
fact = map (pair a) fact}; |
|
134 |
||
77902 | 135 |
(*syntactic test only!*) |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
136 |
fun is_identity (Morphism {context = _, names, binding, typ, term, fact}) = |
77902 | 137 |
null names andalso null binding andalso null typ andalso null term andalso null fact; |
138 |
||
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
139 |
fun is_empty phi = is_none (#context (rep phi)) andalso is_identity phi; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
140 |
|
78057 | 141 |
fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi)))); |
54740 | 142 |
|
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset
|
143 |
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); |
62663 | 144 |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
145 |
val binding = apply #binding; |
69062 | 146 |
fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of; |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
147 |
val typ = apply #typ; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
148 |
val term = apply #term; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
149 |
fun fact phi = map (join_transfer (#context (rep phi))) #> apply #fact phi; |
21521 | 150 |
val thm = singleton o fact; |
22235 | 151 |
val cterm = Drule.cterm_rule o thm; |
21476 | 152 |
|
54740 | 153 |
|
67650 | 154 |
(* morphism combinators *) |
21492 | 155 |
|
54740 | 156 |
val identity = morphism "" {binding = [], typ = [], term = [], fact = []}; |
157 |
||
78060 | 158 |
val default = the_default identity; |
159 |
||
78057 | 160 |
fun compose phi1 phi2 = |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
161 |
if is_empty phi1 then phi2 |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
162 |
else if is_empty phi2 then phi1 |
78058 | 163 |
else |
164 |
let |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
165 |
val {context = context1, names = names1, binding = binding1, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
166 |
typ = typ1, term = term1, fact = fact1} = rep phi1; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
167 |
val {context = context2, names = names2, binding = binding2, |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
168 |
typ = typ2, term = term2, fact = fact2} = rep phi2; |
78058 | 169 |
in |
170 |
Morphism { |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
171 |
context = join_context (context1, context2), |
78058 | 172 |
names = names1 @ names2, |
173 |
binding = binding1 @ binding2, |
|
174 |
typ = typ1 @ typ2, |
|
175 |
term = term1 @ term2, |
|
176 |
fact = fact1 @ fact2} |
|
177 |
end; |
|
21476 | 178 |
|
22571
3f00e937d1c9
renamed comp to compose (avoid clash with Alice keywords);
wenzelm
parents:
22235
diff
changeset
|
179 |
fun phi1 $> phi2 = compose phi2 phi1; |
21476 | 180 |
|
78072 | 181 |
|
182 |
(* abstract entities *) |
|
183 |
||
78075
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
184 |
datatype 'a entity = Entity of (morphism -> 'a) * morphism; |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
185 |
fun entity f = Entity (f, identity); |
78072 | 186 |
|
78075
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
187 |
fun entity_morphism g (Entity (f, phi)) = Entity (f, g phi); |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
188 |
fun entity_reset_context a = entity_morphism reset_context a; |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
189 |
fun entity_set_context thy a = entity_morphism (set_context thy) a; |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
190 |
fun entity_set_context' ctxt a = entity_morphism (set_context' ctxt) a; |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
191 |
fun entity_set_context'' context a = entity_morphism (set_context'' context) a; |
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
192 |
|
78089 | 193 |
fun transform phi = entity_morphism (compose phi); |
194 |
fun transform_reset_context phi = entity_morphism (reset_context o compose phi); |
|
78078 | 195 |
|
78075
15ab73949713
more careful reset/set_context for stored declarations;
wenzelm
parents:
78072
diff
changeset
|
196 |
fun form (Entity (f, phi)) = f phi; |
78072 | 197 |
fun form_entity f = f identity; |
198 |
||
78112 | 199 |
fun form_context thy x = form (entity_set_context thy x) thy; |
200 |
fun form_context' ctxt x = form (entity_set_context' ctxt x) ctxt; |
|
201 |
fun form_context'' context x = form (entity_set_context'' context x) context; |
|
202 |
||
78085 | 203 |
type declaration = morphism -> Context.generic -> Context.generic; |
204 |
type declaration_entity = (Context.generic -> Context.generic) entity; |
|
22670
c803b2696ada
added Morphism.transform/form (generic non-sense);
wenzelm
parents:
22571
diff
changeset
|
205 |
|
67650 | 206 |
|
207 |
(* concrete morphisms *) |
|
208 |
||
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
209 |
fun binding_morphism a binding = morphism a {binding = [K binding], typ = [], term = [], fact = []}; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
210 |
fun typ_morphism' a typ = morphism a {binding = [], typ = [typ o the_theory], term = [], fact = []}; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
211 |
fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []}; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
212 |
fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []}; |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
213 |
fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []}; |
78081 | 214 |
fun fact_morphism' a fact = morphism a {binding = [], typ = [], term = [], fact = [fact o the_theory]}; |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
215 |
fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]}; |
78081 | 216 |
fun thm_morphism' a thm = morphism a {binding = [], typ = [], term = [], fact = [map o thm o the_theory]}; |
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
217 |
fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]}; |
67650 | 218 |
|
78063 | 219 |
fun transfer_morphism thy = fact_morphism "transfer" I |> set_context thy; |
67664 | 220 |
val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; |
221 |
val transfer_morphism'' = transfer_morphism o Context.theory_of; |
|
222 |
||
67650 | 223 |
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; |
224 |
||
78064
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
225 |
fun set_trim_context thy phi = set_context thy phi $> trim_context_morphism; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
226 |
val set_trim_context' = set_trim_context o Proof_Context.theory_of; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
227 |
val set_trim_context'' = set_trim_context o Context.theory_of; |
4e865c45458b
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents:
78063
diff
changeset
|
228 |
|
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
229 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
230 |
(* instantiate *) |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
231 |
|
74282 | 232 |
fun instantiate_frees_morphism (cinstT, cinst) = |
233 |
if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity |
|
234 |
else |
|
235 |
let |
|
236 |
val instT = TFrees.map (K Thm.typ_of) cinstT; |
|
237 |
val inst = Frees.map (K Thm.term_of) cinst; |
|
238 |
in |
|
239 |
morphism "instantiate_frees" |
|
240 |
{binding = [], |
|
241 |
typ = |
|
242 |
if TFrees.is_empty instT then [] |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
243 |
else [K (Term_Subst.instantiateT_frees instT)], |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
244 |
term = [K (Term_Subst.instantiate_frees (instT, inst))], |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
245 |
fact = [K (map (Thm.instantiate_frees (cinstT, cinst)))]} |
74282 | 246 |
end; |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67664
diff
changeset
|
247 |
|
74282 | 248 |
fun instantiate_morphism (cinstT, cinst) = |
249 |
if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity |
|
250 |
else |
|
251 |
let |
|
252 |
val instT = TVars.map (K Thm.typ_of) cinstT; |
|
253 |
val inst = Vars.map (K Thm.term_of) cinst; |
|
254 |
in |
|
255 |
morphism "instantiate" |
|
256 |
{binding = [], |
|
257 |
typ = |
|
258 |
if TVars.is_empty instT then [] |
|
78062
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
259 |
else [K (Term_Subst.instantiateT instT)], |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
260 |
term = [K (Term_Subst.instantiate (instT, inst))], |
edb195122938
support for context within morphism (for background theory);
wenzelm
parents:
78060
diff
changeset
|
261 |
fact = [K (map (Thm.instantiate (cinstT, cinst)))]} |
74282 | 262 |
end; |
67651
6dd41193a72a
more explicit instantiate_morphism (without checks for typ / term component);
wenzelm
parents:
67650
diff
changeset
|
263 |
|
21476 | 264 |
end; |
265 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
29605
diff
changeset
|
266 |
structure Basic_Morphism: BASIC_MORPHISM = Morphism; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
29605
diff
changeset
|
267 |
open Basic_Morphism; |