author | wenzelm |
Fri, 13 May 2011 23:58:40 +0200 | |
changeset 42795 | 66fcc9882784 |
parent 42388 | a44b0fdaa6c2 |
child 43329 | 84472e198515 |
permissions | -rw-r--r-- |
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
1 |
(* Title: HOL/Tools/enriched_type.ML |
40582 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
40968
a6fcd305f7dc
replace `type_mapper` by the more adequate `type_lifting`
haftmann
parents:
40857
diff
changeset
|
4 |
Functorial structure of types. |
40582 | 5 |
*) |
6 |
||
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
7 |
signature ENRICHED_TYPE = |
40582 | 8 |
sig |
41388 | 9 |
val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list |
10 |
val construct_mapper: Proof.context -> (string * bool -> term) |
|
40582 | 11 |
-> bool -> typ -> typ -> term |
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
12 |
val enriched_type: string option -> term -> local_theory -> Proof.state |
40582 | 13 |
type entry |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
14 |
val entries: Proof.context -> entry list Symtab.table |
40582 | 15 |
end; |
16 |
||
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
17 |
structure Enriched_Type : ENRICHED_TYPE = |
40582 | 18 |
struct |
19 |
||
41395 | 20 |
(* bookkeeping *) |
21 |
||
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
22 |
val compN = "comp"; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
23 |
val idN = "id"; |
40611 | 24 |
val compositionalityN = "compositionality"; |
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
25 |
val identityN = "identity"; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
26 |
|
41387 | 27 |
type entry = { mapper: term, variances: (sort * (bool * bool)) list, |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
28 |
comp: thm, id: thm }; |
40582 | 29 |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41395
diff
changeset
|
30 |
structure Data = Generic_Data |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41395
diff
changeset
|
31 |
( |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
32 |
type T = entry list Symtab.table |
40582 | 33 |
val empty = Symtab.empty |
34 |
val extend = I |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41395
diff
changeset
|
35 |
fun merge data = Symtab.merge (K true) data |
40582 | 36 |
); |
37 |
||
41388 | 38 |
val entries = Data.get o Context.Proof; |
40582 | 39 |
|
40 |
||
41 |
(* type analysis *) |
|
42 |
||
41389 | 43 |
fun term_with_typ ctxt T t = Envir.subst_term_types |
42361 | 44 |
(Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; |
41389 | 45 |
|
41388 | 46 |
fun find_atomic ctxt T = |
40582 | 47 |
let |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
48 |
val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt); |
40582 | 49 |
fun add_variance is_contra T = |
50 |
AList.map_default (op =) (T, (false, false)) |
|
51 |
((if is_contra then apsnd else apfst) (K true)); |
|
52 |
fun analyze' is_contra (_, (co, contra)) T = |
|
53 |
(if co then analyze is_contra T else I) |
|
54 |
#> (if contra then analyze (not is_contra) T else I) |
|
55 |
and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco |
|
56 |
of NONE => add_variance is_contra T |
|
57 |
| SOME variances => fold2 (analyze' is_contra) variances Ts) |
|
58 |
| analyze is_contra T = add_variance is_contra T; |
|
59 |
in analyze false T [] end; |
|
60 |
||
41388 | 61 |
fun construct_mapper ctxt atomic = |
40582 | 62 |
let |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
63 |
val lookup = hd o Symtab.lookup_list (entries ctxt); |
40582 | 64 |
fun constructs is_contra (_, (co, contra)) T T' = |
65 |
(if co then [construct is_contra T T'] else []) |
|
66 |
@ (if contra then [construct (not is_contra) T T'] else []) |
|
67 |
and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) = |
|
68 |
let |
|
41388 | 69 |
val { mapper = raw_mapper, variances, ... } = lookup tyco; |
40582 | 70 |
val args = maps (fn (arg_pattern, (T, T')) => |
71 |
constructs is_contra arg_pattern T T') |
|
72 |
(variances ~~ (Ts ~~ Ts')); |
|
73 |
val (U, U') = if is_contra then (T', T) else (T, T'); |
|
41388 | 74 |
val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper; |
75 |
in list_comb (mapper, args) end |
|
40582 | 76 |
| construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); |
77 |
in construct end; |
|
78 |
||
79 |
||
80 |
(* mapper properties *) |
|
81 |
||
41387 | 82 |
val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss; |
83 |
||
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
84 |
fun make_comp_prop ctxt variances (tyco, mapper) = |
40582 | 85 |
let |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
86 |
val sorts = map fst variances |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
87 |
val (((vs3, vs2), vs1), _) = ctxt |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
88 |
|> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
89 |
||>> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
90 |
||>> Variable.invent_types sorts |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
91 |
val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3); |
40582 | 92 |
fun mk_argT ((T, T'), (_, (co, contra))) = |
93 |
(if co then [(T --> T')] else []) |
|
94 |
@ (if contra then [(T' --> T)] else []); |
|
95 |
val contras = maps (fn (_, (co, contra)) => |
|
96 |
(if co then [false] else []) @ (if contra then [true] else [])) variances; |
|
97 |
val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); |
|
98 |
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
99 |
fun invents n k nctxt = |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
100 |
let |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
101 |
val names = Name.invents nctxt n k; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
102 |
in (names, fold Name.declare names nctxt) end; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
103 |
val ((names21, names32), nctxt) = Variable.names_of ctxt |
40582 | 104 |
|> invents "f" (length Ts21) |
105 |
||>> invents "f" (length Ts32); |
|
106 |
val T1 = Type (tyco, Ts1); |
|
107 |
val T2 = Type (tyco, Ts2); |
|
108 |
val T3 = Type (tyco, Ts3); |
|
109 |
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); |
|
110 |
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => |
|
111 |
if not is_contra then |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
112 |
HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) |
40582 | 113 |
else |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
114 |
HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) |
40582 | 115 |
) contras (args21 ~~ args32) |
41395 | 116 |
fun mk_mapper T T' args = list_comb |
117 |
(term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args); |
|
41387 | 118 |
val mapper21 = mk_mapper T2 T1 (map Free args21); |
119 |
val mapper32 = mk_mapper T3 T2 (map Free args32); |
|
120 |
val mapper31 = mk_mapper T3 T1 args31; |
|
41395 | 121 |
val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
122 |
(HOLogic.mk_comp (mapper21, mapper32), mapper31); |
|
41387 | 123 |
val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3) |
41395 | 124 |
val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
125 |
(mapper21 $ (mapper32 $ x), mapper31 $ x); |
|
41387 | 126 |
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1; |
127 |
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2; |
|
128 |
fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop |
|
129 |
(K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]] |
|
130 |
THEN' Simplifier.asm_lr_simp_tac compositionality_ss |
|
131 |
THEN_ALL_NEW (Goal.assume_rule_tac ctxt)))); |
|
132 |
in (comp_prop, prove_compositionality) end; |
|
133 |
||
134 |
val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss; |
|
40582 | 135 |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
136 |
fun make_id_prop ctxt variances (tyco, mapper) = |
40582 | 137 |
let |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
138 |
val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt; |
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
139 |
val Ts = map TFree vs; |
40582 | 140 |
fun bool_num b = if b then 1 else 0; |
141 |
fun mk_argT (T, (_, (co, contra))) = |
|
41387 | 142 |
replicate (bool_num co + bool_num contra) T |
143 |
val arg_Ts = maps mk_argT (Ts ~~ variances) |
|
40582 | 144 |
val T = Type (tyco, Ts); |
41387 | 145 |
val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper; |
146 |
val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); |
|
147 |
val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); |
|
148 |
val rhs = HOLogic.id_const T; |
|
41395 | 149 |
val (id_prop, identity_prop) = pairself |
150 |
(HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); |
|
41387 | 151 |
fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop |
152 |
(K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss))); |
|
153 |
in (id_prop, prove_identity) end; |
|
40582 | 154 |
|
155 |
||
40597 | 156 |
(* analyzing and registering mappers *) |
40582 | 157 |
|
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
158 |
fun consume eq x [] = (false, []) |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
159 |
| consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys); |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
160 |
|
40587 | 161 |
fun split_mapper_typ "fun" T = |
162 |
let |
|
163 |
val (Ts', T') = strip_type T; |
|
164 |
val (Ts'', T'') = split_last Ts'; |
|
165 |
val (Ts''', T''') = split_last Ts''; |
|
166 |
in (Ts''', T''', T'' --> T') end |
|
167 |
| split_mapper_typ tyco T = |
|
168 |
let |
|
169 |
val (Ts', T') = strip_type T; |
|
170 |
val (Ts'', T'') = split_last Ts'; |
|
171 |
in (Ts'', T'', T') end; |
|
172 |
||
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
173 |
fun analyze_variances ctxt tyco T = |
40587 | 174 |
let |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
175 |
fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T); |
40587 | 176 |
val (Ts, T1, T2) = split_mapper_typ tyco T |
177 |
handle List.Empty => bad_typ (); |
|
178 |
val _ = pairself |
|
179 |
((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) |
|
41387 | 180 |
handle TYPE _ => bad_typ (); |
40587 | 181 |
val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) |
182 |
handle TYPE _ => bad_typ (); |
|
183 |
val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) |
|
184 |
then bad_typ () else (); |
|
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
185 |
fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
186 |
let |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
187 |
val coT = TFree var1 --> TFree var2; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
188 |
val contraT = TFree var2 --> TFree var1; |
42361 | 189 |
val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2); |
40594
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
190 |
in |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
191 |
consume (op =) coT |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
192 |
##>> consume (op =) contraT |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
193 |
#>> pair sort |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
194 |
end; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
195 |
val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts; |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
196 |
val _ = if null left_variances then () else bad_typ (); |
fae1da97bb5e
infer variances of user-given mapper operation; proper thm storing
haftmann
parents:
40587
diff
changeset
|
197 |
in variances end; |
40587 | 198 |
|
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
199 |
fun gen_enriched_type prep_term some_prfx raw_mapper lthy = |
40583 | 200 |
let |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
201 |
val input_mapper = prep_term lthy raw_mapper; |
41389 | 202 |
val T = fastype_of input_mapper; |
40587 | 203 |
val _ = Type.no_tvars T; |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
204 |
val mapper = singleton (Variable.polymorphic lthy) input_mapper; |
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
205 |
val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then () |
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
206 |
else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T); |
40587 | 207 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
208 |
| add_tycos _ = I; |
|
209 |
val tycos = add_tycos T []; |
|
210 |
val tyco = if tycos = ["fun"] then "fun" |
|
211 |
else case remove (op =) "fun" tycos |
|
212 |
of [tyco] => tyco |
|
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
213 |
| _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T); |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
214 |
val prfx = the_default (Long_Name.base_name tyco) some_prfx; |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
215 |
val variances = analyze_variances lthy tyco T; |
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
216 |
val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper); |
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
217 |
val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper); |
40856
3ad8a5925ba4
optional explicit prefix for type mapper theorems
haftmann
parents:
40855
diff
changeset
|
218 |
val qualify = Binding.qualify true prfx o Binding.name; |
41389 | 219 |
fun mapper_declaration comp_thm id_thm phi context = |
220 |
let |
|
42388 | 221 |
val typ_instance = Sign.typ_instance (Context.theory_of context); |
41389 | 222 |
val mapper' = Morphism.term phi mapper; |
223 |
val T_T' = pairself fastype_of (mapper, mapper'); |
|
42388 | 224 |
in |
225 |
if typ_instance T_T' andalso typ_instance (swap T_T') |
|
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
226 |
then (Data.map o Symtab.cons_list) (tyco, |
41389 | 227 |
{ mapper = mapper', variances = variances, |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
228 |
comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context |
41389 | 229 |
else context |
230 |
end; |
|
41387 | 231 |
fun after_qed [single_comp_thm, single_id_thm] lthy = |
40587 | 232 |
lthy |
41387 | 233 |
|> Local_Theory.note ((qualify compN, []), single_comp_thm) |
234 |
||>> Local_Theory.note ((qualify idN, []), single_id_thm) |
|
235 |
|-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy => |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
236 |
lthy |
41388 | 237 |
|> Local_Theory.note ((qualify compositionalityN, []), |
238 |
[prove_compositionality lthy comp_thm]) |
|
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
239 |
|> snd |
41388 | 240 |
|> Local_Theory.note ((qualify identityN, []), |
241 |
[prove_identity lthy id_thm]) |
|
242 |
|> snd |
|
41389 | 243 |
|> Local_Theory.declaration false (mapper_declaration comp_thm id_thm)) |
40583 | 244 |
in |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
245 |
lthy |
41371
35d2241c169c
prove more algebraic version of functorial properties; retain old properties for convenience
haftmann
parents:
41298
diff
changeset
|
246 |
|> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) |
40583 | 247 |
end |
248 |
||
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
249 |
val enriched_type = gen_enriched_type Syntax.check_term; |
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
250 |
val enriched_type_cmd = gen_enriched_type Syntax.read_term; |
40583 | 251 |
|
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
252 |
val _ = Outer_Syntax.local_theory_to_proof "enriched_type" |
41390
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
253 |
"register operations managing the functorial structure of a type" |
207ee8f8a19c
full localization with possibly multiple entries;
haftmann
parents:
41389
diff
changeset
|
254 |
Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term |
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41472
diff
changeset
|
255 |
>> (fn (prfx, t) => enriched_type_cmd prfx t)); |
40583 | 256 |
|
40582 | 257 |
end; |