major restructurings
authorhaftmann
Fri Dec 29 20:35:03 2006 +0100 (2006-12-29)
changeset 21954ffeb00290397
parent 21953 ab834c5c3858
child 21955 c1a6fad248ca
major restructurings
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Tools/class_package.ML	Fri Dec 29 20:35:02 2006 +0100
     1.2 +++ b/src/Pure/Tools/class_package.ML	Fri Dec 29 20:35:03 2006 +0100
     1.3 @@ -7,31 +7,22 @@
     1.4  
     1.5  signature CLASS_PACKAGE =
     1.6  sig
     1.7 -  val class: bstring -> class list -> Element.context Locale.element list -> theory ->
     1.8 -    string * Proof.context
     1.9 -  val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory ->
    1.10 +  val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
    1.11      string * Proof.context
    1.12 -  val instance_arity: ((bstring * string list) * string) list
    1.13 -    -> ((bstring * Attrib.src list) * string) list
    1.14 -    -> theory -> Proof.state
    1.15 -  val instance_arity_i: ((bstring * sort list) * sort) list
    1.16 +  val instance_arity: ((bstring * sort list) * sort) list
    1.17      -> ((bstring * attribute list) * term) list
    1.18      -> theory -> Proof.state
    1.19    val prove_instance_arity: tactic -> ((string * sort list) * sort) list
    1.20      -> ((bstring * attribute list) * term) list
    1.21      -> theory -> theory
    1.22 -  val instance_sort: string * string -> theory -> Proof.state
    1.23 -  val instance_sort_i: class * sort -> theory -> Proof.state
    1.24 +  val instance_sort: class * sort -> theory -> Proof.state
    1.25    val prove_instance_sort: tactic -> class * sort -> theory -> theory
    1.26  
    1.27 -  val certify_class: theory -> class -> class
    1.28 -  val certify_sort: theory -> sort -> sort
    1.29 -  val read_class: theory -> xstring -> class
    1.30 -  val read_sort: theory -> string -> sort
    1.31    val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
    1.32    val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
    1.33      (*'a must not keep any reference to theory*)
    1.34  
    1.35 +  (* experimental class target *)
    1.36    val add_def: class * thm -> theory -> theory
    1.37    val export_typ: theory -> class -> typ -> typ
    1.38    val export_def: theory -> class -> term -> term
    1.39 @@ -45,172 +36,59 @@
    1.40  structure ClassPackage : CLASS_PACKAGE =
    1.41  struct
    1.42  
    1.43 -
    1.44 -(** theory data **)
    1.45 +(** axclasses with implicit parameter handling **)
    1.46  
    1.47 -datatype class_data = ClassData of {
    1.48 -  locale: string,
    1.49 -  var: string,
    1.50 -  consts: (string * (string * typ)) list
    1.51 -    (*locale parameter ~> toplevel theory constant*),
    1.52 -  propnames: string list,
    1.53 -  defs: thm list
    1.54 -};
    1.55 +(* axclass instances *)
    1.56  
    1.57 -fun rep_classdata (ClassData c) = c;
    1.58 +local
    1.59  
    1.60 -structure ClassData = TheoryDataFun (
    1.61 -  struct
    1.62 -    val name = "Pure/classes";
    1.63 -    type T = class_data Symtab.table;
    1.64 -    val empty = Symtab.empty;
    1.65 -    val copy = I;
    1.66 -    val extend = I;
    1.67 -    fun merge _ = Symtab.merge (K true);
    1.68 -    fun print _ _ = ();
    1.69 -  end
    1.70 -);
    1.71 +fun gen_instance mk_prop add_thm after_qed insts thy =
    1.72 +  let
    1.73 +    fun after_qed' results =
    1.74 +      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
    1.75 +  in
    1.76 +    thy
    1.77 +    |> ProofContext.init
    1.78 +    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
    1.79 +  end;
    1.80  
    1.81 -val _ = Context.add_setup ClassData.init;
    1.82 +in
    1.83 +
    1.84 +val axclass_instance_arity =
    1.85 +  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
    1.86 +val axclass_instance_sort =
    1.87 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
    1.88 +    AxClass.add_classrel I o single;
    1.89 +
    1.90 +end; (* local *)
    1.91  
    1.92  
    1.93 -(* queries *)
    1.94 -
    1.95 -val lookup_class_data = Option.map rep_classdata oo Symtab.lookup o ClassData.get;
    1.96 -
    1.97 -fun the_class_data thy class =
    1.98 -  case lookup_class_data thy class
    1.99 -    of NONE => error ("undeclared constructive class " ^ quote class)
   1.100 -     | SOME data => data;
   1.101 -
   1.102 -fun the_ancestry thy classes =
   1.103 -  let
   1.104 -    fun proj_class class =
   1.105 -      if is_some (lookup_class_data thy class)
   1.106 -      then [class]
   1.107 -      else (Sign.certify_sort thy o maps proj_class o Sign.super_classes thy) class;
   1.108 -    fun ancestry class anc =
   1.109 -      anc
   1.110 -      |> insert (op =) class
   1.111 -      |> fold ancestry ((maps proj_class o Sign.super_classes thy) class);
   1.112 -  in fold ancestry classes [] end;
   1.113 -
   1.114 -val the_parm_map = #consts oo the_class_data;
   1.115 -
   1.116 -val the_propnames = #propnames oo the_class_data;
   1.117 -
   1.118 -fun subst_clsvar v ty_subst =
   1.119 -  map_type_tfree (fn u as (w, _) =>
   1.120 -    if w = v then ty_subst else TFree u);
   1.121 +(* introducing axclasses with implicit parameter handling *)
   1.122  
   1.123 -fun print_classes thy =
   1.124 +fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms thy =
   1.125    let
   1.126 -    val algebra = Sign.classes_of thy;
   1.127 -    val arities =
   1.128 -      Symtab.empty
   1.129 -      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   1.130 -           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   1.131 -             ((#arities o Sorts.rep_algebra) algebra);
   1.132 -    val the_arities = these o Symtab.lookup arities;
   1.133 -    fun mk_arity class tyco =
   1.134 -      let
   1.135 -        val Ss = Sorts.mg_domain algebra tyco [class];
   1.136 -      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
   1.137 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   1.138 -      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
   1.139 -    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   1.140 -      (SOME o Pretty.str) ("class " ^ class ^ ":"),
   1.141 -      (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.142 -        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
   1.143 -      Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
   1.144 -      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   1.145 -        o these o Option.map #params o try (AxClass.get_definition thy)) class,
   1.146 -      (SOME o Pretty.block o Pretty.breaks) [
   1.147 -        Pretty.str "instances:",
   1.148 -        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   1.149 -      ]
   1.150 -    ]
   1.151 +    val superclasses = map (Sign.certify_class thy) raw_superclasses;
   1.152 +    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   1.153 +    fun add_const ((c, ty), syn) =
   1.154 +      Sign.add_consts_authentic [(c, ty, syn)] #> pair (Sign.full_name thy c, ty);
   1.155 +    fun mk_axioms cs thy =
   1.156 +      raw_dep_axioms thy cs
   1.157 +      |> (map o apsnd o map) (Sign.cert_prop thy)
   1.158 +      |> rpair thy;
   1.159 +    fun add_constraint class (c, ty) =
   1.160 +      Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   1.161    in
   1.162 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
   1.163 -      algebra
   1.164 +    thy
   1.165 +    |> fold_map add_const consts
   1.166 +    |-> (fn cs => mk_axioms cs
   1.167 +    #-> (fn axioms => AxClass.define_class_i (name, superclasses) (map fst cs) axioms
   1.168 +    #-> (fn class => `(fn thy => AxClass.get_definition thy class)
   1.169 +    #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
   1.170 +    #> pair (class, ((intro, axioms), cs))))))
   1.171    end;
   1.172  
   1.173  
   1.174 -(* updaters *)
   1.175 -
   1.176 -fun add_class_data (class, (locale, var, consts, propnames)) =
   1.177 -  ClassData.map (
   1.178 -    Symtab.update_new (class, ClassData {
   1.179 -      locale = locale,
   1.180 -      var = var,
   1.181 -      consts = consts,
   1.182 -      propnames = propnames,
   1.183 -      defs = []})
   1.184 -  );
   1.185 -
   1.186 -fun add_def (class, thm) =
   1.187 -  (ClassData.map o Symtab.map_entry class)
   1.188 -    (fn ClassData { locale,
   1.189 -      var, consts, propnames, defs } => ClassData { locale = locale,
   1.190 -      var = var,
   1.191 -      consts = consts, propnames = propnames, defs = thm :: defs });
   1.192 -
   1.193 -
   1.194 -(* experimental class target *)
   1.195 -
   1.196 -fun export_typ thy loc =
   1.197 -  let
   1.198 -    val class = loc (*FIXME*);
   1.199 -    val (v, _) = AxClass.params_of_class thy class;
   1.200 -  in
   1.201 -    Term.map_type_tfree (fn var as (w, sort) =>
   1.202 -      if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   1.203 -        (sort, [class])) else TFree var)
   1.204 -  end;
   1.205 -
   1.206 -fun export_def thy loc =
   1.207 -  let
   1.208 -    val class = loc (*FIXME*);
   1.209 -    val data = the_class_data thy class;
   1.210 -    val consts = #consts data;
   1.211 -    val v = #var data;
   1.212 -    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.213 -      if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   1.214 -        (sort, [class])) else TFree var)
   1.215 -    fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v
   1.216 -         of SOME c_ty => Const c_ty
   1.217 -          | NONE => t)
   1.218 -      | subst t = t;
   1.219 -  in
   1.220 -    Term.map_aterms subst #> map_types subst_typ
   1.221 -  end;
   1.222 -
   1.223 -fun export_thm thy loc =
   1.224 -  let
   1.225 -    val class = loc (*FIXME*);
   1.226 -    val thms = (#defs o the_class_data thy) class;
   1.227 -  in
   1.228 -    MetaSimplifier.rewrite_rule thms
   1.229 -  end;
   1.230 -
   1.231 -
   1.232 -(* certification and reading *)
   1.233 -
   1.234 -fun certify_class thy class =
   1.235 -  (fn class => (the_class_data thy class; class)) (Sign.certify_class thy class);
   1.236 -
   1.237 -fun certify_sort thy sort =
   1.238 -  map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort);
   1.239 -
   1.240 -fun read_class thy =
   1.241 -  certify_class thy o Sign.intern_class thy;
   1.242 -
   1.243 -fun read_sort thy =
   1.244 -  certify_sort thy o Sign.read_sort thy;
   1.245 -
   1.246 -
   1.247 -
   1.248 -(** contexts with arity assumptions **)
   1.249 +(* contexts with arity assumptions *)
   1.250  
   1.251  fun assume_arities_of_sort thy arities ty_sort =
   1.252    let
   1.253 @@ -227,172 +105,7 @@
   1.254    in f thy_read end;
   1.255  
   1.256  
   1.257 -
   1.258 -(** tactics and methods **)
   1.259 -
   1.260 -fun intro_classes_tac facts st =
   1.261 -  (ALLGOALS (Method.insert_tac facts THEN'
   1.262 -      REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st))))
   1.263 -    THEN Tactic.distinct_subgoals_tac) st;
   1.264 -
   1.265 -fun default_intro_classes_tac [] = intro_classes_tac []
   1.266 -  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   1.267 -
   1.268 -fun default_tac rules ctxt facts =
   1.269 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   1.270 -    default_intro_classes_tac facts;
   1.271 -
   1.272 -val _ = Context.add_setup (Method.add_methods
   1.273 - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   1.274 -    "back-chain introduction rules of classes"),
   1.275 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.276 -    "apply some intro/elim rule")]);
   1.277 -
   1.278 -
   1.279 -
   1.280 -(** axclass instances **)
   1.281 -
   1.282 -local
   1.283 -
   1.284 -fun gen_instance mk_prop add_thm after_qed insts thy =
   1.285 -  let
   1.286 -    fun after_qed' results =
   1.287 -      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
   1.288 -  in
   1.289 -    thy
   1.290 -    |> ProofContext.init
   1.291 -    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
   1.292 -  end;
   1.293 -
   1.294 -in
   1.295 -
   1.296 -val axclass_instance_arity =
   1.297 -  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity;
   1.298 -val axclass_instance_arity_i =
   1.299 -  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   1.300 -val axclass_instance_sort =      
   1.301 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
   1.302 -    AxClass.add_classrel I o single;
   1.303 -
   1.304 -end;
   1.305 -
   1.306 -
   1.307 -
   1.308 -(** classes and instances **)
   1.309 -
   1.310 -local
   1.311 -
   1.312 -fun add_axclass_i (name, supsort) params axs thy =
   1.313 -  let
   1.314 -    val (c, thy') = thy
   1.315 -      |> AxClass.define_class_i (name, supsort) params axs;
   1.316 -    val {intro, axioms, ...} = AxClass.get_definition thy' c;
   1.317 -  in ((c, (intro, axioms)), thy') end;
   1.318 -
   1.319 -(*FIXME proper locale interface*)
   1.320 -fun prove_interpretation_i (prfx, atts) expr insts tac thy =
   1.321 -  let
   1.322 -    fun ad_hoc_term (Const (c, ty)) =
   1.323 -          let
   1.324 -            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
   1.325 -            val s = c ^ "::" ^ Pretty.output p;
   1.326 -          in s end
   1.327 -      | ad_hoc_term t =
   1.328 -          let
   1.329 -            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
   1.330 -            val s = Pretty.output p;
   1.331 -          in s end;
   1.332 -  in
   1.333 -    thy
   1.334 -    |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts)
   1.335 -    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   1.336 -    |> ProofContext.theory_of
   1.337 -  end;
   1.338 -
   1.339 -fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   1.340 -  let
   1.341 -    val (elems, exprs) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.342 -                                   | Locale.Expr e => apsnd (cons e))
   1.343 -      raw_elems ([], []);
   1.344 -    val supclasses = map (prep_class thy) raw_supclasses;
   1.345 -    val supsort =
   1.346 -      supclasses
   1.347 -      |> Sign.certify_sort thy
   1.348 -      |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
   1.349 -    val expr_supclasses = Locale.Merge
   1.350 -      (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   1.351 -    val expr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses
   1.352 -      @ exprs);
   1.353 -    val mapp_sup = AList.make
   1.354 -      (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses))
   1.355 -      ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses);
   1.356 -    fun extract_tyvar_consts thy name_locale =
   1.357 -      let
   1.358 -        fun extract_classvar ((c, ty), _) w =
   1.359 -          (case Term.add_tfreesT ty []
   1.360 -           of [(v, _)] => (case w
   1.361 -               of SOME u => if u = v then w else error ("Additonal type variable in type signature of constant " ^ quote c)
   1.362 -                | NONE => SOME v)
   1.363 -            | [] => error ("No type variable in type signature of constant " ^ quote c)
   1.364 -            | _ => error ("More than one type variable in type signature of constant " ^ quote c));
   1.365 -        val consts1 =
   1.366 -          Locale.parameters_of thy name_locale
   1.367 -          |> map (apsnd (TheoryTarget.fork_mixfix false true #> fst))
   1.368 -        val SOME v = fold extract_classvar consts1 NONE;
   1.369 -        val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
   1.370 -      in (v, chop (length mapp_sup) consts2) end;
   1.371 -    fun add_consts v raw_cs_sup raw_cs_this thy =
   1.372 -      let
   1.373 -        fun add_global_const ((c, ty), syn) thy =
   1.374 -          ((c, (Sign.full_name thy c, ty)),
   1.375 -            thy
   1.376 -            |> Sign.add_consts_authentic [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]);
   1.377 -      in
   1.378 -        thy
   1.379 -        |> fold_map add_global_const raw_cs_this
   1.380 -      end;
   1.381 -    fun extract_assumes thy name_locale cs_mapp =
   1.382 -      let
   1.383 -        val subst_assume =
   1.384 -          map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
   1.385 -                       | t => t)
   1.386 -        fun prep_asm ((name, atts), ts) =
   1.387 -          ((NameSpace.base name, map (Attrib.attribute thy) atts), map subst_assume ts)
   1.388 -      in
   1.389 -        (map prep_asm o Locale.local_asms_of thy) name_locale
   1.390 -      end;
   1.391 -    fun add_global_constraint v class (_, (c, ty)) thy =
   1.392 -      thy
   1.393 -      |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
   1.394 -    fun mk_const thy class v (c, ty) =
   1.395 -      Const (c, subst_clsvar v (TFree (v, [class])) ty);
   1.396 -  in
   1.397 -    thy
   1.398 -    |> add_locale bname expr elems
   1.399 -    |-> (fn name_locale => ProofContext.theory
   1.400 -          (`(fn thy => extract_tyvar_consts thy name_locale)
   1.401 -    #-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
   1.402 -          add_consts v raw_cs_sup raw_cs_this
   1.403 -    #-> (fn mapp_this =>
   1.404 -          `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
   1.405 -    #-> (fn loc_axioms =>
   1.406 -          add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms
   1.407 -    #-> (fn (name_axclass, (_, ax_axioms)) =>
   1.408 -          fold (add_global_constraint v name_axclass) mapp_this
   1.409 -    #> add_class_data (name_locale, (name_locale, v, mapp_this,
   1.410 -          map (fst o fst) loc_axioms))
   1.411 -    #> prove_interpretation_i (Logic.const_of_class bname, [])
   1.412 -          (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
   1.413 -          ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   1.414 -    ))))) #> pair name_locale)
   1.415 -  end;
   1.416 -
   1.417 -in
   1.418 -
   1.419 -val class = gen_class (Locale.add_locale false) read_class;
   1.420 -val class_i = gen_class (Locale.add_locale_i false) certify_class;
   1.421 -
   1.422 -end; (*local*)
   1.423 +(* instances with implicit parameter handling *)
   1.424  
   1.425  local
   1.426  
   1.427 @@ -407,8 +120,8 @@
   1.428        | _ => SOME raw_name;
   1.429    in (c, (insts, ((name, t), atts))) end;
   1.430  
   1.431 -fun read_def thy = gen_read_def thy Attrib.attribute read_axm;
   1.432 -fun read_def_i thy = gen_read_def thy (K I) (K I);
   1.433 +fun read_def_e thy = gen_read_def thy Attrib.attribute read_axm;
   1.434 +fun read_def thy = gen_read_def thy (K I) (K I);
   1.435  
   1.436  fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory =
   1.437    let
   1.438 @@ -420,9 +133,10 @@
   1.439       of [] => ()
   1.440        | dupl_tycos => error ("type constructors occur more than once in arities: "
   1.441          ^ (commas o map quote) dupl_tycos);
   1.442 +    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
   1.443      fun get_consts_class tyco ty class =
   1.444        let
   1.445 -        val (_, cs) = AxClass.params_of_class theory class;
   1.446 +        val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
   1.447          val subst_ty = map_type_tfree (K ty);
   1.448        in
   1.449          map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs
   1.450 @@ -430,7 +144,7 @@
   1.451      fun get_consts_sort (tyco, asorts, sort) =
   1.452        let
   1.453          val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
   1.454 -      in maps (get_consts_class tyco ty) (the_ancestry theory sort) end;
   1.455 +      in maps (get_consts_class tyco ty) (super_sort sort) end;
   1.456      val cs = maps get_consts_sort arities;
   1.457      fun mk_typnorm thy (ty, ty_sc) =
   1.458        case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
   1.459 @@ -474,22 +188,339 @@
   1.460      theory
   1.461      |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   1.462      ||>> add_defs defs
   1.463 -    |-> (fn (cs, def_thms) => do_proof (after_qed cs) arities)
   1.464 +    |-> (fn (cs, _) => do_proof (after_qed cs) arities)
   1.465    end;
   1.466  
   1.467 -fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
   1.468 +fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
   1.469 +  read_def_e do_proof;
   1.470 +fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity (K I)
   1.471    read_def do_proof;
   1.472 -fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I)
   1.473 -  read_def_i do_proof;
   1.474  fun tactic_proof tac after_qed arities =
   1.475    fold (fn arity => AxClass.prove_arity arity tac) arities
   1.476    #> after_qed;
   1.477  
   1.478  in
   1.479  
   1.480 -val instance_arity = instance_arity' axclass_instance_arity_i;
   1.481 -val instance_arity_i = instance_arity_i' axclass_instance_arity_i;
   1.482 -val prove_instance_arity = instance_arity_i' o tactic_proof;
   1.483 +val instance_arity_e = instance_arity_e' axclass_instance_arity;
   1.484 +val instance_arity = instance_arity' axclass_instance_arity;
   1.485 +val prove_instance_arity = instance_arity' o tactic_proof;
   1.486 +
   1.487 +end; (* local *)
   1.488 +
   1.489 +
   1.490 +
   1.491 +(** combining locales and axclasses **)
   1.492 +
   1.493 +(* theory data *)
   1.494 +
   1.495 +datatype class_data = ClassData of {
   1.496 +  locale: string,
   1.497 +  consts: (string * string) list
   1.498 +    (*locale parameter ~> toplevel theory constant*),
   1.499 +  propnames: string list,
   1.500 +  defs: thm list
   1.501 +    (*for experimental class target*)
   1.502 +};
   1.503 +
   1.504 +fun rep_classdata (ClassData c) = c;
   1.505 +
   1.506 +structure ClassData = TheoryDataFun (
   1.507 +  struct
   1.508 +    val name = "Pure/classes";
   1.509 +    type T = class_data Graph.T;
   1.510 +    val empty = Graph.empty;
   1.511 +    val copy = I;
   1.512 +    val extend = I;
   1.513 +    fun merge _ = Graph.merge (K true);
   1.514 +    fun print _ _ = ();
   1.515 +  end
   1.516 +);
   1.517 +
   1.518 +val _ = Context.add_setup ClassData.init;
   1.519 +
   1.520 +
   1.521 +(* queries *)
   1.522 +
   1.523 +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get;
   1.524 +val is_class = can o Graph.get_node o ClassData.get;
   1.525 +fun the_class_data thy class =
   1.526 +  case lookup_class_data thy class
   1.527 +    of NONE => error ("undeclared class " ^ quote class)
   1.528 +     | SOME data => data;
   1.529 +
   1.530 +fun the_ancestry thy = Graph.all_succs (ClassData.get thy);
   1.531 +
   1.532 +fun the_parm_map thy class =
   1.533 +  let
   1.534 +    val const_typs = (#params o AxClass.get_definition thy) class;
   1.535 +    val const_names = (#consts o the_class_data thy) class;
   1.536 +  in
   1.537 +    map (apsnd (fn c => (c, (the o AList.lookup (op =) const_typs) c))) const_names
   1.538 +  end;
   1.539 +
   1.540 +val the_propnames = #propnames oo the_class_data;
   1.541 +
   1.542 +fun print_classes thy =
   1.543 +  let
   1.544 +    val algebra = Sign.classes_of thy;
   1.545 +    val arities =
   1.546 +      Symtab.empty
   1.547 +      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   1.548 +           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   1.549 +             ((#arities o Sorts.rep_algebra) algebra);
   1.550 +    val the_arities = these o Symtab.lookup arities;
   1.551 +    fun mk_arity class tyco =
   1.552 +      let
   1.553 +        val Ss = Sorts.mg_domain algebra tyco [class];
   1.554 +      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
   1.555 +    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   1.556 +      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
   1.557 +    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   1.558 +      (SOME o Pretty.str) ("class " ^ class ^ ":"),
   1.559 +      (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.560 +        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
   1.561 +      Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
   1.562 +      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   1.563 +        o these o Option.map #params o try (AxClass.get_definition thy)) class,
   1.564 +      (SOME o Pretty.block o Pretty.breaks) [
   1.565 +        Pretty.str "instances:",
   1.566 +        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   1.567 +      ]
   1.568 +    ]
   1.569 +  in
   1.570 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
   1.571 +      algebra
   1.572 +  end;
   1.573 +
   1.574 +
   1.575 +(* updaters *)
   1.576 +
   1.577 +fun add_class_data ((class, superclasses), (locale, consts, propnames)) =
   1.578 +  ClassData.map (
   1.579 +    Graph.new_node (class, ClassData {
   1.580 +      locale = locale,
   1.581 +      consts = consts,
   1.582 +      propnames = propnames,
   1.583 +      defs = []})
   1.584 +    #> fold (curry Graph.add_edge class) superclasses
   1.585 +  );
   1.586 +
   1.587 +fun add_def (class, thm) =
   1.588 +  (ClassData.map o Graph.map_node class)
   1.589 +    (fn ClassData { locale,
   1.590 +      consts, propnames, defs } => ClassData { locale = locale,
   1.591 +      consts = consts, propnames = propnames, defs = thm :: defs });
   1.592 +
   1.593 +
   1.594 +(* tactics and methods *)
   1.595 +
   1.596 +fun intro_classes_tac facts st =
   1.597 +  (ALLGOALS (Method.insert_tac facts THEN'
   1.598 +      REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st))))
   1.599 +    THEN Tactic.distinct_subgoals_tac) st;
   1.600 +
   1.601 +fun default_intro_classes_tac [] = intro_classes_tac []
   1.602 +  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   1.603 +
   1.604 +fun default_tac rules ctxt facts =
   1.605 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   1.606 +    default_intro_classes_tac facts;
   1.607 +
   1.608 +val _ = Context.add_setup (Method.add_methods
   1.609 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   1.610 +    "back-chain introduction rules of classes"),
   1.611 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.612 +    "apply some intro/elim rule")]);
   1.613 +
   1.614 +
   1.615 +(* classes and instances *)
   1.616 +
   1.617 +local
   1.618 +
   1.619 +fun add_axclass (name, supsort) params axs thy =
   1.620 +  let
   1.621 +    val (c, thy') = thy
   1.622 +      |> AxClass.define_class_i (name, supsort) params axs;
   1.623 +    val {intro, axioms, ...} = AxClass.get_definition thy' c;
   1.624 +  in ((c, (intro, axioms)), thy') end;
   1.625 +
   1.626 +fun certify_class thy class =
   1.627 +  tap (the_class_data thy) (Sign.certify_class thy class);
   1.628 +
   1.629 +fun read_class thy =
   1.630 +  certify_class thy o Sign.intern_class thy;
   1.631 +
   1.632 +(*FIXME proper locale interface*)
   1.633 +fun prove_interpretation (prfx, atts) expr insts tac thy =
   1.634 +  let
   1.635 +    fun ad_hoc_term (Const (c, ty)) =
   1.636 +          let
   1.637 +            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
   1.638 +            val s = c ^ "::" ^ Pretty.output p;
   1.639 +          in s end
   1.640 +      | ad_hoc_term t =
   1.641 +          let
   1.642 +            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
   1.643 +            val s = Pretty.output p;
   1.644 +          in s end;
   1.645 +  in
   1.646 +    thy
   1.647 +    |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts)
   1.648 +    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   1.649 +    |> ProofContext.theory_of
   1.650 +  end;
   1.651 +
   1.652 +(*
   1.653 +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   1.654 +  let
   1.655 +    val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
   1.656 +    val supclasses = map (prep_class thy) raw_supclasses;
   1.657 +    val supsort =
   1.658 +      supclasses
   1.659 +      |> Sign.certify_sort thy
   1.660 +      |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
   1.661 +    val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   1.662 +    val supconsts = AList.make
   1.663 +      (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses))
   1.664 +      ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr);
   1.665 +    fun check_locale thy name_locale =
   1.666 +      let
   1.667 +        val tfrees =
   1.668 +          []
   1.669 +          |> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale)
   1.670 +          |> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale);
   1.671 +      in case tfrees
   1.672 +       of [(_, _)] => ()
   1.673 +        (*| [(_, sort)] => error ("Additional sort constraint on class variable: "
   1.674 +            ^ Sign.string_of_sort thy sort) FIXME what to do about this?*)
   1.675 +        | [] => error ("No type variable in class specification")
   1.676 +        | tfrees => error ("More than one type variable in class specification: " ^
   1.677 +            (commas o map fst) tfrees)
   1.678 +      end;
   1.679 +    fun extract_params thy name_locale =
   1.680 +      Locale.parameters_of thy name_locale
   1.681 +      |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
   1.682 +      |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst)
   1.683 +      |> chop (length supconsts)
   1.684 +      |> snd;
   1.685 +    val LOC_AXIOMS = ref [] : string list ref;
   1.686 +    fun extract_assumes name_locale params thy cs =
   1.687 +      let
   1.688 +        val consts = supconsts @ (map (fst o fst) params ~~ cs);
   1.689 +        (*FIXME is this type handling correct?*)
   1.690 +        fun subst (Free (c, ty)) =
   1.691 +          Const ((fst o the o AList.lookup (op =) consts) c, ty);
   1.692 +        fun prep_asm ((name, atts), ts) =
   1.693 +          (*FIXME*)
   1.694 +          ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts);
   1.695 +      in
   1.696 +        Locale.local_asms_of thy name_locale
   1.697 +        |> map prep_asm
   1.698 +        |> tap (fn assms => LOC_AXIOMS := map (fst o fst) assms)
   1.699 +      end;
   1.700 +    fun mk_const thy class (c, ty) =
   1.701 +      Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   1.702 +  in
   1.703 +    thy
   1.704 +    |> add_locale bname supexpr elems
   1.705 +    |-> (fn name_locale => ProofContext.theory_result (
   1.706 +      tap (fn thy => check_locale thy name_locale)
   1.707 +      #> `(fn thy => extract_params thy name_locale)
   1.708 +      #-> (fn params =>
   1.709 +        axclass_params (bname, supsort) params (extract_assumes name_locale params)
   1.710 +      #-> (fn (name_axclass, ((_, ax_axioms), consts)) =>
   1.711 +        add_class_data ((name_axclass, supclasses), (name_locale, map (fst o fst) params ~~ map fst consts,
   1.712 +            ! LOC_AXIOMS))
   1.713 +      #> prove_interpretation (Logic.const_of_class bname, [])
   1.714 +            (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   1.715 +            ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   1.716 +      #> pair name_axclass
   1.717 +      ))))
   1.718 +  end;
   1.719 +*)
   1.720 +
   1.721 +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   1.722 +  let
   1.723 +    val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
   1.724 +    val supclasses = map (prep_class thy) raw_supclasses;
   1.725 +    val supsort =
   1.726 +      supclasses
   1.727 +      |> Sign.certify_sort thy
   1.728 +      |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
   1.729 +    val expr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   1.730 +    val mapp_sup = AList.make
   1.731 +      (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses))
   1.732 +      ((map (fst o fst) o Locale.parameters_of_expr thy) expr);
   1.733 +    fun extract_consts thy name_locale =
   1.734 +      let
   1.735 +        val tfrees =
   1.736 +          []
   1.737 +          |> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale)
   1.738 +          |> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale);
   1.739 +        val _ = case tfrees
   1.740 +         of [(_, _)] => ()
   1.741 +          (*| [(_, sort)] => error ("Additional sort constraint on class variable: "
   1.742 +              ^ Sign.string_of_sort thy sort) FIXME what to do about this?*)
   1.743 +          | [] => error ("No type variable in class specification")
   1.744 +          | tfrees => error ("More than one type variable in class specification: " ^
   1.745 +              (commas o map fst) tfrees);
   1.746 +        val consts =
   1.747 +          Locale.parameters_of thy name_locale
   1.748 +          |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
   1.749 +          |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst);
   1.750 +      in chop (length mapp_sup) consts |> snd end;
   1.751 +    fun add_consts raw_cs_this thy =
   1.752 +      let
   1.753 +        fun add_global_const ((c, ty), syn) thy =
   1.754 +          ((c, (Sign.full_name thy c, ty)),
   1.755 +            thy
   1.756 +            |> Sign.add_consts_authentic
   1.757 +                 [(c, ty |> Term.map_type_tfree (fn (v, _) => TFree (v, Sign.defaultS thy)), syn)]);
   1.758 +      in
   1.759 +        thy
   1.760 +        |> fold_map add_global_const raw_cs_this
   1.761 +      end;
   1.762 +    fun extract_assumes thy name_locale cs_mapp =
   1.763 +      let
   1.764 +        val subst_assume =
   1.765 +          map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
   1.766 +                       | t => t)
   1.767 +        fun prep_asm ((name, atts), ts) =
   1.768 +          (*FIXME*)
   1.769 +          ((NameSpace.base name, map (Attrib.attribute thy) atts), map subst_assume ts)
   1.770 +      in
   1.771 +        (map prep_asm o Locale.local_asms_of thy) name_locale
   1.772 +      end;
   1.773 +    fun add_global_constraint class (_, (c, ty)) thy =
   1.774 +      thy
   1.775 +      |> Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   1.776 +    fun mk_const thy class (c, ty) =
   1.777 +      Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   1.778 +  in
   1.779 +    thy
   1.780 +    |> add_locale bname expr elems
   1.781 +    |-> (fn name_locale => ProofContext.theory
   1.782 +          (`(fn thy => extract_consts thy name_locale)
   1.783 +    #-> (fn raw_cs_this =>
   1.784 +          add_consts raw_cs_this
   1.785 +    #-> (fn mapp_this =>
   1.786 +          `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
   1.787 +    #-> (fn loc_axioms =>
   1.788 +          add_axclass (bname, supsort) (map (fst o snd) mapp_this) loc_axioms
   1.789 +    #-> (fn (name_axclass, (_, ax_axioms)) =>
   1.790 +          fold (add_global_constraint name_axclass) mapp_this
   1.791 +    #> add_class_data ((name_axclass, supclasses), (name_locale, map (apsnd fst) mapp_this,
   1.792 +          map (fst o fst) loc_axioms))
   1.793 +    #> prove_interpretation (Logic.const_of_class bname, [])
   1.794 +          (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd (mapp_sup @ mapp_this)))
   1.795 +          ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   1.796 +    ))))) #> pair name_locale)
   1.797 +  end;
   1.798 +
   1.799 +in
   1.800 +
   1.801 +val class_e = gen_class (Locale.add_locale false) read_class;
   1.802 +val class = gen_class (Locale.add_locale_i false) certify_class;
   1.803  
   1.804  end; (*local*)
   1.805  
   1.806 @@ -502,14 +533,12 @@
   1.807    |> ProofContext.theory_of;
   1.808  
   1.809  (*FIXME very ad-hoc, needs proper locale interface*)
   1.810 -fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
   1.811 +fun instance_sort' do_proof (class, sort) theory =
   1.812    let
   1.813 -    val class = prep_class theory raw_class;
   1.814 -    val sort = prep_sort theory raw_sort;
   1.815      val loc_name = (#locale o the_class_data theory) class;
   1.816      val loc_expr =
   1.817        (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort;
   1.818 -    val const_names = (map (NameSpace.base o fst o snd)
   1.819 +    val const_names = (map (NameSpace.base o snd)
   1.820        o maps (#consts o the_class_data theory)
   1.821        o the_ancestry theory) [class];
   1.822      fun get_thms thy =
   1.823 @@ -532,20 +561,68 @@
   1.824      |> do_proof after_qed (loc_name, loc_expr)
   1.825    end;
   1.826  
   1.827 -fun instance_sort' do_proof = gen_instance_sort read_class read_sort do_proof;
   1.828 -fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof;
   1.829 -val setup_proof = Locale.interpretation_in_locale o ProofContext.theory;
   1.830 -val tactic_proof = prove_interpretation_in;
   1.831 +val prove_instance_sort = instance_sort' o prove_interpretation_in;
   1.832 +
   1.833 +fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   1.834 +  let
   1.835 +    val class = prep_class theory raw_class;
   1.836 +    val sort = prep_sort theory raw_sort;
   1.837 +  in if is_class theory class andalso forall (is_class theory) sort then
   1.838 +    theory
   1.839 +    |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   1.840 +  else case sort
   1.841 +   of [class'] =>
   1.842 +        theory
   1.843 +        |> axclass_instance_sort (class, class')
   1.844 +    | _ => error ("Exactly one class expected: " ^ Sign.string_of_sort theory sort)
   1.845 +  end;
   1.846  
   1.847  in
   1.848  
   1.849 -val instance_sort = instance_sort' setup_proof;
   1.850 -val instance_sort_i = instance_sort_i' setup_proof;
   1.851 -val prove_instance_sort = instance_sort_i' o tactic_proof;
   1.852 +val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort;
   1.853 +val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
   1.854 +val prove_instance_sort = prove_instance_sort;
   1.855  
   1.856  end; (* local *)
   1.857  
   1.858  
   1.859 +(** experimental class target **)
   1.860 +
   1.861 +fun export_typ thy loc =
   1.862 +  let
   1.863 +    val class = loc (*FIXME*);
   1.864 +    val (v, _) = AxClass.params_of_class thy class;
   1.865 +  in
   1.866 +    Term.map_type_tfree (fn var as (w, sort) =>
   1.867 +      if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   1.868 +        (sort, [class])) else TFree var)
   1.869 +  end;
   1.870 +
   1.871 +fun export_def thy loc =
   1.872 +  let
   1.873 +    val class = loc (*FIXME*);
   1.874 +    val consts = the_parm_map thy class;
   1.875 +    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.876 +      if w = AxClass.param_tyvarname then TFree (w, Sorts.inter_sort (Sign.classes_of thy)
   1.877 +        (sort, [class])) else TFree var)
   1.878 +    fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v
   1.879 +         of SOME c_ty => Const c_ty
   1.880 +          | NONE => t)
   1.881 +      | subst t = t;
   1.882 +  in
   1.883 +    Term.map_aterms subst #> map_types subst_typ
   1.884 +  end;
   1.885 +
   1.886 +fun export_thm thy loc =
   1.887 +  let
   1.888 +    val class = loc (*FIXME*);
   1.889 +    val thms = (#defs o the_class_data thy) class;
   1.890 +  in
   1.891 +    MetaSimplifier.rewrite_rule thms
   1.892 +  end;
   1.893 +
   1.894 +
   1.895 +
   1.896  (** toplevel interface **)
   1.897  
   1.898  local
   1.899 @@ -557,11 +634,6 @@
   1.900  
   1.901  val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
   1.902  
   1.903 -fun wrap_add_instance_sort (class, sort) thy =
   1.904 -  (if forall (is_some o lookup_class_data thy) (Sign.read_sort thy sort)
   1.905 -    andalso (is_some o lookup_class_data thy) (Sign.intern_class thy class)
   1.906 -  then instance_sort else axclass_instance_sort) (class, sort) thy;
   1.907 -
   1.908  val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   1.909  val class_bodyP = P.!!! (Scan.repeat1 P.locale_element);
   1.910  
   1.911 @@ -579,14 +651,14 @@
   1.912      -- P.opt_begin
   1.913      >> (fn ((bname, (supclasses, elems)), begin) =>
   1.914          Toplevel.begin_local_theory begin
   1.915 -          (class bname supclasses elems #-> TheoryTarget.begin true)));
   1.916 +          (class_e bname supclasses elems #-> TheoryTarget.begin true)));
   1.917  
   1.918  val instanceP =
   1.919    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   1.920 -      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort
   1.921 +      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   1.922 +           >> instance_sort_e
   1.923        || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
   1.924 -           >> (fn ([((tyco, asorts), sort)], []) => axclass_instance_arity I [(tyco, asorts, sort)]
   1.925 -                | (arities, defs) => instance_arity arities defs)
   1.926 +           >> (fn (arities, defs) => instance_arity_e arities defs)
   1.927      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   1.928  
   1.929  val print_classesP =