moved intro_classes from AxClass to ClassPackage
authorhaftmann
Mon Feb 20 11:37:18 2006 +0100 (2006-02-20)
changeset 191104bda27adcd2e
parent 19109 9804aa8d5756
child 19111 1f6112de1d0f
moved intro_classes from AxClass to ClassPackage
src/HOLCF/pcpodef_package.ML
src/Provers/classical.ML
src/Pure/Tools/class_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOLCF/pcpodef_package.ML	Sun Feb 19 22:40:18 2006 +0100
     1.2 +++ b/src/HOLCF/pcpodef_package.ML	Mon Feb 20 11:37:18 2006 +0100
     1.3 @@ -98,12 +98,12 @@
     1.4      fun make_po tac thy =
     1.5        thy
     1.6        |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
     1.7 -      |>> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.sq_ord"])
     1.8 -           (AxClass.intro_classes_tac [])
     1.9 +      |>> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Porder.sq_ord"])
    1.10 +           (ClassPackage.intro_classes_tac [])
    1.11        |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap)
    1.12        |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) =>
    1.13             thy'
    1.14 -           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.po"])
    1.15 +           |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Porder.po"])
    1.16               (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
    1.17             |> rpair (type_definition, less_definition, set_def));
    1.18      
    1.19 @@ -113,7 +113,7 @@
    1.20          val cpo_thms = [type_def, less_def, admissible'];
    1.21          val (_, theory') =
    1.22            theory
    1.23 -          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
    1.24 +          |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Pcpo.cpo"])
    1.25              (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
    1.26            |> Theory.add_path name
    1.27            |> PureThy.add_thms
    1.28 @@ -132,7 +132,7 @@
    1.29          val pcpo_thms = [type_def, less_def, UUmem'];
    1.30          val (_, theory') =
    1.31            theory
    1.32 -          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
    1.33 +          |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Pcpo.pcpo"])
    1.34              (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
    1.35            |> Theory.add_path name
    1.36            |> PureThy.add_thms
     2.1 --- a/src/Provers/classical.ML	Sun Feb 19 22:40:18 2006 +0100
     2.2 +++ b/src/Provers/classical.ML	Mon Feb 20 11:37:18 2006 +0100
     2.3 @@ -1029,7 +1029,7 @@
     2.4  
     2.5  fun default_tac rules ctxt cs facts =
     2.6    HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
     2.7 -  AxClass.default_intro_classes_tac facts;
     2.8 +  ClassPackage.default_intro_classes_tac facts;
     2.9  
    2.10  in
    2.11    val rule = METHOD_CLASET' o rule_tac;
     3.1 --- a/src/Pure/Tools/class_package.ML	Sun Feb 19 22:40:18 2006 +0100
     3.2 +++ b/src/Pure/Tools/class_package.ML	Mon Feb 20 11:37:18 2006 +0100
     3.3 @@ -12,17 +12,29 @@
     3.4    val add_class_i: bstring -> class list -> Element.context_i list -> theory
     3.5      -> ProofContext.context * theory
     3.6    val add_instance_arity: (xstring * string list) * string
     3.7 -    -> ((bstring * string) * Attrib.src list) list
     3.8 +    -> ((bstring * Attrib.src list) * string) list
     3.9      -> theory -> Proof.state
    3.10    val add_instance_arity_i: (string * sort list) * sort
    3.11 -    -> ((bstring * term) * attribute list) list
    3.12 +    -> ((bstring * attribute list) * term) list
    3.13      -> theory -> Proof.state
    3.14 -  val add_classentry: class -> xstring list -> theory -> theory
    3.15 -  val add_classinsts: class -> xstring list -> theory -> theory
    3.16 +  val prove_instance_arity: tactic -> (xstring * string list) * string
    3.17 +    -> ((bstring * Attrib.src list) * string) list
    3.18 +    -> theory -> theory
    3.19 +  val prove_instance_arity_i: tactic -> (string * sort list) * sort
    3.20 +    -> ((bstring * attribute list) * term) list
    3.21 +    -> theory -> theory
    3.22 +  val add_instance_sort: string * string -> theory -> Proof.state
    3.23 +  val add_instance_sort_i: class * sort -> theory -> Proof.state
    3.24 +  val prove_instance_sort: tactic -> string * string -> theory -> theory
    3.25 +  val prove_instance_sort_i: tactic -> class * sort -> theory -> theory
    3.26  
    3.27 -  val intern_class: theory -> xstring -> string
    3.28 -  val extern_class: theory -> string -> xstring
    3.29 +  val intern_class: theory -> xstring -> class
    3.30 +  val intern_sort: theory -> sort -> sort
    3.31 +  val extern_class: theory -> class -> xstring
    3.32 +  val extern_sort: theory -> sort -> sort
    3.33    val certify_class: theory -> class -> class
    3.34 +  val certify_sort: theory -> sort -> sort
    3.35 +  val read_sort: theory -> string -> sort
    3.36    val operational_sort_of: theory -> sort -> sort
    3.37    val the_superclasses: theory -> class -> class list
    3.38    val the_consts_sign: theory -> class -> string * (string * typ) list
    3.39 @@ -30,7 +42,10 @@
    3.40    val the_instances: theory -> class -> (string * string) list
    3.41    val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
    3.42    val get_classtab: theory -> (string list * (string * string) list) Symtab.table
    3.43 +
    3.44    val print_classes: theory -> unit
    3.45 +  val intro_classes_tac: thm list -> tactic
    3.46 +  val default_intro_classes_tac: thm list -> tactic
    3.47  
    3.48    type sortcontext = (string * sort) list
    3.49    datatype classlookup = Instance of (class * string) * classlookup list list
    3.50 @@ -47,32 +62,32 @@
    3.51  (* theory data *)
    3.52  
    3.53  type class_data = {
    3.54 -  superclasses: class list,
    3.55    name_locale: string,
    3.56    name_axclass: string,
    3.57 +  intro: thm option,
    3.58    var: string,
    3.59    consts: (string * typ) list,
    3.60 -  insts: (string * string) list
    3.61 +  insts: (string * string) list (* [type constructor ~> theory name] *)
    3.62  };
    3.63  
    3.64  structure ClassData = TheoryDataFun (
    3.65    struct
    3.66      val name = "Pure/classes";
    3.67 -    type T = class_data Symtab.table * (class Symtab.table * string Symtab.table);
    3.68 -    val empty = (Symtab.empty, (Symtab.empty, Symtab.empty));
    3.69 +    type T = class_data Graph.T * (class Symtab.table * string Symtab.table);
    3.70 +    val empty = (Graph.empty, (Symtab.empty, Symtab.empty));
    3.71      val copy = I;
    3.72      val extend = I;
    3.73      fun merge _ ((t1, (c1, l1)), (t2, (c2, l2)))=
    3.74 -      (Symtab.merge (op =) (t1, t2),
    3.75 +      (Graph.merge (op =) (t1, t2),
    3.76         (Symtab.merge (op =) (c1, c2), Symtab.merge (op =) (l1, l2)));
    3.77 -    fun print thy (tab, _) =
    3.78 +    fun print thy (gr, _) =
    3.79        let
    3.80 -        fun pretty_class (name, {superclasses, name_locale, name_axclass, var, consts, insts}) =
    3.81 +        fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts, insts}) =
    3.82            (Pretty.block o Pretty.fbreaks) [
    3.83              Pretty.str ("class " ^ name ^ ":"),
    3.84              (Pretty.block o Pretty.fbreaks) (
    3.85                Pretty.str "superclasses: "
    3.86 -              :: map Pretty.str superclasses
    3.87 +              :: (map Pretty.str o Graph.imm_succs gr) name
    3.88              ),
    3.89              Pretty.str ("locale: " ^ name_locale),
    3.90              Pretty.str ("axclass: " ^ name_axclass),
    3.91 @@ -87,7 +102,8 @@
    3.92              )
    3.93            ]
    3.94        in
    3.95 -        (Pretty.writeln o Pretty.chunks o map pretty_class o Symtab.dest) tab
    3.96 +        (Pretty.writeln o Pretty.chunks o map (pretty_class gr)
    3.97 +          o AList.make (Graph.get_node gr) o Library.flat o Graph.strong_conn) gr
    3.98        end;
    3.99    end
   3.100  );
   3.101 @@ -98,7 +114,7 @@
   3.102  
   3.103  (* queries *)
   3.104  
   3.105 -val lookup_class_data = Symtab.lookup o fst o ClassData.get;
   3.106 +val lookup_class_data = try o Graph.get_node o fst o ClassData.get;
   3.107  val lookup_const_class = Symtab.lookup o fst o snd o ClassData.get;
   3.108  val lookup_locale_class = Symtab.lookup o snd o snd o ClassData.get;
   3.109  
   3.110 @@ -115,10 +131,10 @@
   3.111  fun operational_sort_of thy sort =
   3.112    let
   3.113      val classes = Sign.classes_of thy;
   3.114 -    fun get_sort cls =
   3.115 -      if is_class thy cls
   3.116 -      then [cls]
   3.117 -      else operational_sort_of thy (Sorts.superclasses classes cls);
   3.118 +    fun get_sort class =
   3.119 +      if is_class thy class
   3.120 +      then [class]
   3.121 +      else operational_sort_of thy (Sorts.superclasses classes class);
   3.122    in
   3.123      map get_sort sort
   3.124      |> Library.flat
   3.125 @@ -133,6 +149,13 @@
   3.126    else
   3.127      error ("no syntactic class: " ^ class);
   3.128  
   3.129 +fun get_superclass_derivation thy (subclass, superclass) =
   3.130 +  if subclass = superclass
   3.131 +    then SOME [subclass]
   3.132 +    else case Graph.find_paths ((fst o ClassData.get) thy) (subclass, superclass)
   3.133 +      of [] => NONE
   3.134 +       | (p::_) => (SOME o filter (is_class thy)) p;
   3.135 +
   3.136  fun the_ancestry thy classes =
   3.137    let
   3.138      fun ancestry class anc =
   3.139 @@ -141,6 +164,11 @@
   3.140        |> fold ancestry (the_superclasses thy class);
   3.141    in fold ancestry classes [] end;
   3.142  
   3.143 +fun the_intros thy =
   3.144 +  let
   3.145 +    val gr = (fst o ClassData.get) thy;
   3.146 +  in (List.mapPartial (#intro o Graph.get_node gr) o Graph.keys) gr end;
   3.147 +
   3.148  fun subst_clsvar v ty_subst =
   3.149    map_type_tfree (fn u as (w, _) =>
   3.150      if w = v then ty_subst else TFree u);
   3.151 @@ -175,7 +203,7 @@
   3.152    in (vsorts, inst_signs) end;
   3.153  
   3.154  fun get_classtab thy =
   3.155 -  Symtab.fold
   3.156 +  Graph.fold_nodes
   3.157      (fn (class, { consts = consts, insts = insts, ... }) =>
   3.158        Symtab.update_new (class, (map fst consts, insts)))
   3.159         ((fst o ClassData.get) thy) Symtab.empty;
   3.160 @@ -183,17 +211,18 @@
   3.161  
   3.162  (* updaters *)
   3.163  
   3.164 -fun add_class_data (class, (superclasses, name_locale, name_axclass, classvar, consts)) =
   3.165 +fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
   3.166    ClassData.map (fn (classtab, (consttab, loctab)) => (
   3.167      classtab
   3.168 -    |> Symtab.update (class, {
   3.169 -         superclasses = superclasses,
   3.170 +    |> Graph.new_node (class, {
   3.171           name_locale = name_locale,
   3.172           name_axclass = name_axclass,
   3.173 -         var = classvar,
   3.174 +         intro = intro,
   3.175 +         var = var,
   3.176           consts = consts,
   3.177           insts = []
   3.178 -       }),
   3.179 +       })
   3.180 +    |> fold (curry Graph.add_edge_acyclic class) superclasses,
   3.181      (consttab
   3.182      |> fold (fn (c, _) => Symtab.update (c, class)) consts,
   3.183      loctab
   3.184 @@ -201,12 +230,12 @@
   3.185    ));
   3.186  
   3.187  fun add_inst_data (class, inst) =
   3.188 -  (ClassData.map o apfst o Symtab.map_entry class)
   3.189 -    (fn {superclasses, name_locale, name_axclass, var, consts, insts}
   3.190 +  (ClassData.map o apfst o Graph.map_node class)
   3.191 +    (fn {name_locale, name_axclass, intro, var, consts, insts}
   3.192        => {
   3.193 -           superclasses = superclasses,
   3.194             name_locale = name_locale,
   3.195             name_axclass = name_axclass,
   3.196 +           intro = intro,
   3.197             var = var,
   3.198             consts = consts,
   3.199             insts = insts @ [inst]
   3.200 @@ -216,36 +245,118 @@
   3.201  (* name handling *)
   3.202  
   3.203  fun certify_class thy class =
   3.204 -  (the_class_data thy class; class);
   3.205 +  (fn class => (the_class_data thy class; class)) (Sign.certify_class thy class);
   3.206 +
   3.207 +fun certify_sort thy sort =
   3.208 +  map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort);
   3.209 +
   3.210 +fun intern_class thy =
   3.211 +  certify_class thy o Sign.intern_class thy;
   3.212 +
   3.213 +fun intern_sort thy =
   3.214 +  certify_sort thy o Sign.intern_sort thy;
   3.215 +
   3.216 +fun extern_class thy =
   3.217 +  Sign.extern_class thy o certify_class thy;
   3.218 +
   3.219 +fun extern_sort thy =
   3.220 +  Sign.extern_sort thy o certify_sort thy;
   3.221  
   3.222 -fun intern_class thy raw_class =
   3.223 -  certify_class thy (Sign.intern_class thy raw_class);
   3.224 +fun read_sort thy =
   3.225 +  certify_sort thy o Sign.read_sort thy;
   3.226 +
   3.227 +
   3.228 +(* tactics and methods *)
   3.229 +
   3.230 +fun class_loc_axms thy =
   3.231 +  AxClass.class_axms thy @ the_intros thy;
   3.232  
   3.233 -fun extern_class thy class =
   3.234 -  Sign.extern_class thy (certify_class thy class);
   3.235 +fun intro_classes_tac facts st =
   3.236 +  (ALLGOALS (Method.insert_tac facts THEN'
   3.237 +      REPEAT_ALL_NEW (resolve_tac (class_loc_axms (Thm.theory_of_thm st))))
   3.238 +    THEN Tactic.distinct_subgoals_tac) st;
   3.239 +
   3.240 +fun default_intro_classes_tac [] = intro_classes_tac []
   3.241 +  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   3.242 +
   3.243 +fun default_tac rules ctxt facts =
   3.244 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   3.245 +    default_intro_classes_tac facts;
   3.246  
   3.247  
   3.248  (* classes and instances *)
   3.249  
   3.250  local
   3.251  
   3.252 -fun intern_expr thy (Locale.Locale xname) = Locale.Locale (Locale.intern thy xname)
   3.253 -  | intern_expr thy (Locale.Merge exprs) = Locale.Merge (map (intern_expr thy) exprs)
   3.254 -  | intern_expr thy (Locale.Rename (expr, xs)) = Locale.Rename (intern_expr thy expr, xs);
   3.255 +fun intro_incr thy name expr =
   3.256 +  let
   3.257 +    fun fish_thm basename =
   3.258 +      try (PureThy.get_thm thy) ((Name o NameSpace.append basename) "intro");
   3.259 +  in if expr = Locale.empty
   3.260 +    then fish_thm name
   3.261 +    else fish_thm (name ^ "_axioms")
   3.262 +  end;
   3.263 +
   3.264 +fun add_locale opn name expr body thy =
   3.265 +  thy
   3.266 +  |> Locale.add_locale opn name expr body
   3.267 +  ||>> `(fn thy => intro_incr thy name expr)
   3.268 +  |-> (fn (ctxt, intro) => pair ((Sign.full_name thy name, intro), ctxt));
   3.269 +
   3.270 +fun add_locale_i opn name expr body thy =
   3.271 +  thy
   3.272 +  |> Locale.add_locale_i opn name expr body
   3.273 +  ||>> `(fn thy => intro_incr thy name expr)
   3.274 +  |-> (fn (ctxt, intro) => pair ((name, intro), ctxt));
   3.275  
   3.276 -fun gen_add_class add_locale prep_expr eval_expr do_proof bname raw_expr raw_body thy =
   3.277 +fun add_axclass_i (name, supsort) axs thy =
   3.278 +  let
   3.279 +    fun rearrange_axioms ((name, atts), ts) =
   3.280 +      map (rpair atts o pair "") ts
   3.281 +  in
   3.282 +    thy
   3.283 +    |> AxClass.add_axclass_i (name, supsort)
   3.284 +          ((Library.flat o map rearrange_axioms) axs)
   3.285 +    |-> (fn { intro, axioms } =>
   3.286 +              pair (Sign.full_name thy name, (intro, axioms)))
   3.287 +  end;
   3.288 +
   3.289 +fun prove_interpretation_i (prfx, atts) expr insts tac thy =
   3.290    let
   3.291 -    val ((import_asms, supclasses), locexpr) = (eval_expr thy o prep_expr thy) raw_expr;
   3.292 +    fun ad_hoc_term NONE = NONE
   3.293 +      | ad_hoc_term (SOME (Const (c, ty))) =
   3.294 +          let
   3.295 +            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
   3.296 +            val s = c ^ "::" ^ Pretty.output p;
   3.297 +            val _ = writeln s;
   3.298 +          in SOME s end
   3.299 +      | ad_hoc_term (SOME t) =
   3.300 +          let
   3.301 +            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
   3.302 +            val s = Pretty.output p;
   3.303 +            val _ = writeln s;
   3.304 +          in SOME s end;
   3.305 +  in
   3.306 +    thy
   3.307 +    |> Locale.interpretation (prfx, atts) expr (map ad_hoc_term insts)
   3.308 +    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   3.309 +    |-> (fn _ => I)
   3.310 +  end;
   3.311 +
   3.312 +fun gen_add_class add_locale prep_class bname raw_supclasses raw_elems thy =
   3.313 +  let
   3.314 +    val supclasses = map (prep_class thy) raw_supclasses;
   3.315      val supsort =
   3.316        supclasses
   3.317        |> map (#name_axclass o the_class_data thy)
   3.318        |> Sorts.certify_sort (Sign.classes_of thy)
   3.319        |> null ? K (Sign.defaultS thy);
   3.320 -    val _ = writeln ("got sort: " ^ Sign.string_of_sort thy supsort);
   3.321 -    val _ = writeln ("got asms: " ^ (cat_lines o map (Sign.string_of_term thy) o Library.flat o map (snd o fst)) import_asms);
   3.322 -    val supcs = (Library.flat o map (snd o the_consts_sign thy) o the_ancestry thy) supclasses;
   3.323 -    fun mk_c_lookup c_global supcs c_adds =
   3.324 -      map2 (fn ((c, _), _) => pair c) c_global supcs @ c_adds;
   3.325 +    val supcs = (Library.flat o map (snd o the_consts_sign thy) o the_ancestry thy)
   3.326 +      supclasses;
   3.327 +    val expr = if null supclasses
   3.328 +      then Locale.empty
   3.329 +      else
   3.330 +       (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses;
   3.331      fun extract_tyvar_consts thy name_locale =
   3.332        let
   3.333          fun extract_tyvar_name thy tys =
   3.334 @@ -256,135 +367,222 @@
   3.335                      else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
   3.336                 | [] => error ("no class type variable")
   3.337                 | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
   3.338 -        val raw_consts =
   3.339 +        val consts1 =
   3.340            Locale.parameters_of thy name_locale
   3.341            |> map (apsnd Syntax.unlocalize_mixfix)
   3.342 -          |> Library.chop (length supcs);
   3.343 -        val v = (extract_tyvar_name thy o map (snd o fst) o op @) raw_consts;
   3.344 -        fun subst_ty cs =
   3.345 -          map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) cs;
   3.346 -        val consts = (subst_ty (fst raw_consts), subst_ty (snd raw_consts));
   3.347 -        (*val _ = (writeln o commas o map (fst o fst)) (fst consts);
   3.348 -        val _ = (writeln o commas o map (fst o fst)) (snd consts);*)
   3.349 -      in (v, consts) end;
   3.350 -    fun add_global_const v ((c, ty), syn) thy =
   3.351 +        val v = (extract_tyvar_name thy o map (snd o fst)) consts1;
   3.352 +        val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
   3.353 +      in (v, Library.chop (length supcs) consts2) end;
   3.354 +    fun add_consts v raw_cs_sup raw_cs_this thy =
   3.355 +      let
   3.356 +        val mapp_sub = map2 (fn ((c, _), _) => pair c) raw_cs_sup supcs
   3.357 +        fun add_global_const ((c, ty), syn) thy =
   3.358 +          thy
   3.359 +          |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
   3.360 +          |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
   3.361 +      in
   3.362 +        thy
   3.363 +        |> fold_map add_global_const raw_cs_this
   3.364 +        |-> (fn mapp_this => pair (mapp_sub @ mapp_this, map snd mapp_this))
   3.365 +      end;
   3.366 +    fun extract_assumes thy name_locale cs_mapp =
   3.367 +      let
   3.368 +        val subst_assume =
   3.369 +          map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
   3.370 +                       | t => t)
   3.371 +        fun prep_asm ((name, atts), ts) =
   3.372 +          ((name, map (Attrib.attribute thy) atts), map subst_assume ts)
   3.373 +      in
   3.374 +        (map prep_asm o Locale.local_asms_of thy) name_locale
   3.375 +      end;
   3.376 +    fun add_global_constraint v class (c, ty) thy =
   3.377        thy
   3.378 -      |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
   3.379 -      |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
   3.380 -    fun subst_assume c_lookup renaming =
   3.381 -      map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) c_lookup o perhaps (AList.lookup (op =) renaming)) c, ty)
   3.382 -                   | t => t)
   3.383 -    fun extract_assumes thy name_locale c_lookup =
   3.384 -      map (rpair []) (Locale.local_asms_of thy name_locale) @ import_asms
   3.385 -      |> map (fn (((name, atts), ts), renaming) => ((name, map (Attrib.attribute thy) atts), (map (subst_assume c_lookup renaming)) ts));
   3.386 -    fun rearrange_assumes ((name, atts), ts) =
   3.387 -      map (rpair atts o pair "") ts
   3.388 -    fun add_global_constraint v class (_, (c, ty)) thy = thy
   3.389 -      |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
   3.390 -    fun ad_hoc_const thy class v (c, ty) =
   3.391 -      let
   3.392 -        val ty' = subst_clsvar v (TFree (v, [class])) ty;
   3.393 -        val s_ty = setmp print_mode [] (setmp show_types true (setmp show_sorts true (Sign.string_of_typ thy))) ty';
   3.394 -        val s = c ^ "::" ^ enclose "(" ")" s_ty;
   3.395 -        val _ = writeln ("our constant: " ^ s);
   3.396 -      in SOME s end;
   3.397 -    fun interpret name_locale name_axclass v cs ax_axioms thy =
   3.398 -      thy
   3.399 -      |> Locale.interpretation (NameSpace.base name_locale, [])
   3.400 -           (Locale.Locale name_locale) (map (ad_hoc_const thy name_axclass v) cs)
   3.401 -      |> do_proof ax_axioms;
   3.402 +      |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TVar ((v, 0), [class])) ty));
   3.403 +    fun mk_const thy class v (c, ty) =
   3.404 +      Const (c, subst_clsvar v (TFree (v, [class])) ty);
   3.405    in
   3.406      thy
   3.407 -    |> add_locale bname locexpr raw_body
   3.408 -    |-> (fn ctxt =>
   3.409 -       `(fn thy => Locale.intern thy bname)
   3.410 -    #-> (fn name_locale =>
   3.411 +    |> add_locale bname expr raw_elems
   3.412 +    |-> (fn ((name_locale, intro), ctxt) =>
   3.413            `(fn thy => extract_tyvar_consts thy name_locale)
   3.414 -    #-> (fn (v, (c_global, c_defs)) =>
   3.415 -          fold_map (add_global_const v) c_defs
   3.416 -    #-> (fn c_adds =>
   3.417 -       `(fn thy => extract_assumes thy name_locale (mk_c_lookup c_global supcs c_adds))
   3.418 -    #-> (fn assumes =>
   3.419 -          AxClass.add_axclass_i (bname, supsort) ((Library.flat o map rearrange_assumes) assumes))
   3.420 -    #-> (fn { axioms = ax_axioms : thm list, ...} =>
   3.421 -          `(fn thy => Sign.intern_class thy bname)
   3.422 -    #-> (fn name_axclass =>
   3.423 -          fold (add_global_constraint v name_axclass) c_adds
   3.424 -    #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, map snd c_adds))
   3.425 -    #> interpret name_locale name_axclass v (supcs @ map snd c_adds) ax_axioms
   3.426 -    ))))))
   3.427 +    #-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
   3.428 +          add_consts v raw_cs_sup raw_cs_this
   3.429 +    #-> (fn (cs_map, cs_this) =>
   3.430 +          `(fn thy => extract_assumes thy name_locale cs_map)
   3.431 +    #-> (fn loc_axioms =>
   3.432 +          add_axclass_i (bname, supsort) loc_axioms
   3.433 +    #-> (fn (name_axclass, (_, ax_axioms)) =>
   3.434 +          fold (add_global_constraint v name_axclass) cs_this
   3.435 +    #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, intro, v, cs_this))
   3.436 +    #> prove_interpretation_i (NameSpace.base name_locale, [])
   3.437 +          (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (supcs @ cs_this))
   3.438 +          ((ALLGOALS o resolve_tac) ax_axioms)
   3.439 +    #> pair ctxt
   3.440 +    )))))
   3.441    end;
   3.442  
   3.443 -fun eval_expr_supclasses thy [] = (([], []), Locale.empty)
   3.444 -  | eval_expr_supclasses thy supclasses =
   3.445 -      (([], supclasses),
   3.446 -        (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses);
   3.447 -
   3.448  in
   3.449  
   3.450 -val add_class = gen_add_class (Locale.add_locale true) (map o intern_class)
   3.451 -  eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
   3.452 -val add_class_i = gen_add_class (Locale.add_locale_i true) (map o certify_class)
   3.453 -  eval_expr_supclasses (fn ax_axioms => Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE));
   3.454 -val add_class_exp = gen_add_class (Locale.add_locale true) (map o intern_class)
   3.455 -  eval_expr_supclasses (K I);
   3.456 +val add_class = gen_add_class (add_locale true) intern_class;
   3.457 +val add_class_i = gen_add_class (add_locale_i true) certify_class;
   3.458  
   3.459  end; (* local *)
   3.460  
   3.461 -fun gen_instance_arity prep_arity add_defs tap_def raw_arity raw_defs thy =
   3.462 +local
   3.463 +
   3.464 +fun lift_local_theory_yield f thy =
   3.465 +  thy
   3.466 +  |> LocalTheory.init NONE
   3.467 +  |> f
   3.468 +  ||>> LocalTheory.exit
   3.469 +  |-> (fn (x, _) => pair x);
   3.470 +
   3.471 +fun gen_add_defs_overloaded prep_att tap_def add_defs tyco raw_defs thy =
   3.472    let
   3.473 -    val pp = Sign.pp thy;
   3.474 -    val arity as (tyco, asorts, sort) = prep_arity thy ((fn ((x, y), z) => (x, y, z)) raw_arity);
   3.475 +    fun invent_name raw_t =
   3.476 +      let
   3.477 +        val t = tap_def thy raw_t;
   3.478 +        val c = (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals) t;
   3.479 +      in
   3.480 +        Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco)
   3.481 +      end;
   3.482 +    fun prep_def (_, (("", a), t)) =
   3.483 +          let
   3.484 +            val n = invent_name t
   3.485 +          in ((n, t), map (prep_att thy) a) end
   3.486 +      | prep_def (_, ((n, a), t)) =
   3.487 +          ((n, t), map (prep_att thy) a);
   3.488 +  in
   3.489 +    thy
   3.490 +    |> add_defs true (map prep_def raw_defs)
   3.491 +  end;
   3.492 +
   3.493 +val add_defs_overloaded = gen_add_defs_overloaded Attrib.attribute Sign.read_term PureThy.add_defs;
   3.494 +val add_defs_overloaded_i = gen_add_defs_overloaded (K I) (K I) PureThy.add_defs_i;
   3.495 +
   3.496 +fun gen_instance_arity prep_arity add_defs tap_def do_proof raw_arity raw_defs theory =
   3.497 +  let
   3.498 +    val pp = Sign.pp theory;
   3.499 +    val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
   3.500      val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
   3.501 -    fun get_c_req class =
   3.502 +    fun get_classes thy tyco sort =
   3.503        let
   3.504 -        val data = the_class_data thy class;
   3.505 +        fun get class classes =
   3.506 +          if AList.defined (op =) ((#insts o the_class_data thy) class) tyco
   3.507 +            then classes
   3.508 +            else classes
   3.509 +              |> cons class
   3.510 +              |> fold get (the_superclasses thy class)
   3.511 +      in fold get sort [] end;
   3.512 +    val classes = get_classes theory tyco sort;
   3.513 +    val _ = if null classes then error ("already instantiated") else ();
   3.514 +    fun get_consts class =
   3.515 +      let
   3.516 +        val data = the_class_data theory class;
   3.517          val subst_ty = map_type_tfree (fn (var as (v, _)) =>
   3.518            if #var data = v then ty_inst else TFree var)
   3.519        in (map (apsnd subst_ty) o #consts) data end;
   3.520 -    val c_req = (Library.flat o map get_c_req) sort;
   3.521 -    fun get_remove_contraint c thy = thy
   3.522 -      |> Sign.add_const_constraint_i (c, NONE)
   3.523 -      |> pair (c, SOME (Type.unvarifyT (Sign.the_const_constraint thy c)));
   3.524 +    val cs = (Library.flat o map get_consts) classes;
   3.525 +    fun get_remove_contraint c thy =
   3.526 +      let
   3.527 +        val ty = Sign.the_const_constraint thy c;
   3.528 +      in
   3.529 +        thy
   3.530 +        |> Sign.add_const_constraint_i (c, NONE)
   3.531 +        |> pair (c, ty)
   3.532 +      end;
   3.533      fun check_defs raw_defs c_req thy =
   3.534        let
   3.535 -        val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
   3.536 +        val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy;
   3.537          fun get_c raw_def =
   3.538 -          (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
   3.539 +          (fst o Sign.cert_def pp o tap_def thy' o snd) raw_def;
   3.540          val c_given = map get_c raw_defs;
   3.541 -(*         spec_opt_name   *)
   3.542          fun eq_c ((c1, ty1), (c2, ty2)) =
   3.543            let
   3.544              val ty1' = Type.varifyT ty1;
   3.545              val ty2' = Type.varifyT ty2;
   3.546            in
   3.547              c1 = c2
   3.548 -            andalso Sign.typ_instance thy (ty1', ty2')
   3.549 -            andalso Sign.typ_instance thy (ty2', ty1')
   3.550 +            andalso Sign.typ_instance thy' (ty1', ty2')
   3.551 +            andalso Sign.typ_instance thy' (ty2', ty1')
   3.552            end;
   3.553          val _ = case fold (remove eq_c) c_req c_given
   3.554           of [] => ()
   3.555            | cs => error ("superfluous definition(s) given for "
   3.556 -                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
   3.557 -        (*val _ = case fold (remove eq_c) c_given c_req
   3.558 -      of [] => ()
   3.559 +                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy' ty))) cs);
   3.560 +        val _ = case fold (remove eq_c) c_given c_req
   3.561 +         of [] => ()
   3.562            | cs => error ("no definition(s) given for "
   3.563 -                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*)
   3.564 +                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy' ty))) cs);
   3.565        in thy end;
   3.566 -    fun after_qed cs =
   3.567 -      fold Sign.add_const_constraint_i cs
   3.568 -      #> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
   3.569 +    fun mangle_alldef_name tyco sort =
   3.570 +      Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);
   3.571 +    fun note_all tyco sort thms thy =
   3.572 +      thy
   3.573 +      |> PureThy.note_thmss_i PureThy.internalK [((mangle_alldef_name tyco sort, []), [(thms, [])])]
   3.574 +      |> snd;
   3.575 +    fun after_qed cs thy =
   3.576 +      thy
   3.577 +      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
   3.578 +      |> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
   3.579    in
   3.580 -    thy
   3.581 -    |> tap (fn thy => check_defs raw_defs c_req thy)
   3.582 -    |> fold_map get_remove_contraint (map fst c_req)
   3.583 -    ||> add_defs (true, raw_defs)
   3.584 -    |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
   3.585 +    theory
   3.586 +    |> check_defs raw_defs cs
   3.587 +    |> fold_map get_remove_contraint (map fst cs)
   3.588 +    ||>> add_defs tyco (map (pair NONE) raw_defs)
   3.589 +    |-> (fn (cs, defnames) => note_all tyco sort defnames #> pair cs)
   3.590 +    |-> (fn cs => do_proof (after_qed cs) arity)
   3.591    end;
   3.592  
   3.593 -val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
   3.594 -val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
   3.595 +fun instance_arity do_proof = gen_instance_arity AxClass.read_arity add_defs_overloaded
   3.596 +  (fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof;
   3.597 +fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity add_defs_overloaded_i
   3.598 +  (K I) do_proof;
   3.599 +val setup_proof = AxClass.instance_arity_i;
   3.600 +fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i after_qed arity tac;
   3.601 +
   3.602 +in
   3.603 +
   3.604 +val add_instance_arity = instance_arity setup_proof;
   3.605 +val add_instance_arity_i = instance_arity_i setup_proof;
   3.606 +val prove_instance_arity = instance_arity o tactic_proof;
   3.607 +val prove_instance_arity_i = instance_arity_i o tactic_proof;
   3.608 +
   3.609 +end; (* local *)
   3.610 +
   3.611 +local
   3.612 +
   3.613 +val _ = ();
   3.614  
   3.615 +fun gen_add_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
   3.616 +  let
   3.617 +    val class = prep_class theory raw_class;
   3.618 +    val sort = prep_sort theory raw_sort;
   3.619 +  in
   3.620 +    theory
   3.621 +    |> do_proof
   3.622 +  end;
   3.623 +
   3.624 +fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof;
   3.625 +fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof;
   3.626 +val setup_proof = AxClass.instance_arity_i I ("", [], []);
   3.627 +fun tactic_proof tac = AxClass.add_inst_arity_i I ("", [], []) tac;
   3.628 +
   3.629 +in
   3.630 +
   3.631 +val add_instance_sort = instance_sort setup_proof;
   3.632 +val add_instance_sort_i = instance_sort_i setup_proof;
   3.633 +val prove_instance_sort = instance_sort o tactic_proof;
   3.634 +val prove_instance_sort_i = instance_sort_i o tactic_proof;
   3.635 +
   3.636 +(*
   3.637 +interpretation_in_locale: loc_name * loc_expr -> theory -> Proof.state
   3.638 +  --> rausdestilieren
   3.639 +*)
   3.640 +(* switch: wenn es nur axclasses sind
   3.641 +  --> alte Methode, diesen switch möglichst weit am Parser dran *)
   3.642 +
   3.643 +end; (* local *)
   3.644  
   3.645  (* extracting dictionary obligations from types *)
   3.646  
   3.647 @@ -403,23 +601,22 @@
   3.648      val typ_def = Type.varifyT raw_typ_def;
   3.649      val typ_use = Type.varifyT raw_typ_use;
   3.650      val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
   3.651 -    fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
   3.652 -    fun get_superclass_derivation (subclasses, superclass) =
   3.653 -      (the oo get_first) (fn subclass =>
   3.654 -        Sorts.class_le_path (Sign.classes_of thy) (subclass, superclass)
   3.655 -      ) subclasses;
   3.656 -    fun find_index_class subclass subclasses =
   3.657 +    fun get_first_index f =
   3.658        let
   3.659 -        val i = find_index_eq subclass subclasses;
   3.660 -        val _ = if i < 0 then error "could not find class" else ();
   3.661 -      in case subclasses
   3.662 -       of [_] => ~1
   3.663 -        | _ => i
   3.664 -      end;
   3.665 +        fun get _ [] = NONE
   3.666 +          | get i (x::xs) = 
   3.667 +              case f x
   3.668 +               of NONE => get (i+1) xs
   3.669 +                | SOME y => SOME (i, y)
   3.670 +      in get 0 end;
   3.671 +    fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
   3.672      fun mk_class_deriv thy subclasses superclass =
   3.673 -      case get_superclass_derivation (subclasses, superclass)
   3.674 -      of (subclass::deriv) =>
   3.675 -        ((rev o filter (is_class thy)) deriv, find_index_class subclass subclasses);
   3.676 +      let
   3.677 +        val (i, (subclass::deriv)) = (the oo get_first_index) (fn subclass =>
   3.678 +            get_superclass_derivation thy (subclass, superclass)
   3.679 +          ) subclasses;
   3.680 +        val i' = if length subclasses = 1 then ~1 else i;
   3.681 +      in (rev deriv, i') end;
   3.682      fun mk_lookup (sort_def, (Type (tycon, tys))) =
   3.683            let
   3.684              val arity_lookup = map2 (curry mk_lookup)
   3.685 @@ -472,41 +669,6 @@
   3.686    end;
   3.687  
   3.688  
   3.689 -(* intermediate auxiliary *)
   3.690 -
   3.691 -fun add_classentry raw_class raw_cs thy =
   3.692 -  let
   3.693 -    val class = Sign.intern_class thy raw_class;
   3.694 -    val cs_proto =
   3.695 -      raw_cs
   3.696 -      |> map (Sign.intern_const thy)
   3.697 -      |> map (fn c => (c, Sign.the_const_constraint thy c));
   3.698 -    val used =
   3.699 -      []
   3.700 -      |> fold (fn (_, ty) => curry (gen_union (op =))
   3.701 -           ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto
   3.702 -    val v = hd (Term.invent_names used "'a" 1);
   3.703 -    val cs =
   3.704 -      cs_proto
   3.705 -      |> map (fn (c, ty) => (c, map_type_tvar (fn var as ((tvar', _), sort) =>
   3.706 -          if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
   3.707 -          then TFree (v, [])
   3.708 -          else TVar var
   3.709 -         ) ty));
   3.710 -  in
   3.711 -    thy
   3.712 -    |> add_class_data (class, ([], "", class, v, cs))
   3.713 -  end;
   3.714 -
   3.715 -fun add_classinsts raw_class raw_insts thy =
   3.716 -  let
   3.717 -    val class = Sign.intern_class thy raw_class;
   3.718 -    val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts;
   3.719 -  in
   3.720 -    thy
   3.721 -    |> fold (curry add_inst_data class) insts
   3.722 -  end;
   3.723 -
   3.724  (* toplevel interface *)
   3.725  
   3.726  local
   3.727 @@ -538,23 +700,22 @@
   3.728        >> (Toplevel.theory_context
   3.729            o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
   3.730  
   3.731 -val classP_exp =
   3.732 -  OuterSyntax.command (classK ^ "_exp") "operational type classes" K.thy_goal (
   3.733 -    P.name --| P.$$$ "="
   3.734 -    -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
   3.735 -    -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
   3.736 -      >> ((Toplevel.print oo Toplevel.theory_to_proof)
   3.737 -          o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
   3.738 -
   3.739  val instanceP =
   3.740    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   3.741 -      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
   3.742 -      || parse_inst -- Scan.repeat P.spec_name
   3.743 +      P.$$$ "target_atom" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.sort)
   3.744 +           >> (fn (class, sort) => add_instance_sort (class, sort))
   3.745 +      || P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
   3.746 +      || parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
   3.747             >> (fn (((tyco, asorts), sort), []) => AxClass.instance_arity I (tyco, asorts, sort)
   3.748                  | (inst, defs) => add_instance_arity inst defs)
   3.749      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   3.750  
   3.751 -val _ = OuterSyntax.add_parsers [classP, classP_exp, instanceP];
   3.752 +val _ = OuterSyntax.add_parsers [classP, instanceP];
   3.753 +
   3.754 +val _ = Context.add_setup (Method.add_methods
   3.755 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   3.756 +    "back-chain introduction rules of classes"),
   3.757 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
   3.758  
   3.759  end; (* local *)
   3.760  
     4.1 --- a/src/Pure/axclass.ML	Sun Feb 19 22:40:18 2006 +0100
     4.2 +++ b/src/Pure/axclass.ML	Mon Feb 20 11:37:18 2006 +0100
     4.3 @@ -18,16 +18,15 @@
     4.4    val add_arity_thms: thm list -> theory -> theory
     4.5    val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
     4.6    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
     4.7 -  val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
     4.8 -  val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     4.9 +  val add_inst_arity: (theory -> theory) -> xstring * string list * string -> tactic -> theory -> theory
    4.10 +  val add_inst_arity_i: (theory -> theory) -> string * sort list * sort -> tactic -> theory -> theory
    4.11    val instance_subclass: xstring * xstring -> theory -> Proof.state
    4.12    val instance_subclass_i: class * class -> theory -> Proof.state
    4.13    val instance_arity: (theory -> theory) -> xstring * string list * string -> theory -> Proof.state
    4.14    val instance_arity_i: (theory -> theory) -> string * sort list * sort -> theory -> Proof.state
    4.15    val read_arity: theory -> xstring * string list * string -> arity
    4.16    val cert_arity: theory -> string * sort list * sort -> arity
    4.17 -  val intro_classes_tac: thm list -> tactic
    4.18 -  val default_intro_classes_tac: thm list -> tactic
    4.19 +  val class_axms: theory -> thm list
    4.20  end;
    4.21  
    4.22  structure AxClass: AX_CLASS =
    4.23 @@ -278,7 +277,7 @@
    4.24        cat_error msg ("The error(s) above occurred while trying to prove " ^ txt);
    4.25    in add_classrel_thms [th] thy end;
    4.26  
    4.27 -fun ext_inst_arity prep_arity raw_arity tac thy =
    4.28 +fun ext_inst_arity prep_arity (after_qed : theory -> theory) raw_arity tac thy =
    4.29    let
    4.30      val arity = prep_arity thy raw_arity;
    4.31      val txt = quote (Sign.string_of_arity thy arity);
    4.32 @@ -287,7 +286,11 @@
    4.33      val ths = Goal.prove_multi thy [] [] props
    4.34        (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    4.35          cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt);
    4.36 -  in add_arity_thms ths thy end;
    4.37 +  in
    4.38 +    thy
    4.39 +    |> add_arity_thms ths
    4.40 +    |> after_qed
    4.41 +  end;
    4.42  
    4.43  in
    4.44  
    4.45 @@ -323,26 +326,6 @@
    4.46  end;
    4.47  
    4.48  
    4.49 -(* tactics and methods *)
    4.50 -
    4.51 -fun intro_classes_tac facts st =
    4.52 -  (ALLGOALS (Method.insert_tac facts THEN'
    4.53 -      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.theory_of_thm st))))
    4.54 -    THEN Tactic.distinct_subgoals_tac) st;
    4.55 -
    4.56 -fun default_intro_classes_tac [] = intro_classes_tac []
    4.57 -  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
    4.58 -
    4.59 -fun default_tac rules ctxt facts =
    4.60 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    4.61 -    default_intro_classes_tac facts;
    4.62 -
    4.63 -val _ = Context.add_setup (Method.add_methods
    4.64 - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    4.65 -    "back-chain introduction rules of axiomatic type classes"),
    4.66 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
    4.67 -
    4.68 -
    4.69  
    4.70  (** outer syntax **)
    4.71