src/Pure/Isar/class.ML
author haftmann
Mon Dec 10 11:24:15 2007 +0100 (2007-12-10)
changeset 25597 34860182b250
parent 25574 016f677ad7b8
child 25603 4b7a58fc168c
permissions -rw-r--r--
moved instance parameter management from class.ML to axclass.ML
     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: string list * sort list * sort -> theory -> local_theory
    35   val prep_spec: local_theory -> term -> term
    36   val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    37   val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    38   val conclude_instantiation: local_theory -> local_theory
    39   val instantiation_param: Proof.context -> string -> string option
    40   val confirm_declaration: string -> local_theory -> local_theory
    41 
    42   (*old axclass layer*)
    43   val axclass_cmd: bstring * xstring list
    44     -> ((bstring * Attrib.src list) * string list) list
    45     -> theory -> class * theory
    46   val classrel_cmd: xstring * xstring -> theory -> Proof.state
    47 
    48   (*old instance layer*)
    49   val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    50   val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    51 end;
    52 
    53 structure Class : CLASS =
    54 struct
    55 
    56 (** auxiliary **)
    57 
    58 val classN = "class";
    59 val introN = "intro";
    60 
    61 fun prove_interpretation tac prfx_atts expr inst =
    62   Locale.interpretation_i I prfx_atts expr inst
    63   #> Proof.global_terminal_proof
    64       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    65   #> ProofContext.theory_of;
    66 
    67 fun prove_interpretation_in tac after_qed (name, expr) =
    68   Locale.interpretation_in_locale
    69       (ProofContext.theory after_qed) (name, expr)
    70   #> Proof.global_terminal_proof
    71       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    72   #> ProofContext.theory_of;
    73 
    74 fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2);
    75 
    76 fun strip_all_ofclass thy sort =
    77   let
    78     val typ = TVar ((Name.aT, 0), sort);
    79     fun prem_inclass t =
    80       case Logic.strip_imp_prems t
    81        of ofcls :: _ => try Logic.dest_inclass ofcls
    82         | [] => NONE;
    83     fun strip_ofclass class thm =
    84       thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
    85     fun strip thm = case (prem_inclass o Thm.prop_of) thm
    86      of SOME (_, class) => thm |> strip_ofclass class |> strip
    87       | NONE => thm;
    88   in strip end;
    89 
    90 fun get_remove_global_constraint c thy =
    91   let
    92     val ty = Sign.the_const_constraint thy c;
    93   in
    94     thy
    95     |> Sign.add_const_constraint (c, NONE)
    96     |> pair (c, Logic.unvarifyT ty)
    97   end;
    98 
    99 
   100 (** primitive axclass and instance commands **)
   101 
   102 fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   103   let
   104     val ctxt = ProofContext.init thy;
   105     val superclasses = map (Sign.read_class thy) raw_superclasses;
   106     val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   107       raw_specs;
   108     val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   109           raw_specs)
   110       |> snd
   111       |> (map o map) fst;
   112   in
   113     AxClass.define_class (class, superclasses) []
   114       (name_atts ~~ axiomss) thy
   115   end;
   116 
   117 local
   118 
   119 fun gen_instance mk_prop add_thm after_qed insts thy =
   120   let
   121     fun after_qed' results =
   122       ProofContext.theory ((fold o fold) add_thm results #> after_qed);
   123   in
   124     thy
   125     |> ProofContext.init
   126     |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
   127         o mk_prop thy) insts)
   128   end;
   129 
   130 in
   131 
   132 val instance_arity =
   133   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   134 val instance_arity_cmd =
   135   gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
   136 val classrel =
   137   gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
   138 val classrel_cmd =
   139   gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
   140 
   141 end; (*local*)
   142 
   143 
   144 (** class data **)
   145 
   146 datatype class_data = ClassData of {
   147   consts: (string * string) list
   148     (*locale parameter ~> constant name*),
   149   base_sort: sort,
   150   inst: term option list
   151     (*canonical interpretation*),
   152   morphism: morphism,
   153     (*partial morphism of canonical interpretation*)
   154   intro: thm,
   155   defs: thm list,
   156   operations: (string * (class * (typ * term))) list
   157 };
   158 
   159 fun rep_class_data (ClassData d) = d;
   160 fun mk_class_data ((consts, base_sort, inst, morphism, intro),
   161     (defs, operations)) =
   162   ClassData { consts = consts, base_sort = base_sort, inst = inst,
   163     morphism = morphism, intro = intro, defs = defs,
   164     operations = operations };
   165 fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
   166     defs, operations }) =
   167   mk_class_data (f ((consts, base_sort, inst, morphism, intro),
   168     (defs, operations)));
   169 fun merge_class_data _ (ClassData { consts = consts,
   170     base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
   171     defs = defs1, operations = operations1 },
   172   ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
   173     defs = defs2, operations = operations2 }) =
   174   mk_class_data ((consts, base_sort, inst, morphism, intro),
   175     (Thm.merge_thms (defs1, defs2),
   176       AList.merge (op =) (K true) (operations1, operations2)));
   177 
   178 structure ClassData = TheoryDataFun
   179 (
   180   type T = class_data Graph.T
   181   val empty = Graph.empty;
   182   val copy = I;
   183   val extend = I;
   184   fun merge _ = Graph.join merge_class_data;
   185 );
   186 
   187 
   188 (* queries *)
   189 
   190 val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
   191 
   192 fun the_class_data thy class = case lookup_class_data thy class
   193  of NONE => error ("Undeclared class " ^ quote class)
   194   | SOME data => data;
   195 
   196 val is_class = is_some oo lookup_class_data;
   197 
   198 val ancestry = Graph.all_succs o ClassData.get;
   199 
   200 fun these_params thy =
   201   let
   202     fun params class =
   203       let
   204         val const_typs = (#params o AxClass.get_info thy) class;
   205         val const_names = (#consts o the_class_data thy) class;
   206       in
   207         (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
   208       end;
   209   in maps params o ancestry thy end;
   210 
   211 fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   212 
   213 fun morphism thy = #morphism o the_class_data thy;
   214 
   215 fun these_intros thy =
   216   Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   217     (ClassData.get thy) [];
   218 
   219 fun these_operations thy =
   220   maps (#operations o the_class_data thy) o ancestry thy;
   221 
   222 fun print_classes thy =
   223   let
   224     val ctxt = ProofContext.init thy;
   225     val algebra = Sign.classes_of thy;
   226     val arities =
   227       Symtab.empty
   228       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   229            Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   230              ((#arities o Sorts.rep_algebra) algebra);
   231     val the_arities = these o Symtab.lookup arities;
   232     fun mk_arity class tyco =
   233       let
   234         val Ss = Sorts.mg_domain algebra tyco [class];
   235       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   236     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   237       ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   238     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   239       (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   240       (SOME o Pretty.block) [Pretty.str "supersort: ",
   241         (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   242       if is_class thy class then (SOME o Pretty.str)
   243         ("locale: " ^ Locale.extern thy class) else NONE,
   244       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   245           (Pretty.str "parameters:" :: ps)) o map mk_param
   246         o these o Option.map #params o try (AxClass.get_info thy)) class,
   247       (SOME o Pretty.block o Pretty.breaks) [
   248         Pretty.str "instances:",
   249         Pretty.list "" "" (map (mk_arity class) (the_arities class))
   250       ]
   251     ]
   252   in
   253     (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   254       o map mk_entry o Sorts.all_classes) algebra
   255   end;
   256 
   257 
   258 (* updaters *)
   259 
   260 fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   261   let
   262     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   263       (c, (class, (ty, Free v_ty)))) cs;
   264     val cs = (map o pairself) fst cs;
   265     val add_class = Graph.new_node (class,
   266         mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
   267       #> fold (curry Graph.add_edge class) superclasses;
   268   in
   269     ClassData.map add_class thy
   270   end;
   271 
   272 fun register_operation class (c, (t, some_def)) thy =
   273   let
   274     val base_sort = (#base_sort o the_class_data thy) class;
   275     val prep_typ = map_atyps
   276       (fn TVar (vi as (v, _), sort) => if Name.aT = v
   277         then TFree (v, base_sort) else TVar (vi, sort));
   278     val t' = map_types prep_typ t;
   279     val ty' = Term.fastype_of t';
   280   in
   281     thy
   282     |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   283       (fn (defs, operations) =>
   284         (fold cons (the_list some_def) defs,
   285           (c, (class, (ty', t'))) :: operations))
   286   end;
   287 
   288 
   289 (** rule calculation, tactics and methods **)
   290 
   291 val class_prefix = Logic.const_of_class o Sign.base_name;
   292 
   293 fun calculate_morphism class cs =
   294   let
   295     val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
   296       if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
   297     fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   298          of SOME (c, _) => Const (c, ty)
   299           | NONE => t)
   300       | subst_aterm t = t;
   301     val subst_term = map_aterms subst_aterm #> map_types subst_typ;
   302   in
   303     Morphism.term_morphism subst_term
   304     $> Morphism.typ_morphism subst_typ
   305   end;
   306 
   307 fun class_intro thy class sups =
   308   let
   309     fun class_elim class =
   310       case (#axioms o AxClass.get_info thy) class
   311        of [thm] => SOME (Drule.unconstrainTs thm)
   312         | [] => NONE;
   313     val pred_intro = case Locale.intros thy class
   314      of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   315       | ([intro], []) => SOME intro
   316       | ([], [intro]) => SOME intro
   317       | _ => NONE;
   318     val pred_intro' = pred_intro
   319       |> Option.map (fn intro => intro OF map_filter class_elim sups);
   320     val class_intro = (#intro o AxClass.get_info thy) class;
   321     val raw_intro = case pred_intro'
   322      of SOME pred_intro => class_intro |> OF_LAST pred_intro
   323       | NONE => class_intro;
   324     val sort = Sign.super_classes thy class;
   325     val typ = TVar ((Name.aT, 0), sort);
   326     val defs = these_defs thy sups;
   327   in
   328     raw_intro
   329     |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   330     |> strip_all_ofclass thy sort
   331     |> Thm.strip_shyps
   332     |> MetaSimplifier.rewrite_rule defs
   333     |> Drule.unconstrainTs
   334   end;
   335 
   336 fun class_interpretation class facts defs thy =
   337   let
   338     val params = these_params thy [class];
   339     val inst = (#inst o the_class_data thy) class;
   340     val tac = ALLGOALS (ProofContext.fact_tac facts);
   341     val prfx = class_prefix class;
   342   in
   343     thy
   344     |> fold_map (get_remove_global_constraint o fst o snd) params
   345     ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
   346           (inst, map (fn def => (("", []), def)) defs)
   347     |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   348   end;
   349 
   350 fun intro_classes_tac facts st =
   351   let
   352     val thy = Thm.theory_of_thm st;
   353     val classes = Sign.all_classes thy;
   354     val class_trivs = map (Thm.class_triv thy) classes;
   355     val class_intros = these_intros thy;
   356     val axclass_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   357   in
   358     Method.intros_tac (class_trivs @ class_intros @ axclass_intros) facts st
   359   end;
   360 
   361 fun default_intro_classes_tac [] = intro_classes_tac []
   362   | default_intro_classes_tac _ = no_tac;
   363 
   364 fun default_tac rules ctxt facts =
   365   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   366     default_intro_classes_tac facts;
   367 
   368 val _ = Context.add_setup (Method.add_methods
   369  [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   370     "back-chain introduction rules of classes"),
   371   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   372     "apply some intro/elim rule")]);
   373 
   374 fun subclass_rule thy (sub, sup) =
   375   let
   376     val ctxt = Locale.init sub thy;
   377     val ctxt_thy = ProofContext.init thy;
   378     val props =
   379       Locale.global_asms_of thy sup
   380       |> maps snd
   381       |> map (ObjectLogic.ensure_propT thy);
   382     fun tac { prems, context } =
   383       Locale.intro_locales_tac true context prems
   384         ORELSE ALLGOALS assume_tac;
   385   in
   386     Goal.prove_multi ctxt [] [] props tac
   387     |> map (Assumption.export false ctxt ctxt_thy)
   388     |> Variable.export ctxt ctxt_thy
   389   end;
   390 
   391 fun prove_single_subclass (sub, sup) thms ctxt thy =
   392   let
   393     val ctxt_thy = ProofContext.init thy;
   394     val subclass_rule = Conjunction.intr_balanced thms
   395       |> Assumption.export false ctxt ctxt_thy
   396       |> singleton (Variable.export ctxt ctxt_thy);
   397     val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
   398     val sub_ax = #axioms (AxClass.get_info thy sub);
   399     val classrel =
   400       #intro (AxClass.get_info thy sup)
   401       |> Drule.instantiate' [SOME sub_inst] []
   402       |> OF_LAST (subclass_rule OF sub_ax)
   403       |> strip_all_ofclass thy (Sign.super_classes thy sup)
   404       |> Thm.strip_shyps
   405   in
   406     thy
   407     |> AxClass.add_classrel classrel
   408     |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
   409          I (sub, Locale.Locale sup)
   410     |> ClassData.map (Graph.add_edge (sub, sup))
   411   end;
   412 
   413 fun prove_subclass (sub, sup) thms ctxt thy =
   414   let
   415     val classes = ClassData.get thy;
   416     val is_sup = not o null o curry (Graph.irreducible_paths classes) sub;
   417     val supclasses = Graph.all_succs classes [sup] |> filter_out is_sup;
   418     fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
   419   in
   420     thy
   421     |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
   422          (transform sup') ctxt) supclasses
   423  end;
   424 
   425 
   426 (** classes and class target **)
   427 
   428 (* class context syntax *)
   429 
   430 structure ClassSyntax = ProofDataFun(
   431   type T = {
   432     local_constraints: (string * typ) list,
   433     global_constraints: (string * typ) list,
   434     base_sort: sort,
   435     operations: (string * (typ * term)) list,
   436     unchecks: (term * term) list,
   437     passed: bool
   438   };
   439   fun init _ = {
   440     local_constraints = [],
   441     global_constraints = [],
   442     base_sort = [],
   443     operations = [],
   444     unchecks = [],
   445     passed = true
   446   };;
   447 );
   448 
   449 fun synchronize_syntax sups base_sort ctxt =
   450   let
   451     val thy = ProofContext.theory_of ctxt;
   452     fun subst_class_typ sort = map_atyps
   453       (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
   454     val operations = these_operations thy sups;
   455     val local_constraints =
   456       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   457     val global_constraints =
   458       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   459     fun declare_const (c, _) =
   460       let val b = Sign.base_name c
   461       in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   462     val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   463   in
   464     ctxt
   465     |> fold declare_const local_constraints
   466     |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
   467     |> ClassSyntax.put {
   468         local_constraints = local_constraints,
   469         global_constraints = global_constraints,
   470         base_sort = base_sort,
   471         operations = (map o apsnd) snd operations,
   472         unchecks = unchecks,
   473         passed = false
   474       }
   475   end;
   476 
   477 fun refresh_syntax class ctxt =
   478   let
   479     val thy = ProofContext.theory_of ctxt;
   480     val base_sort = (#base_sort o the_class_data thy) class;
   481   in synchronize_syntax [class] base_sort ctxt end;
   482 
   483 val mark_passed = ClassSyntax.map
   484   (fn { local_constraints, global_constraints, base_sort, operations, unchecks, passed } =>
   485     { local_constraints = local_constraints, global_constraints = global_constraints,
   486       base_sort = base_sort, operations = operations, unchecks = unchecks, passed = true });
   487 
   488 fun sort_term_check ts ctxt =
   489   let
   490     val { local_constraints, global_constraints, base_sort, operations, passed, ... } =
   491       ClassSyntax.get ctxt;
   492     fun check_improve (Const (c, ty)) = (case AList.lookup (op =) local_constraints c
   493          of SOME ty0 => (case try (Type.raw_match (ty0, ty)) Vartab.empty
   494              of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   495                  of SOME (_, TVar (tvar as (vi, _))) =>
   496                       if TypeInfer.is_param vi then cons tvar else I
   497                   | _ => I)
   498               | NONE => I)
   499           | NONE => I)
   500       | check_improve _ = I;
   501     val improvements = (fold o fold_aterms) check_improve ts [];
   502     val ts' = (map o map_types o map_atyps) (fn ty as TVar tvar =>
   503         if member (op =) improvements tvar
   504           then TFree (Name.aT, base_sort) else ty | ty => ty) ts;
   505     fun check t0 = Envir.expand_term (fn Const (c, ty) => (case AList.lookup (op =) operations c
   506          of SOME (ty0, t) =>
   507               if Type.typ_instance (ProofContext.tsig_of ctxt) (ty, ty0)
   508               then SOME (ty0, check t) else NONE
   509           | NONE => NONE)
   510       | _ => NONE) t0;
   511     val ts'' = map check ts';
   512   in if eq_list (op aconv) (ts, ts'') andalso passed then NONE
   513   else
   514     ctxt
   515     |> fold (ProofContext.add_const_constraint o apsnd SOME) global_constraints
   516     |> mark_passed
   517     |> pair ts''
   518     |> SOME
   519   end;
   520 
   521 fun sort_term_uncheck ts ctxt =
   522   let
   523     val thy = ProofContext.theory_of ctxt;
   524     val unchecks = (#unchecks o ClassSyntax.get) ctxt;
   525     val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
   526   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   527 
   528 fun init_ctxt sups base_sort ctxt =
   529   ctxt
   530   |> Variable.declare_term
   531       (Logic.mk_type (TFree (Name.aT, base_sort)))
   532   |> synchronize_syntax sups base_sort
   533   |> Context.proof_map (
   534       Syntax.add_term_check 0 "class" sort_term_check
   535       #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
   536 
   537 fun init class thy =
   538   thy
   539   |> Locale.init class
   540   |> init_ctxt [class] ((#base_sort o the_class_data thy) class);
   541 
   542 
   543 (* class definition *)
   544 
   545 local
   546 
   547 fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   548   let
   549     val supclasses = map (prep_class thy) raw_supclasses;
   550     val sups = filter (is_class thy) supclasses;
   551     fun the_base_sort class = lookup_class_data thy class
   552       |> Option.map #base_sort
   553       |> the_default [class];
   554     val base_sort = Sign.minimize_sort thy (maps the_base_sort supclasses);
   555     val supsort = Sign.minimize_sort thy supclasses;
   556     val suplocales = map Locale.Locale sups;
   557     val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   558       | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   559     val supexpr = Locale.Merge suplocales;
   560     val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   561     val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups))
   562       (map fst supparams);
   563     val mergeexpr = Locale.Merge (suplocales @ includes);
   564     val constrain = Element.Constrains ((map o apsnd o map_atyps)
   565       (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
   566   in
   567     ProofContext.init thy
   568     |> Locale.cert_expr supexpr [constrain]
   569     |> snd
   570     |> init_ctxt sups base_sort
   571     |> process_expr Locale.empty raw_elems
   572     |> fst
   573     |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
   574           (*FIXME*) if null includes then constrain :: elems else elems)))
   575   end;
   576 
   577 val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   578 val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   579 
   580 fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   581   let
   582     val superclasses = map (Sign.certify_class thy) raw_superclasses;
   583     val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   584     fun add_const ((c, ty), syn) =
   585       Sign.declare_const [] (c, Type.strip_sorts ty, syn) #>> Term.dest_Const;
   586     fun mk_axioms cs thy =
   587       raw_dep_axioms thy cs
   588       |> (map o apsnd o map) (Sign.cert_prop thy)
   589       |> rpair thy;
   590     fun constrain_typs class = (map o apsnd o Term.map_type_tfree)
   591       (fn (v, _) => TFree (v, [class]))
   592   in
   593     thy
   594     |> Sign.add_path (Logic.const_of_class name)
   595     |> fold_map add_const consts
   596     ||> Sign.restore_naming thy
   597     |-> (fn cs => mk_axioms cs
   598     #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   599            (map fst cs @ other_consts) axioms_prop
   600     #-> (fn class => `(fn _ => constrain_typs class cs)
   601     #-> (fn cs' => `(fn thy => AxClass.get_info thy class)
   602     #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs'
   603     #> pair (class, (cs', axioms)))))))
   604   end;
   605 
   606 fun gen_class prep_spec prep_param bname
   607     raw_supclasses raw_includes_elems raw_other_consts thy =
   608   let
   609     val class = Sign.full_name thy bname;
   610     val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
   611       prep_spec thy raw_supclasses raw_includes_elems;
   612     val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   613     fun mk_inst class cs =
   614       (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
   615     fun fork_syntax (Element.Fixes xs) =
   616           fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   617           #>> Element.Fixes
   618       | fork_syntax x = pair x;
   619     val (elems, global_syn) = fold_map fork_syntax elems_syn [];
   620     fun globalize (c, ty) =
   621       ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
   622         (the_default NoSyn o AList.lookup (op =) global_syn) c);
   623     fun extract_params thy =
   624       let
   625         val params = map fst (Locale.parameters_of thy class);
   626       in
   627         (params, (map globalize o snd o chop (length supconsts)) params)
   628       end;
   629     fun extract_assumes params thy cs =
   630       let
   631         val consts = supconsts @ (map (fst o fst) params ~~ cs);
   632         fun subst (Free (c, ty)) =
   633               Const ((fst o the o AList.lookup (op =) consts) c, ty)
   634           | subst t = t;
   635         fun prep_asm ((name, atts), ts) =
   636           ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
   637             (map o map_aterms) subst ts);
   638       in
   639         Locale.global_asms_of thy class
   640         |> map prep_asm
   641       end;
   642   in
   643     thy
   644     |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   645     |> snd
   646     |> ProofContext.theory_of
   647     |> `extract_params
   648     |-> (fn (all_params, params) =>
   649         define_class_params (bname, supsort) params
   650           (extract_assumes params) other_consts
   651       #-> (fn (_, (consts, axioms)) =>
   652         `(fn thy => class_intro thy class sups)
   653       #-> (fn class_intro =>
   654         PureThy.note_thmss_qualified "" (NameSpace.append class classN)
   655           [((introN, []), [([class_intro], [])])]
   656       #-> (fn [(_, [class_intro])] =>
   657         add_class_data ((class, sups),
   658           (map fst params ~~ consts, base_sort,
   659             mk_inst class (map snd supconsts @ consts),
   660               calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
   661       #> class_interpretation class axioms []
   662       ))))
   663     |> init class
   664     |> pair class
   665   end;
   666 
   667 fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy);
   668 
   669 in
   670 
   671 val class_cmd = gen_class read_class_spec read_const;
   672 val class = gen_class check_class_spec (K I);
   673 
   674 end; (*local*)
   675 
   676 
   677 (* class target *)
   678 
   679 fun logical_const class pos ((c, mx), dict) thy =
   680   let
   681     val prfx = class_prefix class;
   682     val thy' = thy |> Sign.add_path prfx;
   683     val phi = morphism thy' class;
   684 
   685     val c' = Sign.full_name thy' c;
   686     val dict' = Morphism.term phi dict;
   687     val dict_def = map_types Logic.unvarifyT dict';
   688     val ty' = Term.fastype_of dict_def;
   689     val ty'' = Type.strip_sorts ty';
   690     val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   691   in
   692     thy'
   693     |> Sign.declare_const pos (c, ty'', mx) |> snd
   694     |> Thm.add_def false false (c, def_eq)
   695     |>> Thm.symmetric
   696     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   697           #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   698     |> Sign.restore_naming thy
   699     |> Sign.add_const_constraint (c', SOME ty')
   700   end;
   701 
   702 fun syntactic_const class prmode pos ((c, mx), rhs) thy =
   703   let
   704     val prfx = class_prefix class;
   705     val thy' = thy |> Sign.add_path prfx;
   706     val phi = morphism thy class;
   707 
   708     val c' = Sign.full_name thy' c;
   709     val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
   710     val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
   711     val ty' = Logic.unvarifyT (Term.fastype_of rhs');
   712   in
   713     thy'
   714     |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   715     |> Sign.add_const_constraint (c', SOME ty')
   716     |> Sign.notation true prmode [(Const (c', ty'), mx)]
   717     |> register_operation class (c', (rhs', NONE))
   718     |> Sign.restore_naming thy
   719   end;
   720 
   721 
   722 (** instantiation target **)
   723 
   724 (* bookkeeping *)
   725 
   726 datatype instantiation = Instantiation of {
   727   arities: string list * sort list * sort,
   728   params: ((string * string) * (string * typ)) list
   729     (*(instantiation const, type constructor), (local instantiation parameter, typ)*)
   730 }
   731 
   732 structure Instantiation = ProofDataFun
   733 (
   734   type T = instantiation
   735   fun init _ = Instantiation { arities = ([], [], []), params = [] };
   736 );
   737 
   738 fun mk_instantiation (arities, params) =
   739   Instantiation { arities = arities, params = params };
   740 fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
   741  of Instantiation data => data;
   742 fun map_instantiation f = (LocalTheory.target o Instantiation.map)
   743   (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   744 
   745 fun the_instantiation lthy = case get_instantiation lthy
   746  of { arities = ([], [], []), ... } => error "No instantiation target"
   747   | data => data;
   748 
   749 val instantiation_params = #params o get_instantiation;
   750 
   751 fun instantiation_param lthy v = instantiation_params lthy
   752   |> find_first (fn (_, (v', _)) => v = v')
   753   |> Option.map (fst o fst);
   754 
   755 fun confirm_declaration c = (map_instantiation o apsnd)
   756   (filter_out (fn (_, (c', _)) => c' = c));
   757 
   758 
   759 (* syntax *)
   760 
   761 fun subst_param thy params = map_aterms (fn t as Const (c, ty) =>
   762     (case AxClass.inst_tyco_of thy (c, ty)
   763      of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   764          of SOME v_ty => Free v_ty
   765           | NONE => t)
   766       | NONE => t)
   767   | t => t);
   768 
   769 fun prep_spec lthy =
   770   let
   771     val thy = ProofContext.theory_of lthy;
   772     val params = instantiation_params lthy;
   773   in subst_param thy params end;
   774 
   775 fun inst_term_check ts lthy =
   776   let
   777     val params = instantiation_params lthy;
   778     val tsig = ProofContext.tsig_of lthy;
   779     val thy = ProofContext.theory_of lthy;
   780 
   781     fun check_improve (Const (c, ty)) = (case AxClass.inst_tyco_of thy (c, ty)
   782          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   783              of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
   784               | NONE => I)
   785           | NONE => I)
   786       | check_improve _ = I;
   787     val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
   788     val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
   789     val ts'' = map (subst_param thy params) ts';
   790   in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
   791 
   792 fun inst_term_uncheck ts lthy =
   793   let
   794     val params = instantiation_params lthy;
   795     val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
   796        (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
   797          of SOME c => Const (c, ty)
   798           | NONE => t)
   799       | t => t) ts;
   800   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
   801 
   802 
   803 (* target *)
   804 
   805 val sanatize_name = (*FIXME*)
   806   let
   807     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   808       orelse s = "'" orelse s = "_";
   809     val is_junk = not o is_valid andf Symbol.is_regular;
   810     val junk = Scan.many is_junk;
   811     val scan_valids = Symbol.scanner "Malformed input"
   812       ((junk |--
   813         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   814         --| junk))
   815       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   816   in
   817     explode #> scan_valids #> implode
   818   end;
   819 
   820 fun init_instantiation (tycos, sorts, sort) thy =
   821   let
   822     val _ = if null tycos then error "At least one arity must be given" else ();
   823     val _ = map (the_class_data thy) sort;
   824     val vs = map TFree (Name.names Name.context Name.aT sorts);
   825     fun type_name "*" = "prod"
   826       | type_name "+" = "sum"
   827       | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   828     fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
   829       then NONE else SOME ((AxClass.unoverload_const thy (c, ty), tyco),
   830         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
   831     val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
   832   in
   833     thy
   834     |> ProofContext.init
   835     |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
   836     |> fold (Variable.declare_term o Logic.mk_type) vs
   837     |> fold (Variable.declare_names o Free o snd) params
   838     |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
   839     |> Context.proof_map (
   840         Syntax.add_term_check 0 "instance" inst_term_check
   841         #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
   842   end;
   843 
   844 fun gen_instantiation_instance do_proof after_qed lthy =
   845   let
   846     val (tycos, sorts, sort) = (#arities o the_instantiation) lthy;
   847     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   848     fun after_qed' results =
   849       LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   850       #> after_qed;
   851   in
   852     lthy
   853     |> do_proof after_qed' arities_proof
   854   end;
   855 
   856 val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   857   Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   858 
   859 fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   860   fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   861     (fn {context, ...} => tac context)) ts) lthy) I;
   862 
   863 fun conclude_instantiation lthy =
   864   let
   865     val { arities, params } = the_instantiation lthy;
   866     val (tycos, sorts, sort) = arities;
   867     val thy = ProofContext.theory_of lthy;
   868     val _ = map (fn tyco => if Sign.of_sort thy
   869         (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
   870       then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   871         tycos;
   872   in lthy end;
   873 
   874 end;