author  wenzelm 
Thu, 11 Oct 2007 16:05:35 +0200  
changeset 24964  526df61afe97 
parent 24929  408becab067e 
child 25486  b944ef973109 
permissions  rwrr 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/axclass.ML 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

4 

24964  5 
Type classes defined as predicates, associated with a record of 
6 
parameters. 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

7 
*) 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

8 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

9 
signature AX_CLASS = 
3938  10 
sig 
24589  11 
val define_class: bstring * class list > string list > 
12 
((bstring * attribute list) * term list) list > theory > class * theory 

13 
val add_classrel: thm > theory > theory 

14 
val add_arity: thm > theory > theory 

15 
val prove_classrel: class * class > tactic > theory > theory 

16 
val prove_arity: string * sort list * sort > tactic > theory > theory 

24964  17 
val get_info: theory > class > 
18 
{def: thm, intro: thm, axioms: thm list, params: (string * typ) list} 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

19 
val class_intros: theory > thm list 
20107  20 
val class_of_param: theory > string > class option 
19405  21 
val cert_classrel: theory > class * class > class * class 
22 
val read_classrel: theory > xstring * xstring > class * class 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

23 
val axiomatize_class: bstring * class list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

24 
val axiomatize_class_cmd: bstring * xstring list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

25 
val axiomatize_classrel: (class * class) list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

26 
val axiomatize_classrel_cmd: (xstring * xstring) list > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

27 
val axiomatize_arity: arity > theory > theory 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

28 
val axiomatize_arity_cmd: xstring * string list * string > theory > theory 
19574  29 
type cache 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

30 
val of_sort: theory > typ * sort > cache > thm list * cache (*exception Sorts.CLASS_ERROR*) 
19574  31 
val cache: cache 
3938  32 
end; 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

33 

15801  34 
structure AxClass: AX_CLASS = 
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

35 
struct 
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

36 

19405  37 
(** theory data **) 
423  38 

19405  39 
(* class parameters (canonical order) *) 
423  40 

19405  41 
type param = string * class; 
423  42 

19405  43 
fun add_param pp ((x, c): param) params = 
44 
(case AList.lookup (op =) params x of 

45 
NONE => (x, c) :: params 

46 
 SOME c' => error ("Duplicate class parameter " ^ quote x ^ 

47 
" for " ^ Pretty.string_of_sort pp [c] ^ 

48 
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c']))); 

423  49 

19405  50 
fun merge_params _ ([], qs) = qs 
51 
 merge_params pp (ps, qs) = 

52 
fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; 

423  53 

54 

19511  55 
(* axclasses *) 
6379  56 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

57 
val introN = "intro"; 
19511  58 
val superN = "super"; 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

59 
val axiomsN = "axioms"; 
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

60 

19392  61 
datatype axclass = AxClass of 
19460  62 
{def: thm, 
19392  63 
intro: thm, 
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
20628
diff
changeset

64 
axioms: thm list, 
21925  65 
params: (string * typ) list}; 
19392  66 

19460  67 
type axclasses = axclass Symtab.table * param list; 
19392  68 

21925  69 
fun make_axclass ((def, intro, axioms), params) = 
70 
AxClass {def = def, intro = intro, axioms = axioms, params = params}; 

19405  71 

72 
fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses = 

73 
(Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2)); 

74 

19392  75 

76 
(* instances *) 

77 

20628  78 
val classrel_prefix = "classrel_"; 
79 
val arity_prefix = "arity_"; 

19511  80 

19574  81 
type instances = 
82 
((class * class) * thm) list * 

83 
((class * sort list) * thm) list Symtab.table; 

6379  84 

19574  85 
fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) = 
86 
(merge (eq_fst op =) (classrel1, classrel2), 

87 
Symtab.join (K (merge (eq_fst op =))) (arities1, arities2)); 

19392  88 

89 

19511  90 
(* setup data *) 
19392  91 

92 
structure AxClassData = TheoryDataFun 

22846  93 
( 
19574  94 
type T = axclasses * instances; 
22846  95 
val empty = ((Symtab.empty, []), ([], Symtab.empty)); 
19574  96 
val copy = I; 
97 
val extend = I; 

98 
fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) = 

99 
(merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2))); 

22846  100 
); 
6379  101 

102 

19574  103 
(* maintain axclasses *) 
19392  104 

19574  105 
val get_axclasses = #1 o AxClassData.get; 
106 
fun map_axclasses f = AxClassData.map (apfst f); 

107 

108 
val lookup_def = Symtab.lookup o #1 o get_axclasses; 

6379  109 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

110 
fun get_info thy c = 
19511  111 
(case lookup_def thy c of 
19392  112 
SOME (AxClass info) => info 
21919  113 
 NONE => error ("No such axclass: " ^ quote c)); 
6379  114 

19123  115 
fun class_intros thy = 
19392  116 
let 
117 
fun add_intro c = 

19511  118 
(case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro  _ => I); 
21931
314f9e2a442c
replaced Sign.classes by Sign.all_classes (topologically sorted);
wenzelm
parents:
21925
diff
changeset

119 
val classes = Sign.all_classes thy; 
19392  120 
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

121 

a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

122 

19460  123 
fun get_params thy pred = 
19574  124 
let val params = #2 (get_axclasses thy); 
19460  125 
in fold (fn (x, c) => if pred c then cons x else I) params [] end; 
126 

127 
fun params_of thy c = get_params thy (fn c' => c' = c); 

128 
fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); 

129 

24964  130 
fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy)); 
19460  131 

21919  132 

19511  133 
(* maintain instances *) 
19503  134 

19574  135 
val get_instances = #2 o AxClassData.get; 
136 
fun map_instances f = AxClassData.map (apsnd f); 

19528  137 

138 

19574  139 
fun the_classrel thy (c1, c2) = 
140 
(case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of 

141 
SOME th => Thm.transfer thy th 

24920  142 
 NONE => error ("Unproven class relation " ^ 
143 
Syntax.string_of_classrel (ProofContext.init thy) [c1, c2])); 

19574  144 

145 
fun put_classrel arg = map_instances (fn (classrel, arities) => 

146 
(insert (eq_fst op =) arg classrel, arities)); 

19503  147 

148 

19574  149 
fun the_arity thy a (c, Ss) = 
24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

150 
(case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of 
19574  151 
SOME th => Thm.transfer thy th 
24920  152 
 NONE => error ("Unproven type arity " ^ 
153 
Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c]))); 

19503  154 

19574  155 
fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) => 
156 
(classrel, arities > Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)))); 

19503  157 

158 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

159 

19511  160 
(** instances **) 
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

161 

03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

162 
(* class relations *) 
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

163 

19405  164 
fun cert_classrel thy raw_rel = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

165 
let 
19405  166 
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; 
24271  167 
val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy); 
19405  168 
val _ = 
19460  169 
(case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of 
19405  170 
[] => () 
171 
 xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^ 

172 
commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], [])); 

173 
in (c1, c2) end; 

174 

175 
fun read_classrel thy raw_rel = 

176 
cert_classrel thy (pairself (Sign.read_class thy) raw_rel) 

177 
handle TYPE (msg, _, _) => error msg; 

178 

179 

180 
(* primitive rules *) 

181 

182 
fun add_classrel th thy = 

183 
let 

184 
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); 

22691  185 
val prop = Thm.plain_prop_of (Thm.transfer thy th); 
19405  186 
val rel = Logic.dest_classrel prop handle TERM _ => err (); 
187 
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); 

19574  188 
in 
189 
thy 

190 
> Sign.primitive_classrel (c1, c2) 

191 
> put_classrel ((c1, c2), Drule.unconstrainTs th) 

192 
end; 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

193 

19405  194 
fun add_arity th thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

195 
let 
19528  196 
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); 
22691  197 
val prop = Thm.plain_prop_of (Thm.transfer thy th); 
19528  198 
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); 
24731  199 
val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); 
19574  200 
in 
201 
thy 

202 
> Sign.primitive_arity (t, Ss, [c]) 

203 
> put_arity ((t, Ss, c), Drule.unconstrainTs th) 

204 
end; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

205 

dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

206 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

207 
(* tactical proofs *) 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

208 

19405  209 
fun prove_classrel raw_rel tac thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

210 
let 
24920  211 
val ctxt = ProofContext.init thy; 
19405  212 
val (c1, c2) = cert_classrel thy raw_rel; 
24920  213 
val th = Goal.prove ctxt [] [] 
20049  214 
(Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

215 
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ 
24920  216 
quote (Syntax.string_of_classrel ctxt [c1, c2])); 
19511  217 
in 
218 
thy 

20628  219 
> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])] 
19511  220 
> (fn [th'] => add_classrel th') 
221 
end; 

404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset

222 

19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

223 
fun prove_arity raw_arity tac thy = 
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

224 
let 
24920  225 
val ctxt = ProofContext.init thy; 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

226 
val arity = Sign.cert_arity thy raw_arity; 
20628  227 
val names = map (prefix arity_prefix) (Logic.name_arities arity); 
19405  228 
val props = Logic.mk_arities arity; 
24920  229 
val ths = Goal.prove_multi ctxt [] [] props 
21687  230 
(fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => 
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset

231 
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ 
24920  232 
quote (Syntax.string_of_arity ctxt arity)); 
19511  233 
in 
234 
thy 

20628  235 
> PureThy.add_thms (map (rpair []) (names ~~ ths)) 
19511  236 
> fold add_arity 
237 
end; 

238 

239 

240 

241 
(** class definitions **) 

242 

23421  243 
fun split_defined n eq = 
244 
let 

245 
val intro = 

246 
(eq RS Drule.equal_elim_rule2) 

247 
> Conjunction.curry_balanced n 

248 
> n = 0 ? Thm.eq_assumption 1; 

249 
val dests = 

250 
if n = 0 then [] 

251 
else 

252 
(eq RS Drule.equal_elim_rule1) 

253 
> BalancedTree.dest (fn th => 

254 
(th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; 

255 
in (intro, dests) end; 

256 

24964  257 
fun define_class (bclass, raw_super) raw_params raw_specs thy = 
19511  258 
let 
259 
val ctxt = ProofContext.init thy; 

24964  260 
val pp = Syntax.pp ctxt; 
19511  261 

262 

24964  263 
(* class *) 
19511  264 

265 
val bconst = Logic.const_of_class bclass; 

266 
val class = Sign.full_name thy bclass; 

24731  267 
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); 
19511  268 

24964  269 
fun check_constraint (a, S) = 
270 
if Sign.subsort thy (super, S) then () 

271 
else error ("Sort constraint of type variable " ^ 

272 
setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ 

273 
" needs to be weaker than " ^ Pretty.string_of_sort pp super); 

274 

275 

276 
(* params *) 

277 

278 
val params = raw_params > map (fn p => 

279 
let 

280 
val T = Sign.the_const_type thy p; 

281 
val _ = 

282 
(case Term.add_tvarsT T [] of 

283 
[((a, _), S)] => check_constraint (a, S) 

284 
 _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); 

285 
val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T; 

286 
in (p, T') end); 

287 

288 

289 
(* axioms *) 

290 

19511  291 
fun prep_axiom t = 
292 
(case Term.add_tfrees t [] of 

24964  293 
[(a, S)] => check_constraint (a, S) 
294 
 [] => () 

295 
 _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t); 

296 
t 

297 
> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT []  U => U)) 

298 
> Logic.close_form); 

19511  299 

24681  300 
val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; 
22745  301 
val name_atts = map fst raw_specs; 
19511  302 

303 

304 
(* definition *) 

305 

306 
val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; 

307 
val class_eq = 

23421  308 
Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs); 
19511  309 

310 
val ([def], def_thy) = 

311 
thy 

312 
> Sign.primitive_class (bclass, super) 

313 
> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])]; 

314 
val (raw_intro, (raw_classrel, raw_axioms)) = 

23421  315 
split_defined (length conjs) def > chop (length super); 
19392  316 

19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

317 

19511  318 
(* facts *) 
319 

320 
val class_triv = Thm.class_triv def_thy class; 

321 
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = 

322 
def_thy 

323 
> PureThy.note_thmss_qualified "" bconst 

324 
[((introN, []), [([Drule.standard raw_intro], [])]), 

325 
((superN, []), [(map Drule.standard raw_classrel, [])]), 

326 
((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; 

327 

24847  328 

19511  329 
(* result *) 
330 

24964  331 
val axclass = make_axclass ((def, intro, axioms), params); 
19511  332 
val result_thy = 
333 
facts_thy 

19574  334 
> fold put_classrel (map (pair class) super ~~ classrel) 
19511  335 
> Sign.add_path bconst 
336 
> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) > snd 

337 
> Sign.restore_naming facts_thy 

19574  338 
> map_axclasses (fn (axclasses, parameters) => 
21919  339 
(Symtab.update (class, axclass) axclasses, 
24964  340 
fold (fn (x, _) => add_param pp (x, class)) params parameters)); 
19511  341 

342 
in (class, result_thy) end; 

343 

344 

19531  345 

19511  346 
(** axiomatizations **) 
347 

348 
local 

349 

20628  350 
fun axiomatize prep mk name add raw_args thy = 
351 
let 

352 
val args = prep thy raw_args; 

353 
val specs = mk args; 

354 
val names = name args; 

355 
in thy > PureThy.add_axioms_i (map (rpair []) (names ~~ specs)) > fold add end; 

19511  356 

357 
fun ax_classrel prep = 

20628  358 
axiomatize (map o prep) (map Logic.mk_classrel) 
359 
(map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; 

19511  360 

361 
fun ax_arity prep = 

20628  362 
axiomatize prep Logic.mk_arities 
363 
(map (prefix arity_prefix) o Logic.name_arities) add_arity; 

19511  364 

19706  365 
fun class_const c = 
366 
(Logic.const_of_class c, Term.itselfT (Term.aT []) > propT); 

367 

19511  368 
fun ax_class prep_class prep_classrel (bclass, raw_super) thy = 
369 
let 

370 
val class = Sign.full_name thy bclass; 

24731  371 
val super = map (prep_class thy) raw_super > Sign.minimize_sort thy; 
19511  372 
in 
373 
thy 

374 
> Sign.primitive_class (bclass, super) 

375 
> ax_classrel prep_classrel (map (fn c => (class, c)) super) 

19706  376 
> Theory.add_deps "" (class_const class) (map class_const super) 
19511  377 
end; 
378 

379 
in 

380 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

381 
val axiomatize_class = ax_class Sign.certify_class cert_classrel; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

382 
val axiomatize_class_cmd = ax_class Sign.read_class read_classrel; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

383 
val axiomatize_classrel = ax_classrel cert_classrel; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

384 
val axiomatize_classrel_cmd = ax_classrel read_classrel; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

385 
val axiomatize_arity = ax_arity Sign.cert_arity; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

386 
val axiomatize_arity_cmd = ax_arity Sign.read_arity; 
19511  387 

388 
end; 

389 

390 

391 

392 
(** explicit derivations  cached **) 

393 

19574  394 
datatype cache = Types of (class * thm) list Typtab.table; 
395 

19511  396 
local 
19503  397 

19574  398 
fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache; 
399 
fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache); 

19503  400 

19522  401 
fun derive_type _ (_, []) = [] 
402 
 derive_type thy (typ, sort) = 

403 
let 

19528  404 
val vars = Term.fold_atyps 
19522  405 
(fn T as TFree (_, S) => insert (eq_fst op =) (T, S) 
406 
 T as TVar (_, S) => insert (eq_fst op =) (T, S) 

19528  407 
 _ => I) typ []; 
19574  408 
val hyps = vars 
409 
> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); 

19642  410 
val ths = (typ, sort) > Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy) 
22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22385
diff
changeset

411 
{class_relation = 
19574  412 
fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2), 
22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22385
diff
changeset

413 
type_constructor = 
19574  414 
fn a => fn dom => fn c => 
415 
let val Ss = map (map snd) dom and ths = maps (map fst) dom 

416 
in ths MRS the_arity thy a (c, Ss) end, 

22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22385
diff
changeset

417 
type_variable = 
19574  418 
the_default [] o AList.lookup (op =) hyps}; 
419 
in ths end; 

19503  420 

19511  421 
in 
422 

19574  423 
fun of_sort thy (typ, sort) cache = 
424 
let 

425 
val sort' = filter (is_none o lookup_type cache typ) sort; 

426 
val ths' = derive_type thy (typ, sort') 

427 
handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^ 

428 
Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort'); 

429 
val cache' = cache > fold (insert_type typ) (sort' ~~ ths'); 

430 
val ths = 

431 
sort > map (fn c => 

432 
Goal.finish (the (lookup_type cache' typ c) RS 

433 
Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c)))) 

20260  434 
> Thm.adjust_maxidx_thm ~1); 
19574  435 
in (ths, cache') end; 
19503  436 

19511  437 
end; 
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset

438 

24929
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

439 
val cache = Types Typtab.empty; 
408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
wenzelm
parents:
24920
diff
changeset

440 

15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset

441 
end; 