src/Pure/Isar/class.ML
changeset 25062 af5ef0d4d655
parent 25060 17c313217998
child 25066 344b9611c150
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature CLASS =
     1.6  sig
     1.7 -  val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
     1.8 +  val fork_mixfix: bool -> bool -> mixfix -> (mixfix * mixfix) * mixfix
     1.9  
    1.10    val axclass_cmd: bstring * xstring list
    1.11      -> ((bstring * Attrib.src list) * string list) list
    1.12 @@ -19,9 +19,9 @@
    1.13    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    1.14      -> xstring list -> theory -> string * Proof.context
    1.15    val init: class -> Proof.context -> Proof.context
    1.16 -  val add_const_in_class: string -> (string * mixfix) * (string * term)
    1.17 +  val add_const_in_class: string -> (string * mixfix) * term
    1.18      -> theory -> string * theory
    1.19 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
    1.20 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term
    1.21      -> theory -> string * theory
    1.22    val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.23    val is_class: theory -> class -> bool
    1.24 @@ -54,13 +54,15 @@
    1.25  
    1.26  (** auxiliary **)
    1.27  
    1.28 -fun fork_mixfix is_locale is_class mx =
    1.29 -  let
    1.30 -    val mx' = Syntax.unlocalize_mixfix mx;
    1.31 -    val mx_global = if not is_locale orelse (is_class andalso not (mx = mx'))
    1.32 -      then mx' else NoSyn;
    1.33 -    val mx_local = if is_locale then mx else NoSyn;
    1.34 -  in (mx_global, mx_local) end;
    1.35 +val classN = "class";
    1.36 +val introN = "intro";
    1.37 +
    1.38 +fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
    1.39 +  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
    1.40 +  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
    1.41 +      (*let
    1.42 +        val mx' = Syntax.unlocalize_mixfix mx;
    1.43 +      in if mx' = mx then ((NoSyn, mx), NoSyn) else ((mx', mx), NoSyn) end;*)
    1.44  
    1.45  fun prove_interpretation tac prfx_atts expr inst =
    1.46    Locale.interpretation_i I prfx_atts expr inst
    1.47 @@ -315,36 +317,36 @@
    1.48  datatype class_data = ClassData of {
    1.49    consts: (string * string) list
    1.50      (*locale parameter ~> constant name*),
    1.51 -  local_sort: sort,
    1.52 +  base_sort: sort,
    1.53    inst: (typ option list * term option list) * term Symtab.table
    1.54      (*canonical interpretation FIXME*),
    1.55 +  morphism: morphism,
    1.56 +    (*partial morphism of canonical interpretation*)
    1.57    intro: thm,
    1.58    defs: thm list,
    1.59 -  operations: (string * (term * (typ * int))) list
    1.60 -    (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*),
    1.61 -  operations_rev: (string * string) list
    1.62 -    (*locale operation ~> constant name*)
    1.63 +  operations: (string * ((term * typ) * (typ * int))) list
    1.64 +    (*constant name ~> (locale term & typ,
    1.65 +        (constant constraint, instantiaton index of class typ))*)
    1.66  };
    1.67  
    1.68  fun rep_class_data (ClassData d) = d;
    1.69 -fun mk_class_data ((consts, local_sort, inst, intro),
    1.70 -    (defs, operations, operations_rev)) =
    1.71 -  ClassData { consts = consts, local_sort = local_sort, inst = inst,
    1.72 -    intro = intro, defs = defs, operations = operations,
    1.73 -    operations_rev = operations_rev };
    1.74 -fun map_class_data f (ClassData { consts, local_sort, inst, intro,
    1.75 -    defs, operations, operations_rev }) =
    1.76 -  mk_class_data (f ((consts, local_sort, inst, intro),
    1.77 -    (defs, operations, operations_rev)));
    1.78 +fun mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.79 +    (defs, operations)) =
    1.80 +  ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.81 +    morphism = morphism, intro = intro, defs = defs,
    1.82 +    operations = operations };
    1.83 +fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
    1.84 +    defs, operations }) =
    1.85 +  mk_class_data (f ((consts, base_sort, inst, morphism, intro),
    1.86 +    (defs, operations)));
    1.87  fun merge_class_data _ (ClassData { consts = consts,
    1.88 -    local_sort = local_sort, inst = inst, intro = intro,
    1.89 -    defs = defs1, operations = operations1, operations_rev = operations_rev1 },
    1.90 -  ClassData { consts = _, local_sort = _, inst = _, intro = _,
    1.91 -    defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
    1.92 -  mk_class_data ((consts, local_sort, inst, intro),
    1.93 +    base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
    1.94 +    defs = defs1, operations = operations1 },
    1.95 +  ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
    1.96 +    defs = defs2, operations = operations2 }) =
    1.97 +  mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.98      (Thm.merge_thms (defs1, defs2),
    1.99 -      AList.merge (op =) (K true) (operations1, operations2),
   1.100 -      AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
   1.101 +      AList.merge (op =) (K true) (operations1, operations2)));
   1.102  
   1.103  structure ClassData = TheoryDataFun
   1.104  (
   1.105 @@ -381,6 +383,8 @@
   1.106  
   1.107  fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   1.108  
   1.109 +fun morphism thy = #morphism o the_class_data thy;
   1.110 +
   1.111  fun these_intros thy =
   1.112    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   1.113      (ClassData.get thy) [];
   1.114 @@ -388,26 +392,21 @@
   1.115  fun these_operations thy =
   1.116    maps (#operations o the_class_data thy) o ancestry thy;
   1.117  
   1.118 -fun these_operations_rev thy =
   1.119 -  maps (#operations_rev o the_class_data thy) o ancestry thy;
   1.120 -
   1.121  fun local_operation thy = AList.lookup (op =) o these_operations thy;
   1.122  
   1.123 -fun global_operation thy = AList.lookup (op =) o these_operations_rev thy;
   1.124 -
   1.125 -fun sups_local_sort thy sort =
   1.126 +fun sups_base_sort thy sort =
   1.127    let
   1.128 -    val sups = filter (is_some o lookup_class_data thy) sort
   1.129 +    val sups = filter (is_class thy) sort
   1.130        |> Sign.minimize_sort thy;
   1.131 -    val local_sort = case sups
   1.132 -     of sup :: _ => #local_sort (the_class_data thy sup)
   1.133 +    val base_sort = case sups
   1.134 +     of _ :: _ => maps (#base_sort o the_class_data thy) sups
   1.135 +          |> Sign.minimize_sort thy
   1.136        | [] => sort;
   1.137 -  in (sups, local_sort) end;
   1.138 +  in (sups, base_sort) end;
   1.139  
   1.140  fun print_classes thy =
   1.141    let
   1.142      val ctxt = ProofContext.init thy;
   1.143 -
   1.144      val algebra = Sign.classes_of thy;
   1.145      val arities =
   1.146        Symtab.empty
   1.147 @@ -422,11 +421,13 @@
   1.148      fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   1.149        ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   1.150      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   1.151 -      (SOME o Pretty.str) ("class " ^ class ^ ":"),
   1.152 +      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   1.153        (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.154          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   1.155 -      if is_class thy class then (SOME o Pretty.str) ("locale: " ^ class) else NONE,
   1.156 -      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   1.157 +      if is_class thy class then (SOME o Pretty.str)
   1.158 +        ("locale: " ^ Locale.extern thy class) else NONE,
   1.159 +      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   1.160 +          (Pretty.str "parameters:" :: ps)) o map mk_param
   1.161          o these o Option.map #params o try (AxClass.get_info thy)) class,
   1.162        (SOME o Pretty.block o Pretty.breaks) [
   1.163          Pretty.str "instances:",
   1.164 @@ -441,7 +442,7 @@
   1.165  
   1.166  (* updaters *)
   1.167  
   1.168 -fun add_class_data ((class, superclasses), (cs, local_sort, inst, intro)) thy =
   1.169 +fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   1.170    let
   1.171      (*FIXME*)
   1.172      val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs [])
   1.173 @@ -453,26 +454,50 @@
   1.174          (Locale.parameters_of_expr thy (Locale.Locale class));
   1.175      val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))];
   1.176      val inst' = ((instT, inst_params), inst);
   1.177 -    val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
   1.178 +    val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
   1.179 +      (c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs;
   1.180      val cs = (map o pairself) fst cs;
   1.181      val add_class = Graph.new_node (class,
   1.182 -        mk_class_data ((cs, local_sort, inst', intro), ([], operations, [])))
   1.183 +        mk_class_data ((cs, base_sort, inst', phi, intro), ([], operations)))
   1.184        #> fold (curry Graph.add_edge class) superclasses;
   1.185    in
   1.186      ClassData.map add_class thy
   1.187    end;
   1.188  
   1.189 -fun register_operation class (entry, some_def) =
   1.190 -  (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   1.191 -    (fn (defs, operations, operations_rev) =>
   1.192 -      (case some_def of NONE => defs | SOME def => def :: defs,
   1.193 -        entry :: operations, (*FIXME*)operations_rev));
   1.194 +fun register_operation class ((c, rhs), some_def) thy =
   1.195 +  let
   1.196 +    val ty = Sign.the_const_constraint thy c;
   1.197 +    val typargs = Sign.const_typargs thy (c, ty);
   1.198 +    val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
   1.199 +    val ty' = Term.fastype_of rhs;
   1.200 +  in
   1.201 +    thy
   1.202 +    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   1.203 +      (fn (defs, operations) =>
   1.204 +        (case some_def of NONE => defs | SOME def => def :: defs,
   1.205 +          (c, ((rhs, ty'), (ty, typidx))) :: operations))
   1.206 +  end;
   1.207  
   1.208  
   1.209  (** rule calculation, tactics and methods **)
   1.210  
   1.211  val class_prefix = Logic.const_of_class o Sign.base_name;
   1.212  
   1.213 +fun calculate_morphism class cs =
   1.214 +  let
   1.215 +    val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
   1.216 +      if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
   1.217 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   1.218 +         of SOME (c, _) => Const (c, ty)
   1.219 +          | NONE => t)
   1.220 +      | subst_aterm t = t;
   1.221 +    val subst_term = map_aterms subst_aterm #> map_types subst_typ;
   1.222 +  in
   1.223 +    Morphism.identity
   1.224 +    $> Morphism.term_morphism subst_term
   1.225 +    $> Morphism.typ_morphism subst_typ
   1.226 +  end;
   1.227 +
   1.228  fun class_intro thy class sups =
   1.229    let
   1.230      fun class_elim class =
   1.231 @@ -506,8 +531,6 @@
   1.232    let
   1.233      val params = these_params thy [class];
   1.234      val { inst = ((_, inst), _), ... } = the_class_data thy class;
   1.235 -    (*val _ = tracing ("interpreting with " ^ cat_lines (map (setmp show_sorts true makestring)
   1.236 -      (map_filter I inst)));*)
   1.237      val tac = ALLGOALS (ProofContext.fact_tac facts);
   1.238      val prfx = class_prefix class;
   1.239    in
   1.240 @@ -548,82 +571,86 @@
   1.241  
   1.242  (* class context syntax *)
   1.243  
   1.244 -fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt =
   1.245 +fun internal_remove_constraint base_sort (c, (_, (ty, _))) ctxt =
   1.246    let
   1.247 -    val consts = ProofContext.consts_of ctxt;
   1.248 -    val typargs = Consts.typargs consts (c, ty);
   1.249 -    val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs;
   1.250 -    val ty' = Consts.instance consts (c, typargs');
   1.251 -  in ProofContext.add_const_constraint (c, SOME ty') ctxt end;
   1.252 +    val ty' = ty
   1.253 +      |> map_atyps (fn ty as TVar ((v, 0), _) =>
   1.254 +           if v = Name.aT then TVar ((v, 0), base_sort) else ty)
   1.255 +      |> SOME;
   1.256 +  in ProofContext.add_const_constraint (c, ty') ctxt end;
   1.257  
   1.258  fun remove_constraint class c ctxt =
   1.259    let
   1.260      val thy = ProofContext.theory_of ctxt;
   1.261 +    val base_sort = (#base_sort o the_class_data thy) class;
   1.262      val SOME entry = local_operation thy [class] c;
   1.263    in
   1.264 -    internal_remove_constraint
   1.265 -      ((#local_sort o the_class_data thy) class) (c, entry) ctxt
   1.266 +    internal_remove_constraint base_sort (c, entry) ctxt
   1.267    end;
   1.268  
   1.269 -fun sort_term_check sups local_sort ts ctxt =
   1.270 +fun sort_term_check sups base_sort ts ctxt =
   1.271    let
   1.272      val thy = ProofContext.theory_of ctxt;
   1.273 -    val local_operation = local_operation thy sups;
   1.274 +    val local_operation = local_operation thy sups o fst;
   1.275 +    val typargs = Consts.typargs (ProofContext.consts_of ctxt);
   1.276      val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
   1.277 -    val consts = ProofContext.consts_of ctxt;
   1.278 -    fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   1.279 -     of TFree (v, _) => if v = Name.aT
   1.280 -          then apfst (AList.update (op =) ((c, ty), t')) else I
   1.281 -      | TVar (vi, _) => if TypeInfer.is_param vi
   1.282 -          then apfst (AList.update (op =) ((c, ty), t'))
   1.283 +    fun check_typ (c, ty) (TFree (v, _)) t = if v = Name.aT
   1.284 +          then apfst (AList.update (op =) ((c, ty), t)) else I
   1.285 +      | check_typ (c, ty) (TVar (vi, _)) t = if TypeInfer.is_param vi
   1.286 +          then apfst (AList.update (op =) ((c, ty), t))
   1.287              #> apsnd (insert (op =) vi) else I
   1.288 -      | _ => I;
   1.289 -    fun add_const (Const (c, ty)) = (case local_operation c
   1.290 -         of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx)
   1.291 -          | NONE => I)
   1.292 +      | check_typ _ _ _ = I;
   1.293 +    fun check_const (c, ty) ((t, _), (_, idx)) =
   1.294 +      check_typ (c, ty) (nth (typargs (c, ty)) idx) t;
   1.295 +    fun add_const (Const c_ty) = Option.map (check_const c_ty) (local_operation c_ty)
   1.296 +          |> the_default I
   1.297        | add_const _ = I;
   1.298      val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   1.299 -    val ts' = map (map_aterms
   1.300 +    val subst_typ = map_type_tvar (fn var as (vi, _) =>
   1.301 +      if member (op =) typarams vi then TFree (Name.aT, base_sort) else TVar var);
   1.302 +    val subst_term = map_aterms
   1.303          (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
   1.304 -      #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
   1.305 -           then TFree (Name.aT, local_sort) else TVar var)) ts;
   1.306 +          #> map_types subst_typ;
   1.307 +    val ts' = map subst_term ts;
   1.308      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   1.309    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
   1.310  
   1.311 -val uncheck = ref false;
   1.312 +val uncheck = ref true;
   1.313  
   1.314  fun sort_term_uncheck sups ts ctxt =
   1.315    let
   1.316 +    (*FIXME abbreviations*)
   1.317      val thy = ProofContext.theory_of ctxt;
   1.318 -    val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst;
   1.319 -    val global_operation = global_operation thy sups;
   1.320 -    fun globalize (t as Free (v, ty)) = (case global_param v
   1.321 -         of SOME c => Const (c, ty)
   1.322 -          | NONE => t)
   1.323 -      | globalize (t as Const (c, ty)) = (case global_operation c
   1.324 -         of SOME c => Const (c, ty)
   1.325 -          | NONE => t)
   1.326 -      | globalize t = t;
   1.327 -    val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
   1.328 +    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
   1.329 +      | rew_app f t = t;
   1.330 +    val rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) (these_operations thy sups);
   1.331 +    val rews' = (map o apfst o rew_app) (Pattern.rewrite_term thy rews []) rews;
   1.332 +    val _ = map (Thm.cterm_of thy o Logic.mk_equals) rews';
   1.333 +    val ts' = if ! uncheck
   1.334 +      then map (Pattern.rewrite_term thy rews' []) ts else ts;
   1.335    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.336  
   1.337 -fun init_class_ctxt sups local_sort ctxt =
   1.338 +fun init_class_ctxt sups base_sort ctxt =
   1.339    let
   1.340      val operations = these_operations (ProofContext.theory_of ctxt) sups;
   1.341 +    fun standard_infer_types ts ctxt =
   1.342 +      let
   1.343 +        val ts' = ProofContext.standard_infer_types ctxt ts;
   1.344 +      in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.345    in
   1.346      ctxt
   1.347      |> Variable.declare_term
   1.348 -        (Logic.mk_type (TFree (Name.aT, local_sort)))
   1.349 -    |> fold (internal_remove_constraint local_sort) operations
   1.350 -    |> Context.proof_map (Syntax.add_term_check 50 "class"
   1.351 -        (sort_term_check sups local_sort)
   1.352 -        #> Syntax.add_term_uncheck 50 "class"
   1.353 -          (sort_term_uncheck sups))
   1.354 +        (Logic.mk_type (TFree (Name.aT, base_sort)))
   1.355 +    |> fold (internal_remove_constraint base_sort) operations
   1.356 +    |> Context.proof_map (Syntax.add_term_check 1 "class"
   1.357 +            (sort_term_check sups base_sort)
   1.358 +        #> Syntax.add_term_check 1 "standard" standard_infer_types
   1.359 +        #> Syntax.add_term_uncheck (~10) "class" (sort_term_uncheck sups))
   1.360    end;
   1.361  
   1.362  fun init class ctxt =
   1.363    init_class_ctxt [class]
   1.364 -    ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
   1.365 +    ((#base_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
   1.366  
   1.367  
   1.368  (* class definition *)
   1.369 @@ -633,7 +660,7 @@
   1.370  fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   1.371    let
   1.372      val supclasses = map (prep_class thy) raw_supclasses;
   1.373 -    val (sups, local_sort) = sups_local_sort thy supclasses;
   1.374 +    val (sups, base_sort) = sups_base_sort thy supclasses;
   1.375      val supsort = Sign.minimize_sort thy supclasses;
   1.376      val suplocales = map Locale.Locale sups;
   1.377      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.378 @@ -649,10 +676,10 @@
   1.379      ProofContext.init thy
   1.380      |> Locale.cert_expr supexpr [constrain]
   1.381      |> snd
   1.382 -    |> init_class_ctxt sups local_sort
   1.383 +    |> init_class_ctxt sups base_sort
   1.384      |> process_expr Locale.empty raw_elems
   1.385      |> fst
   1.386 -    |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
   1.387 +    |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
   1.388            (*FIXME*) if null includes then constrain :: elems else elems)))
   1.389    end;
   1.390  
   1.391 @@ -688,26 +715,26 @@
   1.392      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.393    let
   1.394      val class = Sign.full_name thy bname;
   1.395 -    val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
   1.396 +    val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
   1.397        prep_spec thy raw_supclasses raw_includes_elems;
   1.398      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   1.399      fun mk_inst class param_names cs =
   1.400        Symtab.empty
   1.401        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   1.402             (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   1.403 +    fun fork_syntax (Element.Fixes xs) =
   1.404 +          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   1.405 +          #>> Element.Fixes
   1.406 +      | fork_syntax x = pair x;
   1.407 +    val (elems, global_syn) = fold_map fork_syntax elems_syn [];
   1.408 +    fun globalize (c, ty) = 
   1.409 +      ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
   1.410 +        (the_default NoSyn o AList.lookup (op =) global_syn) c);
   1.411      fun extract_params thy =
   1.412        let
   1.413 -        val params = Locale.parameters_of thy class;
   1.414 -        val _ = if Sign.subsort thy (supsort, local_sort) then () else error
   1.415 -          ("Sort " ^ Sign.string_of_sort thy local_sort
   1.416 -            ^ " is less general than permitted least general sort "
   1.417 -            ^ Sign.string_of_sort thy supsort);
   1.418 +        val params = map fst (Locale.parameters_of thy class);
   1.419        in
   1.420 -        (map fst params, params
   1.421 -        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
   1.422 -        |> (map o apsnd) (fork_mixfix true true #> fst)
   1.423 -        |> chop (length supconsts)
   1.424 -        |> snd)
   1.425 +        (params, (map globalize o snd o chop (length supconsts)) params)
   1.426        end;
   1.427      fun extract_assumes params thy cs =
   1.428        let
   1.429 @@ -722,28 +749,26 @@
   1.430          Locale.global_asms_of thy class
   1.431          |> map prep_asm
   1.432        end;
   1.433 -    fun note_intro class_intro =
   1.434 -      PureThy.note_thmss_qualified "" (class_prefix class)
   1.435 -        [(("intro", []), [([class_intro], [])])]
   1.436 -      #> snd
   1.437    in
   1.438      thy
   1.439      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.440      |> snd
   1.441      |> ProofContext.theory (`extract_params
   1.442 -      #-> (fn (globals, params) =>
   1.443 +      #-> (fn (all_params, params) =>
   1.444          define_class_params (bname, supsort) params
   1.445            (extract_assumes params) other_consts
   1.446        #-> (fn (_, (consts, axioms)) =>
   1.447          `(fn thy => class_intro thy class sups)
   1.448        #-> (fn class_intro =>
   1.449 +        PureThy.note_thmss_qualified "" (NameSpace.append class classN)
   1.450 +          [((introN, []), [([class_intro], [])])]
   1.451 +      #-> (fn [(_, [class_intro])] =>
   1.452          add_class_data ((class, sups),
   1.453 -          (map fst params ~~ consts, local_sort,
   1.454 -            mk_inst class (map fst globals) (map snd supconsts @ consts),
   1.455 -              class_intro))
   1.456 -      #> note_intro class_intro
   1.457 +          (map fst params ~~ consts, base_sort,
   1.458 +            mk_inst class (map fst all_params) (map snd supconsts @ consts),
   1.459 +              calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
   1.460        #> class_interpretation class axioms []
   1.461 -      ))))
   1.462 +      )))))
   1.463      |> pair class
   1.464    end;
   1.465  
   1.466 @@ -757,56 +782,29 @@
   1.467  
   1.468  (* definition in class target *)
   1.469  
   1.470 -fun export_fixes thy class =
   1.471 +fun add_const_in_class class ((c, mx), rhs) thy =
   1.472    let
   1.473 -    val cs = these_params thy [class];
   1.474 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   1.475 -         of SOME (c, _) => Const (c, ty)
   1.476 -          | NONE => t)
   1.477 -      | subst_aterm t = t;
   1.478 -  in Term.map_aterms subst_aterm end;
   1.479 -
   1.480 -fun mk_operation_entry thy (c, rhs) =
   1.481 -  let
   1.482 -    val ty = Logic.unvarifyT (Sign.the_const_constraint thy c);
   1.483 -    val typargs = Sign.const_typargs thy (c, ty);
   1.484 -    val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   1.485 -  in (c, (rhs, (ty, typidx))) end;
   1.486 -
   1.487 -fun add_const_in_class class ((c, mx), (c_loc, rhs)) thy =
   1.488 -  let
   1.489 -    val _ = tracing c_loc;
   1.490      val prfx = class_prefix class;
   1.491      val thy' = thy |> Sign.add_path prfx;
   1.492 +    val phi = morphism thy' class;
   1.493  
   1.494 -    val rhs' = export_fixes thy' class rhs;
   1.495 -    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.496 -      if w = Name.aT then TFree (w, [class]) else TFree var);
   1.497 +    val c' = Sign.full_name thy' c;
   1.498 +    val ((mx', _), _) = fork_mixfix true true mx;
   1.499 +    val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
   1.500      val ty' = Term.fastype_of rhs';
   1.501 -    val ty'' = subst_typ ty';
   1.502 -    val c' = Sign.full_name thy' c;
   1.503 -    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.504      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   1.505 -    val (mx', _) = fork_mixfix true true mx;
   1.506 -    fun interpret def thy =
   1.507 -      let
   1.508 -        val def' = symmetric def;
   1.509 -        val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def';
   1.510 -      in
   1.511 -        thy
   1.512 -        |> class_interpretation class [def'] [def_eq]
   1.513 -        |> Sign.add_const_constraint (c', SOME ty'')
   1.514 -        |> `(fn thy => mk_operation_entry thy (c', rhs))
   1.515 -        |-> (fn entry => register_operation class (entry, SOME def'))
   1.516 -      end;
   1.517 +    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.518    in
   1.519      thy'
   1.520      |> Sign.hide_consts_i false [c'']
   1.521      |> Sign.declare_const [] (c, ty', mx') |> snd
   1.522      |> Sign.parent_path
   1.523      |> Sign.sticky_prefix prfx
   1.524 -    |> PureThy.add_defs_i false [(def, [])]
   1.525 -    |-> (fn [def] => interpret def)
   1.526 +    |> yield_singleton (PureThy.add_defs_i false) (def, [])
   1.527 +    |>> Thm.symmetric
   1.528 +    |-> (fn def => class_interpretation class [def]
   1.529 +                [(map_types Logic.unvarifyT o Thm.prop_of) def]
   1.530 +          #> register_operation class ((c', rhs), SOME def))
   1.531      |> Sign.restore_naming thy
   1.532      |> pair c'
   1.533    end;
   1.534 @@ -814,20 +812,20 @@
   1.535  
   1.536  (* abbreviation in class target *)
   1.537  
   1.538 -fun add_abbrev_in_class class prmode ((c, mx), (c_loc, rhs)) thy =
   1.539 +fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
   1.540    let
   1.541 -    val _ = tracing c_loc;
   1.542      val prfx = class_prefix class;
   1.543 +    val phi = morphism thy class;
   1.544 +
   1.545      val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx;
   1.546        (*FIXME*)
   1.547      val c' = NameSpace.full naming c;
   1.548 -    val rhs' = export_fixes thy class rhs;
   1.549 +    val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
   1.550      val ty' = Term.fastype_of rhs';
   1.551 -    val entry = mk_operation_entry thy (c', rhs);
   1.552    in
   1.553      thy
   1.554      |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.555 -    |> register_operation class (entry, NONE)
   1.556 +    |> register_operation class ((c', rhs), NONE)
   1.557      |> pair c'
   1.558    end;
   1.559