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


10 
val fork_mixfix: bool > string option > mixfix > mixfix * mixfix


11 


12 
val axclass_cmd: bstring * xstring list


13 
> ((bstring * Attrib.src list) * string list) list > theory > class * theory


14 
val class: bstring > class list > Element.context_i Locale.element list


15 
> string list > theory > string * Proof.context


16 
val class_cmd: bstring > string list > Element.context Locale.element list


17 
> string list > theory > string * Proof.context


18 
val instance_arity: arity list > ((bstring * Attrib.src list) * term) list


19 
> theory > Proof.state


20 
val instance_arity_cmd: (bstring * string list * string) list


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


22 
> theory > Proof.state


23 
val prove_instance_arity: tactic > arity list


24 
> ((bstring * Attrib.src list) * term) list


25 
> theory > theory


26 
val instance_class: class * class > theory > Proof.state


27 
val instance_class_cmd: string * string > theory > Proof.state


28 
val instance_sort: class * sort > theory > Proof.state


29 
val instance_sort_cmd: string * string > theory > Proof.state


30 
val prove_instance_sort: tactic > class * sort > theory > theory


31 


32 
val class_of_locale: theory > string > class option


33 
val add_const_in_class: string > (string * term) * Syntax.mixfix


34 
> theory > theory


35 


36 
val print_classes: theory > unit


37 
val intro_classes_tac: thm list > tactic


38 
val default_intro_classes_tac: thm list > tactic


39 
end;


40 


41 
structure Class : CLASS =


42 
struct


43 


44 
(** auxiliary **)


45 


46 
fun fork_mixfix is_loc some_class mx =


47 
let


48 
val mx' = Syntax.unlocalize_mixfix mx;


49 
val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')


50 
then NoSyn else mx';


51 
val mx_local = if is_loc then mx else NoSyn;


52 
in (mx_global, mx_local) end;


53 


54 
fun axclass_cmd (class, raw_superclasses) raw_specs thy =


55 
let


56 
val ctxt = ProofContext.init thy;


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


58 
val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;


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


60 
> snd


61 
> (map o map) fst;


62 
in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;


63 


64 


65 
(** axclasses with implicit parameter handling **)


66 


67 
(* axclass instances *)


68 


69 
local


70 


71 
fun gen_instance mk_prop add_thm after_qed insts thy =


72 
let


73 
fun after_qed' results =


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


75 
in


76 
thy


77 
> ProofContext.init


78 
> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)


79 
end;


80 


81 
in


82 


83 
val axclass_instance_arity =


84 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;


85 
val axclass_instance_sort =


86 
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))


87 
AxClass.add_classrel I o single;


88 


89 
end; (*local*)


90 


91 


92 
(* introducing axclasses with implicit parameter handling *)


93 


94 
fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =


95 
let


96 
val superclasses = map (Sign.certify_class thy) raw_superclasses;


97 
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;


98 
val prefix = Logic.const_of_class name;


99 
fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)


100 
(Sign.full_name thy c);


101 
fun add_const ((c, ty), syn) =


102 
Sign.add_consts_authentic [(c, ty, syn)]


103 
#> pair (mk_const_name c, ty);


104 
fun mk_axioms cs thy =


105 
raw_dep_axioms thy cs


106 
> (map o apsnd o map) (Sign.cert_prop thy)


107 
> rpair thy;


108 
fun add_constraint class (c, ty) =


109 
Sign.add_const_constraint_i (c, SOME


110 
(Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));


111 
in


112 
thy


113 
> Theory.add_path prefix


114 
> fold_map add_const consts


115 
> Theory.restore_naming thy


116 
> (fn cs => mk_axioms cs


117 
#> (fn axioms_prop => AxClass.define_class (name, superclasses)


118 
(map fst cs @ other_consts) axioms_prop


119 
#> (fn class => `(fn thy => AxClass.get_definition thy class)


120 
#> (fn {intro, axioms, ...} => fold (add_constraint class) cs


121 
#> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))


122 
end;


123 


124 


125 
(* instances with implicit parameter handling *)


126 


127 
local


128 


129 
fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =


130 
let


131 
val (_, t) = read_def thy (raw_name, raw_t);


132 
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;


133 
val atts = map (prep_att thy) raw_atts;


134 
val insts = Consts.typargs (Sign.consts_of thy) (c, ty);


135 
val name = case raw_name


136 
of "" => NONE


137 
 _ => SOME raw_name;


138 
in (c, (insts, ((name, t), atts))) end;


139 


140 
fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;


141 
fun read_def thy = gen_read_def thy (K I) (K I);


142 


143 
fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =


144 
let


145 
val arities = map (prep_arity theory) raw_arities;


146 
val _ = if null arities then error "at least one arity must be given" else ();


147 
val _ = case (duplicates (op =) o map #1) arities


148 
of [] => ()


149 
 dupl_tycos => error ("type constructors occur more than once in arities: "


150 
^ (commas o map quote) dupl_tycos);


151 
val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory


152 
fun get_consts_class tyco ty class =


153 
let


154 
val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;


155 
val subst_ty = map_type_tfree (K ty);


156 
in


157 
map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs


158 
end;


159 
fun get_consts_sort (tyco, asorts, sort) =


160 
let


161 
val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))


162 
in maps (get_consts_class tyco ty) (super_sort sort) end;


163 
val cs = maps get_consts_sort arities;


164 
fun mk_typnorm thy (ty, ty_sc) =


165 
case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty


166 
of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)


167 
 NONE => NONE;


168 
fun read_defs defs cs thy_read =


169 
let


170 
fun read raw_def cs =


171 
let


172 
val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;


173 
val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);


174 
val ((tyco, class), ty') = case AList.lookup (op =) cs c


175 
of NONE => error ("illegal definition for constant " ^ quote c)


176 
 SOME class_ty => class_ty;


177 
val name = case name_opt


178 
of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))


179 
 SOME name => name;


180 
val t' = case mk_typnorm thy_read (ty', ty)


181 
of NONE => error ("illegal definition for constant " ^


182 
quote (c ^ "::" ^ setmp show_sorts true


183 
(Sign.string_of_typ thy_read) ty))


184 
 SOME norm => map_types norm t


185 
in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;


186 
in fold_map read defs cs end;


187 
val (defs, _) = read_defs raw_defs cs


188 
(fold Sign.primitive_arity arities (Theory.copy theory));


189 
fun get_remove_contraint c thy =


190 
let


191 
val ty = Sign.the_const_constraint thy c;


192 
in


193 
thy


194 
> Sign.add_const_constraint_i (c, NONE)


195 
> pair (c, Logic.unvarifyT ty)


196 
end;


197 
fun add_defs defs thy =


198 
thy


199 
> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)


200 
> (fn thms => pair (map fst defs ~~ thms));


201 
fun after_qed cs defs thy =


202 
thy


203 
> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)


204 
> fold (Code.add_func false o snd) defs;


205 
in


206 
theory


207 
> fold_map get_remove_contraint (map fst cs > distinct (op =))


208 
>> add_defs defs


209 
> (fn (cs, defs) => do_proof (after_qed cs defs) arities)


210 
end;


211 


212 
fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;


213 
fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;


214 
fun tactic_proof tac after_qed arities =


215 
fold (fn arity => AxClass.prove_arity arity tac) arities


216 
#> after_qed;


217 


218 
in


219 


220 
val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;


221 
val instance_arity = instance_arity' axclass_instance_arity;


222 
val prove_instance_arity = instance_arity' o tactic_proof;


223 


224 
end; (*local*)


225 


226 


227 


228 
(** combining locales and axclasses **)


229 


230 
(* theory data *)


231 


232 
datatype class_data = ClassData of {


233 
locale: string,


234 
consts: (string * string) list


235 
(*locale parameter ~> toplevel theory constant*),


236 
v: string option,


237 
intro: thm


238 
} * thm list (*derived defs*);


239 


240 
fun rep_classdata (ClassData c) = c;


241 


242 
fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));


243 


244 
structure ClassData = TheoryDataFun


245 
(


246 
type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);


247 
val empty = (Graph.empty, Symtab.empty);


248 
val copy = I;


249 
val extend = I;


250 
fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));


251 
);


252 


253 


254 
(* queries *)


255 


256 
val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;


257 
fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);


258 


259 
fun the_class_data thy class =


260 
case lookup_class_data thy class


261 
of NONE => error ("undeclared class " ^ quote class)


262 
 SOME data => data;


263 


264 
val ancestry = Graph.all_succs o fst o ClassData.get;


265 


266 
fun param_map thy =


267 
let


268 
fun params class =


269 
let


270 
val const_typs = (#params o AxClass.get_definition thy) class;


271 
val const_names = (#consts o fst o the_class_data thy) class;


272 
in


273 
(map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names


274 
end;


275 
in maps params o ancestry thy end;


276 


277 
fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy;


278 


279 
fun these_intros thy =


280 
Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data))


281 
((fst o ClassData.get) thy) [];


282 


283 
fun print_classes thy =


284 
let


285 
val algebra = Sign.classes_of thy;


286 
val arities =


287 
Symtab.empty


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


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


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


291 
val the_arities = these o Symtab.lookup arities;


292 
fun mk_arity class tyco =


293 
let


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


295 
in Sign.pretty_arity thy (tyco, Ss, [class]) end;


296 
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "


297 
^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);


298 
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [


299 
(SOME o Pretty.str) ("class " ^ class ^ ":"),


300 
(SOME o Pretty.block) [Pretty.str "supersort: ",


301 
(Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],


302 
Option.map (Pretty.str o prefix "locale: " o #locale o fst) (lookup_class_data thy class),


303 
((fn [] => NONE  ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param


304 
o these o Option.map #params o try (AxClass.get_definition thy)) class,


305 
(SOME o Pretty.block o Pretty.breaks) [


306 
Pretty.str "instances:",


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


308 
]


309 
]


310 
in


311 
(Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)


312 
algebra


313 
end;


314 


315 


316 
(* updaters *)


317 


318 
fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =


319 
ClassData.map (fn (gr, tab) => (


320 
gr


321 
> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,


322 
v = v, intro = intro }, []))


323 
> fold (curry Graph.add_edge class) superclasses,


324 
tab


325 
> Symtab.update (locale, class)


326 
));


327 


328 
fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)


329 
(fn ClassData (data, thms) => ClassData (data, thm :: thms));


330 


331 
(* tactics and methods *)


332 


333 
fun intro_classes_tac facts st =


334 
let


335 
val thy = Thm.theory_of_thm st;


336 
val classes = Sign.all_classes thy;


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


338 
val class_intros = these_intros thy;


339 
fun add_axclass_intro class =


340 
case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro  _ => I;


341 
val axclass_intros = fold add_axclass_intro classes [];


342 
in


343 
st


344 
> ((ALLGOALS (Method.insert_tac facts THEN'


345 
REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))))


346 
THEN Tactic.distinct_subgoals_tac)


347 
end;


348 


349 
fun default_intro_classes_tac [] = intro_classes_tac []


350 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*)


351 


352 
fun default_tac rules ctxt facts =


353 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE


354 
default_intro_classes_tac facts;


355 


356 
val _ = Context.add_setup (Method.add_methods


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


358 
"backchain introduction rules of classes"),


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


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


361 


362 


363 
(* tactical interfaces to locale commands *)


364 


365 
fun prove_interpretation tac prfx_atts expr insts thy =


366 
thy


367 
> Locale.interpretation_i I prfx_atts expr insts


368 
> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)


369 
> ProofContext.theory_of;


370 


371 
fun prove_interpretation_in tac after_qed (name, expr) thy =


372 
thy


373 
> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)


374 
> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)


375 
> ProofContext.theory_of;


376 


377 


378 
(* constructing class introduction and other rules from axclass and locale rules *)


379 


380 
fun mk_instT class = Symtab.empty


381 
> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));


382 


383 
fun mk_inst class param_names cs =


384 
Symtab.empty


385 
> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const


386 
(c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;


387 


388 
fun OF_LAST thm1 thm2 =


389 
let


390 
val n = (length o Logic.strip_imp_prems o prop_of) thm2;


391 
in (thm1 RSN (n, thm2)) end;


392 


393 
fun strip_all_ofclass thy sort =


394 
let


395 
val typ = TVar ((AxClass.param_tyvarname, 0), sort);


396 
fun prem_inclass t =


397 
case Logic.strip_imp_prems t


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


399 
 [] => NONE;


400 
fun strip_ofclass class thm =


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


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


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


404 
 NONE => thm;


405 
in strip end;


406 


407 
fun class_intro thy locale class sups =


408 
let


409 
fun class_elim class =


410 
case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class


411 
of [thm] => SOME thm


412 
 [] => NONE;


413 
val pred_intro = case Locale.intros thy locale


414 
of ([ax_intro], [intro]) => intro > OF_LAST ax_intro > SOME


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


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


417 
 _ => NONE;


418 
val pred_intro' = pred_intro


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


420 
val class_intro = (#intro o AxClass.get_definition thy) class;


421 
val raw_intro = case pred_intro'


422 
of SOME pred_intro => class_intro > OF_LAST pred_intro


423 
 NONE => class_intro;


424 
val sort = Sign.super_classes thy class;


425 
val typ = TVar ((AxClass.param_tyvarname, 0), sort);


426 
val defs = these_defs thy sups;


427 
in


428 
raw_intro


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


430 
> strip_all_ofclass thy sort


431 
> Thm.strip_shyps


432 
> MetaSimplifier.rewrite_rule defs


433 
> Drule.unconstrainTs


434 
end;


435 


436 
fun interpretation_in_rule thy (class1, class2) =


437 
let


438 
val (params, consts) = split_list (param_map thy [class1]);


439 
(*FIXME also remember this at add_class*)


440 
fun mk_axioms class =


441 
let


442 
val name_locale = (#locale o fst o the_class_data thy) class;


443 
val inst = mk_inst class params consts;


444 
in


445 
Locale.global_asms_of thy name_locale


446 
> maps snd


447 
> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s  t => t)


448 
> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1])  T => T)


449 
> map (ObjectLogic.ensure_propT thy)


450 
end;


451 
val (prems, concls) = pairself mk_axioms (class1, class2);


452 
in


453 
Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)


454 
(Locale.intro_locales_tac true (ProofContext.init thy))


455 
end;


456 


457 


458 
(* classes *)


459 


460 
local


461 


462 
fun read_param thy raw_t =


463 
let


464 
val t = Sign.read_term thy raw_t


465 
in case try dest_Const t


466 
of SOME (c, _) => c


467 
 NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)


468 
end;


469 


470 
fun gen_class add_locale prep_class prep_param bname


471 
raw_supclasses raw_elems raw_other_consts thy =


472 
let


473 
(*FIXME need proper concept for reading locale statements*)


474 
fun subst_classtyvar (_, _) =


475 
TFree (AxClass.param_tyvarname, [])


476 
 subst_classtyvar (v, sort) =


477 
error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);


478 
(*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,


479 
typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)


480 
val other_consts = map (prep_param thy) raw_other_consts;


481 
val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)


482 
 Locale.Expr i => apsnd (cons i)) raw_elems ([], []);


483 
val supclasses = map (prep_class thy) raw_supclasses;


484 
val sups = filter (is_some o lookup_class_data thy) supclasses


485 
> Sign.certify_sort thy;


486 
val supsort = Sign.certify_sort thy supclasses;


487 
val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups;


488 
val supexpr = Locale.Merge (suplocales @ includes);


489 
val supparams = (map fst o Locale.parameters_of_expr thy)


490 
(Locale.Merge suplocales);


491 
val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups))


492 
(map fst supparams);


493 
(*val elems_constrains = map


494 
(Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)


495 
fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,


496 
if Sign.subsort thy (supsort, sort) then sort else error


497 
("Sort " ^ Sign.string_of_sort thy sort


498 
^ " is less general than permitted least general sort "


499 
^ Sign.string_of_sort thy supsort));


500 
fun extract_params thy name_locale =


501 
let


502 
val params = Locale.parameters_of thy name_locale;


503 
val v = case (maps typ_tfrees o map (snd o fst)) params


504 
of (v, _) :: _ => SOME v


505 
 _ => NONE;


506 
in


507 
(v, (map (fst o fst) params, params


508 
> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar


509 
> (map o apsnd) (fork_mixfix true NONE #> fst)


510 
> chop (length supconsts)


511 
> snd))


512 
end;


513 
fun extract_assumes name_locale params thy cs =


514 
let


515 
val consts = supconsts @ (map (fst o fst) params ~~ cs);


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


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


518 
 subst t = t;


519 
val super_defs = these_defs thy sups;


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


521 
((NameSpace.base name, map (Attrib.attribute thy) atts),


522 
(map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts);


523 
in


524 
Locale.global_asms_of thy name_locale


525 
> map prep_asm


526 
end;


527 
fun note_intro name_axclass class_intro =


528 
PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)


529 
[(("intro", []), [([class_intro], [])])]


530 
#> snd


531 
in


532 
thy


533 
> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)


534 
> (fn name_locale => ProofContext.theory_result (


535 
`(fn thy => extract_params thy name_locale)


536 
#> (fn (v, (param_names, params)) =>


537 
axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts


538 
#> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>


539 
`(fn thy => class_intro thy name_locale name_axclass sups)


540 
#> (fn class_intro =>


541 
add_class_data ((name_axclass, sups),


542 
(name_locale, map (fst o fst) params ~~ map fst consts, v,


543 
class_intro))


544 
(*FIXME: class_data should already contain data relevant


545 
for interpretation; use this later for class target*)


546 
(*FIXME: general export_fixes which may be parametrized


547 
with pieces of an emerging class*)


548 
#> note_intro name_axclass class_intro


549 
#> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)


550 
((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)


551 
((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), [])


552 
#> pair name_axclass


553 
)))))


554 
end;


555 


556 
in


557 


558 
val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;


559 
val class = gen_class Locale.add_locale_i Sign.certify_class (K I);


560 


561 
end; (*local*)


562 


563 
local


564 


565 
fun instance_subclass (class1, class2) thy =


566 
let


567 
val interp = interpretation_in_rule thy (class1, class2);


568 
val ax = #axioms (AxClass.get_definition thy class1);


569 
val intro = #intro (AxClass.get_definition thy class2)


570 
> Drule.instantiate' [SOME (Thm.ctyp_of thy


571 
(TVar ((AxClass.param_tyvarname, 0), [class1])))] [];


572 
val thm =


573 
intro


574 
> OF_LAST (interp OF ax)


575 
> strip_all_ofclass thy (Sign.super_classes thy class2);


576 
in


577 
thy > AxClass.add_classrel thm


578 
end;


579 


580 
fun instance_subsort (class, sort) thy =


581 
let


582 
val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra


583 
o Sign.classes_of) thy sort;


584 
val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))


585 
(rev super_sort);


586 
in


587 
thy > fold (curry instance_subclass class) classes


588 
end;


589 


590 
fun instance_sort' do_proof (class, sort) theory =


591 
let


592 
val loc_name = (#locale o fst o the_class_data theory) class;


593 
val loc_expr =


594 
(Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort;


595 
in


596 
theory


597 
> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)


598 
end;


599 


600 
fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =


601 
let


602 
val class = prep_class theory raw_class;


603 
val sort = prep_sort theory raw_sort;


604 
in


605 
theory


606 
> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)


607 
end;


608 


609 
fun gen_instance_class prep_class (raw_class, raw_superclass) theory =


610 
let


611 
val class = prep_class theory raw_class;


612 
val superclass = prep_class theory raw_superclass;


613 
in


614 
theory


615 
> axclass_instance_sort (class, superclass)


616 
end;


617 


618 
in


619 


620 
val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort;


621 
val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;


622 
val prove_instance_sort = instance_sort' o prove_interpretation_in;


623 
val instance_class_cmd = gen_instance_class Sign.read_class;


624 
val instance_class = gen_instance_class Sign.certify_class;


625 


626 
end; (*local*)


627 


628 


629 
(** class target **)


630 


631 
fun export_fixes thy class =


632 
let


633 
val v = (#v o fst o the_class_data thy) class;


634 
val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];


635 
val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>


636 
if SOME w = v then TFree (w, constrain_sort sort) else TFree var);


637 
val consts = param_map thy [class];


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


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


640 
 NONE => t)


641 
 subst_aterm t = t;


642 
in map_types subst_typ #> Term.map_aterms subst_aterm end;


643 


644 
fun add_const_in_class class ((c, rhs), syn) thy =


645 
let


646 
val prfx = (Logic.const_of_class o NameSpace.base) class;


647 
fun mk_name inject c =


648 
let


649 
val n1 = Sign.full_name thy c;


650 
val n2 = NameSpace.qualifier n1;


651 
val n3 = NameSpace.base n1;


652 
in NameSpace.implode (n2 :: inject @ [n3]) end;


653 
val abbr' = mk_name [prfx, prfx] c;


654 
val rhs' = export_fixes thy class rhs;


655 
val ty' = Term.fastype_of rhs';


656 
val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));


657 
val (syn', _) = fork_mixfix true NONE syn;


658 
fun interpret def =


659 
let


660 
val def' = symmetric def


661 
val tac = (ALLGOALS o ProofContext.fact_tac) [def'];


662 
val name_locale = (#locale o fst o the_class_data thy) class;


663 
val def_eq = Thm.prop_of def';


664 
val (params, consts) = split_list (param_map thy [class]);


665 
in


666 
prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)


667 
((mk_instT class, mk_inst class params consts), [def_eq])


668 
#> add_class_const_thm (class, def')


669 
end;


670 
in


671 
thy


672 
> Sign.hide_consts_i true [abbr']


673 
> Sign.add_path prfx


674 
> Sign.add_consts_authentic [(c, ty', syn')]


675 
> Sign.parent_path


676 
> Sign.sticky_prefix prfx


677 
> PureThy.add_defs_i false [(def, [])]


678 
> (fn [def] => interpret def)


679 
> Sign.restore_naming thy


680 
end;


681 


682 
end;
