rearranged target theories
authorhaftmann
Mon Jan 05 15:36:24 2009 +0100 (2009-01-05)
changeset 29358efdfe5dfe008
parent 29357 11956fa598b7
child 29359 f831192b9366
rearranged target theories
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/subclass.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Jan 05 15:35:42 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Mon Jan 05 15:36:24 2009 +0100
     1.3 @@ -36,10 +36,10 @@
     1.4    General/stack.ML General/symbol.ML General/symbol_pos.ML		\
     1.5    General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
     1.6    Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
     1.7 -  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML	\
     1.8 +  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
     1.9    Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML		\
    1.10    Isar/element.ML Isar/expression.ML Isar/find_theorems.ML		\
    1.11 -  Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
    1.12 +  Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
    1.13    Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
    1.14    Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML	\
    1.15    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    1.16 @@ -47,7 +47,7 @@
    1.17    Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    1.18    Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    1.19    Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML			\
    1.20 -  Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML		\
    1.21 +  Isar/spec_parse.ML Isar/specification.ML		\
    1.22    Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML		\
    1.23    ML-Systems/alice.ML ML-Systems/exn.ML					\
    1.24    ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
     2.1 --- a/src/Pure/Isar/ROOT.ML	Mon Jan 05 15:35:42 2009 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Jan 05 15:36:24 2009 +0100
     2.3 @@ -55,11 +55,10 @@
     2.4  use "overloading.ML";
     2.5  use "locale.ML";
     2.6  use "new_locale.ML";
     2.7 -use "class.ML";
     2.8 +use "class_target.ML";
     2.9  use "theory_target.ML";
    2.10  use "expression.ML";
    2.11 -use "instance.ML";
    2.12 -use "subclass.ML";
    2.13 +use "class.ML";
    2.14  
    2.15  (*complex proof machineries*)
    2.16  use "../simplifier.ML";
     3.1 --- a/src/Pure/Isar/class.ML	Mon Jan 05 15:35:42 2009 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Mon Jan 05 15:36:24 2009 +0100
     3.3 @@ -1,361 +1,30 @@
     3.4 -(*  Title:      Pure/Isar/class.ML
     3.5 -    ID:         $Id$
     3.6 +(*  Title:      Pure/Isar/ML
     3.7      Author:     Florian Haftmann, TU Muenchen
     3.8  
     3.9 -Type classes derived from primitive axclasses and locales.
    3.10 +Type classes derived from primitive axclasses and locales - interfaces
    3.11  *)
    3.12  
    3.13  signature CLASS =
    3.14  sig
    3.15 -  (*classes*)
    3.16 +  include CLASS_TARGET
    3.17 +    (*FIXME the split in class_target.ML, theory_target.ML and
    3.18 +      ML is artificial*)
    3.19 +
    3.20    val class: bstring -> class list -> Element.context_i list
    3.21      -> theory -> string * Proof.context
    3.22    val class_cmd: bstring -> xstring list -> Element.context list
    3.23      -> theory -> string * Proof.context
    3.24 -
    3.25 -  val init: class -> theory -> Proof.context
    3.26 -  val declare: class -> Properties.T
    3.27 -    -> (string * mixfix) * term -> theory -> theory
    3.28 -  val abbrev: class -> Syntax.mode -> Properties.T
    3.29 -    -> (string * mixfix) * term -> theory -> theory
    3.30 -  val refresh_syntax: class -> Proof.context -> Proof.context
    3.31 -
    3.32 -  val intro_classes_tac: thm list -> tactic
    3.33 -  val default_intro_tac: Proof.context -> thm list -> tactic
    3.34 -  val prove_subclass: class * class -> thm option -> theory -> theory
    3.35 -
    3.36 -  val class_prefix: string -> string
    3.37 -  val is_class: theory -> class -> bool
    3.38 -  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    3.39 -  val print_classes: theory -> unit
    3.40 -
    3.41 -  (*instances*)
    3.42 -  val init_instantiation: string list * (string * sort) list * sort
    3.43 -    -> theory -> local_theory
    3.44 -  val instantiation_instance: (local_theory -> local_theory)
    3.45 -    -> local_theory -> Proof.state
    3.46 -  val prove_instantiation_instance: (Proof.context -> tactic)
    3.47 -    -> local_theory -> local_theory
    3.48 -  val prove_instantiation_exit: (Proof.context -> tactic)
    3.49 -    -> local_theory -> theory
    3.50 -  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    3.51 -    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    3.52 -  val conclude_instantiation: local_theory -> local_theory
    3.53 -  val instantiation_param: local_theory -> string -> string option
    3.54 -  val confirm_declaration: string -> local_theory -> local_theory
    3.55 -  val pretty_instantiation: local_theory -> Pretty.T
    3.56 -  val type_name: string -> string
    3.57 -
    3.58 -  (*old axclass layer*)
    3.59 -  val axclass_cmd: bstring * xstring list
    3.60 -    -> (Attrib.binding * string list) list
    3.61 -    -> theory -> class * theory
    3.62 -  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    3.63 -
    3.64 -  (*old instance layer*)
    3.65 -  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    3.66 -  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    3.67 +  val prove_subclass: tactic -> class -> local_theory -> local_theory
    3.68 +  val subclass: class -> local_theory -> Proof.state
    3.69 +  val subclass_cmd: xstring -> local_theory -> Proof.state
    3.70  end;
    3.71  
    3.72  structure Class : CLASS =
    3.73  struct
    3.74  
    3.75 -(*temporary adaption code to mediate between old and new locale code*)
    3.76 -
    3.77 -structure Old_Locale =
    3.78 -struct
    3.79 -
    3.80 -val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
    3.81 -
    3.82 -val interpretation = Locale.interpretation;
    3.83 -val interpretation_in_locale = Locale.interpretation_in_locale;
    3.84 -val get_interpret_morph = Locale.get_interpret_morph;
    3.85 -val Locale = Locale.Locale;
    3.86 -val extern = Locale.extern;
    3.87 -val intros = Locale.intros;
    3.88 -val dests = Locale.dests;
    3.89 -val init = Locale.init;
    3.90 -val Merge = Locale.Merge;
    3.91 -val parameters_of_expr = Locale.parameters_of_expr;
    3.92 -val empty = Locale.empty;
    3.93 -val cert_expr = Locale.cert_expr;
    3.94 -val read_expr = Locale.read_expr;
    3.95 -val parameters_of = Locale.parameters_of;
    3.96 -val add_locale = Locale.add_locale;
    3.97 -
    3.98 -end;
    3.99 -
   3.100 -(*structure New_Locale =
   3.101 -struct
   3.102 -
   3.103 -val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
   3.104 -
   3.105 -val interpretation = Locale.interpretation; (*!*)
   3.106 -val interpretation_in_locale = Locale.interpretation_in_locale; (*!*)
   3.107 -val get_interpret_morph = Locale.get_interpret_morph; (*!*)
   3.108 -fun Locale loc = ([(loc, ("", Expression.Positional []))], []);
   3.109 -val extern = NewLocale.extern;
   3.110 -val intros = Locale.intros; (*!*)
   3.111 -val dests = Locale.dests; (*!*)
   3.112 -val init = NewLocale.init;
   3.113 -fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []);
   3.114 -val parameters_of_expr = Locale.parameters_of_expr; (*!*)
   3.115 -val empty = ([], []);
   3.116 -val cert_expr = Locale.cert_expr; (*!"*)
   3.117 -val read_expr = Locale.read_expr; (*!"*)
   3.118 -val parameters_of = NewLocale.params_of; (*why typ option?*)
   3.119 -val add_locale = Expression.add_locale;
   3.120 -
   3.121 -end;*)
   3.122 -
   3.123 -structure Locale = Old_Locale;
   3.124 -
   3.125 -(*proper code again*)
   3.126 -
   3.127 -
   3.128 -(** auxiliary **)
   3.129 -
   3.130 -fun prove_interpretation tac prfx_atts expr inst =
   3.131 -  Locale.interpretation I prfx_atts expr inst
   3.132 -  ##> Proof.global_terminal_proof
   3.133 -      (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   3.134 -  ##> ProofContext.theory_of;
   3.135 -
   3.136 -fun prove_interpretation_in tac after_qed (name, expr) =
   3.137 -  Locale.interpretation_in_locale
   3.138 -      (ProofContext.theory after_qed) (name, expr)
   3.139 -  #> Proof.global_terminal_proof
   3.140 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   3.141 -  #> ProofContext.theory_of;
   3.142 -
   3.143 -val class_prefix = Logic.const_of_class o Sign.base_name;
   3.144 -
   3.145 -fun class_name_morphism class =
   3.146 -  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
   3.147 -
   3.148 -fun activate_class_morphism thy class inst morphism =
   3.149 -  Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
   3.150 -
   3.151 -fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
   3.152 -  let
   3.153 -    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
   3.154 -      [class]))) (Sign.the_const_type thy c)) consts;
   3.155 -    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
   3.156 -    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
   3.157 -    fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
   3.158 -      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
   3.159 -    val prfx = class_prefix class;
   3.160 -  in
   3.161 -    thy
   3.162 -    |> fold2 add_constraint (map snd consts) no_constraints
   3.163 -    |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
   3.164 -          (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
   3.165 -    ||> fold2 add_constraint (map snd consts) constraints
   3.166 -  end;
   3.167 -
   3.168 -
   3.169 -(** primitive axclass and instance commands **)
   3.170 -
   3.171 -fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   3.172 -  let
   3.173 -    val ctxt = ProofContext.init thy;
   3.174 -    val superclasses = map (Sign.read_class thy) raw_superclasses;
   3.175 -    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   3.176 -      raw_specs;
   3.177 -    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   3.178 -          raw_specs)
   3.179 -      |> snd
   3.180 -      |> (map o map) fst;
   3.181 -  in
   3.182 -    AxClass.define_class (class, superclasses) []
   3.183 -      (name_atts ~~ axiomss) thy
   3.184 -  end;
   3.185 -
   3.186 -local
   3.187 -
   3.188 -fun gen_instance mk_prop add_thm after_qed insts thy =
   3.189 -  let
   3.190 -    fun after_qed' results =
   3.191 -      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
   3.192 -  in
   3.193 -    thy
   3.194 -    |> ProofContext.init
   3.195 -    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
   3.196 -        o mk_prop thy) insts)
   3.197 -  end;
   3.198 -
   3.199 -in
   3.200 -
   3.201 -val instance_arity =
   3.202 -  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   3.203 -val instance_arity_cmd =
   3.204 -  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
   3.205 -val classrel =
   3.206 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
   3.207 -val classrel_cmd =
   3.208 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
   3.209 -
   3.210 -end; (*local*)
   3.211 -
   3.212 -
   3.213 -(** class data **)
   3.214 -
   3.215 -datatype class_data = ClassData of {
   3.216 +open Class_Target;
   3.217  
   3.218 -  (* static part *)
   3.219 -  consts: (string * string) list
   3.220 -    (*locale parameter ~> constant name*),
   3.221 -  base_sort: sort,
   3.222 -  inst: term list
   3.223 -    (*canonical interpretation*),
   3.224 -  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
   3.225 -    (*morphism cookie of canonical interpretation*),
   3.226 -  assm_intro: thm option,
   3.227 -  of_class: thm,
   3.228 -  axiom: thm option,
   3.229 -  
   3.230 -  (* dynamic part *)
   3.231 -  defs: thm list,
   3.232 -  operations: (string * (class * (typ * term))) list
   3.233 -
   3.234 -};
   3.235 -
   3.236 -fun rep_class_data (ClassData d) = d;
   3.237 -fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   3.238 -    (defs, operations)) =
   3.239 -  ClassData { consts = consts, base_sort = base_sort, inst = inst,
   3.240 -    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
   3.241 -    defs = defs, operations = operations };
   3.242 -fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
   3.243 -    of_class, axiom, defs, operations }) =
   3.244 -  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   3.245 -    (defs, operations)));
   3.246 -fun merge_class_data _ (ClassData { consts = consts,
   3.247 -    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
   3.248 -    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
   3.249 -  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
   3.250 -    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
   3.251 -  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   3.252 -    (Thm.merge_thms (defs1, defs2),
   3.253 -      AList.merge (op =) (K true) (operations1, operations2)));
   3.254 -
   3.255 -structure ClassData = TheoryDataFun
   3.256 -(
   3.257 -  type T = class_data Graph.T
   3.258 -  val empty = Graph.empty;
   3.259 -  val copy = I;
   3.260 -  val extend = I;
   3.261 -  fun merge _ = Graph.join merge_class_data;
   3.262 -);
   3.263 -
   3.264 -
   3.265 -(* queries *)
   3.266 -
   3.267 -val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
   3.268 -
   3.269 -fun the_class_data thy class = case lookup_class_data thy class
   3.270 - of NONE => error ("Undeclared class " ^ quote class)
   3.271 -  | SOME data => data;
   3.272 -
   3.273 -val is_class = is_some oo lookup_class_data;
   3.274 -
   3.275 -val ancestry = Graph.all_succs o ClassData.get;
   3.276 -
   3.277 -fun the_inst thy = #inst o the_class_data thy;
   3.278 -
   3.279 -fun these_params thy =
   3.280 -  let
   3.281 -    fun params class =
   3.282 -      let
   3.283 -        val const_typs = (#params o AxClass.get_info thy) class;
   3.284 -        val const_names = (#consts o the_class_data thy) class;
   3.285 -      in
   3.286 -        (map o apsnd)
   3.287 -          (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names
   3.288 -      end;
   3.289 -  in maps params o ancestry thy end;
   3.290 -
   3.291 -fun these_assm_intros thy =
   3.292 -  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   3.293 -    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   3.294 -
   3.295 -fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   3.296 -
   3.297 -fun these_operations thy =
   3.298 -  maps (#operations o the_class_data thy) o ancestry thy;
   3.299 -
   3.300 -fun morphism thy class =
   3.301 -  let
   3.302 -    val { inst, morphism, ... } = the_class_data thy class;
   3.303 -  in activate_class_morphism thy class inst morphism end;
   3.304 -
   3.305 -fun print_classes thy =
   3.306 -  let
   3.307 -    val ctxt = ProofContext.init thy;
   3.308 -    val algebra = Sign.classes_of thy;
   3.309 -    val arities =
   3.310 -      Symtab.empty
   3.311 -      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   3.312 -           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   3.313 -             ((#arities o Sorts.rep_algebra) algebra);
   3.314 -    val the_arities = these o Symtab.lookup arities;
   3.315 -    fun mk_arity class tyco =
   3.316 -      let
   3.317 -        val Ss = Sorts.mg_domain algebra tyco [class];
   3.318 -      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   3.319 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   3.320 -      ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   3.321 -    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   3.322 -      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   3.323 -      (SOME o Pretty.block) [Pretty.str "supersort: ",
   3.324 -        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   3.325 -      if is_class thy class then (SOME o Pretty.str)
   3.326 -        ("locale: " ^ Locale.extern thy class) else NONE,
   3.327 -      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   3.328 -          (Pretty.str "parameters:" :: ps)) o map mk_param
   3.329 -        o these o Option.map #params o try (AxClass.get_info thy)) class,
   3.330 -      (SOME o Pretty.block o Pretty.breaks) [
   3.331 -        Pretty.str "instances:",
   3.332 -        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   3.333 -      ]
   3.334 -    ]
   3.335 -  in
   3.336 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   3.337 -      o map mk_entry o Sorts.all_classes) algebra
   3.338 -  end;
   3.339 -
   3.340 -
   3.341 -(* updaters *)
   3.342 -
   3.343 -fun add_class_data ((class, superclasses),
   3.344 -    (params, base_sort, inst, phi, axiom, assm_intro, of_class)) thy =
   3.345 -  let
   3.346 -    val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   3.347 -      (c, (class, (ty, Free v_ty)))) params;
   3.348 -    val add_class = Graph.new_node (class,
   3.349 -        mk_class_data (((map o pairself) fst params, base_sort,
   3.350 -          inst, phi, assm_intro, of_class, axiom), ([], operations)))
   3.351 -      #> fold (curry Graph.add_edge class) superclasses;
   3.352 -  in ClassData.map add_class thy end;
   3.353 -
   3.354 -fun register_operation class (c, (t, some_def)) thy =
   3.355 -  let
   3.356 -    val base_sort = (#base_sort o the_class_data thy) class;
   3.357 -    val prep_typ = map_type_tvar
   3.358 -      (fn (vi as (v, _), sort) => if Name.aT = v
   3.359 -        then TFree (v, base_sort) else TVar (vi, sort));
   3.360 -    val t' = map_types prep_typ t;
   3.361 -    val ty' = Term.fastype_of t';
   3.362 -  in
   3.363 -    thy
   3.364 -    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   3.365 -      (fn (defs, operations) =>
   3.366 -        (fold cons (the_list some_def) defs,
   3.367 -          (c, (class, (ty', t'))) :: operations))
   3.368 -  end;
   3.369 -
   3.370 -
   3.371 -(** rule calculation, tactics and methods **)
   3.372 +(** rule calculation **)
   3.373  
   3.374  fun calculate_axiom thy sups base_sort assm_axiom param_map class =
   3.375    case Locale.intros thy class
   3.376 @@ -366,7 +35,7 @@
   3.377            (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
   3.378              (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
   3.379                Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
   3.380 -        val axiom_premises = map_filter (#axiom o the_class_data thy) sups
   3.381 +        val axiom_premises = map_filter (fst o rules thy) sups
   3.382            @ the_list assm_axiom;
   3.383        in intro
   3.384          |> instantiate thy [class]
   3.385 @@ -394,7 +63,7 @@
   3.386          (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
   3.387      val of_class_sups = if null sups
   3.388        then map (fixate o Thm.class_triv thy) base_sort
   3.389 -      else map (fixate o #of_class o the_class_data thy) sups;
   3.390 +      else map (fixate o snd o rules thy) sups;
   3.391      val locale_dests = map Drule.standard' (Locale.dests thy class);
   3.392      val num_trivs = case length locale_dests
   3.393       of 0 => if is_none axiom then 0 else 1
   3.394 @@ -411,23 +80,6 @@
   3.395        |> Thm.close_derivation;
   3.396    in (assm_intro, of_class) end;
   3.397  
   3.398 -fun prove_subclass (sub, sup) some_thm thy =
   3.399 -  let
   3.400 -    val of_class = (#of_class o the_class_data thy) sup;
   3.401 -    val intro = case some_thm
   3.402 -     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
   3.403 -      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
   3.404 -          ([], [sub])], []) of_class;
   3.405 -    val classrel = (intro OF (the_list o #axiom o the_class_data thy) sub)
   3.406 -      |> Thm.close_derivation;
   3.407 -  in
   3.408 -    thy
   3.409 -    |> AxClass.add_classrel classrel
   3.410 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
   3.411 -         I (sub, Locale.Locale sup)
   3.412 -    |> ClassData.map (Graph.add_edge (sub, sup))
   3.413 -  end;
   3.414 -
   3.415  fun note_assm_intro class assm_intro thy =
   3.416    thy
   3.417    |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
   3.418 @@ -435,147 +87,8 @@
   3.419    |> snd
   3.420    |> Sign.restore_naming thy;
   3.421  
   3.422 -fun intro_classes_tac facts st =
   3.423 -  let
   3.424 -    val thy = Thm.theory_of_thm st;
   3.425 -    val classes = Sign.all_classes thy;
   3.426 -    val class_trivs = map (Thm.class_triv thy) classes;
   3.427 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   3.428 -    val assm_intros = these_assm_intros thy;
   3.429 -  in
   3.430 -    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   3.431 -  end;
   3.432  
   3.433 -fun default_intro_tac ctxt [] =
   3.434 -      intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
   3.435 -      Locale.intro_locales_tac true ctxt []
   3.436 -  | default_intro_tac _ _ = no_tac;
   3.437 -
   3.438 -fun default_tac rules ctxt facts =
   3.439 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   3.440 -    default_intro_tac ctxt facts;
   3.441 -
   3.442 -val _ = Context.>> (Context.map_theory
   3.443 -  (Method.add_methods
   3.444 -   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   3.445 -      "back-chain introduction rules of classes"),
   3.446 -    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   3.447 -      "apply some intro/elim rule")]));
   3.448 -
   3.449 -
   3.450 -(** classes and class target **)
   3.451 -
   3.452 -(* class context syntax *)
   3.453 -
   3.454 -fun synchronize_class_syntax sups base_sort ctxt =
   3.455 -  let
   3.456 -    val thy = ProofContext.theory_of ctxt;
   3.457 -    val algebra = Sign.classes_of thy;
   3.458 -    val operations = these_operations thy sups;
   3.459 -    fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
   3.460 -    val primary_constraints =
   3.461 -      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   3.462 -    val secondary_constraints =
   3.463 -      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   3.464 -    fun declare_const (c, _) =
   3.465 -      let val b = Sign.base_name c
   3.466 -      in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   3.467 -    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
   3.468 -     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
   3.469 -         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   3.470 -             of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
   3.471 -                  if TypeInfer.is_param vi
   3.472 -                    andalso Sorts.sort_le algebra (base_sort, sort)
   3.473 -                      then SOME (ty', TFree (Name.aT, base_sort))
   3.474 -                      else NONE
   3.475 -              | _ => NONE)
   3.476 -          | NONE => NONE)
   3.477 -      | NONE => NONE)
   3.478 -    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
   3.479 -    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   3.480 -  in
   3.481 -    ctxt
   3.482 -    |> fold declare_const primary_constraints
   3.483 -    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   3.484 -        (((improve, subst), true), unchecks)), false))
   3.485 -    |> Overloading.set_primary_constraints
   3.486 -  end;
   3.487 -
   3.488 -fun refresh_syntax class ctxt =
   3.489 -  let
   3.490 -    val thy = ProofContext.theory_of ctxt;
   3.491 -    val base_sort = (#base_sort o the_class_data thy) class;
   3.492 -  in synchronize_class_syntax [class] base_sort ctxt end;
   3.493 -
   3.494 -fun init_ctxt sups base_sort ctxt =
   3.495 -  ctxt
   3.496 -  |> Variable.declare_term
   3.497 -      (Logic.mk_type (TFree (Name.aT, base_sort)))
   3.498 -  |> synchronize_class_syntax sups base_sort
   3.499 -  |> Overloading.add_improvable_syntax;
   3.500 -
   3.501 -fun init class thy =
   3.502 -  thy
   3.503 -  |> Locale.init class
   3.504 -  |> init_ctxt [class] ((#base_sort o the_class_data thy) class);
   3.505 -
   3.506 -
   3.507 -(* class target *)
   3.508 -
   3.509 -fun declare class pos ((c, mx), dict) thy =
   3.510 -  let
   3.511 -    val prfx = class_prefix class;
   3.512 -    val thy' = thy |> Sign.add_path prfx;
   3.513 -    val phi = morphism thy' class;
   3.514 -    val inst = the_inst thy' class;
   3.515 -    val params = map (apsnd fst o snd) (these_params thy' [class]);
   3.516 -
   3.517 -    val c' = Sign.full_bname thy' c;
   3.518 -    val dict' = Morphism.term phi dict;
   3.519 -    val dict_def = map_types Logic.unvarifyT dict';
   3.520 -    val ty' = Term.fastype_of dict_def;
   3.521 -    val ty'' = Type.strip_sorts ty';
   3.522 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   3.523 -    fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   3.524 -  in
   3.525 -    thy'
   3.526 -    |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
   3.527 -    |> Thm.add_def false false (c, def_eq)
   3.528 -    |>> Thm.symmetric
   3.529 -    ||>> get_axiom
   3.530 -    |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
   3.531 -      #> snd
   3.532 -        (*assumption: interpretation cookie does not change
   3.533 -          by adding equations to interpretation*)
   3.534 -      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   3.535 -      #> PureThy.store_thm (c ^ "_raw", def')
   3.536 -      #> snd)
   3.537 -    |> Sign.restore_naming thy
   3.538 -    |> Sign.add_const_constraint (c', SOME ty')
   3.539 -  end;
   3.540 -
   3.541 -fun abbrev class prmode pos ((c, mx), rhs) thy =
   3.542 -  let
   3.543 -    val prfx = class_prefix class;
   3.544 -    val thy' = thy |> Sign.add_path prfx;
   3.545 -
   3.546 -    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   3.547 -      (these_operations thy [class]);
   3.548 -    val c' = Sign.full_bname thy' c;
   3.549 -    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   3.550 -    val rhs'' = map_types Logic.varifyT rhs';
   3.551 -    val ty' = Term.fastype_of rhs';
   3.552 -  in
   3.553 -    thy'
   3.554 -    |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd
   3.555 -    |> Sign.add_const_constraint (c', SOME ty')
   3.556 -    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   3.557 -    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   3.558 -    |> Sign.restore_naming thy
   3.559 -  end;
   3.560 -
   3.561 -
   3.562 -(* class definition *)
   3.563 +(** define classes **)
   3.564  
   3.565  local
   3.566  
   3.567 @@ -591,7 +104,7 @@
   3.568        else ();
   3.569      val base_sort = if null sups then supsort else
   3.570        foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   3.571 -        (map (#base_sort o the_class_data thy) sups);
   3.572 +        (map (base_sort thy) sups);
   3.573      val suplocales = map Locale.Locale sups;
   3.574      val supexpr = Locale.Merge suplocales;
   3.575      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   3.576 @@ -610,7 +123,7 @@
   3.577        ProofContext.init thy
   3.578        |> Locale.cert_expr supexpr [constrain]
   3.579        |> snd
   3.580 -      |> init_ctxt sups base_sort
   3.581 +      |> begin sups base_sort
   3.582        |> process_expr Locale.empty raw_elems
   3.583        |> fst
   3.584        |> fork_syntax
   3.585 @@ -692,8 +205,8 @@
   3.586      #-> (fn phi =>
   3.587          `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
   3.588      #-> (fn (assm_intro, of_class) =>
   3.589 -        add_class_data ((class, sups), (params, base_sort, inst,
   3.590 -          morphism, axiom, assm_intro, of_class))
   3.591 +        register class sups params base_sort inst
   3.592 +          morphism axiom assm_intro of_class
   3.593      #> fold (note_assm_intro class) (the_list assm_intro))))))
   3.594      |> init class
   3.595      |> pair class
   3.596 @@ -707,196 +220,58 @@
   3.597  end; (*local*)
   3.598  
   3.599  
   3.600 -
   3.601 -(** instantiation target **)
   3.602 -
   3.603 -(* bookkeeping *)
   3.604 -
   3.605 -datatype instantiation = Instantiation of {
   3.606 -  arities: string list * (string * sort) list * sort,
   3.607 -  params: ((string * string) * (string * typ)) list
   3.608 -    (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
   3.609 -}
   3.610 -
   3.611 -structure Instantiation = ProofDataFun
   3.612 -(
   3.613 -  type T = instantiation
   3.614 -  fun init _ = Instantiation { arities = ([], [], []), params = [] };
   3.615 -);
   3.616 +(** subclass relations **)
   3.617  
   3.618 -fun mk_instantiation (arities, params) =
   3.619 -  Instantiation { arities = arities, params = params };
   3.620 -fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
   3.621 - of Instantiation data => data;
   3.622 -fun map_instantiation f = (LocalTheory.target o Instantiation.map)
   3.623 -  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   3.624 -
   3.625 -fun the_instantiation lthy = case get_instantiation lthy
   3.626 - of { arities = ([], [], []), ... } => error "No instantiation target"
   3.627 -  | data => data;
   3.628 -
   3.629 -val instantiation_params = #params o get_instantiation;
   3.630 -
   3.631 -fun instantiation_param lthy v = instantiation_params lthy
   3.632 -  |> find_first (fn (_, (v', _)) => v = v')
   3.633 -  |> Option.map (fst o fst);
   3.634 -
   3.635 +local
   3.636  
   3.637 -(* syntax *)
   3.638 -
   3.639 -fun synchronize_inst_syntax ctxt =
   3.640 +fun gen_subclass prep_class do_proof raw_sup lthy =
   3.641    let
   3.642 -    val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
   3.643 -    val thy = ProofContext.theory_of ctxt;
   3.644 -    fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   3.645 -         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   3.646 -             of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   3.647 -              | NONE => NONE)
   3.648 -          | NONE => NONE;
   3.649 -    val unchecks =
   3.650 -      map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   3.651 +    val thy = ProofContext.theory_of lthy;
   3.652 +    val sup = prep_class thy raw_sup;
   3.653 +    val sub = case TheoryTarget.peek lthy
   3.654 +     of {is_class = false, ...} => error "Not a class context"
   3.655 +      | {target, ...} => target;
   3.656 +    val _ = if Sign.subsort thy ([sup], [sub])
   3.657 +      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
   3.658 +        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
   3.659 +      else ();
   3.660 +    val sub_params = map fst (these_params thy [sub]);
   3.661 +    val sup_params = map fst (these_params thy [sup]);
   3.662 +    val err_params = subtract (op =) sub_params sup_params;
   3.663 +    val _ = if null err_params then [] else
   3.664 +      error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
   3.665 +        commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
   3.666 +    val sublocale_prop =
   3.667 +      Locale.global_asms_of thy sup
   3.668 +      |> maps snd
   3.669 +      |> try the_single
   3.670 +      |> Option.map (ObjectLogic.ensure_propT thy);
   3.671 +    fun after_qed some_thm =
   3.672 +      LocalTheory.theory (prove_subclass_relation (sub, sup) some_thm)
   3.673 +      #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
   3.674    in
   3.675 -    ctxt
   3.676 -    |> Overloading.map_improvable_syntax
   3.677 -         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
   3.678 -            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   3.679 -  end;
   3.680 -
   3.681 -
   3.682 -(* target *)
   3.683 -
   3.684 -val sanatize_name = (*FIXME*)
   3.685 -  let
   3.686 -    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   3.687 -      orelse s = "'" orelse s = "_";
   3.688 -    val is_junk = not o is_valid andf Symbol.is_regular;
   3.689 -    val junk = Scan.many is_junk;
   3.690 -    val scan_valids = Symbol.scanner "Malformed input"
   3.691 -      ((junk |--
   3.692 -        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   3.693 -        --| junk))
   3.694 -      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   3.695 -  in
   3.696 -    explode #> scan_valids #> implode
   3.697 +    do_proof after_qed sublocale_prop lthy
   3.698    end;
   3.699  
   3.700 -fun type_name "*" = "prod"
   3.701 -  | type_name "+" = "sum"
   3.702 -  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   3.703 -
   3.704 -fun resort_terms pp algebra consts constraints ts =
   3.705 -  let
   3.706 -    fun matchings (Const (c_ty as (c, _))) = (case constraints c
   3.707 -         of NONE => I
   3.708 -          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
   3.709 -              (Consts.typargs consts c_ty) sorts)
   3.710 -      | matchings _ = I
   3.711 -    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
   3.712 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
   3.713 -    val inst = map_type_tvar
   3.714 -      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   3.715 -  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
   3.716 -
   3.717 -fun init_instantiation (tycos, vs, sort) thy =
   3.718 -  let
   3.719 -    val _ = if null tycos then error "At least one arity must be given" else ();
   3.720 -    val params = these_params thy sort;
   3.721 -    fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco)
   3.722 -      then NONE else SOME ((c, tyco),
   3.723 -        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   3.724 -    val inst_params = map_product get_param tycos params |> map_filter I;
   3.725 -    val primary_constraints = map (apsnd
   3.726 -      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
   3.727 -    val pp = Syntax.pp_global thy;
   3.728 -    val algebra = Sign.classes_of thy
   3.729 -      |> fold (fn tyco => Sorts.add_arities pp
   3.730 -            (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   3.731 -    val consts = Sign.consts_of thy;
   3.732 -    val improve_constraints = AList.lookup (op =)
   3.733 -      (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
   3.734 -    fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
   3.735 -     of NONE => NONE
   3.736 -      | SOME ts' => SOME (ts', ctxt);
   3.737 -    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   3.738 -     of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   3.739 -         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
   3.740 -          | NONE => NONE)
   3.741 -      | NONE => NONE;
   3.742 -  in
   3.743 -    thy
   3.744 -    |> ProofContext.init
   3.745 -    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
   3.746 -    |> fold (Variable.declare_typ o TFree) vs
   3.747 -    |> fold (Variable.declare_names o Free o snd) inst_params
   3.748 -    |> (Overloading.map_improvable_syntax o apfst)
   3.749 -         (fn ((_, _), ((_, subst), unchecks)) =>
   3.750 -            ((primary_constraints, []), (((improve, K NONE), false), [])))
   3.751 -    |> Overloading.add_improvable_syntax
   3.752 -    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   3.753 -    |> synchronize_inst_syntax
   3.754 -  end;
   3.755 +fun user_proof after_qed NONE =
   3.756 +      Proof.theorem_i NONE (K (after_qed NONE)) [[]]
   3.757 +  | user_proof after_qed (SOME prop) =
   3.758 +      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
   3.759  
   3.760 -fun confirm_declaration c = (map_instantiation o apsnd)
   3.761 -  (filter_out (fn (_, (c', _)) => c' = c))
   3.762 -  #> LocalTheory.target synchronize_inst_syntax
   3.763 -
   3.764 -fun gen_instantiation_instance do_proof after_qed lthy =
   3.765 -  let
   3.766 -    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   3.767 -    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   3.768 -    fun after_qed' results =
   3.769 -      LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   3.770 -      #> after_qed;
   3.771 -  in
   3.772 -    lthy
   3.773 -    |> do_proof after_qed' arities_proof
   3.774 -  end;
   3.775 -
   3.776 -val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   3.777 -  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   3.778 -
   3.779 -fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   3.780 -  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   3.781 -    (fn {context, ...} => tac context)) ts) lthy) I;
   3.782 -
   3.783 -fun prove_instantiation_exit tac = prove_instantiation_instance tac
   3.784 -  #> LocalTheory.exit_global;
   3.785 +fun tactic_proof tac after_qed NONE lthy =
   3.786 +      after_qed NONE lthy
   3.787 +  | tactic_proof tac after_qed (SOME prop) lthy =
   3.788 +      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
   3.789 +        (K tac))) lthy;
   3.790  
   3.791 -fun prove_instantiation_exit_result f tac x lthy =
   3.792 -  let
   3.793 -    val phi = ProofContext.export_morphism lthy
   3.794 -      (ProofContext.init (ProofContext.theory_of lthy));
   3.795 -    val y = f phi x;
   3.796 -  in
   3.797 -    lthy
   3.798 -    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
   3.799 -    |> pair y
   3.800 -  end;
   3.801 +in
   3.802  
   3.803 -fun conclude_instantiation lthy =
   3.804 -  let
   3.805 -    val { arities, params } = the_instantiation lthy;
   3.806 -    val (tycos, vs, sort) = arities;
   3.807 -    val thy = ProofContext.theory_of lthy;
   3.808 -    val _ = map (fn tyco => if Sign.of_sort thy
   3.809 -        (Type (tyco, map TFree vs), sort)
   3.810 -      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   3.811 -        tycos;
   3.812 -  in lthy end;
   3.813 +val subclass = gen_subclass (K I) user_proof;
   3.814 +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
   3.815 +val subclass_cmd = gen_subclass Sign.read_class user_proof;
   3.816  
   3.817 -fun pretty_instantiation lthy =
   3.818 -  let
   3.819 -    val { arities, params } = the_instantiation lthy;
   3.820 -    val (tycos, vs, sort) = arities;
   3.821 -    val thy = ProofContext.theory_of lthy;
   3.822 -    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   3.823 -    fun pr_param ((c, _), (v, ty)) =
   3.824 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   3.825 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   3.826 -  in
   3.827 -    (Pretty.block o Pretty.fbreaks)
   3.828 -      (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   3.829 -  end;
   3.830 +end; (*local*)
   3.831 +
   3.832  
   3.833  end;
   3.834  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Isar/class_target.ML	Mon Jan 05 15:36:24 2009 +0100
     4.3 @@ -0,0 +1,723 @@
     4.4 +(*  Title:      Pure/Isar/class_target.ML
     4.5 +    Author:     Florian Haftmann, TU Muenchen
     4.6 +
     4.7 +Type classes derived from primitive axclasses and locales - mechanisms.
     4.8 +*)
     4.9 +
    4.10 +signature CLASS_TARGET =
    4.11 +sig
    4.12 +  (*classes*)
    4.13 +  type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
    4.14 +  val register: class -> class list -> ((string * typ) * (string * typ)) list
    4.15 +    -> sort -> term list -> raw_morphism
    4.16 +    -> thm option -> thm option -> thm -> theory -> theory
    4.17 +
    4.18 +  val begin: class list -> sort -> Proof.context -> Proof.context
    4.19 +  val init: class -> theory -> Proof.context
    4.20 +  val declare: class -> Properties.T
    4.21 +    -> (string * mixfix) * term -> theory -> theory
    4.22 +  val abbrev: class -> Syntax.mode -> Properties.T
    4.23 +    -> (string * mixfix) * term -> theory -> theory
    4.24 +  val refresh_syntax: class -> Proof.context -> Proof.context
    4.25 +
    4.26 +  val intro_classes_tac: thm list -> tactic
    4.27 +  val default_intro_tac: Proof.context -> thm list -> tactic
    4.28 +  val activate_class_morphism: theory -> class -> term list
    4.29 +    -> raw_morphism -> morphism
    4.30 +  val prove_class_interpretation: class -> term list -> (class * string) list
    4.31 +    -> thm list -> thm list -> theory -> raw_morphism * theory
    4.32 +  val prove_subclass_relation: class * class -> thm option -> theory -> theory
    4.33 +
    4.34 +  val class_prefix: string -> string
    4.35 +  val is_class: theory -> class -> bool
    4.36 +  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    4.37 +  val these_defs: theory -> sort -> thm list
    4.38 +  val base_sort: theory -> class -> sort
    4.39 +  val rules: theory -> class -> thm option * thm
    4.40 +  val print_classes: theory -> unit
    4.41 +
    4.42 +  (*instances*)
    4.43 +  val init_instantiation: string list * (string * sort) list * sort
    4.44 +    -> theory -> local_theory
    4.45 +  val instantiation_instance: (local_theory -> local_theory)
    4.46 +    -> local_theory -> Proof.state
    4.47 +  val prove_instantiation_instance: (Proof.context -> tactic)
    4.48 +    -> local_theory -> local_theory
    4.49 +  val prove_instantiation_exit: (Proof.context -> tactic)
    4.50 +    -> local_theory -> theory
    4.51 +  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    4.52 +    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    4.53 +  val conclude_instantiation: local_theory -> local_theory
    4.54 +  val instantiation_param: local_theory -> string -> string option
    4.55 +  val confirm_declaration: string -> local_theory -> local_theory
    4.56 +  val pretty_instantiation: local_theory -> Pretty.T
    4.57 +  val type_name: string -> string
    4.58 +
    4.59 +  (*old axclass layer*)
    4.60 +  val axclass_cmd: bstring * xstring list
    4.61 +    -> (Attrib.binding * string list) list
    4.62 +    -> theory -> class * theory
    4.63 +  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    4.64 +
    4.65 +  (*old instance layer*)
    4.66 +  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    4.67 +  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    4.68 +end;
    4.69 +
    4.70 +structure Class_Target : CLASS_TARGET =
    4.71 +struct
    4.72 +
    4.73 +(*temporary adaption code to mediate between old and new locale code*)
    4.74 +
    4.75 +structure Old_Locale =
    4.76 +struct
    4.77 +
    4.78 +val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
    4.79 +
    4.80 +val interpretation = Locale.interpretation;
    4.81 +val interpretation_in_locale = Locale.interpretation_in_locale;
    4.82 +val get_interpret_morph = Locale.get_interpret_morph;
    4.83 +val Locale = Locale.Locale;
    4.84 +val extern = Locale.extern;
    4.85 +val intros = Locale.intros;
    4.86 +val dests = Locale.dests;
    4.87 +val init = Locale.init;
    4.88 +val Merge = Locale.Merge;
    4.89 +val parameters_of_expr = Locale.parameters_of_expr;
    4.90 +val empty = Locale.empty;
    4.91 +val cert_expr = Locale.cert_expr;
    4.92 +val read_expr = Locale.read_expr;
    4.93 +val parameters_of = Locale.parameters_of;
    4.94 +val add_locale = Locale.add_locale;
    4.95 +
    4.96 +end;
    4.97 +
    4.98 +(*structure New_Locale =
    4.99 +struct
   4.100 +
   4.101 +val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
   4.102 +
   4.103 +val interpretation = Locale.interpretation; (*!*)
   4.104 +val interpretation_in_locale = Locale.interpretation_in_locale; (*!*)
   4.105 +val get_interpret_morph = Locale.get_interpret_morph; (*!*)
   4.106 +fun Locale loc = ([(loc, ("", Expression.Positional []))], []);
   4.107 +val extern = NewLocale.extern;
   4.108 +val intros = Locale.intros; (*!*)
   4.109 +val dests = Locale.dests; (*!*)
   4.110 +val init = NewLocale.init;
   4.111 +fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []);
   4.112 +val parameters_of_expr = Locale.parameters_of_expr; (*!*)
   4.113 +val empty = ([], []);
   4.114 +val cert_expr = Locale.cert_expr; (*!"*)
   4.115 +val read_expr = Locale.read_expr; (*!"*)
   4.116 +val parameters_of = NewLocale.params_of; (*why typ option?*)
   4.117 +val add_locale = Expression.add_locale;
   4.118 +
   4.119 +end;*)
   4.120 +
   4.121 +structure Locale = Old_Locale;
   4.122 +
   4.123 +(*proper code again*)
   4.124 +
   4.125 +
   4.126 +(** auxiliary **)
   4.127 +
   4.128 +fun prove_interpretation tac prfx_atts expr inst =
   4.129 +  Locale.interpretation I prfx_atts expr inst
   4.130 +  ##> Proof.global_terminal_proof
   4.131 +      (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   4.132 +  ##> ProofContext.theory_of;
   4.133 +
   4.134 +fun prove_interpretation_in tac after_qed (name, expr) =
   4.135 +  Locale.interpretation_in_locale
   4.136 +      (ProofContext.theory after_qed) (name, expr)
   4.137 +  #> Proof.global_terminal_proof
   4.138 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   4.139 +  #> ProofContext.theory_of;
   4.140 +
   4.141 +val class_prefix = Logic.const_of_class o Sign.base_name;
   4.142 +
   4.143 +fun class_name_morphism class =
   4.144 +  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
   4.145 +
   4.146 +type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
   4.147 +
   4.148 +fun activate_class_morphism thy class inst morphism =
   4.149 +  Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
   4.150 +
   4.151 +
   4.152 +(** primitive axclass and instance commands **)
   4.153 +
   4.154 +fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   4.155 +  let
   4.156 +    val ctxt = ProofContext.init thy;
   4.157 +    val superclasses = map (Sign.read_class thy) raw_superclasses;
   4.158 +    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   4.159 +      raw_specs;
   4.160 +    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   4.161 +          raw_specs)
   4.162 +      |> snd
   4.163 +      |> (map o map) fst;
   4.164 +  in
   4.165 +    AxClass.define_class (class, superclasses) []
   4.166 +      (name_atts ~~ axiomss) thy
   4.167 +  end;
   4.168 +
   4.169 +local
   4.170 +
   4.171 +fun gen_instance mk_prop add_thm after_qed insts thy =
   4.172 +  let
   4.173 +    fun after_qed' results =
   4.174 +      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
   4.175 +  in
   4.176 +    thy
   4.177 +    |> ProofContext.init
   4.178 +    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
   4.179 +        o mk_prop thy) insts)
   4.180 +  end;
   4.181 +
   4.182 +in
   4.183 +
   4.184 +val instance_arity =
   4.185 +  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   4.186 +val instance_arity_cmd =
   4.187 +  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
   4.188 +val classrel =
   4.189 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
   4.190 +val classrel_cmd =
   4.191 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
   4.192 +
   4.193 +end; (*local*)
   4.194 +
   4.195 +
   4.196 +(** class data **)
   4.197 +
   4.198 +datatype class_data = ClassData of {
   4.199 +
   4.200 +  (* static part *)
   4.201 +  consts: (string * string) list
   4.202 +    (*locale parameter ~> constant name*),
   4.203 +  base_sort: sort,
   4.204 +  inst: term list
   4.205 +    (*canonical interpretation*),
   4.206 +  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
   4.207 +    (*morphism cookie of canonical interpretation*),
   4.208 +  assm_intro: thm option,
   4.209 +  of_class: thm,
   4.210 +  axiom: thm option,
   4.211 +  
   4.212 +  (* dynamic part *)
   4.213 +  defs: thm list,
   4.214 +  operations: (string * (class * (typ * term))) list
   4.215 +
   4.216 +};
   4.217 +
   4.218 +fun rep_class_data (ClassData d) = d;
   4.219 +fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   4.220 +    (defs, operations)) =
   4.221 +  ClassData { consts = consts, base_sort = base_sort, inst = inst,
   4.222 +    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
   4.223 +    defs = defs, operations = operations };
   4.224 +fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
   4.225 +    of_class, axiom, defs, operations }) =
   4.226 +  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   4.227 +    (defs, operations)));
   4.228 +fun merge_class_data _ (ClassData { consts = consts,
   4.229 +    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
   4.230 +    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
   4.231 +  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
   4.232 +    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
   4.233 +  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
   4.234 +    (Thm.merge_thms (defs1, defs2),
   4.235 +      AList.merge (op =) (K true) (operations1, operations2)));
   4.236 +
   4.237 +structure ClassData = TheoryDataFun
   4.238 +(
   4.239 +  type T = class_data Graph.T
   4.240 +  val empty = Graph.empty;
   4.241 +  val copy = I;
   4.242 +  val extend = I;
   4.243 +  fun merge _ = Graph.join merge_class_data;
   4.244 +);
   4.245 +
   4.246 +
   4.247 +(* queries *)
   4.248 +
   4.249 +val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
   4.250 +
   4.251 +fun the_class_data thy class = case lookup_class_data thy class
   4.252 + of NONE => error ("Undeclared class " ^ quote class)
   4.253 +  | SOME data => data;
   4.254 +
   4.255 +val is_class = is_some oo lookup_class_data;
   4.256 +
   4.257 +val ancestry = Graph.all_succs o ClassData.get;
   4.258 +
   4.259 +fun the_inst thy = #inst o the_class_data thy;
   4.260 +
   4.261 +fun these_params thy =
   4.262 +  let
   4.263 +    fun params class =
   4.264 +      let
   4.265 +        val const_typs = (#params o AxClass.get_info thy) class;
   4.266 +        val const_names = (#consts o the_class_data thy) class;
   4.267 +      in
   4.268 +        (map o apsnd)
   4.269 +          (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names
   4.270 +      end;
   4.271 +  in maps params o ancestry thy end;
   4.272 +
   4.273 +fun these_assm_intros thy =
   4.274 +  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   4.275 +    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   4.276 +
   4.277 +fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   4.278 +
   4.279 +fun these_operations thy =
   4.280 +  maps (#operations o the_class_data thy) o ancestry thy;
   4.281 +
   4.282 +val base_sort = #base_sort oo the_class_data;
   4.283 +
   4.284 +fun rules thy class = let
   4.285 +    val { axiom, of_class, ... } = the_class_data thy class
   4.286 +  in (axiom, of_class) end;
   4.287 +
   4.288 +fun morphism thy class =
   4.289 +  let
   4.290 +    val { inst, morphism, ... } = the_class_data thy class;
   4.291 +  in activate_class_morphism thy class inst morphism end;
   4.292 +
   4.293 +fun print_classes thy =
   4.294 +  let
   4.295 +    val ctxt = ProofContext.init thy;
   4.296 +    val algebra = Sign.classes_of thy;
   4.297 +    val arities =
   4.298 +      Symtab.empty
   4.299 +      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   4.300 +           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   4.301 +             ((#arities o Sorts.rep_algebra) algebra);
   4.302 +    val the_arities = these o Symtab.lookup arities;
   4.303 +    fun mk_arity class tyco =
   4.304 +      let
   4.305 +        val Ss = Sorts.mg_domain algebra tyco [class];
   4.306 +      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   4.307 +    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   4.308 +      ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   4.309 +    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   4.310 +      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   4.311 +      (SOME o Pretty.block) [Pretty.str "supersort: ",
   4.312 +        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   4.313 +      if is_class thy class then (SOME o Pretty.str)
   4.314 +        ("locale: " ^ Locale.extern thy class) else NONE,
   4.315 +      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   4.316 +          (Pretty.str "parameters:" :: ps)) o map mk_param
   4.317 +        o these o Option.map #params o try (AxClass.get_info thy)) class,
   4.318 +      (SOME o Pretty.block o Pretty.breaks) [
   4.319 +        Pretty.str "instances:",
   4.320 +        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   4.321 +      ]
   4.322 +    ]
   4.323 +  in
   4.324 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   4.325 +      o map mk_entry o Sorts.all_classes) algebra
   4.326 +  end;
   4.327 +
   4.328 +
   4.329 +(* updaters *)
   4.330 +
   4.331 +fun register class superclasses params base_sort inst phi
   4.332 +    axiom assm_intro of_class thy =
   4.333 +  let
   4.334 +    val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   4.335 +      (c, (class, (ty, Free v_ty)))) params;
   4.336 +    val add_class = Graph.new_node (class,
   4.337 +        mk_class_data (((map o pairself) fst params, base_sort,
   4.338 +          inst, phi, assm_intro, of_class, axiom), ([], operations)))
   4.339 +      #> fold (curry Graph.add_edge class) superclasses;
   4.340 +  in ClassData.map add_class thy end;
   4.341 +
   4.342 +fun register_operation class (c, (t, some_def)) thy =
   4.343 +  let
   4.344 +    val base_sort = base_sort thy class;
   4.345 +    val prep_typ = map_type_tvar
   4.346 +      (fn (vi as (v, _), sort) => if Name.aT = v
   4.347 +        then TFree (v, base_sort) else TVar (vi, sort));
   4.348 +    val t' = map_types prep_typ t;
   4.349 +    val ty' = Term.fastype_of t';
   4.350 +  in
   4.351 +    thy
   4.352 +    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   4.353 +      (fn (defs, operations) =>
   4.354 +        (fold cons (the_list some_def) defs,
   4.355 +          (c, (class, (ty', t'))) :: operations))
   4.356 +  end;
   4.357 +
   4.358 +
   4.359 +(** tactics and methods **)
   4.360 +
   4.361 +fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
   4.362 +  let
   4.363 +    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
   4.364 +      [class]))) (Sign.the_const_type thy c)) consts;
   4.365 +    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
   4.366 +    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
   4.367 +    fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
   4.368 +      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
   4.369 +    val prfx = class_prefix class;
   4.370 +  in
   4.371 +    thy
   4.372 +    |> fold2 add_constraint (map snd consts) no_constraints
   4.373 +    |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
   4.374 +          (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
   4.375 +    ||> fold2 add_constraint (map snd consts) constraints
   4.376 +  end;
   4.377 +
   4.378 +fun prove_subclass_relation (sub, sup) some_thm thy =
   4.379 +  let
   4.380 +    val of_class = (snd o rules thy) sup;
   4.381 +    val intro = case some_thm
   4.382 +     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
   4.383 +      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
   4.384 +          ([], [sub])], []) of_class;
   4.385 +    val classrel = (intro OF (the_list o fst o rules thy) sub)
   4.386 +      |> Thm.close_derivation;
   4.387 +  in
   4.388 +    thy
   4.389 +    |> AxClass.add_classrel classrel
   4.390 +    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
   4.391 +         I (sub, Locale.Locale sup)
   4.392 +    |> ClassData.map (Graph.add_edge (sub, sup))
   4.393 +  end;
   4.394 +
   4.395 +fun intro_classes_tac facts st =
   4.396 +  let
   4.397 +    val thy = Thm.theory_of_thm st;
   4.398 +    val classes = Sign.all_classes thy;
   4.399 +    val class_trivs = map (Thm.class_triv thy) classes;
   4.400 +    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   4.401 +    val assm_intros = these_assm_intros thy;
   4.402 +  in
   4.403 +    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   4.404 +  end;
   4.405 +
   4.406 +fun default_intro_tac ctxt [] =
   4.407 +      intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
   4.408 +      Locale.intro_locales_tac true ctxt []
   4.409 +  | default_intro_tac _ _ = no_tac;
   4.410 +
   4.411 +fun default_tac rules ctxt facts =
   4.412 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   4.413 +    default_intro_tac ctxt facts;
   4.414 +
   4.415 +val _ = Context.>> (Context.map_theory
   4.416 +  (Method.add_methods
   4.417 +   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   4.418 +      "back-chain introduction rules of classes"),
   4.419 +    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   4.420 +      "apply some intro/elim rule")]));
   4.421 +
   4.422 +
   4.423 +(** classes and class target **)
   4.424 +
   4.425 +(* class context syntax *)
   4.426 +
   4.427 +fun synchronize_class_syntax sups base_sort ctxt =
   4.428 +  let
   4.429 +    val thy = ProofContext.theory_of ctxt;
   4.430 +    val algebra = Sign.classes_of thy;
   4.431 +    val operations = these_operations thy sups;
   4.432 +    fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
   4.433 +    val primary_constraints =
   4.434 +      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   4.435 +    val secondary_constraints =
   4.436 +      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   4.437 +    fun declare_const (c, _) =
   4.438 +      let val b = Sign.base_name c
   4.439 +      in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   4.440 +    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
   4.441 +     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
   4.442 +         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   4.443 +             of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
   4.444 +                  if TypeInfer.is_param vi
   4.445 +                    andalso Sorts.sort_le algebra (base_sort, sort)
   4.446 +                      then SOME (ty', TFree (Name.aT, base_sort))
   4.447 +                      else NONE
   4.448 +              | _ => NONE)
   4.449 +          | NONE => NONE)
   4.450 +      | NONE => NONE)
   4.451 +    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
   4.452 +    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   4.453 +  in
   4.454 +    ctxt
   4.455 +    |> fold declare_const primary_constraints
   4.456 +    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   4.457 +        (((improve, subst), true), unchecks)), false))
   4.458 +    |> Overloading.set_primary_constraints
   4.459 +  end;
   4.460 +
   4.461 +fun refresh_syntax class ctxt =
   4.462 +  let
   4.463 +    val thy = ProofContext.theory_of ctxt;
   4.464 +    val base_sort = base_sort thy class;
   4.465 +  in synchronize_class_syntax [class] base_sort ctxt end;
   4.466 +
   4.467 +fun begin sups base_sort ctxt =
   4.468 +  ctxt
   4.469 +  |> Variable.declare_term
   4.470 +      (Logic.mk_type (TFree (Name.aT, base_sort)))
   4.471 +  |> synchronize_class_syntax sups base_sort
   4.472 +  |> Overloading.add_improvable_syntax;
   4.473 +
   4.474 +fun init class thy =
   4.475 +  thy
   4.476 +  |> Locale.init class
   4.477 +  |> begin [class] (base_sort thy class);
   4.478 +
   4.479 +
   4.480 +(* class target *)
   4.481 +
   4.482 +fun declare class pos ((c, mx), dict) thy =
   4.483 +  let
   4.484 +    val prfx = class_prefix class;
   4.485 +    val thy' = thy |> Sign.add_path prfx;
   4.486 +    val phi = morphism thy' class;
   4.487 +    val inst = the_inst thy' class;
   4.488 +    val params = map (apsnd fst o snd) (these_params thy' [class]);
   4.489 +
   4.490 +    val c' = Sign.full_bname thy' c;
   4.491 +    val dict' = Morphism.term phi dict;
   4.492 +    val dict_def = map_types Logic.unvarifyT dict';
   4.493 +    val ty' = Term.fastype_of dict_def;
   4.494 +    val ty'' = Type.strip_sorts ty';
   4.495 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   4.496 +    fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   4.497 +  in
   4.498 +    thy'
   4.499 +    |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
   4.500 +    |> Thm.add_def false false (c, def_eq)
   4.501 +    |>> Thm.symmetric
   4.502 +    ||>> get_axiom
   4.503 +    |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
   4.504 +      #> snd
   4.505 +        (*assumption: interpretation cookie does not change
   4.506 +          by adding equations to interpretation*)
   4.507 +      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   4.508 +      #> PureThy.store_thm (c ^ "_raw", def')
   4.509 +      #> snd)
   4.510 +    |> Sign.restore_naming thy
   4.511 +    |> Sign.add_const_constraint (c', SOME ty')
   4.512 +  end;
   4.513 +
   4.514 +fun abbrev class prmode pos ((c, mx), rhs) thy =
   4.515 +  let
   4.516 +    val prfx = class_prefix class;
   4.517 +    val thy' = thy |> Sign.add_path prfx;
   4.518 +
   4.519 +    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   4.520 +      (these_operations thy [class]);
   4.521 +    val c' = Sign.full_bname thy' c;
   4.522 +    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   4.523 +    val rhs'' = map_types Logic.varifyT rhs';
   4.524 +    val ty' = Term.fastype_of rhs';
   4.525 +  in
   4.526 +    thy'
   4.527 +    |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd
   4.528 +    |> Sign.add_const_constraint (c', SOME ty')
   4.529 +    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   4.530 +    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   4.531 +    |> Sign.restore_naming thy
   4.532 +  end;
   4.533 +
   4.534 +
   4.535 +(** instantiation target **)
   4.536 +
   4.537 +(* bookkeeping *)
   4.538 +
   4.539 +datatype instantiation = Instantiation of {
   4.540 +  arities: string list * (string * sort) list * sort,
   4.541 +  params: ((string * string) * (string * typ)) list
   4.542 +    (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
   4.543 +}
   4.544 +
   4.545 +structure Instantiation = ProofDataFun
   4.546 +(
   4.547 +  type T = instantiation
   4.548 +  fun init _ = Instantiation { arities = ([], [], []), params = [] };
   4.549 +);
   4.550 +
   4.551 +fun mk_instantiation (arities, params) =
   4.552 +  Instantiation { arities = arities, params = params };
   4.553 +fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
   4.554 + of Instantiation data => data;
   4.555 +fun map_instantiation f = (LocalTheory.target o Instantiation.map)
   4.556 +  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   4.557 +
   4.558 +fun the_instantiation lthy = case get_instantiation lthy
   4.559 + of { arities = ([], [], []), ... } => error "No instantiation target"
   4.560 +  | data => data;
   4.561 +
   4.562 +val instantiation_params = #params o get_instantiation;
   4.563 +
   4.564 +fun instantiation_param lthy v = instantiation_params lthy
   4.565 +  |> find_first (fn (_, (v', _)) => v = v')
   4.566 +  |> Option.map (fst o fst);
   4.567 +
   4.568 +
   4.569 +(* syntax *)
   4.570 +
   4.571 +fun synchronize_inst_syntax ctxt =
   4.572 +  let
   4.573 +    val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
   4.574 +    val thy = ProofContext.theory_of ctxt;
   4.575 +    fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   4.576 +         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   4.577 +             of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   4.578 +              | NONE => NONE)
   4.579 +          | NONE => NONE;
   4.580 +    val unchecks =
   4.581 +      map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   4.582 +  in
   4.583 +    ctxt
   4.584 +    |> Overloading.map_improvable_syntax
   4.585 +         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
   4.586 +            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   4.587 +  end;
   4.588 +
   4.589 +
   4.590 +(* target *)
   4.591 +
   4.592 +val sanatize_name = (*FIXME*)
   4.593 +  let
   4.594 +    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   4.595 +      orelse s = "'" orelse s = "_";
   4.596 +    val is_junk = not o is_valid andf Symbol.is_regular;
   4.597 +    val junk = Scan.many is_junk;
   4.598 +    val scan_valids = Symbol.scanner "Malformed input"
   4.599 +      ((junk |--
   4.600 +        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   4.601 +        --| junk))
   4.602 +      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   4.603 +  in
   4.604 +    explode #> scan_valids #> implode
   4.605 +  end;
   4.606 +
   4.607 +fun type_name "*" = "prod"
   4.608 +  | type_name "+" = "sum"
   4.609 +  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   4.610 +
   4.611 +fun resort_terms pp algebra consts constraints ts =
   4.612 +  let
   4.613 +    fun matchings (Const (c_ty as (c, _))) = (case constraints c
   4.614 +         of NONE => I
   4.615 +          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
   4.616 +              (Consts.typargs consts c_ty) sorts)
   4.617 +      | matchings _ = I
   4.618 +    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
   4.619 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
   4.620 +    val inst = map_type_tvar
   4.621 +      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   4.622 +  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
   4.623 +
   4.624 +fun init_instantiation (tycos, vs, sort) thy =
   4.625 +  let
   4.626 +    val _ = if null tycos then error "At least one arity must be given" else ();
   4.627 +    val params = these_params thy sort;
   4.628 +    fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco)
   4.629 +      then NONE else SOME ((c, tyco),
   4.630 +        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   4.631 +    val inst_params = map_product get_param tycos params |> map_filter I;
   4.632 +    val primary_constraints = map (apsnd
   4.633 +      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
   4.634 +    val pp = Syntax.pp_global thy;
   4.635 +    val algebra = Sign.classes_of thy
   4.636 +      |> fold (fn tyco => Sorts.add_arities pp
   4.637 +            (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   4.638 +    val consts = Sign.consts_of thy;
   4.639 +    val improve_constraints = AList.lookup (op =)
   4.640 +      (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
   4.641 +    fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
   4.642 +     of NONE => NONE
   4.643 +      | SOME ts' => SOME (ts', ctxt);
   4.644 +    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   4.645 +     of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   4.646 +         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
   4.647 +          | NONE => NONE)
   4.648 +      | NONE => NONE;
   4.649 +  in
   4.650 +    thy
   4.651 +    |> ProofContext.init
   4.652 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
   4.653 +    |> fold (Variable.declare_typ o TFree) vs
   4.654 +    |> fold (Variable.declare_names o Free o snd) inst_params
   4.655 +    |> (Overloading.map_improvable_syntax o apfst)
   4.656 +         (fn ((_, _), ((_, subst), unchecks)) =>
   4.657 +            ((primary_constraints, []), (((improve, K NONE), false), [])))
   4.658 +    |> Overloading.add_improvable_syntax
   4.659 +    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   4.660 +    |> synchronize_inst_syntax
   4.661 +  end;
   4.662 +
   4.663 +fun confirm_declaration c = (map_instantiation o apsnd)
   4.664 +  (filter_out (fn (_, (c', _)) => c' = c))
   4.665 +  #> LocalTheory.target synchronize_inst_syntax
   4.666 +
   4.667 +fun gen_instantiation_instance do_proof after_qed lthy =
   4.668 +  let
   4.669 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   4.670 +    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   4.671 +    fun after_qed' results =
   4.672 +      LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   4.673 +      #> after_qed;
   4.674 +  in
   4.675 +    lthy
   4.676 +    |> do_proof after_qed' arities_proof
   4.677 +  end;
   4.678 +
   4.679 +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   4.680 +  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   4.681 +
   4.682 +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   4.683 +  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   4.684 +    (fn {context, ...} => tac context)) ts) lthy) I;
   4.685 +
   4.686 +fun prove_instantiation_exit tac = prove_instantiation_instance tac
   4.687 +  #> LocalTheory.exit_global;
   4.688 +
   4.689 +fun prove_instantiation_exit_result f tac x lthy =
   4.690 +  let
   4.691 +    val phi = ProofContext.export_morphism lthy
   4.692 +      (ProofContext.init (ProofContext.theory_of lthy));
   4.693 +    val y = f phi x;
   4.694 +  in
   4.695 +    lthy
   4.696 +    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
   4.697 +    |> pair y
   4.698 +  end;
   4.699 +
   4.700 +fun conclude_instantiation lthy =
   4.701 +  let
   4.702 +    val { arities, params } = the_instantiation lthy;
   4.703 +    val (tycos, vs, sort) = arities;
   4.704 +    val thy = ProofContext.theory_of lthy;
   4.705 +    val _ = map (fn tyco => if Sign.of_sort thy
   4.706 +        (Type (tyco, map TFree vs), sort)
   4.707 +      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   4.708 +        tycos;
   4.709 +  in lthy end;
   4.710 +
   4.711 +fun pretty_instantiation lthy =
   4.712 +  let
   4.713 +    val { arities, params } = the_instantiation lthy;
   4.714 +    val (tycos, vs, sort) = arities;
   4.715 +    val thy = ProofContext.theory_of lthy;
   4.716 +    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   4.717 +    fun pr_param ((c, _), (v, ty)) =
   4.718 +      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   4.719 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   4.720 +  in
   4.721 +    (Pretty.block o Pretty.fbreaks)
   4.722 +      (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   4.723 +  end;
   4.724 +
   4.725 +end;
   4.726 +
     5.1 --- a/src/Pure/Isar/expression.ML	Mon Jan 05 15:35:42 2009 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Mon Jan 05 15:36:24 2009 +0100
     5.3 @@ -18,18 +18,18 @@
     5.4      Proof.context -> (term * term list) list list * Proof.context;
     5.5  
     5.6    (* Declaring locales *)
     5.7 -  val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
     5.8 -    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
     5.9 -    Proof.context
    5.10 -  val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    5.11 -    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
    5.12 -    Proof.context
    5.13 +  val add_locale_cmd: string -> bstring -> expression -> Element.context list ->
    5.14 +    theory -> string * local_theory;
    5.15 +  val add_locale: string -> bstring -> expression_i -> Element.context_i list ->
    5.16 +    theory -> string * local_theory;
    5.17  
    5.18    (* Interpretation *)
    5.19    val sublocale_cmd: string -> expression -> theory -> Proof.state;
    5.20    val sublocale: string -> expression_i -> theory -> Proof.state;
    5.21 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state;
    5.22 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state;
    5.23 +  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    5.24 +    theory -> Proof.state;
    5.25 +  val interpretation: expression_i -> (Attrib.binding * term) list ->
    5.26 +    theory -> Proof.state;
    5.27    val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
    5.28    val interpret: expression_i -> bool -> Proof.state -> Proof.state;
    5.29  end;
    5.30 @@ -89,11 +89,11 @@
    5.31      fun params_inst (expr as (loc, (prfx, Positional insts))) =
    5.32            let
    5.33              val (ps, loc') = params_loc loc;
    5.34 -	    val d = length ps - length insts;
    5.35 -	    val insts' =
    5.36 -	      if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    5.37 +            val d = length ps - length insts;
    5.38 +            val insts' =
    5.39 +              if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    5.40                  quote (NewLocale.extern thy loc))
    5.41 -	      else insts @ replicate d NONE;
    5.42 +              else insts @ replicate d NONE;
    5.43              val ps' = (ps ~~ insts') |>
    5.44                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    5.45            in (ps', (loc', (prfx, Positional insts'))) end
    5.46 @@ -333,9 +333,9 @@
    5.47  local
    5.48  
    5.49  fun prep_full_context_statement parse_typ parse_prop parse_inst prep_vars prep_expr
    5.50 -    strict do_close context raw_import raw_elems raw_concl =
    5.51 +    strict do_close raw_import raw_elems raw_concl ctxt1 =
    5.52    let
    5.53 -    val thy = ProofContext.theory_of context;
    5.54 +    val thy = ProofContext.theory_of ctxt1;
    5.55  
    5.56      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    5.57  
    5.58 @@ -366,22 +366,23 @@
    5.59          val concl = parse_concl parse_prop ctxt raw_concl;
    5.60        in check_autofix insts elems concl ctxt end;
    5.61  
    5.62 -    val fors = prep_vars fixed context |> fst;
    5.63 -    val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
    5.64 -    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt);
    5.65 -    val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
    5.66 -    val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
    5.67 +    val fors = prep_vars fixed ctxt1 |> fst;
    5.68 +    val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
    5.69 +    val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
    5.70 +    val (_, elems'', ctxt4) = fold prep_elem raw_elems (insts', [], ctxt3);
    5.71 +    val (insts, elems, concl, ctxt5) =
    5.72 +      prep_concl raw_concl (insts', elems'', ctxt4);
    5.73  
    5.74      (* Retrieve parameter types *)
    5.75      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
    5.76        _ => fn ps => ps) (Fixes fors :: elems) [];
    5.77 -    val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
    5.78 +    val (Ts, ctxt6) = fold_map ProofContext.inferred_param xs ctxt5; 
    5.79      val parms = xs ~~ Ts;  (* params from expression and elements *)
    5.80  
    5.81      val Fixes fors' = finish_primitive parms I (Fixes fors);
    5.82 -    val (deps, elems') = finish ctxt' parms do_close insts elems;
    5.83 +    val (deps, elems') = finish ctxt6 parms do_close insts elems;
    5.84  
    5.85 -  in ((fors', deps, elems', concl), (parms, ctxt')) end
    5.86 +  in ((fors', deps, elems', concl), (parms, ctxt6)) end
    5.87  
    5.88  in
    5.89  
    5.90 @@ -400,7 +401,8 @@
    5.91  
    5.92  fun prep_statement prep activate raw_elems raw_concl context =
    5.93    let
    5.94 -     val ((_, _, elems, concl), _) = prep true false context ([], []) raw_elems raw_concl;
    5.95 +     val ((_, _, elems, concl), _) =
    5.96 +       prep true false ([], []) raw_elems raw_concl context ;
    5.97       val (_, context') = activate elems (ProofContext.set_stmt true context);
    5.98    in (concl, context') end;
    5.99  
   5.100 @@ -418,7 +420,8 @@
   5.101  
   5.102  fun prep_declaration prep activate raw_import raw_elems context =
   5.103    let
   5.104 -    val ((fixed, deps, elems, _), (parms, ctxt')) = prep false true context raw_import raw_elems [];
   5.105 +    val ((fixed, deps, elems, _), (parms, ctxt')) =
   5.106 +      prep false true raw_import raw_elems [] context ;
   5.107      (* Declare parameters and imported facts *)
   5.108      val context' = context |>
   5.109        ProofContext.add_fixes_i fixed |> snd |>
   5.110 @@ -449,7 +452,8 @@
   5.111    let
   5.112      val thy = ProofContext.theory_of context;
   5.113  
   5.114 -    val ((fixed, deps, _, _), _) = prep true true context expression [] [];
   5.115 +    val ((fixed, deps, _, _), _) =
   5.116 +      prep true true expression [] [] context;
   5.117      (* proof obligations *)
   5.118      val propss = map (props_of thy) deps;
   5.119  
   5.120 @@ -718,7 +722,6 @@
   5.121        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   5.122      val asm = if is_some b_statement then b_statement else a_statement;
   5.123  
   5.124 -    (* These are added immediately. *)
   5.125      val notes =
   5.126          if is_some asm
   5.127          then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
   5.128 @@ -726,7 +729,6 @@
   5.129              [(Attrib.internal o K) NewLocale.witness_attrib])])])]
   5.130          else [];
   5.131  
   5.132 -    (* These will be added in the local theory. *)
   5.133      val notes' = body_elems |>
   5.134        map (defines_to_notes thy') |>
   5.135        map (Element.morph_ctxt a_satisfy) |>
   5.136 @@ -737,13 +739,14 @@
   5.137  
   5.138      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
   5.139  
   5.140 -    val loc_ctxt = thy' |>
   5.141 -      NewLocale.register_locale bname (extraTs, params)
   5.142 -        (asm, rev defs) ([], [])
   5.143 -        (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
   5.144 -      NewLocale.init name;
   5.145 +    val loc_ctxt = thy'
   5.146 +      |> NewLocale.register_locale bname (extraTs, params)
   5.147 +          (asm, rev defs) ([], [])
   5.148 +          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
   5.149 +      |> TheoryTarget.init (SOME name)
   5.150 +      |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
   5.151  
   5.152 -  in ((name, notes'), loc_ctxt) end;
   5.153 +  in (name, loc_ctxt) end;
   5.154  
   5.155  in
   5.156  
     6.1 --- a/src/Pure/Isar/instance.ML	Mon Jan 05 15:35:42 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,28 +0,0 @@
     6.4 -(*  Title:      Pure/Isar/instance.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Florian Haftmann, TU Muenchen
     6.7 -
     6.8 -Wrapper for instantiation command.
     6.9 -*)
    6.10 -
    6.11 -signature INSTANCE =
    6.12 -sig
    6.13 -  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
    6.14 -end;
    6.15 -
    6.16 -structure Instance : INSTANCE =
    6.17 -struct
    6.18 -
    6.19 -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    6.20 -  let
    6.21 -    val all_arities = map (fn raw_tyco => Sign.read_arity thy
    6.22 -      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    6.23 -    val tycos = map #1 all_arities;
    6.24 -    val (_, sorts, sort) = hd all_arities;
    6.25 -    val vs = Name.names Name.context Name.aT sorts;
    6.26 -  in (tycos, vs, sort) end;
    6.27 -
    6.28 -fun instantiation_cmd raw_arities thy =
    6.29 -  TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
    6.30 -
    6.31 -end;
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jan 05 15:35:42 2009 +0100
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jan 05 15:36:24 2009 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      Pure/Isar/isar_syn.ML
     7.5 -    ID:         $Id$
     7.6      Author:     Markus Wenzel, TU Muenchen
     7.7  
     7.8  Isar/Pure outer syntax.
     7.9 @@ -394,9 +393,7 @@
    7.10      (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
    7.11        >> (fn ((name, (expr, elems)), begin) =>
    7.12            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    7.13 -            (Expression.add_locale_cmd name name expr elems #>
    7.14 -              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
    7.15 -                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
    7.16 +            (Expression.add_locale_cmd name name expr elems #> snd)));
    7.17  
    7.18  val _ =
    7.19    OuterSyntax.command "sublocale"
    7.20 @@ -477,13 +474,13 @@
    7.21  
    7.22  val _ =
    7.23    OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
    7.24 -    (P.xname >> Subclass.subclass_cmd);
    7.25 +    (P.xname >> Class.subclass_cmd);
    7.26  
    7.27  val _ =
    7.28    OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
    7.29     (P.multi_arity --| P.begin
    7.30       >> (fn arities => Toplevel.print o
    7.31 -         Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    7.32 +         Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
    7.33  
    7.34  val _ =
    7.35    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
     8.1 --- a/src/Pure/Isar/subclass.ML	Mon Jan 05 15:35:42 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,67 +0,0 @@
     8.4 -(*  Title:      Pure/Isar/subclass.ML
     8.5 -    Author:     Florian Haftmann, TU Muenchen
     8.6 -
     8.7 -User interface for proving subclass relationship between type classes.
     8.8 -*)
     8.9 -
    8.10 -signature SUBCLASS =
    8.11 -sig
    8.12 -  val subclass: class -> local_theory -> Proof.state
    8.13 -  val subclass_cmd: xstring -> local_theory -> Proof.state
    8.14 -  val prove_subclass: tactic -> class -> local_theory -> local_theory
    8.15 -end;
    8.16 -
    8.17 -structure Subclass : SUBCLASS =
    8.18 -struct
    8.19 -
    8.20 -local
    8.21 -
    8.22 -fun gen_subclass prep_class do_proof raw_sup lthy =
    8.23 -  let
    8.24 -    val thy = ProofContext.theory_of lthy;
    8.25 -    val sup = prep_class thy raw_sup;
    8.26 -    val sub = case TheoryTarget.peek lthy
    8.27 -     of {is_class = false, ...} => error "Not a class context"
    8.28 -      | {target, ...} => target;
    8.29 -    val _ = if Sign.subsort thy ([sup], [sub])
    8.30 -      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
    8.31 -        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
    8.32 -      else ();
    8.33 -    val sub_params = map fst (Class.these_params thy [sub]);
    8.34 -    val sup_params = map fst (Class.these_params thy [sup]);
    8.35 -    val err_params = subtract (op =) sub_params sup_params;
    8.36 -    val _ = if null err_params then [] else
    8.37 -      error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
    8.38 -        commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
    8.39 -    val sublocale_prop =
    8.40 -      Locale.global_asms_of thy sup
    8.41 -      |> maps snd
    8.42 -      |> try the_single
    8.43 -      |> Option.map (ObjectLogic.ensure_propT thy);
    8.44 -    fun after_qed some_thm =
    8.45 -      LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
    8.46 -      #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
    8.47 -  in
    8.48 -    do_proof after_qed sublocale_prop lthy
    8.49 -  end;
    8.50 -
    8.51 -fun user_proof after_qed NONE =
    8.52 -      Proof.theorem_i NONE (K (after_qed NONE)) [[]]
    8.53 -  | user_proof after_qed (SOME prop) =
    8.54 -      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
    8.55 -
    8.56 -fun tactic_proof tac after_qed NONE lthy =
    8.57 -      after_qed NONE lthy
    8.58 -  | tactic_proof tac after_qed (SOME prop) lthy =
    8.59 -      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
    8.60 -        (K tac))) lthy;
    8.61 -
    8.62 -in
    8.63 -
    8.64 -val subclass = gen_subclass (K I) user_proof;
    8.65 -val subclass_cmd = gen_subclass Sign.read_class user_proof;
    8.66 -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
    8.67 -
    8.68 -end; (*local*)
    8.69 -
    8.70 -end;
     9.1 --- a/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:35:42 2009 +0100
     9.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:36:24 2009 +0100
     9.3 @@ -13,6 +13,7 @@
     9.4    val begin: string -> Proof.context -> local_theory
     9.5    val context: xstring -> theory -> local_theory
     9.6    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     9.7 +  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
     9.8    val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     9.9    val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    9.10  end;
    9.11 @@ -82,7 +83,7 @@
    9.12    Pretty.block [Pretty.str "theory", Pretty.brk 1,
    9.13        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    9.14      (if not (null overloading) then [Overloading.pretty ctxt]
    9.15 -     else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt]
    9.16 +     else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
    9.17       else pretty_thy ctxt target is_locale is_class);
    9.18  
    9.19  
    9.20 @@ -108,7 +109,7 @@
    9.21  
    9.22  fun class_target (Target {target, ...}) f =
    9.23    LocalTheory.raw_theory f #>
    9.24 -  LocalTheory.target (Class.refresh_syntax target);
    9.25 +  LocalTheory.target (Class_Target.refresh_syntax target);
    9.26  
    9.27  
    9.28  (* notes *)
    9.29 @@ -207,7 +208,7 @@
    9.30      val (prefix', _) = Binding.dest b';
    9.31      val class_global = Binding.base_name b = Binding.base_name b'
    9.32        andalso not (null prefix')
    9.33 -      andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
    9.34 +      andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
    9.35    in
    9.36      not (is_class andalso (similar_body orelse class_global)) ?
    9.37        (Context.mapping_result
    9.38 @@ -231,11 +232,11 @@
    9.39      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    9.40      fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    9.41      val declare_const =
    9.42 -      (case Class.instantiation_param lthy c of
    9.43 +      (case Class_Target.instantiation_param lthy c of
    9.44          SOME c' =>
    9.45            if mx3 <> NoSyn then syntax_error c'
    9.46            else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
    9.47 -            ##> Class.confirm_declaration c
    9.48 +            ##> Class_Target.confirm_declaration c
    9.49          | NONE =>
    9.50              (case Overloading.operation lthy c of
    9.51                SOME (c', _) =>
    9.52 @@ -248,7 +249,7 @@
    9.53    in
    9.54      lthy'
    9.55      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
    9.56 -    |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
    9.57 +    |> is_class ? class_target ta (Class_Target.declare target tags ((c, mx1), t))
    9.58      |> LocalDefs.add_def ((b, NoSyn), t)
    9.59    end;
    9.60  
    9.61 @@ -275,7 +276,7 @@
    9.62          #-> (fn (lhs, _) =>
    9.63            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    9.64              term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
    9.65 -            is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
    9.66 +            is_class ? class_target ta (Class_Target.abbrev target prmode tags ((c, mx1), t'))
    9.67            end)
    9.68        else
    9.69          LocalTheory.theory
    9.70 @@ -311,7 +312,7 @@
    9.71          SOME (_, checked) =>
    9.72            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    9.73        | NONE =>
    9.74 -          if is_none (Class.instantiation_param lthy c)
    9.75 +          if is_none (Class_Target.instantiation_param lthy c)
    9.76            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    9.77            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    9.78      val (global_def, lthy3) = lthy2
    9.79 @@ -334,14 +335,14 @@
    9.80  fun init_target _ NONE = global_target
    9.81    | init_target thy (SOME target) =
    9.82        make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
    9.83 -      true (Class.is_class thy target) ([], [], []) [];
    9.84 +      true (Class_Target.is_class thy target) ([], [], []) [];
    9.85  
    9.86  fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
    9.87 -  if not (null (#1 instantiation)) then Class.init_instantiation instantiation
    9.88 +  if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
    9.89    else if not (null overloading) then Overloading.init overloading
    9.90    else if not is_locale then ProofContext.init
    9.91    else if not is_class then locale_init new_locale target
    9.92 -  else Class.init target;
    9.93 +  else Class_Target.init target;
    9.94  
    9.95  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
    9.96    Data.put ta #>
    9.97 @@ -355,11 +356,20 @@
    9.98      declaration = declaration ta,
    9.99      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   9.100      exit = LocalTheory.target_of o
   9.101 -      (if not (null (#1 instantiation)) then Class.conclude_instantiation
   9.102 +      (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
   9.103         else if not (null overloading) then Overloading.conclude
   9.104         else I)}
   9.105  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   9.106  
   9.107 +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   9.108 +  let
   9.109 +    val all_arities = map (fn raw_tyco => Sign.read_arity thy
   9.110 +      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
   9.111 +    val tycos = map #1 all_arities;
   9.112 +    val (_, sorts, sort) = hd all_arities;
   9.113 +    val vs = Name.names Name.context Name.aT sorts;
   9.114 +  in (tycos, vs, sort) end;
   9.115 +
   9.116  fun gen_overloading prep_const raw_ops thy =
   9.117    let
   9.118      val ctxt = ProofContext.init thy;
   9.119 @@ -377,6 +387,8 @@
   9.120        (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
   9.121  
   9.122  fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
   9.123 +fun instantiation_cmd raw_arities thy =
   9.124 +  instantiation (read_multi_arity thy raw_arities) thy;
   9.125  
   9.126  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   9.127  val overloading_cmd = gen_overloading Syntax.read_term;