320 val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses |
320 val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses |
321 @ exprs); |
321 @ exprs); |
322 val mapp_sup = AList.make |
322 val mapp_sup = AList.make |
323 (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) |
323 (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) |
324 ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses); |
324 ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses); |
325 fun unlocalize syn = |
|
326 let |
|
327 val syn' = Syntax.unlocalize_mixfix true syn; |
|
328 in if syn = syn' then NoSyn else syn' end; |
|
329 fun extract_tyvar_consts thy name_locale = |
325 fun extract_tyvar_consts thy name_locale = |
330 let |
326 let |
331 fun extract_classvar ((c, ty), _) w = |
327 fun extract_classvar ((c, ty), _) w = |
332 (case Term.add_tfreesT ty [] |
328 (case Term.add_tfreesT ty [] |
333 of [(v, _)] => (case w |
329 of [(v, _)] => (case w |
335 | NONE => SOME v) |
331 | NONE => SOME v) |
336 | [] => error ("No type variable in type signature of constant " ^ quote c) |
332 | [] => error ("No type variable in type signature of constant " ^ quote c) |
337 | _ => error ("More than one type variable in type signature of constant " ^ quote c)); |
333 | _ => error ("More than one type variable in type signature of constant " ^ quote c)); |
338 val consts1 = |
334 val consts1 = |
339 Locale.parameters_of thy name_locale |
335 Locale.parameters_of thy name_locale |
340 |> map (apsnd unlocalize) |
336 |> map (apsnd (Syntax.unlocalize_mixfix true)) |
341 val SOME v = fold extract_classvar consts1 NONE; |
337 val SOME v = fold extract_classvar consts1 NONE; |
342 val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1; |
338 val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1; |
343 in (v, chop (length mapp_sup) consts2) end; |
339 in (v, chop (length mapp_sup) consts2) end; |
344 fun add_consts v raw_cs_sup raw_cs_this thy = |
340 fun add_consts v raw_cs_sup raw_cs_this thy = |
345 let |
341 let |
379 add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms |
375 add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms |
380 #-> (fn (name_axclass, (_, ax_axioms)) => |
376 #-> (fn (name_axclass, (_, ax_axioms)) => |
381 fold (add_global_constraint v name_axclass) mapp_this |
377 fold (add_global_constraint v name_axclass) mapp_this |
382 #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this, |
378 #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this, |
383 map (fst o fst) loc_axioms)) |
379 map (fst o fst) loc_axioms)) |
384 #> prove_interpretation_i (bname, []) |
380 #> prove_interpretation_i (Logic.const_of_class bname, []) |
385 (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) |
381 (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) |
386 ((ALLGOALS o ProofContext.fact_tac) ax_axioms) |
382 ((ALLGOALS o ProofContext.fact_tac) ax_axioms) |
387 ))))) #> pair name_locale) |
383 ))))) #> pair name_locale) |
388 end; |
384 end; |
389 |
385 |
543 o maps (#consts o fst o the_class_data theory) |
539 o maps (#consts o fst o the_class_data theory) |
544 o the_ancestry theory) [class]; |
540 o the_ancestry theory) [class]; |
545 fun get_thms thy = |
541 fun get_thms thy = |
546 the_ancestry thy sort |
542 the_ancestry thy sort |
547 |> AList.make (the_propnames thy) |
543 |> AList.make (the_propnames thy) |
548 |> map (apsnd (map (NameSpace.append (loc_name)))) |
544 |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name)))) |
549 |> map_filter (fn (superclass, thm_names) => |
545 |> map_filter (fn (superclass, thm_names) => |
550 case map_filter (try (PureThy.get_thm thy o Name)) thm_names |
546 case map_filter (try (PureThy.get_thm thy o Name)) thm_names |
551 of [] => NONE |
547 of [] => NONE |
552 | thms => SOME (superclass, thms)); |
548 | thms => SOME (superclass, thms)); |
553 fun after_qed thy = |
549 fun after_qed thy = |