author  haftmann 
Fri, 07 Dec 2007 15:08:09 +0100  
changeset 25574  016f677ad7b8 
parent 25536  01753a944433 
child 25597  34860182b250 
permissions  rwrr 
24218  1 
(* Title: Pure/Isar/class.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

5 
Type classes derived from primitive axclasses and locales. 

6 
*) 

7 

8 
signature CLASS = 

9 
sig 

25462  10 
(*classes*) 
25002  11 
val class: bstring > class list > Element.context_i Locale.element list 
24218  12 
> string list > theory > string * Proof.context 
25002  13 
val class_cmd: bstring > xstring list > Element.context Locale.element list 
24589  14 
> xstring list > theory > string * Proof.context 
25485  15 

25311  16 
val init: class > theory > Proof.context 
25485  17 
val logical_const: string > Markup.property list 
25104  18 
> (string * mixfix) * term > theory > theory 
25485  19 
val syntactic_const: string > Syntax.mode > Markup.property list 
25104  20 
> (string * mixfix) * term > theory > theory 
25083  21 
val refresh_syntax: class > Proof.context > Proof.context 
25485  22 

24589  23 
val intro_classes_tac: thm list > tactic 
24 
val default_intro_classes_tac: thm list > tactic 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

25 
val prove_subclass: class * class > thm list > Proof.context 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

26 
> theory > theory 
25485  27 

28 
val class_prefix: string > string 

29 
val is_class: theory > class > bool 

30 
val these_params: theory > sort > (string * (string * typ)) list 

24589  31 
val print_classes: theory > unit 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

32 

25462  33 
(*instances*) 
25536  34 
val init_instantiation: string list * sort list * sort > theory > local_theory 
35 
val prep_spec: local_theory > term > term 

25485  36 
val instantiation_instance: (local_theory > local_theory) > local_theory > Proof.state 
37 
val prove_instantiation_instance: (Proof.context > tactic) > local_theory > local_theory 

38 
val conclude_instantiation: local_theory > local_theory 

39 

25518  40 
val overloaded_const: string * typ > theory > term * theory 
25485  41 
val overloaded_def: string > string * term > theory > thm * theory 
42 
val instantiation_param: Proof.context > string > string option 

43 
val confirm_declaration: string > local_theory > local_theory 

44 

45 
val unoverload: theory > thm > thm 

46 
val overload: theory > thm > thm 

47 
val unoverload_conv: theory > conv 

48 
val overload_conv: theory > conv 

25462  49 
val unoverload_const: theory > string * typ > string 
25485  50 
val param_of_inst: theory > string * string > string 
51 
val inst_of_param: theory > string > (string * string) option 

25462  52 

53 
(*old axclass layer*) 

54 
val axclass_cmd: bstring * xstring list 

55 
> ((bstring * Attrib.src list) * string list) list 

56 
> theory > class * theory 

57 
val classrel_cmd: xstring * xstring > theory > Proof.state 

58 

59 
(*old instance layer*) 

25536  60 
val instance_arity: (theory > theory) > arity > theory > Proof.state 
61 
val instance_arity_cmd: bstring * xstring list * xstring > theory > Proof.state 

24218  62 
end; 
63 

64 
structure Class : CLASS = 

65 
struct 

66 

67 
(** auxiliary **) 

68 

25062  69 
val classN = "class"; 
70 
val introN = "intro"; 

71 

25002  72 
fun prove_interpretation tac prfx_atts expr inst = 
73 
Locale.interpretation_i I prfx_atts expr inst 

24589  74 
#> Proof.global_terminal_proof 
75 
(Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) 

76 
#> ProofContext.theory_of; 

77 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

78 
fun prove_interpretation_in tac after_qed (name, expr) = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

79 
Locale.interpretation_in_locale 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

80 
(ProofContext.theory after_qed) (name, expr) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

81 
#> Proof.global_terminal_proof 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

82 
(Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

83 
#> ProofContext.theory_of; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

84 

25020  85 
fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2); 
24589  86 

87 
fun strip_all_ofclass thy sort = 

88 
let 

24847  89 
val typ = TVar ((Name.aT, 0), sort); 
24589  90 
fun prem_inclass t = 
91 
case Logic.strip_imp_prems t 

92 
of ofcls :: _ => try Logic.dest_inclass ofcls 

93 
 [] => NONE; 

94 
fun strip_ofclass class thm = 

95 
thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; 

96 
fun strip thm = case (prem_inclass o Thm.prop_of) thm 

97 
of SOME (_, class) => thm > strip_ofclass class > strip 

98 
 NONE => thm; 

99 
in strip end; 

100 

25038  101 
fun get_remove_global_constraint c thy = 
102 
let 

103 
val ty = Sign.the_const_constraint thy c; 

104 
in 

105 
thy 

106 
> Sign.add_const_constraint (c, NONE) 

107 
> pair (c, Logic.unvarifyT ty) 

108 
end; 

109 

24589  110 

25485  111 
(** primitive axclass and instance commands **) 
24589  112 

24218  113 
fun axclass_cmd (class, raw_superclasses) raw_specs thy = 
114 
let 

115 
val ctxt = ProofContext.init thy; 

116 
val superclasses = map (Sign.read_class thy) raw_superclasses; 

24589  117 
val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) 
118 
raw_specs; 

119 
val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) 

120 
raw_specs) 

24218  121 
> snd 
122 
> (map o map) fst; 

24589  123 
in 
124 
AxClass.define_class (class, superclasses) [] 

125 
(name_atts ~~ axiomss) thy 

126 
end; 

24218  127 

128 
local 

129 

130 
fun gen_instance mk_prop add_thm after_qed insts thy = 

131 
let 

132 
fun after_qed' results = 

133 
ProofContext.theory ((fold o fold) add_thm results #> after_qed); 

134 
in 

135 
thy 

136 
> ProofContext.init 

24589  137 
> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) 
25536  138 
o mk_prop thy) insts) 
24218  139 
end; 
140 

141 
in 

142 

24589  143 
val instance_arity = 
24218  144 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 
25502  145 
val instance_arity_cmd = 
146 
gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I; 

24589  147 
val classrel = 
25536  148 
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I; 
24589  149 
val classrel_cmd = 
25536  150 
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I; 
24218  151 

152 
end; (*local*) 

153 

154 

25462  155 
(** basic overloading **) 
156 

157 
(* bookkeeping *) 

24304  158 

159 
structure InstData = TheoryDataFun 

160 
( 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

161 
type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

162 
(*constant name ~> type constructor ~> (constant name, equation), 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

163 
constant name ~> (constant name, type constructor)*) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

164 
val empty = (Symtab.empty, Symtab.empty); 
24304  165 
val copy = I; 
166 
val extend = I; 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

167 
fun merge _ ((taba1, tabb1), (taba2, tabb2)) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

168 
(Symtab.join (K (Symtab.merge (K true))) (taba1, taba2), 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

169 
Symtab.merge (K true) (tabb1, tabb2)); 
24304  170 
); 
171 

25462  172 
val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs; 
173 

174 
fun inst thy (c, tyco) = 

175 
(the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco; 

176 

25485  177 
val param_of_inst = fst oo inst; 
25462  178 

25020  179 
fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) 
25462  180 
(InstData.get thy) []; 
181 

25485  182 
val inst_of_param = Symtab.lookup o snd o InstData.get; 
25462  183 

24589  184 
fun add_inst (c, tyco) inst = (InstData.map o apfst 
185 
o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

186 
#> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco))); 
24304  187 

25485  188 
fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy); 
189 
fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy)); 

190 

191 
fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy); 

192 
fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); 

24304  193 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

194 
fun unoverload_const thy (c_ty as (c, _)) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

195 
case AxClass.class_of_param thy c 
25462  196 
of SOME class => (case inst_tyco thy c_ty 
25485  197 
of SOME tyco => try (param_of_inst thy) (c, tyco) > the_default c 
25462  198 
 NONE => c) 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

199 
 NONE => c; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24304
diff
changeset

200 

25462  201 

202 
(* declaration and definition of instances of overloaded constants *) 

203 

204 
fun primitive_note kind (name, thm) = 

205 
PureThy.note_thmss_i kind [((name, []), [([thm], [])])] 

206 
#>> (fn [(_, [thm])] => thm); 

207 

25518  208 
fun overloaded_const (c, ty) thy = 
25462  209 
let 
210 
val SOME class = AxClass.class_of_param thy c; 

211 
val SOME tyco = inst_tyco thy (c, ty); 

25485  212 
val name_inst = AxClass.instance_name (tyco, class) ^ "_inst"; 
25502  213 
val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco; 
25462  214 
val ty' = Type.strip_sorts ty; 
215 
in 

216 
thy 

217 
> Sign.sticky_prefix name_inst 

218 
> Sign.no_base_names 

219 
> Sign.declare_const [] (c', ty', NoSyn) 

25518  220 
> (fn const' as Const (c'', _) => Thm.add_def false true 
25462  221 
(Thm.def_name c', Logic.mk_equals (Const (c, ty'), const')) 
222 
#>> Thm.varifyT 

223 
#> (fn thm => add_inst (c, tyco) (c'', thm) 

224 
#> primitive_note Thm.internalK (c', thm) 

225 
#> snd 

226 
#> Sign.restore_naming thy 

227 
#> pair (Const (c, ty)))) 

228 
end; 

229 

25485  230 
fun overloaded_def name (c, t) thy = 
25462  231 
let 
232 
val ty = Term.fastype_of t; 

233 
val SOME tyco = inst_tyco thy (c, ty); 

234 
val (c', eq) = inst thy (c, tyco); 

235 
val prop = Logic.mk_equals (Const (c', ty), t); 

25485  236 
val name' = Thm.def_name_optional 
237 
(NameSpace.base c ^ "_" ^ NameSpace.base tyco) name; 

25462  238 
in 
239 
thy 

25518  240 
> Thm.add_def false false (name', prop) 
25485  241 
>> (fn thm => Drule.transitive_thm OF [eq, thm]) 
25462  242 
end; 
243 

244 

24589  245 
(** class data **) 
24218  246 

247 
datatype class_data = ClassData of { 

248 
consts: (string * string) list 

24836  249 
(*locale parameter ~> constant name*), 
25062  250 
base_sort: sort, 
25083  251 
inst: term option list 
252 
(*canonical interpretation*), 

25062  253 
morphism: morphism, 
254 
(*partial morphism of canonical interpretation*) 

24657  255 
intro: thm, 
256 
defs: thm list, 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

257 
operations: (string * (class * (typ * term))) list 
24657  258 
}; 
24218  259 

24657  260 
fun rep_class_data (ClassData d) = d; 
25062  261 
fun mk_class_data ((consts, base_sort, inst, morphism, intro), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

262 
(defs, operations)) = 
25062  263 
ClassData { consts = consts, base_sort = base_sort, inst = inst, 
264 
morphism = morphism, intro = intro, defs = defs, 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

265 
operations = operations }; 
25062  266 
fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

267 
defs, operations }) = 
25062  268 
mk_class_data (f ((consts, base_sort, inst, morphism, intro), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

269 
(defs, operations))); 
25038  270 
fun merge_class_data _ (ClassData { consts = consts, 
25062  271 
base_sort = base_sort, inst = inst, morphism = morphism, intro = intro, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

272 
defs = defs1, operations = operations1 }, 
25062  273 
ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

274 
defs = defs2, operations = operations2 }) = 
25062  275 
mk_class_data ((consts, base_sort, inst, morphism, intro), 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

276 
(Thm.merge_thms (defs1, defs2), 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

277 
AList.merge (op =) (K true) (operations1, operations2))); 
24218  278 

279 
structure ClassData = TheoryDataFun 

280 
( 

25038  281 
type T = class_data Graph.T 
282 
val empty = Graph.empty; 

24218  283 
val copy = I; 
284 
val extend = I; 

25038  285 
fun merge _ = Graph.join merge_class_data; 
24218  286 
); 
287 

288 

289 
(* queries *) 

290 

25038  291 
val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get; 
24218  292 

24589  293 
fun the_class_data thy class = case lookup_class_data thy class 
25020  294 
of NONE => error ("Undeclared class " ^ quote class) 
24589  295 
 SOME data => data; 
24218  296 

25038  297 
val is_class = is_some oo lookup_class_data; 
298 

299 
val ancestry = Graph.all_succs o ClassData.get; 

24218  300 

25002  301 
fun these_params thy = 
24218  302 
let 
303 
fun params class = 

304 
let 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

305 
val const_typs = (#params o AxClass.get_info thy) class; 
24657  306 
val const_names = (#consts o the_class_data thy) class; 
24218  307 
in 
308 
(map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names 

309 
end; 

310 
in maps params o ancestry thy end; 

311 

24657  312 
fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy; 
24218  313 

25062  314 
fun morphism thy = #morphism o the_class_data thy; 
315 

24218  316 
fun these_intros thy = 
24657  317 
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data)) 
25038  318 
(ClassData.get thy) []; 
24218  319 

24836  320 
fun these_operations thy = 
321 
maps (#operations o the_class_data thy) o ancestry thy; 

24657  322 

24218  323 
fun print_classes thy = 
324 
let 

24920  325 
val ctxt = ProofContext.init thy; 
24218  326 
val algebra = Sign.classes_of thy; 
327 
val arities = 

328 
Symtab.empty 

329 
> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => 

330 
Symtab.map_default (class, []) (insert (op =) tyco)) arities) 

331 
((#arities o Sorts.rep_algebra) algebra); 

332 
val the_arities = these o Symtab.lookup arities; 

333 
fun mk_arity class tyco = 

334 
let 

335 
val Ss = Sorts.mg_domain algebra tyco [class]; 

24920  336 
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; 
24218  337 
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " 
24920  338 
^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); 
24218  339 
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ 
25062  340 
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), 
24218  341 
(SOME o Pretty.block) [Pretty.str "supersort: ", 
24920  342 
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], 
25062  343 
if is_class thy class then (SOME o Pretty.str) 
344 
("locale: " ^ Locale.extern thy class) else NONE, 

345 
((fn [] => NONE  ps => (SOME o Pretty.block o Pretty.fbreaks) 

346 
(Pretty.str "parameters:" :: ps)) o map mk_param 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

347 
o these o Option.map #params o try (AxClass.get_info thy)) class, 
24218  348 
(SOME o Pretty.block o Pretty.breaks) [ 
349 
Pretty.str "instances:", 

350 
Pretty.list "" "" (map (mk_arity class) (the_arities class)) 

351 
] 

352 
] 

353 
in 

24589  354 
(Pretty.writeln o Pretty.chunks o separate (Pretty.str "") 
355 
o map mk_entry o Sorts.all_classes) algebra 

24218  356 
end; 
357 

358 

359 
(* updaters *) 

360 

25163  361 
fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy = 
25002  362 
let 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

363 
val operations = map (fn (v_ty as (_, ty), (c, _)) => 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

364 
(c, (class, (ty, Free v_ty)))) cs; 
25002  365 
val cs = (map o pairself) fst cs; 
25038  366 
val add_class = Graph.new_node (class, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

367 
mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations))) 
25002  368 
#> fold (curry Graph.add_edge class) superclasses; 
369 
in 

25038  370 
ClassData.map add_class thy 
25002  371 
end; 
24218  372 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

373 
fun register_operation class (c, (t, some_def)) thy = 
25062  374 
let 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

375 
val base_sort = (#base_sort o the_class_data thy) class; 
25239  376 
val prep_typ = map_atyps 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

377 
(fn TVar (vi as (v, _), sort) => if Name.aT = v 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

378 
then TFree (v, base_sort) else TVar (vi, sort)); 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

379 
val t' = map_types prep_typ t; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

380 
val ty' = Term.fastype_of t'; 
25062  381 
in 
382 
thy 

383 
> (ClassData.map o Graph.map_node class o map_class_data o apsnd) 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

384 
(fn (defs, operations) => 
25096  385 
(fold cons (the_list some_def) defs, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

386 
(c, (class, (ty', t'))) :: operations)) 
25062  387 
end; 
24218  388 

24589  389 

390 
(** rule calculation, tactics and methods **) 

391 

25024  392 
val class_prefix = Logic.const_of_class o Sign.base_name; 
393 

25062  394 
fun calculate_morphism class cs = 
395 
let 

396 
val subst_typ = Term.map_type_tfree (fn var as (v, sort) => 

397 
if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)); 

398 
fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v 

399 
of SOME (c, _) => Const (c, ty) 

400 
 NONE => t) 

401 
 subst_aterm t = t; 

402 
val subst_term = map_aterms subst_aterm #> map_types subst_typ; 

403 
in 

25209  404 
Morphism.term_morphism subst_term 
25062  405 
$> Morphism.typ_morphism subst_typ 
406 
end; 

407 

25038  408 
fun class_intro thy class sups = 
24589  409 
let 
410 
fun class_elim class = 

25020  411 
case (#axioms o AxClass.get_info thy) class 
412 
of [thm] => SOME (Drule.unconstrainTs thm) 

24589  413 
 [] => NONE; 
25038  414 
val pred_intro = case Locale.intros thy class 
24589  415 
of ([ax_intro], [intro]) => intro > OF_LAST ax_intro > SOME 
416 
 ([intro], []) => SOME intro 

417 
 ([], [intro]) => SOME intro 

418 
 _ => NONE; 

419 
val pred_intro' = pred_intro 

420 
> Option.map (fn intro => intro OF map_filter class_elim sups); 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

421 
val class_intro = (#intro o AxClass.get_info thy) class; 
24589  422 
val raw_intro = case pred_intro' 
423 
of SOME pred_intro => class_intro > OF_LAST pred_intro 

424 
 NONE => class_intro; 

425 
val sort = Sign.super_classes thy class; 

24847  426 
val typ = TVar ((Name.aT, 0), sort); 
24589  427 
val defs = these_defs thy sups; 
428 
in 

429 
raw_intro 

430 
> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] 

431 
> strip_all_ofclass thy sort 

432 
> Thm.strip_shyps 

433 
> MetaSimplifier.rewrite_rule defs 

434 
> Drule.unconstrainTs 

435 
end; 

436 

437 
fun class_interpretation class facts defs thy = 

438 
let 

25038  439 
val params = these_params thy [class]; 
25083  440 
val inst = (#inst o the_class_data thy) class; 
25020  441 
val tac = ALLGOALS (ProofContext.fact_tac facts); 
25038  442 
val prfx = class_prefix class; 
24589  443 
in 
25038  444 
thy 
445 
> fold_map (get_remove_global_constraint o fst o snd) params 

25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
25083
diff
changeset

446 
> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) 
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
25083
diff
changeset

447 
(inst, map (fn def => (("", []), def)) defs) 
25038  448 
> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs) 
24589  449 
end; 
24218  450 

451 
fun intro_classes_tac facts st = 

452 
let 

453 
val thy = Thm.theory_of_thm st; 

454 
val classes = Sign.all_classes thy; 

455 
val class_trivs = map (Thm.class_triv thy) classes; 

456 
val class_intros = these_intros thy; 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

457 
val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; 
24218  458 
in 
25268  459 
Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st 
24218  460 
end; 
461 

462 
fun default_intro_classes_tac [] = intro_classes_tac [] 

24930
cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

463 
 default_intro_classes_tac _ = no_tac; 
24218  464 

465 
fun default_tac rules ctxt facts = 

466 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

467 
default_intro_classes_tac facts; 

468 

469 
val _ = Context.add_setup (Method.add_methods 

470 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

471 
"backchain introduction rules of classes"), 

472 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), 

473 
"apply some intro/elim rule")]); 

474 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

475 
fun subclass_rule thy (sub, sup) = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

476 
let 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

477 
val ctxt = Locale.init sub thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

478 
val ctxt_thy = ProofContext.init thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

479 
val props = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

480 
Locale.global_asms_of thy sup 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

481 
> maps snd 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

482 
> map (ObjectLogic.ensure_propT thy); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

483 
fun tac { prems, context } = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

484 
Locale.intro_locales_tac true context prems 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

485 
ORELSE ALLGOALS assume_tac; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

486 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

487 
Goal.prove_multi ctxt [] [] props tac 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

488 
> map (Assumption.export false ctxt ctxt_thy) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

489 
> Variable.export ctxt ctxt_thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

490 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

491 

62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

492 
fun prove_single_subclass (sub, sup) thms ctxt thy = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

493 
let 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

494 
val ctxt_thy = ProofContext.init thy; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

495 
val subclass_rule = Conjunction.intr_balanced thms 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

496 
> Assumption.export false ctxt ctxt_thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

497 
> singleton (Variable.export ctxt ctxt_thy); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

498 
val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

499 
val sub_ax = #axioms (AxClass.get_info thy sub); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

500 
val classrel = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

501 
#intro (AxClass.get_info thy sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

502 
> Drule.instantiate' [SOME sub_inst] [] 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

503 
> OF_LAST (subclass_rule OF sub_ax) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

504 
> strip_all_ofclass thy (Sign.super_classes thy sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

505 
> Thm.strip_shyps 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

506 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

507 
thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

508 
> AxClass.add_classrel classrel 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

509 
> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms)) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

510 
I (sub, Locale.Locale sup) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

511 
> ClassData.map (Graph.add_edge (sub, sup)) 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

512 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

513 

62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

514 
fun prove_subclass (sub, sup) thms ctxt thy = 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

515 
let 
25268  516 
val classes = ClassData.get thy; 
517 
val is_sup = not o null o curry (Graph.irreducible_paths classes) sub; 

518 
val supclasses = Graph.all_succs classes [sup] > filter_out is_sup; 

25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

519 
fun transform sup' = subclass_rule thy (sup, sup') > map (fn thm => thm OF thms); 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

520 
in 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

521 
thy 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

522 
> fold_rev (fn sup' => prove_single_subclass (sub, sup') 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

523 
(transform sup') ctxt) supclasses 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

524 
end; 
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

525 

24218  526 

24589  527 
(** classes and class target **) 
24218  528 

25002  529 
(* class context syntax *) 
24748  530 

25083  531 
structure ClassSyntax = ProofDataFun( 
532 
type T = { 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

533 
local_constraints: (string * typ) list, 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

534 
global_constraints: (string * typ) list, 
25083  535 
base_sort: sort, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

536 
operations: (string * (typ * term)) list, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

537 
unchecks: (term * term) list, 
25083  538 
passed: bool 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

539 
}; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

540 
fun init _ = { 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

541 
local_constraints = [], 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

542 
global_constraints = [], 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

543 
base_sort = [], 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

544 
operations = [], 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

545 
unchecks = [], 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

546 
passed = true 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

547 
};; 
25083  548 
); 
549 

25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

550 
fun synchronize_syntax sups base_sort ctxt = 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

551 
let 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

552 
val thy = ProofContext.theory_of ctxt; 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

553 
fun subst_class_typ sort = map_atyps 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

554 
(fn TFree _ => TVar ((Name.aT, 0), sort)  ty' => ty'); 
25083  555 
val operations = these_operations thy sups; 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

556 
val local_constraints = 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

557 
(map o apsnd) (subst_class_typ base_sort o fst o snd) operations; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

558 
val global_constraints = 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

559 
(map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; 
25318
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

560 
fun declare_const (c, _) = 
c8352b38d47d
synchronize_syntax: declare operations within the local scope of fixes/consts
wenzelm
parents:
25311
diff
changeset

561 
let val b = Sign.base_name c 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

562 
in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

563 
val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations; 
25083  564 
in 
565 
ctxt 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

566 
> fold declare_const local_constraints 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

567 
> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

568 
> ClassSyntax.put { 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

569 
local_constraints = local_constraints, 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

570 
global_constraints = global_constraints, 
25083  571 
base_sort = base_sort, 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

572 
operations = (map o apsnd) snd operations, 
25195
62638dcafe38
fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
haftmann
parents:
25163
diff
changeset

573 
unchecks = unchecks, 
25083  574 
passed = false 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

575 
} 
25083  576 
end; 
577 

578 
fun refresh_syntax class ctxt = 

25002  579 
let 
580 
val thy = ProofContext.theory_of ctxt; 

25062  581 
val base_sort = (#base_sort o the_class_data thy) class; 
25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

582 
in synchronize_syntax [class] base_sort ctxt end; 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

583 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

584 
val mark_passed = ClassSyntax.map 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

585 
(fn { local_constraints, global_constraints, base_sort, operations, unchecks, passed } => 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

586 
{ local_constraints = local_constraints, global_constraints = global_constraints, 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

587 
base_sort = base_sort, operations = operations, unchecks = unchecks, passed = true }); 
25083  588 

589 
fun sort_term_check ts ctxt = 

24748  590 
let 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

591 
val { local_constraints, global_constraints, base_sort, operations, passed, ... } = 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

592 
ClassSyntax.get ctxt; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

593 
fun check_improve (Const (c, ty)) = (case AList.lookup (op =) local_constraints c 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

594 
of SOME ty0 => (case try (Type.raw_match (ty0, ty)) Vartab.empty 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

595 
of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

596 
of SOME (_, TVar (tvar as (vi, _))) => 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

597 
if TypeInfer.is_param vi then cons tvar else I 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

598 
 _ => I) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

599 
 NONE => I) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

600 
 NONE => I) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

601 
 check_improve _ = I; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

602 
val improvements = (fold o fold_aterms) check_improve ts []; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

603 
val ts' = (map o map_types o map_atyps) (fn ty as TVar tvar => 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

604 
if member (op =) improvements tvar 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

605 
then TFree (Name.aT, base_sort) else ty  ty => ty) ts; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

606 
fun check t0 = Envir.expand_term (fn Const (c, ty) => (case AList.lookup (op =) operations c 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

607 
of SOME (ty0, t) => 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

608 
if Type.typ_instance (ProofContext.tsig_of ctxt) (ty, ty0) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

609 
then SOME (ty0, check t) else NONE 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

610 
 NONE => NONE) 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

611 
 _ => NONE) t0; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

612 
val ts'' = map check ts'; 
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

613 
in if eq_list (op aconv) (ts, ts'') andalso passed then NONE 
25083  614 
else 
615 
ctxt 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

616 
> fold (ProofContext.add_const_constraint o apsnd SOME) global_constraints 
25083  617 
> mark_passed 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

618 
> pair ts'' 
25083  619 
> SOME 
620 
end; 

24748  621 

25083  622 
fun sort_term_uncheck ts ctxt = 
25002  623 
let 
624 
val thy = ProofContext.theory_of ctxt; 

25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

625 
val unchecks = (#unchecks o ClassSyntax.get) ctxt; 
25462  626 
val ts' = map (Pattern.rewrite_term thy unchecks []) ts; 
25060  627 
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; 
25002  628 

25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

629 
fun init_ctxt sups base_sort ctxt = 
25083  630 
ctxt 
631 
> Variable.declare_term 

632 
(Logic.mk_type (TFree (Name.aT, base_sort))) 

25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

633 
> synchronize_syntax sups base_sort 
25083  634 
> Context.proof_map ( 
635 
Syntax.add_term_check 0 "class" sort_term_check 

25103  636 
#> Syntax.add_term_uncheck 0 "class" sort_term_uncheck) 
24901
d3cbf79769b9
added first version of userspace type system for class target
haftmann
parents:
24847
diff
changeset

637 

25311  638 
fun init class thy = 
639 
thy 

640 
> Locale.init class 

25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

641 
> init_ctxt [class] ((#base_sort o the_class_data thy) class); 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24901
diff
changeset

642 

24748  643 

24589  644 
(* class definition *) 
24218  645 

646 
local 

647 

24748  648 
fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems = 
24218  649 
let 
24748  650 
val supclasses = map (prep_class thy) raw_supclasses; 
25209  651 
val sups = filter (is_class thy) supclasses; 
652 
fun the_base_sort class = lookup_class_data thy class 

653 
> Option.map #base_sort 

654 
> the_default [class]; 

655 
val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses); 

24748  656 
val supsort = Sign.minimize_sort thy supclasses; 
25038  657 
val suplocales = map Locale.Locale sups; 
24748  658 
val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) 
659 
 Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); 

660 
val supexpr = Locale.Merge suplocales; 

661 
val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; 

25002  662 
val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups)) 
24748  663 
(map fst supparams); 
664 
val mergeexpr = Locale.Merge (suplocales @ includes); 

665 
val constrain = Element.Constrains ((map o apsnd o map_atyps) 

24847  666 
(fn TFree (_, sort) => TFree (Name.aT, sort)) supparams); 
24748  667 
in 
668 
ProofContext.init thy 

669 
> Locale.cert_expr supexpr [constrain] 

670 
> snd 

25344
00c2179db769
synchronize_syntax: improved declare_const (still inactive);
wenzelm
parents:
25326
diff
changeset

671 
> init_ctxt sups base_sort 
24748  672 
> process_expr Locale.empty raw_elems 
673 
> fst 

25062  674 
> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)), 
24748  675 
(*FIXME*) if null includes then constrain :: elems else elems))) 
676 
end; 

677 

678 
val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr; 

679 
val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr; 

680 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

681 
fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

682 
let 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

683 
val superclasses = map (Sign.certify_class thy) raw_superclasses; 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

684 
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; 
25083  685 
fun add_const ((c, ty), syn) = 
686 
Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const; 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

687 
fun mk_axioms cs thy = 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

688 
raw_dep_axioms thy cs 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

689 
> (map o apsnd o map) (Sign.cert_prop thy) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

690 
> rpair thy; 
25002  691 
fun constrain_typs class = (map o apsnd o Term.map_type_tfree) 
692 
(fn (v, _) => TFree (v, [class])) 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

693 
in 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

694 
thy 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

695 
> Sign.add_path (Logic.const_of_class name) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

696 
> fold_map add_const consts 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

697 
> Sign.restore_naming thy 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

698 
> (fn cs => mk_axioms cs 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

699 
#> (fn axioms_prop => AxClass.define_class (name, superclasses) 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

700 
(map fst cs @ other_consts) axioms_prop 
25002  701 
#> (fn class => `(fn _ => constrain_typs class cs) 
702 
#> (fn cs' => `(fn thy => AxClass.get_info thy class) 

703 
#> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs' 

704 
#> pair (class, (cs', axioms))))))) 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

705 
end; 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

706 

25002  707 
fun gen_class prep_spec prep_param bname 
24748  708 
raw_supclasses raw_includes_elems raw_other_consts thy = 
709 
let 

25038  710 
val class = Sign.full_name thy bname; 
25062  711 
val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) = 
24748  712 
prep_spec thy raw_supclasses raw_includes_elems; 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

713 
val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts; 
25163  714 
fun mk_inst class cs = 
715 
(map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs; 

25062  716 
fun fork_syntax (Element.Fixes xs) = 
717 
fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs 

718 
#>> Element.Fixes 

719 
 fork_syntax x = pair x; 

720 
val (elems, global_syn) = fold_map fork_syntax elems_syn []; 

25326  721 
fun globalize (c, ty) = 
25062  722 
((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty), 
723 
(the_default NoSyn o AList.lookup (op =) global_syn) c); 

25038  724 
fun extract_params thy = 
24218  725 
let 
25062  726 
val params = map fst (Locale.parameters_of thy class); 
24218  727 
in 
25062  728 
(params, (map globalize o snd o chop (length supconsts)) params) 
24218  729 
end; 
25038  730 
fun extract_assumes params thy cs = 
24218  731 
let 
732 
val consts = supconsts @ (map (fst o fst) params ~~ cs); 

733 
fun subst (Free (c, ty)) = 

734 
Const ((fst o the o AList.lookup (op =) consts) c, ty) 

735 
 subst t = t; 

736 
fun prep_asm ((name, atts), ts) = 

25024  737 
((Sign.base_name name, map (Attrib.attribute_i thy) atts), 
24589  738 
(map o map_aterms) subst ts); 
24218  739 
in 
25038  740 
Locale.global_asms_of thy class 
24218  741 
> map prep_asm 
742 
end; 

743 
in 

744 
thy 

24748  745 
> Locale.add_locale_i (SOME "") bname mergeexpr elems 
25038  746 
> snd 
25311  747 
> ProofContext.theory_of 
748 
> `extract_params 

749 
> (fn (all_params, params) => 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

750 
define_class_params (bname, supsort) params 
25038  751 
(extract_assumes params) other_consts 
752 
#> (fn (_, (consts, axioms)) => 

753 
`(fn thy => class_intro thy class sups) 

24218  754 
#> (fn class_intro => 
25062  755 
PureThy.note_thmss_qualified "" (NameSpace.append class classN) 
756 
[((introN, []), [([class_intro], [])])] 

757 
#> (fn [(_, [class_intro])] => 

25038  758 
add_class_data ((class, sups), 
25062  759 
(map fst params ~~ consts, base_sort, 
25163  760 
mk_inst class (map snd supconsts @ consts), 
25062  761 
calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro)) 
25038  762 
#> class_interpretation class axioms [] 
25311  763 
)))) 
25268  764 
> init class 
25038  765 
> pair class 
24218  766 
end; 
767 

25326  768 
fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy); 
769 

24218  770 
in 
771 

25326  772 
val class_cmd = gen_class read_class_spec read_const; 
24748  773 
val class = gen_class check_class_spec (K I); 
24218  774 

775 
end; (*local*) 

776 

777 

25485  778 
(* class target *) 
24218  779 

25485  780 
fun logical_const class pos ((c, mx), dict) thy = 
24218  781 
let 
25024  782 
val prfx = class_prefix class; 
783 
val thy' = thy > Sign.add_path prfx; 

25062  784 
val phi = morphism thy' class; 
25024  785 

25062  786 
val c' = Sign.full_name thy' c; 
25239  787 
val dict' = Morphism.term phi dict; 
788 
val dict_def = map_types Logic.unvarifyT dict'; 

789 
val ty' = Term.fastype_of dict_def; 

25083  790 
val ty'' = Type.strip_sorts ty'; 
25239  791 
val def_eq = Logic.mk_equals (Const (c', ty'), dict_def); 
24218  792 
in 
25024  793 
thy' 
25096  794 
> Sign.declare_const pos (c, ty'', mx) > snd 
25518  795 
> Thm.add_def false false (c, def_eq) 
25062  796 
>> Thm.symmetric 
25083  797 
> (fn def => class_interpretation class [def] [Thm.prop_of def] 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

798 
#> register_operation class (c', (dict', SOME (Thm.varifyT def)))) 
24218  799 
> Sign.restore_naming thy 
25083  800 
> Sign.add_const_constraint (c', SOME ty') 
24218  801 
end; 
802 

25485  803 
fun syntactic_const class prmode pos ((c, mx), rhs) thy = 
24836  804 
let 
25024  805 
val prfx = class_prefix class; 
25096  806 
val thy' = thy > Sign.add_path prfx; 
25062  807 
val phi = morphism thy class; 
808 

25096  809 
val c' = Sign.full_name thy' c; 
25146  810 
val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class]) 
811 
val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs; 

25239  812 
val ty' = Logic.unvarifyT (Term.fastype_of rhs'); 
24836  813 
in 
25096  814 
thy' 
25146  815 
> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') > snd 
25096  816 
> Sign.add_const_constraint (c', SOME ty') 
25024  817 
> Sign.notation true prmode [(Const (c', ty'), mx)] 
25368
f12613fda79d
proper implementation of check phase; nonqualified names for class operations
haftmann
parents:
25344
diff
changeset

818 
> register_operation class (c', (rhs', NONE)) 
25096  819 
> Sign.restore_naming thy 
24836  820 
end; 
821 

25462  822 

823 
(** instantiation target **) 

824 

825 
(* bookkeeping *) 

826 

827 
datatype instantiation = Instantiation of { 

25536  828 
arities: string list * sort list * sort, 
25462  829 
params: ((string * string) * (string * typ)) list 
25574  830 
(*(instantiation const, type constructor), (local instantiation parameter, typ)*) 
25462  831 
} 
832 

833 
structure Instantiation = ProofDataFun 

834 
( 

835 
type T = instantiation 

25536  836 
fun init _ = Instantiation { arities = ([], [], []), params = [] }; 
25462  837 
); 
838 

25485  839 
fun mk_instantiation (arities, params) = 
840 
Instantiation { arities = arities, params = params }; 

25514  841 
fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy) 
25485  842 
of Instantiation data => data; 
25514  843 
fun map_instantiation f = (LocalTheory.target o Instantiation.map) 
844 
(fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); 

25462  845 

25514  846 
fun the_instantiation lthy = case get_instantiation lthy 
25536  847 
of { arities = ([], [], []), ... } => error "No instantiation target" 
25485  848 
 data => data; 
25462  849 

25485  850 
val instantiation_params = #params o get_instantiation; 
25462  851 

25514  852 
fun instantiation_param lthy v = instantiation_params lthy 
25462  853 
> find_first (fn (_, (v', _)) => v = v') 
854 
> Option.map (fst o fst); 

855 

25514  856 
fun confirm_declaration c = (map_instantiation o apsnd) 
25485  857 
(filter_out (fn (_, (c', _)) => c' = c)); 
858 

25462  859 

860 
(* syntax *) 

861 

25536  862 
fun subst_param thy params = map_aterms (fn t as Const (c, ty) => (case inst_tyco thy (c, ty) 
863 
of SOME tyco => (case AList.lookup (op =) params (c, tyco) 

864 
of SOME v_ty => Free v_ty 

865 
 NONE => t) 

866 
 NONE => t) 

867 
 t => t); 

868 

869 
fun prep_spec lthy = 

870 
let 

871 
val thy = ProofContext.theory_of lthy; 

872 
val params = instantiation_params lthy; 

873 
in subst_param thy params end; 

874 

25514  875 
fun inst_term_check ts lthy = 
25462  876 
let 
25514  877 
val params = instantiation_params lthy; 
878 
val tsig = ProofContext.tsig_of lthy; 

879 
val thy = ProofContext.theory_of lthy; 

25462  880 

881 
fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty) 

882 
of SOME tyco => (case AList.lookup (op =) params (c, tyco) 

25502  883 
of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty'))) 
25462  884 
 NONE => I) 
885 
 NONE => I) 

886 
 check_improve _ = I; 

887 
val improvement = (fold o fold_aterms) check_improve ts Vartab.empty; 

888 
val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts; 

25536  889 
val ts'' = map (subst_param thy params) ts'; 
25514  890 
in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end; 
25462  891 

25514  892 
fun inst_term_uncheck ts lthy = 
25462  893 
let 
25514  894 
val params = instantiation_params lthy; 
25462  895 
val ts' = (map o map_aterms) (fn t as Free (v, ty) => 
896 
(case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params 

897 
of SOME c => Const (c, ty) 

898 
 NONE => t) 

899 
 t => t) ts; 

25514  900 
in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end; 
25462  901 

902 

903 
(* target *) 

904 

25485  905 
val sanatize_name = (*FIXME*) 
906 
let 

25574  907 
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s 
908 
orelse s = "'" orelse s = "_"; 

25485  909 
val is_junk = not o is_valid andf Symbol.is_regular; 
910 
val junk = Scan.many is_junk; 

911 
val scan_valids = Symbol.scanner "Malformed input" 

912 
((junk  

913 
(Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) 

914 
 junk)) 

915 
 Scan.repeat ((Scan.many1 is_valid >> implode)  junk) >> op ::); 

916 
in 

917 
explode #> scan_valids #> implode 

918 
end; 

919 

25536  920 
fun init_instantiation (tycos, sorts, sort) thy = 
25462  921 
let 
25536  922 
val _ = if null tycos then error "At least one arity must be given" else (); 
923 
val _ = map (the_class_data thy) sort; 

924 
val vs = map TFree (Name.names Name.context Name.aT sorts); 

25485  925 
fun type_name "*" = "prod" 
926 
 type_name "+" = "sum" 

927 
 type_name s = sanatize_name (NameSpace.base s); (*FIXME*) 

25536  928 
fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco) 
25502  929 
then NONE else SOME ((unoverload_const thy (c, ty), tyco), 
25536  930 
(param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty)); 
931 
val params = map_product get_param tycos (these_params thy sort) > map_filter I; 

25485  932 
in 
933 
thy 

934 
> ProofContext.init 

25536  935 
> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params)) 
936 
> fold (Variable.declare_term o Logic.mk_type) vs 

25574  937 
> fold (Variable.declare_names o Free o snd) params 
25536  938 
> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos 
25485  939 
> Context.proof_map ( 
940 
Syntax.add_term_check 0 "instance" inst_term_check 

941 
#> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck) 

942 
end; 

943 

944 
fun gen_instantiation_instance do_proof after_qed lthy = 

945 
let 

25536  946 
val (tycos, sorts, sort) = (#arities o the_instantiation) lthy; 
947 
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; 

25462  948 
fun after_qed' results = 
949 
LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results) 

950 
#> after_qed; 

951 
in 

952 
lthy 

953 
> do_proof after_qed' arities_proof 

954 
end; 

955 

25485  956 
val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => 
25462  957 
Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); 
958 

25485  959 
fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => 
25502  960 
fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t 
961 
(fn {context, ...} => tac context)) ts) lthy) I; 

25462  962 

963 
fun conclude_instantiation lthy = 

964 
let 

25485  965 
val { arities, params } = the_instantiation lthy; 
25536  966 
val (tycos, sorts, sort) = arities; 
25462  967 
val thy = ProofContext.theory_of lthy; 
968 
(*val _ = map (fn (tyco, sorts, sort) => 

969 
if Sign.of_sort thy 

970 
(Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort) 

971 
then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) 

972 
arities; FIXME activate when old instance command is gone*) 

973 
val params_of = maps (these o try (#params o AxClass.get_info thy)) 

974 
o Sign.complete_sort thy; 

25536  975 
val missing_params = tycos 
976 
> maps (fn tyco => params_of sort > map (rpair tyco)) 

25462  977 
> filter_out (can (inst thy) o apfst fst); 
25485  978 
fun declare_missing ((c, ty0), tyco) thy = 
979 
(*fun declare_missing ((c, tyco), (_, ty)) thy =*) 

25462  980 
let 
981 
val SOME class = AxClass.class_of_param thy c; 

25485  982 
val name_inst = AxClass.instance_name (tyco, class) ^ "_inst"; 
25502  983 
val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco; 
25462  984 
val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []); 
25485  985 
val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0; 
25462  986 
in 
987 
thy 

988 
> Sign.sticky_prefix name_inst 

989 
> Sign.no_base_names 

25485  990 
> Sign.declare_const [] (c', ty, NoSyn) 
25518  991 
> (fn const' as Const (c'', _) => Thm.add_def false true 
25485  992 
(Thm.def_name c', Logic.mk_equals (const', Const (c, ty))) 
25462  993 
#>> Thm.varifyT 
994 
#> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm) 

995 
#> primitive_note Thm.internalK (c', thm) 

996 
#> snd 

997 
#> Sign.restore_naming thy)) 

998 
end; 

999 
in 

1000 
lthy 

1001 
> LocalTheory.theory (fold declare_missing missing_params) 

1002 
end; 

1003 

24218  1004 
end; 