src/Pure/Isar/class.ML
author haftmann
Wed Nov 28 09:01:42 2007 +0100 (2007-11-28)
changeset 25485 33840a854e63
parent 25462 dad0291cb76a
child 25502 9200b36280c0
permissions -rw-r--r--
tuned interfaces of class module
     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   (*classes*)
    11   val class: bstring -> class list -> Element.context_i Locale.element list
    12     -> string list -> theory -> string * Proof.context
    13   val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    14     -> xstring list -> theory -> string * Proof.context
    15 
    16   val init: class -> theory -> Proof.context
    17   val logical_const: string -> Markup.property list
    18     -> (string * mixfix) * term -> theory -> theory
    19   val syntactic_const: string -> Syntax.mode -> Markup.property list
    20     -> (string * mixfix) * term -> theory -> theory
    21   val refresh_syntax: class -> Proof.context -> Proof.context
    22 
    23   val intro_classes_tac: thm list -> tactic
    24   val default_intro_classes_tac: thm list -> tactic
    25   val prove_subclass: class * class -> thm list -> Proof.context
    26     -> theory -> theory
    27 
    28   val class_prefix: string -> string
    29   val is_class: theory -> class -> bool
    30   val these_params: theory -> sort -> (string * (string * typ)) list
    31   val print_classes: theory -> unit
    32 
    33   (*instances*)
    34   val init_instantiation: arity list -> theory -> local_theory
    35   val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    36   val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    37   val conclude_instantiation: local_theory -> local_theory
    38 
    39   val overloaded_const: string * typ * mixfix -> theory -> term * theory
    40   val overloaded_def: string -> string * term -> theory -> thm * theory
    41   val instantiation_param: Proof.context -> string -> string option
    42   val confirm_declaration: string -> local_theory -> local_theory
    43 
    44   val unoverload: theory -> thm -> thm
    45   val overload: theory -> thm -> thm
    46   val unoverload_conv: theory -> conv
    47   val overload_conv: theory -> conv
    48   val unoverload_const: theory -> string * typ -> string
    49   val param_of_inst: theory -> string * string -> string
    50   val inst_of_param: theory -> string -> (string * string) option
    51 
    52   (*old axclass layer*)
    53   val axclass_cmd: bstring * xstring list
    54     -> ((bstring * Attrib.src list) * string list) list
    55     -> theory -> class * theory
    56   val classrel_cmd: xstring * xstring -> theory -> Proof.state
    57 
    58   (*old instance layer*)
    59   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    60   val instance: arity list -> ((bstring * Attrib.src list) * term) list
    61     -> (thm list -> theory -> theory)
    62     -> theory -> Proof.state
    63   val instance_cmd: (bstring * xstring list * xstring) list
    64     -> ((bstring * Attrib.src list) * xstring) list
    65     -> (thm list -> theory -> theory)
    66     -> theory -> Proof.state
    67   val prove_instance: tactic -> arity list
    68     -> ((bstring * Attrib.src list) * term) list
    69     -> theory -> thm list * theory
    70 end;
    71 
    72 structure Class : CLASS =
    73 struct
    74 
    75 (** auxiliary **)
    76 
    77 val classN = "class";
    78 val introN = "intro";
    79 
    80 fun prove_interpretation tac prfx_atts expr inst =
    81   Locale.interpretation_i I prfx_atts expr inst
    82   #> Proof.global_terminal_proof
    83       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    84   #> ProofContext.theory_of;
    85 
    86 fun prove_interpretation_in tac after_qed (name, expr) =
    87   Locale.interpretation_in_locale
    88       (ProofContext.theory after_qed) (name, expr)
    89   #> Proof.global_terminal_proof
    90       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    91   #> ProofContext.theory_of;
    92 
    93 fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2);
    94 
    95 fun strip_all_ofclass thy sort =
    96   let
    97     val typ = TVar ((Name.aT, 0), sort);
    98     fun prem_inclass t =
    99       case Logic.strip_imp_prems t
   100        of ofcls :: _ => try Logic.dest_inclass ofcls
   101         | [] => NONE;
   102     fun strip_ofclass class thm =
   103       thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
   104     fun strip thm = case (prem_inclass o Thm.prop_of) thm
   105      of SOME (_, class) => thm |> strip_ofclass class |> strip
   106       | NONE => thm;
   107   in strip end;
   108 
   109 fun get_remove_global_constraint c thy =
   110   let
   111     val ty = Sign.the_const_constraint thy c;
   112   in
   113     thy
   114     |> Sign.add_const_constraint (c, NONE)
   115     |> pair (c, Logic.unvarifyT ty)
   116   end;
   117 
   118 
   119 (** primitive axclass and instance commands **)
   120 
   121 fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   122   let
   123     val ctxt = ProofContext.init thy;
   124     val superclasses = map (Sign.read_class thy) raw_superclasses;
   125     val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   126       raw_specs;
   127     val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   128           raw_specs)
   129       |> snd
   130       |> (map o map) fst;
   131   in
   132     AxClass.define_class (class, superclasses) []
   133       (name_atts ~~ axiomss) thy
   134   end;
   135 
   136 local
   137 
   138 fun gen_instance mk_prop add_thm after_qed insts thy =
   139   let
   140     fun after_qed' results =
   141       ProofContext.theory ((fold o fold) add_thm results #> after_qed);
   142   in
   143     thy
   144     |> ProofContext.init
   145     |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
   146         o maps (mk_prop thy)) insts)
   147   end;
   148 
   149 in
   150 
   151 val instance_arity =
   152   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   153 val classrel =
   154   gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
   155     AxClass.add_classrel I o single;
   156 val classrel_cmd =
   157   gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
   158     AxClass.add_classrel I o single;
   159 
   160 end; (*local*)
   161 
   162 
   163 (** basic overloading **)
   164 
   165 (* bookkeeping *)
   166 
   167 structure InstData = TheoryDataFun
   168 (
   169   type T = (string * thm) Symtab.table Symtab.table * (string * string) Symtab.table;
   170     (*constant name ~> type constructor ~> (constant name, equation),
   171         constant name ~> (constant name, type constructor)*)
   172   val empty = (Symtab.empty, Symtab.empty);
   173   val copy = I;
   174   val extend = I;
   175   fun merge _ ((taba1, tabb1), (taba2, tabb2)) =
   176     (Symtab.join (K (Symtab.merge (K true))) (taba1, taba2),
   177       Symtab.merge (K true) (tabb1, tabb2));
   178 );
   179 
   180 val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
   181 
   182 fun inst thy (c, tyco) =
   183   (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
   184 
   185 val param_of_inst = fst oo inst;
   186 
   187 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   188   (InstData.get thy) [];
   189 
   190 val inst_of_param = Symtab.lookup o snd o InstData.get;
   191 
   192 fun add_inst (c, tyco) inst = (InstData.map o apfst
   193       o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   194   #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   195 
   196 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
   197 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
   198 
   199 fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   200 fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   201 
   202 fun unoverload_const thy (c_ty as (c, _)) =
   203   case AxClass.class_of_param thy c
   204    of SOME class => (case inst_tyco thy c_ty
   205        of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   206         | NONE => c)
   207     | NONE => c;
   208 
   209 
   210 (* declaration and definition of instances of overloaded constants *)
   211 
   212 fun primitive_note kind (name, thm) =
   213   PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   214   #>> (fn [(_, [thm])] => thm);
   215 
   216 fun overloaded_const (c, ty, mx) thy =
   217   let
   218     val _ = if mx <> NoSyn then
   219       error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
   220       else ()
   221     val SOME class = AxClass.class_of_param thy c;
   222     val SOME tyco = inst_tyco thy (c, ty);
   223     val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   224     val c' = NameSpace.base c;
   225     val ty' = Type.strip_sorts ty;
   226   in
   227     thy
   228     |> Sign.sticky_prefix name_inst
   229     |> Sign.no_base_names
   230     |> Sign.declare_const [] (c', ty', NoSyn)
   231     |-> (fn const' as Const (c'', _) => Thm.add_def true
   232           (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
   233     #>> Thm.varifyT
   234     #-> (fn thm => add_inst (c, tyco) (c'', thm)
   235     #> primitive_note Thm.internalK (c', thm)
   236     #> snd
   237     #> Sign.restore_naming thy
   238     #> pair (Const (c, ty))))
   239   end;
   240 
   241 fun overloaded_def name (c, t) thy =
   242   let
   243     val ty = Term.fastype_of t;
   244     val SOME tyco = inst_tyco thy (c, ty);
   245     val (c', eq) = inst thy (c, tyco);
   246     val prop = Logic.mk_equals (Const (c', ty), t);
   247     val name' = Thm.def_name_optional
   248       (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   249   in
   250     thy
   251     |> Thm.add_def false (name', prop)
   252     |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   253   end;
   254 
   255 
   256 (* legacy *)
   257 
   258 fun add_inst_def (class, tyco) (c, ty) thy =
   259   let
   260     val tyco_base = Sign.base_name tyco;
   261     val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst";
   262     val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base;
   263   in
   264     thy
   265     |> Sign.sticky_prefix name_inst
   266     |> Sign.declare_const [] (c_inst_base, ty, NoSyn)
   267     |-> (fn const as Const (c_inst, _) =>
   268       PureThy.add_defs_i false
   269         [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])]
   270       #-> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm)))
   271     |> Sign.restore_naming thy
   272   end;
   273 
   274 fun add_inst_def' (class, tyco) (c, ty) thy =
   275   if case Symtab.lookup (fst (InstData.get thy)) c
   276    of NONE => true
   277     | SOME tab => is_none (Symtab.lookup tab tyco)
   278   then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
   279   else thy;
   280 
   281 fun add_def ((class, tyco), ((name, prop), atts)) thy =
   282   let
   283     val ((lhs as Const (c, ty), args), rhs) =
   284       (apfst Term.strip_comb o Logic.dest_equals) prop;
   285   in
   286     thy
   287     |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
   288     |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
   289   end;
   290 
   291 
   292 (** instances with implicit parameter handling **)
   293 
   294 local
   295 
   296 fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
   297   let
   298     val ctxt = ProofContext.init thy;
   299     val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
   300     val ((c, ty), _) = Sign.cert_def ctxt t;
   301     val atts = map (prep_att thy) raw_atts;
   302     val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
   303     val name = case raw_name
   304      of "" => NONE
   305       | _ => SOME raw_name;
   306   in (c, (insts, ((name, t), atts))) end;
   307 
   308 fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
   309 fun read_def thy = gen_read_def thy (K I) (K I);
   310 
   311 fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   312   let
   313     val arities = map (prep_arity theory) raw_arities;
   314     val _ = if null arities then error "At least one arity must be given" else ();
   315     val _ = case (duplicates (op =) o map #1) arities
   316      of [] => ()
   317       | dupl_tycos => error ("Type constructors occur more than once in arities: "
   318           ^ commas_quote dupl_tycos);
   319     fun get_consts_class tyco ty class =
   320       let
   321         val cs = (these o try (#params o AxClass.get_info theory)) class;
   322         val subst_ty = map_type_tfree (K ty);
   323       in
   324         map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
   325       end;
   326     fun get_consts_sort (tyco, asorts, sort) =
   327       let
   328         val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
   329           (Name.names Name.context Name.aT asorts))
   330       in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
   331     val cs = maps get_consts_sort arities;
   332     fun mk_typnorm thy (ty, ty_sc) =
   333       case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
   334        of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
   335         | NONE => NONE;
   336     fun read_defs defs cs thy_read =
   337       let
   338         fun read raw_def cs =
   339           let
   340             val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
   341             val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
   342             val ((class, tyco), ty') = case AList.lookup (op =) cs c
   343              of NONE => error ("Illegal definition for constant " ^ quote c)
   344               | SOME class_ty => class_ty;
   345             val name = case name_opt
   346              of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
   347               | SOME name => name;
   348             val t' = case mk_typnorm thy_read (ty', ty)
   349              of NONE => error ("Illegal definition for constant " ^
   350                   quote (c ^ "::" ^ setmp show_sorts true
   351                     (Sign.string_of_typ thy_read) ty))
   352               | SOME norm => map_types norm t
   353           in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
   354       in fold_map read defs cs end;
   355     val (defs, other_cs) = read_defs raw_defs cs
   356       (fold Sign.primitive_arity arities (Theory.copy theory));
   357     fun after_qed' cs defs =
   358       fold Sign.add_const_constraint (map (apsnd SOME) cs)
   359       #> after_qed defs;
   360   in
   361     theory
   362     |> fold_map get_remove_global_constraint (map fst cs |> distinct (op =))
   363     ||>> fold_map add_def defs
   364     ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
   365     |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
   366   end;
   367 
   368 fun tactic_proof tac f arities defs =
   369   fold (fn arity => AxClass.prove_arity arity tac) arities
   370   #> f
   371   #> pair defs;
   372 
   373 in
   374 
   375 val instance = gen_instance Sign.cert_arity read_def
   376   (fn f => fn arities => fn defs => instance_arity f arities);
   377 val instance_cmd = gen_instance Sign.read_arity read_def_cmd
   378   (fn f => fn arities => fn defs => instance_arity f arities);
   379 fun prove_instance tac arities defs =
   380   gen_instance Sign.cert_arity read_def
   381     (tactic_proof tac) arities defs (K I);
   382 
   383 end; (*local*)
   384 
   385 
   386 
   387 (** class data **)
   388 
   389 datatype class_data = ClassData of {
   390   consts: (string * string) list
   391     (*locale parameter ~> constant name*),
   392   base_sort: sort,
   393   inst: term option list
   394     (*canonical interpretation*),
   395   morphism: morphism,
   396     (*partial morphism of canonical interpretation*)
   397   intro: thm,
   398   defs: thm list,
   399   operations: (string * (class * (typ * term))) list
   400 };
   401 
   402 fun rep_class_data (ClassData d) = d;
   403 fun mk_class_data ((consts, base_sort, inst, morphism, intro),
   404     (defs, operations)) =
   405   ClassData { consts = consts, base_sort = base_sort, inst = inst,
   406     morphism = morphism, intro = intro, defs = defs,
   407     operations = operations };
   408 fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
   409     defs, operations }) =
   410   mk_class_data (f ((consts, base_sort, inst, morphism, intro),
   411     (defs, operations)));
   412 fun merge_class_data _ (ClassData { consts = consts,
   413     base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
   414     defs = defs1, operations = operations1 },
   415   ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
   416     defs = defs2, operations = operations2 }) =
   417   mk_class_data ((consts, base_sort, inst, morphism, intro),
   418     (Thm.merge_thms (defs1, defs2),
   419       AList.merge (op =) (K true) (operations1, operations2)));
   420 
   421 structure ClassData = TheoryDataFun
   422 (
   423   type T = class_data Graph.T
   424   val empty = Graph.empty;
   425   val copy = I;
   426   val extend = I;
   427   fun merge _ = Graph.join merge_class_data;
   428 );
   429 
   430 
   431 (* queries *)
   432 
   433 val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
   434 
   435 fun the_class_data thy class = case lookup_class_data thy class
   436  of NONE => error ("Undeclared class " ^ quote class)
   437   | SOME data => data;
   438 
   439 val is_class = is_some oo lookup_class_data;
   440 
   441 val ancestry = Graph.all_succs o ClassData.get;
   442 
   443 fun these_params thy =
   444   let
   445     fun params class =
   446       let
   447         val const_typs = (#params o AxClass.get_info thy) class;
   448         val const_names = (#consts o the_class_data thy) class;
   449       in
   450         (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
   451       end;
   452   in maps params o ancestry thy end;
   453 
   454 fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   455 
   456 fun morphism thy = #morphism o the_class_data thy;
   457 
   458 fun these_intros thy =
   459   Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   460     (ClassData.get thy) [];
   461 
   462 fun these_operations thy =
   463   maps (#operations o the_class_data thy) o ancestry thy;
   464 
   465 fun print_classes thy =
   466   let
   467     val ctxt = ProofContext.init thy;
   468     val algebra = Sign.classes_of thy;
   469     val arities =
   470       Symtab.empty
   471       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   472            Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   473              ((#arities o Sorts.rep_algebra) algebra);
   474     val the_arities = these o Symtab.lookup arities;
   475     fun mk_arity class tyco =
   476       let
   477         val Ss = Sorts.mg_domain algebra tyco [class];
   478       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   479     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   480       ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   481     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   482       (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   483       (SOME o Pretty.block) [Pretty.str "supersort: ",
   484         (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   485       if is_class thy class then (SOME o Pretty.str)
   486         ("locale: " ^ Locale.extern thy class) else NONE,
   487       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   488           (Pretty.str "parameters:" :: ps)) o map mk_param
   489         o these o Option.map #params o try (AxClass.get_info thy)) class,
   490       (SOME o Pretty.block o Pretty.breaks) [
   491         Pretty.str "instances:",
   492         Pretty.list "" "" (map (mk_arity class) (the_arities class))
   493       ]
   494     ]
   495   in
   496     (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   497       o map mk_entry o Sorts.all_classes) algebra
   498   end;
   499 
   500 
   501 (* updaters *)
   502 
   503 fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   504   let
   505     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   506       (c, (class, (ty, Free v_ty)))) cs;
   507     val cs = (map o pairself) fst cs;
   508     val add_class = Graph.new_node (class,
   509         mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
   510       #> fold (curry Graph.add_edge class) superclasses;
   511   in
   512     ClassData.map add_class thy
   513   end;
   514 
   515 fun register_operation class (c, (t, some_def)) thy =
   516   let
   517     val base_sort = (#base_sort o the_class_data thy) class;
   518     val prep_typ = map_atyps
   519       (fn TVar (vi as (v, _), sort) => if Name.aT = v
   520         then TFree (v, base_sort) else TVar (vi, sort));
   521     val t' = map_types prep_typ t;
   522     val ty' = Term.fastype_of t';
   523   in
   524     thy
   525     |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   526       (fn (defs, operations) =>
   527         (fold cons (the_list some_def) defs,
   528           (c, (class, (ty', t'))) :: operations))
   529   end;
   530 
   531 
   532 (** rule calculation, tactics and methods **)
   533 
   534 val class_prefix = Logic.const_of_class o Sign.base_name;
   535 
   536 fun calculate_morphism class cs =
   537   let
   538     val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
   539       if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
   540     fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   541          of SOME (c, _) => Const (c, ty)
   542           | NONE => t)
   543       | subst_aterm t = t;
   544     val subst_term = map_aterms subst_aterm #> map_types subst_typ;
   545   in
   546     Morphism.term_morphism subst_term
   547     $> Morphism.typ_morphism subst_typ
   548   end;
   549 
   550 fun class_intro thy class sups =
   551   let
   552     fun class_elim class =
   553       case (#axioms o AxClass.get_info thy) class
   554        of [thm] => SOME (Drule.unconstrainTs thm)
   555         | [] => NONE;
   556     val pred_intro = case Locale.intros thy class
   557      of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   558       | ([intro], []) => SOME intro
   559       | ([], [intro]) => SOME intro
   560       | _ => NONE;
   561     val pred_intro' = pred_intro
   562       |> Option.map (fn intro => intro OF map_filter class_elim sups);
   563     val class_intro = (#intro o AxClass.get_info thy) class;
   564     val raw_intro = case pred_intro'
   565      of SOME pred_intro => class_intro |> OF_LAST pred_intro
   566       | NONE => class_intro;
   567     val sort = Sign.super_classes thy class;
   568     val typ = TVar ((Name.aT, 0), sort);
   569     val defs = these_defs thy sups;
   570   in
   571     raw_intro
   572     |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   573     |> strip_all_ofclass thy sort
   574     |> Thm.strip_shyps
   575     |> MetaSimplifier.rewrite_rule defs
   576     |> Drule.unconstrainTs
   577   end;
   578 
   579 fun class_interpretation class facts defs thy =
   580   let
   581     val params = these_params thy [class];
   582     val inst = (#inst o the_class_data thy) class;
   583     val tac = ALLGOALS (ProofContext.fact_tac facts);
   584     val prfx = class_prefix class;
   585   in
   586     thy
   587     |> fold_map (get_remove_global_constraint o fst o snd) params
   588     ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
   589           (inst, map (fn def => (("", []), def)) defs)
   590     |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   591   end;
   592 
   593 fun intro_classes_tac facts st =
   594   let
   595     val thy = Thm.theory_of_thm st;
   596     val classes = Sign.all_classes thy;
   597     val class_trivs = map (Thm.class_triv thy) classes;
   598     val class_intros = these_intros thy;
   599     val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   600   in
   601     Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st
   602   end;
   603 
   604 fun default_intro_classes_tac [] = intro_classes_tac []
   605   | default_intro_classes_tac _ = no_tac;
   606 
   607 fun default_tac rules ctxt facts =
   608   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   609     default_intro_classes_tac facts;
   610 
   611 val _ = Context.add_setup (Method.add_methods
   612  [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   613     "back-chain introduction rules of classes"),
   614   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   615     "apply some intro/elim rule")]);
   616 
   617 fun subclass_rule thy (sub, sup) =
   618   let
   619     val ctxt = Locale.init sub thy;
   620     val ctxt_thy = ProofContext.init thy;
   621     val props =
   622       Locale.global_asms_of thy sup
   623       |> maps snd
   624       |> map (ObjectLogic.ensure_propT thy);
   625     fun tac { prems, context } =
   626       Locale.intro_locales_tac true context prems
   627         ORELSE ALLGOALS assume_tac;
   628   in
   629     Goal.prove_multi ctxt [] [] props tac
   630     |> map (Assumption.export false ctxt ctxt_thy)
   631     |> Variable.export ctxt ctxt_thy
   632   end;
   633 
   634 fun prove_single_subclass (sub, sup) thms ctxt thy =
   635   let
   636     val ctxt_thy = ProofContext.init thy;
   637     val subclass_rule = Conjunction.intr_balanced thms
   638       |> Assumption.export false ctxt ctxt_thy
   639       |> singleton (Variable.export ctxt ctxt_thy);
   640     val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
   641     val sub_ax = #axioms (AxClass.get_info thy sub);
   642     val classrel =
   643       #intro (AxClass.get_info thy sup)
   644       |> Drule.instantiate' [SOME sub_inst] []
   645       |> OF_LAST (subclass_rule OF sub_ax)
   646       |> strip_all_ofclass thy (Sign.super_classes thy sup)
   647       |> Thm.strip_shyps
   648   in
   649     thy
   650     |> AxClass.add_classrel classrel
   651     |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
   652          I (sub, Locale.Locale sup)
   653     |> ClassData.map (Graph.add_edge (sub, sup))
   654   end;
   655 
   656 fun prove_subclass (sub, sup) thms ctxt thy =
   657   let
   658     val classes = ClassData.get thy;
   659     val is_sup = not o null o curry (Graph.irreducible_paths classes) sub;
   660     val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup;
   661     fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
   662   in
   663     thy
   664     |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
   665          (transform sup') ctxt) supclasses
   666  end;
   667 
   668 
   669 (** classes and class target **)
   670 
   671 (* class context syntax *)
   672 
   673 structure ClassSyntax = ProofDataFun(
   674   type T = {
   675     local_constraints: (string * typ) list,
   676     global_constraints: (string * typ) list,
   677     base_sort: sort,
   678     operations: (string * (typ * term)) list,
   679     unchecks: (term * term) list,
   680     passed: bool
   681   };
   682   fun init _ = {
   683     local_constraints = [],
   684     global_constraints = [],
   685     base_sort = [],
   686     operations = [],
   687     unchecks = [],
   688     passed = true
   689   };;
   690 );
   691 
   692 fun synchronize_syntax sups base_sort ctxt =
   693   let
   694     val thy = ProofContext.theory_of ctxt;
   695     fun subst_class_typ sort = map_atyps
   696       (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
   697     val operations = these_operations thy sups;
   698     val local_constraints =
   699       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   700     val global_constraints =
   701       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   702     fun declare_const (c, _) =
   703       let val b = Sign.base_name c
   704       in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   705     val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   706   in
   707     ctxt
   708     |> fold declare_const local_constraints
   709     |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
   710     |> ClassSyntax.put {
   711         local_constraints = local_constraints,
   712         global_constraints = global_constraints,
   713         base_sort = base_sort,
   714         operations = (map o apsnd) snd operations,
   715         unchecks = unchecks,
   716         passed = false
   717       }
   718   end;
   719 
   720 fun refresh_syntax class ctxt =
   721   let
   722     val thy = ProofContext.theory_of ctxt;
   723     val base_sort = (#base_sort o the_class_data thy) class;
   724   in synchronize_syntax [class] base_sort ctxt end;
   725 
   726 val mark_passed = ClassSyntax.map
   727   (fn { local_constraints, global_constraints, base_sort, operations, unchecks, passed } =>
   728     { local_constraints = local_constraints, global_constraints = global_constraints,
   729       base_sort = base_sort, operations = operations, unchecks = unchecks, passed = true });
   730 
   731 fun sort_term_check ts ctxt =
   732   let
   733     val { local_constraints, global_constraints, base_sort, operations, passed, ... } =
   734       ClassSyntax.get ctxt;
   735     fun check_improve (Const (c, ty)) = (case AList.lookup (op =) local_constraints c
   736          of SOME ty0 => (case try (Type.raw_match (ty0, ty)) Vartab.empty
   737              of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   738                  of SOME (_, TVar (tvar as (vi, _))) =>
   739                       if TypeInfer.is_param vi then cons tvar else I
   740                   | _ => I)
   741               | NONE => I)
   742           | NONE => I)
   743       | check_improve _ = I;
   744     val improvements = (fold o fold_aterms) check_improve ts [];
   745     val ts' = (map o map_types o map_atyps) (fn ty as TVar tvar =>
   746         if member (op =) improvements tvar
   747           then TFree (Name.aT, base_sort) else ty | ty => ty) ts;
   748     fun check t0 = Envir.expand_term (fn Const (c, ty) => (case AList.lookup (op =) operations c
   749          of SOME (ty0, t) =>
   750               if Type.typ_instance (ProofContext.tsig_of ctxt) (ty, ty0)
   751               then SOME (ty0, check t) else NONE
   752           | NONE => NONE)
   753       | _ => NONE) t0;
   754     val ts'' = map check ts';
   755   in if eq_list (op aconv) (ts, ts'') andalso passed then NONE
   756   else
   757     ctxt
   758     |> fold (ProofContext.add_const_constraint o apsnd SOME) global_constraints
   759     |> mark_passed
   760     |> pair ts''
   761     |> SOME
   762   end;
   763 
   764 fun sort_term_uncheck ts ctxt =
   765   let
   766     val thy = ProofContext.theory_of ctxt;
   767     val unchecks = (#unchecks o ClassSyntax.get) ctxt;
   768     val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
   769   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   770 
   771 fun init_ctxt sups base_sort ctxt =
   772   ctxt
   773   |> Variable.declare_term
   774       (Logic.mk_type (TFree (Name.aT, base_sort)))
   775   |> synchronize_syntax sups base_sort
   776   |> Context.proof_map (
   777       Syntax.add_term_check 0 "class" sort_term_check
   778       #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
   779 
   780 fun init class thy =
   781   thy
   782   |> Locale.init class
   783   |> init_ctxt [class] ((#base_sort o the_class_data thy) class);
   784 
   785 
   786 (* class definition *)
   787 
   788 local
   789 
   790 fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   791   let
   792     val supclasses = map (prep_class thy) raw_supclasses;
   793     val sups = filter (is_class thy) supclasses;
   794     fun the_base_sort class = lookup_class_data thy class
   795       |> Option.map #base_sort
   796       |> the_default [class];
   797     val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses);
   798     val supsort = Sign.minimize_sort thy supclasses;
   799     val suplocales = map Locale.Locale sups;
   800     val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   801       | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   802     val supexpr = Locale.Merge suplocales;
   803     val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   804     val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups))
   805       (map fst supparams);
   806     val mergeexpr = Locale.Merge (suplocales @ includes);
   807     val constrain = Element.Constrains ((map o apsnd o map_atyps)
   808       (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
   809   in
   810     ProofContext.init thy
   811     |> Locale.cert_expr supexpr [constrain]
   812     |> snd
   813     |> init_ctxt sups base_sort
   814     |> process_expr Locale.empty raw_elems
   815     |> fst
   816     |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
   817           (*FIXME*) if null includes then constrain :: elems else elems)))
   818   end;
   819 
   820 val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   821 val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   822 
   823 fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   824   let
   825     val superclasses = map (Sign.certify_class thy) raw_superclasses;
   826     val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   827     fun add_const ((c, ty), syn) =
   828       Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const;
   829     fun mk_axioms cs thy =
   830       raw_dep_axioms thy cs
   831       |> (map o apsnd o map) (Sign.cert_prop thy)
   832       |> rpair thy;
   833     fun constrain_typs class = (map o apsnd o Term.map_type_tfree)
   834       (fn (v, _) => TFree (v, [class]))
   835   in
   836     thy
   837     |> Sign.add_path (Logic.const_of_class name)
   838     |> fold_map add_const consts
   839     ||> Sign.restore_naming thy
   840     |-> (fn cs => mk_axioms cs
   841     #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   842            (map fst cs @ other_consts) axioms_prop
   843     #-> (fn class => `(fn _ => constrain_typs class cs)
   844     #-> (fn cs' => `(fn thy => AxClass.get_info thy class)
   845     #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs'
   846     #> pair (class, (cs', axioms)))))))
   847   end;
   848 
   849 fun gen_class prep_spec prep_param bname
   850     raw_supclasses raw_includes_elems raw_other_consts thy =
   851   let
   852     val class = Sign.full_name thy bname;
   853     val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
   854       prep_spec thy raw_supclasses raw_includes_elems;
   855     val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   856     fun mk_inst class cs =
   857       (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
   858     fun fork_syntax (Element.Fixes xs) =
   859           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   860           #>> Element.Fixes
   861       | fork_syntax x = pair x;
   862     val (elems, global_syn) = fold_map fork_syntax elems_syn [];
   863     fun globalize (c, ty) =
   864       ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
   865         (the_default NoSyn o AList.lookup (op =) global_syn) c);
   866     fun extract_params thy =
   867       let
   868         val params = map fst (Locale.parameters_of thy class);
   869       in
   870         (params, (map globalize o snd o chop (length supconsts)) params)
   871       end;
   872     fun extract_assumes params thy cs =
   873       let
   874         val consts = supconsts @ (map (fst o fst) params ~~ cs);
   875         fun subst (Free (c, ty)) =
   876               Const ((fst o the o AList.lookup (op =) consts) c, ty)
   877           | subst t = t;
   878         fun prep_asm ((name, atts), ts) =
   879           ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
   880             (map o map_aterms) subst ts);
   881       in
   882         Locale.global_asms_of thy class
   883         |> map prep_asm
   884       end;
   885   in
   886     thy
   887     |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   888     |> snd
   889     |> ProofContext.theory_of
   890     |> `extract_params
   891     |-> (fn (all_params, params) =>
   892         define_class_params (bname, supsort) params
   893           (extract_assumes params) other_consts
   894       #-> (fn (_, (consts, axioms)) =>
   895         `(fn thy => class_intro thy class sups)
   896       #-> (fn class_intro =>
   897         PureThy.note_thmss_qualified "" (NameSpace.append class classN)
   898           [((introN, []), [([class_intro], [])])]
   899       #-> (fn [(_, [class_intro])] =>
   900         add_class_data ((class, sups),
   901           (map fst params ~~ consts, base_sort,
   902             mk_inst class (map snd supconsts @ consts),
   903               calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
   904       #> class_interpretation class axioms []
   905       ))))
   906     |> init class
   907     |> pair class
   908   end;
   909 
   910 fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy);
   911 
   912 in
   913 
   914 val class_cmd = gen_class read_class_spec read_const;
   915 val class = gen_class check_class_spec (K I);
   916 
   917 end; (*local*)
   918 
   919 
   920 (* class target *)
   921 
   922 fun logical_const class pos ((c, mx), dict) thy =
   923   let
   924     val prfx = class_prefix class;
   925     val thy' = thy |> Sign.add_path prfx;
   926     val phi = morphism thy' class;
   927 
   928     val c' = Sign.full_name thy' c;
   929     val dict' = Morphism.term phi dict;
   930     val dict_def = map_types Logic.unvarifyT dict';
   931     val ty' = Term.fastype_of dict_def;
   932     val ty'' = Type.strip_sorts ty';
   933     val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   934   in
   935     thy'
   936     |> Sign.declare_const pos (c, ty'', mx) |> snd
   937     |> Thm.add_def false (c, def_eq)
   938     |>> Thm.symmetric
   939     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   940           #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   941     |> Sign.restore_naming thy
   942     |> Sign.add_const_constraint (c', SOME ty')
   943   end;
   944 
   945 fun syntactic_const class prmode pos ((c, mx), rhs) thy =
   946   let
   947     val prfx = class_prefix class;
   948     val thy' = thy |> Sign.add_path prfx;
   949     val phi = morphism thy class;
   950 
   951     val c' = Sign.full_name thy' c;
   952     val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
   953     val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
   954     val ty' = Logic.unvarifyT (Term.fastype_of rhs');
   955   in
   956     thy'
   957     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   958     |> Sign.add_const_constraint (c', SOME ty')
   959     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   960     |> register_operation class (c', (rhs', NONE))
   961     |> Sign.restore_naming thy
   962   end;
   963 
   964 
   965 (** instantiation target **)
   966 
   967 (* bookkeeping *)
   968 
   969 datatype instantiation = Instantiation of {
   970   arities: arity list,
   971   params: ((string * string) * (string * typ)) list
   972 }
   973 
   974 structure Instantiation = ProofDataFun
   975 (
   976   type T = instantiation
   977   fun init _ = Instantiation { arities = [], params = [] };
   978 );
   979 
   980 fun mk_instantiation (arities, params) =
   981   Instantiation { arities = arities, params = params };
   982 fun get_instantiation ctxt = case Instantiation.get ctxt
   983  of Instantiation data => data;
   984 fun map_instantiation f (Instantiation { arities, params }) =
   985   mk_instantiation (f (arities, params));
   986 
   987 fun the_instantiation ctxt = case get_instantiation ctxt
   988  of { arities = [], ... } => error "No instantiation target"
   989   | data => data;
   990 
   991 val instantiation_params = #params o get_instantiation;
   992 
   993 fun instantiation_param ctxt v = instantiation_params ctxt
   994   |> find_first (fn (_, (v', _)) => v = v')
   995   |> Option.map (fst o fst);
   996 
   997 fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
   998   (filter_out (fn (_, (c', _)) => c' = c));
   999 
  1000 
  1001 (* syntax *)
  1002 
  1003 fun inst_term_check ts ctxt =
  1004   let
  1005     val params = instantiation_params ctxt;
  1006     val tsig = ProofContext.tsig_of ctxt;
  1007     val thy = ProofContext.theory_of ctxt;
  1008 
  1009     fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
  1010          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
  1011              of SOME (_, ty') => Type.typ_match tsig (ty, ty')
  1012               | NONE => I)
  1013           | NONE => I)
  1014       | check_improve _ = I;
  1015     val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
  1016     val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
  1017     val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
  1018          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
  1019              of SOME v_ty => Free v_ty
  1020               | NONE => t)
  1021           | NONE => t)
  1022       | t => t) ts';
  1023   in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
  1024 
  1025 fun inst_term_uncheck ts ctxt =
  1026   let
  1027     val params = instantiation_params ctxt;
  1028     val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
  1029        (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
  1030          of SOME c => Const (c, ty)
  1031           | NONE => t)
  1032       | t => t) ts;
  1033   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
  1034 
  1035 
  1036 (* target *)
  1037 
  1038 val sanatize_name = (*FIXME*)
  1039   let
  1040     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
  1041     val is_junk = not o is_valid andf Symbol.is_regular;
  1042     val junk = Scan.many is_junk;
  1043     val scan_valids = Symbol.scanner "Malformed input"
  1044       ((junk |--
  1045         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
  1046         --| junk))
  1047       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
  1048   in
  1049     explode #> scan_valids #> implode
  1050   end;
  1051 
  1052 
  1053 fun init_instantiation arities thy =
  1054   let
  1055     val _ = if null arities then error "At least one arity must be given" else ();
  1056     val _ = case (duplicates (op =) o map #1) arities
  1057      of [] => ()
  1058       | dupl_tycos => error ("Type constructors occur more than once in arities: "
  1059           ^ commas_quote dupl_tycos);
  1060     val ty_insts = map (fn (tyco, sorts, _) =>
  1061         (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
  1062       arities;
  1063     val ty_inst = the o AList.lookup (op =) ty_insts;
  1064     fun type_name "*" = "prod"
  1065       | type_name "+" = "sum"
  1066       | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
  1067     fun get_param tyco sorts (param, (c, ty)) =
  1068       ((unoverload_const thy (c, ty), tyco),
  1069         (param ^ "_" ^ type_name tyco,
  1070           map_atyps (K (ty_inst tyco)) ty));
  1071     fun get_params (tyco, sorts, sort) =
  1072       map (get_param tyco sorts) (these_params thy sort)
  1073     val params = maps get_params arities;
  1074   in
  1075     thy
  1076     |> ProofContext.init
  1077     |> Instantiation.put (mk_instantiation (arities, params))
  1078     |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
  1079     |> fold ProofContext.add_arity arities
  1080     |> Context.proof_map (
  1081         Syntax.add_term_check 0 "instance" inst_term_check
  1082         #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
  1083   end;
  1084 
  1085 fun gen_instantiation_instance do_proof after_qed lthy =
  1086   let
  1087     val ctxt = LocalTheory.target_of lthy;
  1088     val arities = (#arities o the_instantiation) ctxt;
  1089     val arities_proof = maps Logic.mk_arities arities;
  1090     fun after_qed' results =
  1091       LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
  1092       #> after_qed;
  1093   in
  1094     lthy
  1095     |> do_proof after_qed' arities_proof
  1096   end;
  1097 
  1098 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
  1099   Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
  1100 
  1101 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
  1102   fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
  1103     (fn {context, ...} => tac context)) lthy) I;
  1104 
  1105 fun conclude_instantiation lthy =
  1106   let
  1107     val { arities, params } = the_instantiation lthy;
  1108     val thy = ProofContext.theory_of lthy;
  1109     (*val _ = map (fn (tyco, sorts, sort) =>
  1110       if Sign.of_sort thy
  1111         (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
  1112       then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
  1113         arities; FIXME activate when old instance command is gone*)
  1114     val params_of = maps (these o try (#params o AxClass.get_info thy))
  1115       o Sign.complete_sort thy;
  1116     val missing_params = arities
  1117       |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
  1118       |> filter_out (can (inst thy) o apfst fst);
  1119     fun declare_missing ((c, ty0), tyco) thy =
  1120     (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
  1121       let
  1122         val SOME class = AxClass.class_of_param thy c;
  1123         val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
  1124         val c' = NameSpace.base c;
  1125         val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
  1126         val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
  1127       in
  1128         thy
  1129         |> Sign.sticky_prefix name_inst
  1130         |> Sign.no_base_names
  1131         |> Sign.declare_const [] (c', ty, NoSyn)
  1132         |-> (fn const' as Const (c'', _) => Thm.add_def true
  1133               (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
  1134         #>> Thm.varifyT
  1135         #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
  1136         #> primitive_note Thm.internalK (c', thm)
  1137         #> snd
  1138         #> Sign.restore_naming thy))
  1139       end;
  1140   in
  1141     lthy
  1142     |> LocalTheory.theory (fold declare_missing missing_params)
  1143   end;
  1144 
  1145 end;