rudimentary instantiation target
authorhaftmann
Fri Nov 23 21:09:35 2007 +0100 (2007-11-23)
changeset 25462dad0291cb76a
parent 25461 001dfba51869
child 25463 8b9c4582795a
rudimentary instantiation target
src/Pure/Isar/ROOT.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/ROOT.ML	Fri Nov 23 21:09:34 2007 +0100
     1.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Nov 23 21:09:35 2007 +0100
     1.3 @@ -44,6 +44,9 @@
     1.4  (*derived theory and proof elements*)
     1.5  use "calculation.ML";
     1.6  use "obtain.ML";
     1.7 +
     1.8 +(*local theories and target primitives*)
     1.9 +use "local_theory.ML";
    1.10  use "locale.ML";
    1.11  use "class.ML";
    1.12  
    1.13 @@ -52,12 +55,11 @@
    1.14  use "code.ML";
    1.15  
    1.16  (*local theories and specifications*)
    1.17 -use "local_theory.ML";
    1.18  use "theory_target.ML";
    1.19  use "subclass.ML";
    1.20 -use "instance.ML";
    1.21  use "spec_parse.ML";
    1.22  use "specification.ML";
    1.23 +use "instance.ML";
    1.24  use "constdefs.ML";
    1.25  
    1.26  (*toplevel environment*)
     2.1 --- a/src/Pure/Isar/class.ML	Fri Nov 23 21:09:34 2007 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 23 21:09:35 2007 +0100
     2.3 @@ -7,11 +7,7 @@
     2.4  
     2.5  signature CLASS =
     2.6  sig
     2.7 -  val axclass_cmd: bstring * xstring list
     2.8 -    -> ((bstring * Attrib.src list) * string list) list
     2.9 -    -> theory -> class * theory
    2.10 -  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    2.11 -
    2.12 +  (*classes*)
    2.13    val class: bstring -> class list -> Element.context_i Locale.element list
    2.14      -> string list -> theory -> string * Proof.context
    2.15    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    2.16 @@ -30,8 +26,29 @@
    2.17      -> theory -> theory
    2.18    val print_classes: theory -> unit
    2.19    val class_prefix: string -> string
    2.20 -  val uncheck: bool ref
    2.21  
    2.22 +  (*instances*)
    2.23 +  val declare_overloaded: string * typ * mixfix -> theory -> term * theory
    2.24 +  val define_overloaded: string -> string * term -> theory -> thm * theory
    2.25 +  val unoverload: theory -> conv
    2.26 +  val overload: theory -> conv
    2.27 +  val unoverload_const: theory -> string * typ -> string
    2.28 +  val inst_const: theory -> string * string -> string
    2.29 +  val param_const: theory -> string -> (string * string) option
    2.30 +  val instantiation: arity list -> theory -> local_theory
    2.31 +  val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state
    2.32 +  val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory
    2.33 +  val conclude_instantiation: local_theory -> local_theory
    2.34 +  val end_instantiation: local_theory -> Proof.context
    2.35 +  val instantiation_const: Proof.context -> string -> string option
    2.36 +
    2.37 +  (*old axclass layer*)
    2.38 +  val axclass_cmd: bstring * xstring list
    2.39 +    -> ((bstring * Attrib.src list) * string list) list
    2.40 +    -> theory -> class * theory
    2.41 +  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    2.42 +
    2.43 +  (*old instance layer*)
    2.44    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    2.45    val instance: arity list -> ((bstring * Attrib.src list) * term) list
    2.46      -> (thm list -> theory -> theory)
    2.47 @@ -43,11 +60,6 @@
    2.48    val prove_instance: tactic -> arity list
    2.49      -> ((bstring * Attrib.src list) * term) list
    2.50      -> theory -> thm list * theory
    2.51 -  val unoverload: theory -> conv
    2.52 -  val overload: theory -> conv
    2.53 -  val unoverload_const: theory -> string * typ -> string
    2.54 -  val inst_const: theory -> string * string -> string
    2.55 -  val param_const: theory -> string -> (string * string) option
    2.56  end;
    2.57  
    2.58  structure Class : CLASS =
    2.59 @@ -141,7 +153,9 @@
    2.60  end; (*local*)
    2.61  
    2.62  
    2.63 -(** explicit constants for overloaded definitions **)
    2.64 +(** basic overloading **)
    2.65 +
    2.66 +(* bookkeeping *)
    2.67  
    2.68  structure InstData = TheoryDataFun
    2.69  (
    2.70 @@ -156,8 +170,18 @@
    2.71        Symtab.merge (K true) (tabb1, tabb2));
    2.72  );
    2.73  
    2.74 +val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
    2.75 +
    2.76 +fun inst thy (c, tyco) =
    2.77 +  (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
    2.78 +
    2.79 +val inst_const = fst oo inst;
    2.80 +
    2.81  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    2.82 -    (InstData.get thy) [];
    2.83 +  (InstData.get thy) [];
    2.84 +
    2.85 +val param_const = Symtab.lookup o snd o InstData.get;
    2.86 +
    2.87  fun add_inst (c, tyco) inst = (InstData.map o apfst
    2.88        o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    2.89    #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    2.90 @@ -165,19 +189,65 @@
    2.91  fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy);
    2.92  fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    2.93  
    2.94 -fun inst_const thy (c, tyco) =
    2.95 -  (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
    2.96  fun unoverload_const thy (c_ty as (c, _)) =
    2.97    case AxClass.class_of_param thy c
    2.98 -   of SOME class => (case Sign.const_typargs thy c_ty
    2.99 -       of [Type (tyco, _)] => (case Symtab.lookup
   2.100 -           ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
   2.101 +   of SOME class => (case inst_tyco thy c_ty
   2.102 +       of SOME tyco => (case try (inst thy) (c, tyco)
   2.103               of SOME (c, _) => c
   2.104                | NONE => c)
   2.105 -        | [_] => c)
   2.106 +        | NONE => c)
   2.107      | NONE => c;
   2.108  
   2.109 -val param_const = Symtab.lookup o snd o InstData.get;
   2.110 +
   2.111 +(* declaration and definition of instances of overloaded constants *)
   2.112 +
   2.113 +fun primitive_note kind (name, thm) =
   2.114 +  PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   2.115 +  #>> (fn [(_, [thm])] => thm);
   2.116 +
   2.117 +fun declare_overloaded (c, ty, mx) thy =
   2.118 +  let
   2.119 +    val SOME class = AxClass.class_of_param thy c;
   2.120 +    val SOME tyco = inst_tyco thy (c, ty);
   2.121 +    val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   2.122 +    val c' = NameSpace.base c;
   2.123 +    val ty' = Type.strip_sorts ty;
   2.124 +  in
   2.125 +    thy
   2.126 +    |> Sign.sticky_prefix name_inst
   2.127 +    |> Sign.no_base_names
   2.128 +    |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)]
   2.129 +    |> Sign.declare_const [] (c', ty', NoSyn)
   2.130 +    |-> (fn const' as Const (c'', _) => Thm.add_def true
   2.131 +          (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
   2.132 +    #>> Thm.varifyT
   2.133 +    #-> (fn thm => add_inst (c, tyco) (c'', thm)
   2.134 +    #> primitive_note Thm.internalK (c', thm)
   2.135 +    #> snd
   2.136 +    #> Sign.restore_naming thy
   2.137 +    #> pair (Const (c, ty))))
   2.138 +  end;
   2.139 +
   2.140 +fun define_overloaded name (c, t) thy =
   2.141 +  let
   2.142 +    val ty = Term.fastype_of t;
   2.143 +    val SOME tyco = inst_tyco thy (c, ty);
   2.144 +    val (c', eq) = inst thy (c, tyco);
   2.145 +    val [Type (_, tys)] = Sign.const_typargs thy (c, ty);
   2.146 +    val eq' = eq
   2.147 +      |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) [];
   2.148 +          (*FIXME proper recover_sort mechanism*)
   2.149 +    val prop = Logic.mk_equals (Const (c', ty), t);
   2.150 +    val name' = if name = "" then
   2.151 +      Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name;
   2.152 +  in
   2.153 +    thy
   2.154 +    |> Thm.add_def false (name', prop)
   2.155 +    |>> (fn thm => Thm.transitive eq' thm)
   2.156 +  end;
   2.157 +
   2.158 +
   2.159 +(* legacy *)
   2.160  
   2.161  fun add_inst_def (class, tyco) (c, ty) thy =
   2.162    let
   2.163 @@ -206,15 +276,10 @@
   2.164    let
   2.165      val ((lhs as Const (c, ty), args), rhs) =
   2.166        (apfst Term.strip_comb o Logic.dest_equals) prop;
   2.167 -    fun (*add_inst' def ([], (Const (c_inst, ty))) =
   2.168 -          if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
   2.169 -          then add_inst (c, tyco) (c_inst, def)
   2.170 -          else add_inst_def (class, tyco) (c, ty)
   2.171 -      |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty);
   2.172    in
   2.173      thy
   2.174      |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
   2.175 -    |-> (fn [def] => add_inst' def (args, rhs) #> pair def)
   2.176 +    |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
   2.177    end;
   2.178  
   2.179  
   2.180 @@ -690,14 +755,11 @@
   2.181      |> SOME
   2.182    end;
   2.183  
   2.184 -val uncheck = ref true;
   2.185 -
   2.186  fun sort_term_uncheck ts ctxt =
   2.187    let
   2.188      val thy = ProofContext.theory_of ctxt;
   2.189      val unchecks = (#unchecks o ClassSyntax.get) ctxt;
   2.190 -    val ts' = if ! uncheck
   2.191 -      then map (Pattern.rewrite_term thy unchecks []) ts else ts;
   2.192 +    val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
   2.193    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   2.194  
   2.195  fun init_ctxt sups base_sort ctxt =
   2.196 @@ -896,4 +958,174 @@
   2.197      |> Sign.restore_naming thy
   2.198    end;
   2.199  
   2.200 +
   2.201 +(** instantiation target **)
   2.202 +
   2.203 +(* bookkeeping *)
   2.204 +
   2.205 +datatype instantiation = Instantiation of {
   2.206 +  arities: arity list,
   2.207 +  params: ((string * string) * (string * typ)) list
   2.208 +}
   2.209 +
   2.210 +structure Instantiation = ProofDataFun
   2.211 +(
   2.212 +  type T = instantiation
   2.213 +  fun init _ = Instantiation { arities = [], params = [] };
   2.214 +);
   2.215 +
   2.216 +fun mk_instantiation (arities, params) = Instantiation {
   2.217 +    arities = arities, params = params
   2.218 +  };
   2.219 +fun map_instantiation f (Instantiation { arities, params }) =
   2.220 +  mk_instantiation (f (arities, params));
   2.221 +
   2.222 +fun the_instantiation ctxt = case Instantiation.get ctxt
   2.223 + of Instantiation { arities = [], ... } => error "No instantiation target"
   2.224 +  | Instantiation data => data;
   2.225 +
   2.226 +fun init_instantiation arities ctxt =
   2.227 +  let
   2.228 +    val thy = ProofContext.theory_of ctxt;
   2.229 +    val _ = if null arities then error "At least one arity must be given" else ();
   2.230 +    val _ = case (duplicates (op =) o map #1) arities
   2.231 +     of [] => ()
   2.232 +      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   2.233 +          ^ commas_quote dupl_tycos);
   2.234 +    val ty_insts = map (fn (tyco, sorts, _) =>
   2.235 +        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   2.236 +      arities;
   2.237 +    val ty_inst = the o AList.lookup (op =) ty_insts;
   2.238 +    fun type_name "*" = "prod"
   2.239 +      | type_name "+" = "sum"
   2.240 +      | type_name s = NameSpace.base s; (*FIXME*)
   2.241 +    fun get_param tyco sorts (param, (c, ty)) =
   2.242 +      ((unoverload_const thy (c, ty), tyco),
   2.243 +        (param ^ "_" ^ type_name tyco,
   2.244 +          map_atyps (K (ty_inst tyco)) ty));
   2.245 +    fun get_params (tyco, sorts, sort) =
   2.246 +      map (get_param tyco sorts) (these_params thy sort)
   2.247 +    val params = maps get_params arities;
   2.248 +  in
   2.249 +    ctxt
   2.250 +    |> Instantiation.put (mk_instantiation (arities, params))
   2.251 +    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   2.252 +    |> fold (Variable.declare_term o Free o snd) params
   2.253 +  end;
   2.254 +
   2.255 +val instantiation_params = #params o the_instantiation;
   2.256 +
   2.257 +fun instantiation_const ctxt v = instantiation_params ctxt
   2.258 +  |> find_first (fn (_, (v', _)) => v = v')
   2.259 +  |> Option.map (fst o fst);
   2.260 +
   2.261 +
   2.262 +(* syntax *)
   2.263 +
   2.264 +fun inst_term_check ts ctxt =
   2.265 +  let
   2.266 +    val params = instantiation_params ctxt;
   2.267 +    val tsig = ProofContext.tsig_of ctxt;
   2.268 +    val thy = ProofContext.theory_of ctxt;
   2.269 +
   2.270 +    fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
   2.271 +         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   2.272 +             of SOME (_, ty') => Type.typ_match tsig (ty, ty')
   2.273 +              | NONE => I)
   2.274 +          | NONE => I)
   2.275 +      | check_improve _ = I;
   2.276 +    val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
   2.277 +    val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
   2.278 +    val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
   2.279 +         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   2.280 +             of SOME v_ty => Free v_ty
   2.281 +              | NONE => t)
   2.282 +          | NONE => t)
   2.283 +      | t => t) ts';
   2.284 +  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
   2.285 +
   2.286 +fun inst_term_uncheck ts ctxt =
   2.287 +  let
   2.288 +    val params = instantiation_params ctxt;
   2.289 +    val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
   2.290 +       (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
   2.291 +         of SOME c => Const (c, ty)
   2.292 +          | NONE => t)
   2.293 +      | t => t) ts;
   2.294 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   2.295 +
   2.296 +
   2.297 +(* target *)
   2.298 +
   2.299 +fun instantiation arities =
   2.300 +  ProofContext.init
   2.301 +  #> init_instantiation arities
   2.302 +  #> fold ProofContext.add_arity arities
   2.303 +  #> Context.proof_map (
   2.304 +      Syntax.add_term_check 0 "instance" inst_term_check
   2.305 +      #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck);
   2.306 +
   2.307 +fun gen_proof_instantiation do_proof after_qed lthy =
   2.308 +  let
   2.309 +    (*FIXME should work on fresh context but continue local theory afterwards*)
   2.310 +    val ctxt = LocalTheory.target_of lthy;
   2.311 +    val arities = (#arities o the_instantiation) ctxt;
   2.312 +    val arities_proof = maps
   2.313 +      (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities;
   2.314 +    fun after_qed' results =
   2.315 +      LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   2.316 +      #> after_qed;
   2.317 +  in
   2.318 +    lthy
   2.319 +    |> do_proof after_qed' arities_proof
   2.320 +  end;
   2.321 +
   2.322 +val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts =>
   2.323 +  Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   2.324 +
   2.325 +fun prove_instantiation tac = gen_proof_instantiation (fn after_qed =>
   2.326 +  fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
   2.327 +    (fn {context, ...} => tac context)) lthy) I;
   2.328 +
   2.329 +fun conclude_instantiation lthy =
   2.330 +  let
   2.331 +    val arities = (#arities o the_instantiation) lthy;
   2.332 +    val thy = ProofContext.theory_of lthy;
   2.333 +    (*val _ = map (fn (tyco, sorts, sort) =>
   2.334 +      if Sign.of_sort thy
   2.335 +        (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
   2.336 +      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   2.337 +        arities; FIXME activate when old instance command is gone*)
   2.338 +    val params_of = maps (these o try (#params o AxClass.get_info thy))
   2.339 +      o Sign.complete_sort thy;
   2.340 +    val missing_params = arities
   2.341 +      |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
   2.342 +      |> filter_out (can (inst thy) o apfst fst);
   2.343 +    fun declare_missing ((c, ty), tyco) thy =
   2.344 +      let
   2.345 +        val SOME class = AxClass.class_of_param thy c;
   2.346 +        val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   2.347 +        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
   2.348 +        val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty;
   2.349 +        val c' = NameSpace.base c;
   2.350 +      in
   2.351 +        thy
   2.352 +        |> Sign.sticky_prefix name_inst
   2.353 +        |> Sign.no_base_names
   2.354 +        |> Sign.declare_const [] (c', ty', NoSyn)
   2.355 +        |-> (fn const' as Const (c'', _) => Thm.add_def true
   2.356 +              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty')))
   2.357 +        #>> Thm.varifyT
   2.358 +        #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
   2.359 +        #> primitive_note Thm.internalK (c', thm)
   2.360 +        #> snd
   2.361 +        #> Sign.restore_naming thy))
   2.362 +      end;
   2.363 +  in
   2.364 +    lthy
   2.365 +    |> LocalTheory.theory (fold declare_missing missing_params)
   2.366 +  end;
   2.367 +
   2.368 +val end_instantiation = conclude_instantiation #> LocalTheory.target_of;
   2.369 +
   2.370  end;
     3.1 --- a/src/Pure/Isar/code.ML	Fri Nov 23 21:09:34 2007 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Fri Nov 23 21:09:35 2007 +0100
     3.3 @@ -24,6 +24,7 @@
     3.4    val del_post: thm -> theory -> theory
     3.5    val add_datatype: (string * typ) list -> theory -> theory
     3.6    val add_datatype_cmd: string list -> theory -> theory
     3.7 +  val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory
     3.8    val add_case: thm -> theory -> theory
     3.9    val add_undefined: string -> theory -> theory
    3.10  
    3.11 @@ -537,18 +538,15 @@
    3.12  fun aggregate f [] = NONE
    3.13    | aggregate f (x::xs) = SOME (aggr_neutr f x xs);
    3.14  
    3.15 -fun inter_sorts thy =
    3.16 -  let
    3.17 -    val algebra = Sign.classes_of thy;
    3.18 -    val inters = curry (Sorts.inter_sort algebra);
    3.19 -  in aggregate (map2 inters) end;
    3.20 +fun inter_sorts algebra =
    3.21 +  aggregate (map2 (curry (Sorts.inter_sort algebra)));
    3.22  
    3.23  fun specific_constraints thy (class, tyco) =
    3.24    let
    3.25      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    3.26      val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    3.27      val funcs = classparams
    3.28 -      |> map (fn c => Class.inst_const thy (c, tyco))
    3.29 +      |> map_filter (fn c => try (Class.inst_const thy) (c, tyco))
    3.30        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    3.31        |> (map o Option.map) (Susp.force o fst o snd)
    3.32        |> maps these
    3.33 @@ -558,37 +556,53 @@
    3.34      val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
    3.35    in sorts end;
    3.36  
    3.37 -fun weakest_constraints thy (class, tyco) =
    3.38 +fun weakest_constraints thy algebra (class, tyco) =
    3.39    let
    3.40 -    val all_superclasses = Sign.complete_sort thy [class];
    3.41 -  in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    3.42 +    val all_superclasses = Sorts.complete_sort algebra [class];
    3.43 +  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    3.44     of SOME sorts => sorts
    3.45 -    | NONE => Sign.arity_sorts thy tyco [class]
    3.46 +    | NONE => Sorts.mg_domain algebra tyco [class]
    3.47    end;
    3.48  
    3.49 -fun strongest_constraints thy (class, tyco) =
    3.50 +fun strongest_constraints thy algebra (class, tyco) =
    3.51    let
    3.52 -    val algebra = Sign.classes_of thy;
    3.53      val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class];
    3.54      val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses;
    3.55 -  in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    3.56 +  in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    3.57     of SOME sorts => sorts
    3.58      | NONE => replicate
    3.59 -        (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
    3.60 +        (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra))
    3.61 +  end;
    3.62 +
    3.63 +fun get_algebra thy (class, tyco) =
    3.64 +  let
    3.65 +    val base_algebra = Sign.classes_of thy;
    3.66 +  in if can (Sorts.mg_domain base_algebra tyco) [class]
    3.67 +    then base_algebra
    3.68 +    else let
    3.69 +      val superclasses = Sorts.super_classes base_algebra class;
    3.70 +      val sorts = inter_sorts base_algebra
    3.71 +          (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses)
    3.72 +        |> the_default (replicate (Sign.arity_number thy tyco) [])
    3.73 +    in
    3.74 +      base_algebra
    3.75 +      |> Sorts.add_arities (Sign.pp thy) (tyco, [(class, sorts)])
    3.76 +    end
    3.77    end;
    3.78  
    3.79  fun gen_classparam_typ constr thy class (c, tyco) = 
    3.80    let
    3.81 +    val algebra = get_algebra thy (class, tyco);
    3.82      val cs = these (try (#params o AxClass.get_info thy) class);
    3.83 -    val ty = (the o AList.lookup (op =) cs) c;
    3.84 +    val SOME ty = AList.lookup (op =) cs c;
    3.85      val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
    3.86 -      (constr thy (class, tyco));
    3.87 +      (constr thy algebra (class, tyco));
    3.88      val ty_inst = Type (tyco, map TFree sort_args);
    3.89    in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
    3.90  
    3.91  fun retrieve_algebra thy operational =
    3.92    Sorts.subalgebra (Sign.pp thy) operational
    3.93 -    (weakest_constraints thy)
    3.94 +    (weakest_constraints thy (Sign.classes_of thy))
    3.95      (Sign.classes_of thy);
    3.96  
    3.97  in
    3.98 @@ -763,18 +777,22 @@
    3.99  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   3.100    (fn thm => Context.mapping (add_default_func thm) I));
   3.101  
   3.102 +structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =);
   3.103 +val type_interpretation = TypeInterpretation.interpretation;
   3.104 +
   3.105  fun add_datatype raw_cs thy =
   3.106    let
   3.107      val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
   3.108      val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
   3.109 -    val purge_cs = map fst (snd vs_cos);
   3.110 -    val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   3.111 -     of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
   3.112 +    val cs' = map fst (snd vs_cos);
   3.113 +    val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
   3.114 +     of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos)
   3.115        | NONE => NONE;
   3.116    in
   3.117      thy
   3.118 -    |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
   3.119 +    |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos))
   3.120          #> map_funcs (fold (Symtab.delete_safe o fst) cs))
   3.121 +    |> TypeInterpretation.data (tyco, cs')
   3.122    end;
   3.123  
   3.124  fun add_datatype_cmd raw_cs thy =
   3.125 @@ -837,7 +855,8 @@
   3.126        add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
   3.127          || Scan.succeed (mk_attribute add))
   3.128    in
   3.129 -    add_del_attribute ("func", (add_func, del_func))
   3.130 +    TypeInterpretation.init
   3.131 +    #> add_del_attribute ("func", (add_func, del_func))
   3.132      #> add_del_attribute ("inline", (add_inline, del_inline))
   3.133      #> add_del_attribute ("post", (add_post, del_post))
   3.134    end);
     4.1 --- a/src/Pure/Isar/instance.ML	Fri Nov 23 21:09:34 2007 +0100
     4.2 +++ b/src/Pure/Isar/instance.ML	Fri Nov 23 21:09:35 2007 +0100
     4.3 @@ -2,79 +2,74 @@
     4.4      ID:         $Id$
     4.5      Author:     Florian Haftmann, TU Muenchen
     4.6  
     4.7 -User-level instantiation interface for classes.
     4.8 -FIXME not operative for the moment
     4.9 +A primitive instance command, based on instantiation target.
    4.10  *)
    4.11  
    4.12  signature INSTANCE =
    4.13  sig
    4.14 -  val begin_instantiation: arity list -> theory -> local_theory
    4.15 -  val begin_instantiation_cmd: (xstring * string list * string) list
    4.16 +  val instantiate: arity list -> (local_theory -> local_theory)
    4.17 +    -> (Proof.context -> tactic) -> theory -> theory
    4.18 +  val instance: arity list -> ((bstring * Attrib.src list) * term) list
    4.19 +    -> (thm list -> theory -> theory)
    4.20 +    -> theory -> Proof.state
    4.21 +  val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
    4.22 +    -> theory -> thm list * theory
    4.23 +
    4.24 +  val instantiation_cmd: (xstring * sort * xstring) list
    4.25      -> theory -> local_theory
    4.26 -  val proof_instantiation: local_theory -> Proof.state
    4.27 +  val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
    4.28 +    -> (thm list -> theory -> theory)
    4.29 +    -> theory -> Proof.state
    4.30  end;
    4.31  
    4.32  structure Instance : INSTANCE =
    4.33  struct
    4.34  
    4.35 -structure Instantiation = ProofDataFun
    4.36 -(
    4.37 -  type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list;
    4.38 -  fun init _ = ([], []);
    4.39 -);
    4.40 +fun instantiation_cmd raw_arities thy =
    4.41 +  TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy;
    4.42 +
    4.43 +fun instantiate arities f tac =
    4.44 +  TheoryTarget.instantiation arities
    4.45 +  #> f
    4.46 +  #> Class.prove_instantiation tac
    4.47 +  #> LocalTheory.exit
    4.48 +  #> ProofContext.theory_of;
    4.49  
    4.50 -local
    4.51 -
    4.52 -fun gen_begin_instantiation prep_arity raw_arities thy =
    4.53 +fun gen_instance prep_arity prep_attr prep_term do_proof raw_arities defs after_qed thy =
    4.54    let
    4.55 -    fun prep_arity' raw_arity names =
    4.56 +    fun export_defs ctxt = 
    4.57 +      let
    4.58 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
    4.59 +      in
    4.60 +        map (snd o snd)
    4.61 +        #> map (Assumption.export false ctxt ctxt_thy)
    4.62 +        #> Variable.export ctxt ctxt_thy
    4.63 +      end;
    4.64 +    fun mk_def ctxt ((name, raw_attr), raw_t) =
    4.65        let
    4.66 -        val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
    4.67 -        val vs = Name.invents names Name.aT (length sorts);
    4.68 -        val names' = fold Name.declare vs names;
    4.69 -      in (((tyco, vs ~~ sorts), sort), names') end;
    4.70 -    val (arities, _) = fold_map prep_arity' raw_arities Name.context;
    4.71 -    fun get_param tyco ty_subst (param, (c, ty)) =
    4.72 -      ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty),
    4.73 -        Class.unoverload_const thy (c, ty));
    4.74 -    fun get_params ((tyco, vs), sort) =
    4.75 -      Class.these_params thy sort
    4.76 -      |> map (get_param tyco (Type (tyco, map TFree vs)));
    4.77 -    val params = maps get_params arities;
    4.78 -    val ctxt =
    4.79 -      ProofContext.init thy
    4.80 -      |> Instantiation.put (arities, params);
    4.81 -    val thy_target = TheoryTarget.begin "" ctxt;
    4.82 -    val operations = {
    4.83 -        pretty = LocalTheory.pretty,
    4.84 -        axioms = LocalTheory.axioms,
    4.85 -        abbrev = LocalTheory.abbrev,
    4.86 -        define = LocalTheory.define,
    4.87 -        notes = LocalTheory.notes,
    4.88 -        type_syntax = LocalTheory.type_syntax,
    4.89 -        term_syntax = LocalTheory.term_syntax,
    4.90 -        declaration = LocalTheory.pretty,
    4.91 -        reinit = LocalTheory.reinit,
    4.92 -        exit = LocalTheory.exit
    4.93 -      };
    4.94 -  in TheoryTarget.begin "" ctxt end;
    4.95 +        val attr = map (prep_attr thy) raw_attr;
    4.96 +        val t = prep_term ctxt raw_t;
    4.97 +      in (NONE, ((name, attr), t)) end;
    4.98 +    val arities = map (prep_arity thy) raw_arities;
    4.99 +  in
   4.100 +    thy
   4.101 +    |> TheoryTarget.instantiation arities
   4.102 +    |> `(fn ctxt => map (mk_def ctxt) defs)
   4.103 +    |-> (fn defs => fold_map Specification.definition defs)
   4.104 +    |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
   4.105 +    ||> LocalTheory.exit
   4.106 +    ||> ProofContext.theory_of
   4.107 +    ||> TheoryTarget.instantiation arities
   4.108 +    |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs)))
   4.109 +  end;
   4.110  
   4.111 -in
   4.112 -
   4.113 -val begin_instantiation = gen_begin_instantiation Sign.cert_arity;
   4.114 -val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity;
   4.115 +val instance = gen_instance Sign.cert_arity (K I) (K I)
   4.116 +  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
   4.117 +val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src
   4.118 +  (fn ctxt => Syntax.parse_prop ctxt #> Syntax.check_prop ctxt)
   4.119 +  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
   4.120 +fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
   4.121 +  (fn defs => fn after_qed => Class.prove_instantiation (K tac)
   4.122 +    #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
   4.123  
   4.124  end;
   4.125 -
   4.126 -fun gen_proof_instantiation do_proof after_qed lthy =
   4.127 -  let
   4.128 -    val ctxt = LocalTheory.target_of lthy;
   4.129 -    val arities = case Instantiation.get ctxt
   4.130 -     of ([], _) => error "no instantiation target"
   4.131 -      | (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities;
   4.132 -    val thy = ProofContext.theory_of ctxt;
   4.133 -  in (do_proof after_qed arities) thy end;
   4.134 -
   4.135 -val proof_instantiation = gen_proof_instantiation Class.instance_arity I;
   4.136 -
   4.137 -end;
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Nov 23 21:09:34 2007 +0100
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 23 21:09:35 2007 +0100
     5.3 @@ -113,7 +113,7 @@
     5.4  val _ =
     5.5    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     5.6      (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
     5.7 -      Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
     5.8 +      Toplevel.theory (Typedecl.add (a, args, mx) #> snd)));
     5.9  
    5.10  val _ =
    5.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    5.12 @@ -448,18 +448,18 @@
    5.13    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    5.14    ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    5.15      P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    5.16 -      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *))))
    5.17 +      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    5.18      >> (Toplevel.print oo Toplevel.theory_to_proof));
    5.19  
    5.20  val _ =
    5.21    OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
    5.22 -   (P.and_list1 P.arity -- P.opt_begin
    5.23 -     >> (fn (arities, begin) => (begin ? Toplevel.print) o
    5.24 -         Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities)));
    5.25 +   (P.and_list1 P.arity --| P.begin
    5.26 +     >> (fn arities => Toplevel.print o
    5.27 +         Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    5.28  
    5.29  val _ =  (* FIXME incorporate into "instance" *)
    5.30    OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    5.31 -    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation));
    5.32 +    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
    5.33  
    5.34  
    5.35  (* code generation *)
     6.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 23 21:09:34 2007 +0100
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 23 21:09:35 2007 +0100
     6.3 @@ -2,15 +2,17 @@
     6.4      ID:         $Id$
     6.5      Author:     Makarius
     6.6  
     6.7 -Common theory/locale/class targets.
     6.8 +Common theory/locale/class/instantiation targets.
     6.9  *)
    6.10  
    6.11  signature THEORY_TARGET =
    6.12  sig
    6.13 -  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
    6.14 +  val peek: local_theory -> {target: string, is_locale: bool,
    6.15 +    is_class: bool, instantiation: arity list}
    6.16    val init: string option -> theory -> local_theory
    6.17    val begin: string -> Proof.context -> local_theory
    6.18    val context: xstring -> theory -> local_theory
    6.19 +  val instantiation: arity list -> theory -> local_theory
    6.20  end;
    6.21  
    6.22  structure TheoryTarget: THEORY_TARGET =
    6.23 @@ -18,12 +20,14 @@
    6.24  
    6.25  (* context data *)
    6.26  
    6.27 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    6.28 +datatype target = Target of {target: string, is_locale: bool,
    6.29 +  is_class: bool, instantiation: arity list};
    6.30  
    6.31 -fun make_target target is_locale is_class =
    6.32 -  Target {target = target, is_locale = is_locale, is_class = is_class};
    6.33 +fun make_target target is_locale is_class instantiation =
    6.34 +  Target {target = target, is_locale = is_locale,
    6.35 +    is_class = is_class, instantiation = instantiation};
    6.36  
    6.37 -val global_target = make_target "" false false;
    6.38 +val global_target = make_target "" false false [];
    6.39  
    6.40  structure Data = ProofDataFun
    6.41  (
    6.42 @@ -36,7 +40,7 @@
    6.43  
    6.44  (* pretty *)
    6.45  
    6.46 -fun pretty (Target {target, is_locale, is_class}) ctxt =
    6.47 +fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
    6.48    let
    6.49      val thy = ProofContext.theory_of ctxt;
    6.50      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    6.51 @@ -186,13 +190,18 @@
    6.52               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    6.53    end;
    6.54  
    6.55 -fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
    6.56 +fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
    6.57    let
    6.58      val pos = ContextPosition.properties_of lthy;
    6.59      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    6.60      val U = map #2 xs ---> T;
    6.61      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    6.62 -    val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    6.63 +    val declare_const = if null instantiation
    6.64 +      then Sign.declare_const pos (c, U, mx3)
    6.65 +      else case Class.instantiation_const lthy c
    6.66 +       of SOME c' => Class.declare_overloaded (c', U, mx3)
    6.67 +        | NONE => Sign.declare_const pos (c, U, mx3);
    6.68 +    val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
    6.69      val t = Term.list_comb (const, map Free xs);
    6.70    in
    6.71      lthy'
    6.72 @@ -204,7 +213,7 @@
    6.73  
    6.74  (* abbrev *)
    6.75  
    6.76 -fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy =
    6.77 +fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
    6.78    let
    6.79      val pos = ContextPosition.properties_of lthy;
    6.80      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    6.81 @@ -236,7 +245,7 @@
    6.82  
    6.83  (* define *)
    6.84  
    6.85 -fun define (ta as Target {target, is_locale, is_class})
    6.86 +fun define (ta as Target {target, is_locale, is_class, instantiation})
    6.87      kind ((c, mx), ((name, atts), rhs)) lthy =
    6.88    let
    6.89      val thy = ProofContext.theory_of lthy;
    6.90 @@ -253,12 +262,18 @@
    6.91      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    6.92  
    6.93      (*def*)
    6.94 +    val is_instantiation = not (null instantiation)
    6.95 +      andalso is_some (Class.instantiation_const lthy c);
    6.96 +    val define_const = if not is_instantiation
    6.97 +      then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    6.98 +      else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
    6.99      val (global_def, lthy3) = lthy2
   6.100 -      |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs')));
   6.101 -    val def = LocalDefs.trans_terms lthy3
   6.102 +      |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
   6.103 +    val def = if not is_instantiation then LocalDefs.trans_terms lthy3
   6.104        [(*c == global.c xs*)     local_def,
   6.105         (*global.c xs == rhs'*)  global_def,
   6.106 -       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
   6.107 +       (*rhs' == rhs*)          Thm.symmetric rhs_conv]
   6.108 +      else Thm.transitive local_def global_def;
   6.109  
   6.110      (*note*)
   6.111      val ([(res_name, [res])], lthy4) = lthy3
   6.112 @@ -298,14 +313,18 @@
   6.113  local
   6.114  
   6.115  fun init_target _ NONE = global_target
   6.116 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
   6.117 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
   6.118 +
   6.119 +fun init_instantiaton arities = make_target "" false false arities
   6.120  
   6.121 -fun init_ctxt (Target {target, is_locale, is_class}) =
   6.122 -  if not is_locale then ProofContext.init
   6.123 -  else if not is_class then Locale.init target
   6.124 -  else Class.init target;
   6.125 +fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
   6.126 +  if null instantiation then
   6.127 +    if not is_locale then ProofContext.init
   6.128 +    else if not is_class then Locale.init target
   6.129 +    else Class.init target
   6.130 +  else Class.instantiation instantiation;
   6.131  
   6.132 -fun init_lthy (ta as Target {target, ...}) =
   6.133 +fun init_lthy (ta as Target {target, instantiation, ...}) =
   6.134    Data.put ta #>
   6.135    LocalTheory.init (NameSpace.base target)
   6.136     {pretty = pretty ta,
   6.137 @@ -317,7 +336,7 @@
   6.138      term_syntax = term_syntax ta,
   6.139      declaration = declaration ta,
   6.140      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   6.141 -    exit = LocalTheory.target_of}
   6.142 +    exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
   6.143  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   6.144  
   6.145  in
   6.146 @@ -328,6 +347,9 @@
   6.147  fun context "-" thy = init NONE thy
   6.148    | context target thy = init (SOME (Locale.intern thy target)) thy;
   6.149  
   6.150 +fun instantiation raw_arities thy =
   6.151 +  init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
   6.152 +
   6.153  end;
   6.154  
   6.155  end;