improved

--- a/src/HOL/Library/Eval.thy	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Wed Dec 05 14:15:51 2007 +0100
@@ -18,47 +18,64 @@
 structure TypOf =
 struct
 
-val class_typ_of = Sign.intern_class @{theory} "typ_of";
-
-fun term_typ_of_type ty =
+fun mk ty =
   Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
     $ Logic.mk_type ty;
 
-fun mk_typ_of_def ty =
-  let
-    val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
-      $ Free ("x", Term.itselfT ty)
-    val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty
-  in Logic.mk_equals (lhs, rhs) end;
-
-end;
+end
 *}
 
-instance "prop" :: typ_of
-  "typ_of (T\<Colon>prop itself) \<equiv> STR ''prop'' {\<struct>} []" ..
-
-instance itself :: (typ_of) typ_of
-  "typ_of (T\<Colon>'a itself itself) \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
-
-instance set :: (typ_of) typ_of
-  "typ_of (T\<Colon>'a set itself) \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
-
-instance int :: typ_of
-  "typ_of (T\<Colon>int itself) \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
-
 setup {*
 let
-  fun mk arities _ thy =
-    (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def
-      (Type (tyco,
-        map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
-  fun hook specs =
-    DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
-      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
-in DatatypeCodegen.add_codetypes_hook hook end
+  fun define_typ_of ty lthy =
+    let
+      val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
+        $ Free ("T", Term.itselfT ty);
+      val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
+      val eq = Class.prep_spec lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+    in lthy |> Specification.definition (NONE, (("", []), eq)) end;
+  fun interpretator tyco thy =
+    let
+      val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
+      val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
+    in
+      thy
+      |> Instance.instantiate ([tyco], sorts, @{sort typ_of})
+           (define_typ_of ty) ((K o K) (Class.intro_classes_tac []))
+    end;
+in TypedefPackage.interpretation interpretator end
 *}
 
+instantiation "prop" :: typ_of
+begin
+
+definition
+  "typ_of (T\<Colon>prop itself) = STR ''prop'' {\<struct>} []"
+
+instance ..
+
+end
+
+instantiation itself :: (typ_of) typ_of
+begin
+
+definition
+  "typ_of (T\<Colon>'a itself itself) = STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
+
+instance ..
+
+end
+
+instantiation set :: (typ_of) typ_of
+begin
+ 
+definition
+  "typ_of (T\<Colon>'a set itself) = STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
+
+instance ..
+
+end
+
 
 subsection {* @{text term_of} class *}
 
@@ -83,7 +100,7 @@
           val lhs : term = term_term_of dty $ c;
           val rhs : term = Pure_term.mk_term
             (fn (v, ty) => term_term_of ty $ Free (v, ty))
-            (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
+            (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
         in
           HOLogic.mk_eq (lhs, rhs)
         end;
@@ -101,24 +118,43 @@
     PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   fun thy_def ((name, atts), t) =
     PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
-  fun mk arities css _ thy =
+  fun prep_dtyp thy vs tyco =
+    let
+      val (_, cs) = DatatypePackage.the_datatype_spec thy tyco;
+      val prep_typ = map_atyps (fn TFree (v, sort) =>
+        TFree (v, (the o AList.lookup (op =) vs) v));
+      fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)),
+        map Free (Name.names Name.context "a" tys));
+    in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end;
+  fun prep thy tycos =
     let
-      val (_, asorts, _) :: _ = arities;
-      val vs = Name.names Name.context "'a" asorts;
+      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
+      val tyco = hd tycos;
+      val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco;
+      val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos;
+      fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #>
+            fold add_tycos tys
+        | add_tycos _ = I;
+      val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos;
+      val sorts = map (inter_sort o snd) vs_proto;
+      val vs = map fst vs_proto ~~ sorts;
+      val css = map (prep_dtyp thy vs) tycos;
       val defs = map (TermOf.mk_terms_of_defs vs) css;
       val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
-    in
-      thy
-      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
-      |> snd
+    in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
+        andalso not (tycos = [@{type_name typ}])
+      then SOME (sorts, defs')
+      else NONE
     end;
-  fun hook specs =
-    if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
-    else
-      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
-      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [TermOf.class_term_of] ((K o K o pair) []) mk
-in DatatypeCodegen.add_codetypes_hook hook end
+  fun interpretator tycos thy = case prep thy tycos
+   of SOME (sorts, defs) =>
+      thy
+      |> Instance.instantiate (tycos, sorts, @{sort term_of})
+           (pair ()) ((K o K) (Class.intro_classes_tac []))
+      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs
+      |> snd
+    | NONE => thy;
+  in DatatypePackage.interpretation interpretator end
 *}
 
 abbreviation

--- a/src/HOL/ex/ExecutableContent.thy	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Wed Dec 05 14:15:51 2007 +0100
@@ -7,7 +7,7 @@
 theory ExecutableContent
 imports
   Main
-  (*Eval*)
+  Eval
   "~~/src/HOL/ex/Records"
   AssocList
   Binomial

--- a/src/Pure/Isar/class.ML	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/Pure/Isar/class.ML	Wed Dec 05 14:15:51 2007 +0100
@@ -31,7 +31,8 @@
   val print_classes: theory -> unit
 
   (*instances*)
-  val init_instantiation: arity list -> theory -> local_theory
+  val init_instantiation: string list * sort list * sort -> theory -> local_theory
+  val prep_spec: local_theory -> term -> term
   val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
   val conclude_instantiation: local_theory -> local_theory
@@ -56,8 +57,8 @@
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
 
   (*old instance layer*)
-  val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
-  val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state
+  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
+  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
 end;
 
 structure Class : CLASS =
@@ -134,7 +135,7 @@
     thy
     |> ProofContext.init
     |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
-        o maps (mk_prop thy)) insts)
+        o mk_prop thy) insts)
   end;
 
 in
@@ -144,11 +145,9 @@
 val instance_arity_cmd =
   gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
 val classrel =
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
-    AxClass.add_classrel I o single;
+  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
 val classrel_cmd =
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
-    AxClass.add_classrel I o single;
+  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
 
 end; (*local*)
 
@@ -826,14 +825,14 @@
 (* bookkeeping *)
 
 datatype instantiation = Instantiation of {
-  arities: arity list,
+  arities: string list * sort list * sort,
   params: ((string * string) * (string * typ)) list
 }
 
 structure Instantiation = ProofDataFun
 (
   type T = instantiation
-  fun init _ = Instantiation { arities = [], params = [] };
+  fun init _ = Instantiation { arities = ([], [], []), params = [] };
 );
 
 fun mk_instantiation (arities, params) =
@@ -844,7 +843,7 @@
   (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
 
 fun the_instantiation lthy = case get_instantiation lthy
- of { arities = [], ... } => error "No instantiation target"
+ of { arities = ([], [], []), ... } => error "No instantiation target"
   | data => data;
 
 val instantiation_params = #params o get_instantiation;
@@ -859,6 +858,19 @@
 
 (* syntax *)
 
+fun subst_param thy params = map_aterms (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
+     of SOME tyco => (case AList.lookup (op =) params (c, tyco)
+         of SOME v_ty => Free v_ty
+          | NONE => t)
+      | NONE => t)
+  | t => t);
+
+fun prep_spec lthy =
+  let
+    val thy = ProofContext.theory_of lthy;
+    val params = instantiation_params lthy;
+  in subst_param thy params end;
+
 fun inst_term_check ts lthy =
   let
     val params = instantiation_params lthy;
@@ -873,12 +885,7 @@
       | check_improve _ = I;
     val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
     val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
-    val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
-         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
-             of SOME v_ty => Free v_ty
-              | NONE => t)
-          | NONE => t)
-      | t => t) ts';
+    val ts'' = map (subst_param thy params) ts';
   in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
 
 fun inst_term_uncheck ts lthy =
@@ -908,33 +915,24 @@
     explode #> scan_valids #> implode
   end;
 
-fun init_instantiation arities thy =
+fun init_instantiation (tycos, sorts, sort) thy =
   let
-    val _ = if null arities then error "At least one arity must be given" else ();
-    val _ = case (duplicates (op =) o map #1) arities
-     of [] => ()
-      | dupl_tycos => error ("Type constructors occur more than once in arities: "
-          ^ commas_quote dupl_tycos);
-    val _ = map (map (the_class_data thy) o #3) arities;
-    val ty_insts = map (fn (tyco, sorts, _) =>
-        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
-      arities;
-    val ty_inst = the o AList.lookup (op =) ty_insts;
+    val _ = if null tycos then error "At least one arity must be given" else ();
+    val _ = map (the_class_data thy) sort;
+    val vs = map TFree (Name.names Name.context Name.aT sorts);
     fun type_name "*" = "prod"
       | type_name "+" = "sum"
       | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
-    fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco)
+    fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco)
       then NONE else SOME ((unoverload_const thy (c, ty), tyco),
-        (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty));
-    fun get_params (tyco, sorts, sort) =
-      map_filter (get_param tyco sorts) (these_params thy sort)
-    val params = maps get_params arities;
+        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
+    val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
   in
     thy
     |> ProofContext.init
-    |> Instantiation.put (mk_instantiation (arities, params))
-    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
-    |> fold ProofContext.add_arity arities
+    |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
+    |> fold (Variable.declare_term o Logic.mk_type) vs
+    |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
     |> Context.proof_map (
         Syntax.add_term_check 0 "instance" inst_term_check
         #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
@@ -942,8 +940,8 @@
 
 fun gen_instantiation_instance do_proof after_qed lthy =
   let
-    val arities = (#arities o the_instantiation) lthy;
-    val arities_proof = maps Logic.mk_arities arities;
+    val (tycos, sorts, sort) = (#arities o the_instantiation) lthy;
+    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed' results =
       LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
       #> after_qed;
@@ -962,6 +960,7 @@
 fun conclude_instantiation lthy =
   let
     val { arities, params } = the_instantiation lthy;
+    val (tycos, sorts, sort) = arities;
     val thy = ProofContext.theory_of lthy;
     (*val _ = map (fn (tyco, sorts, sort) =>
       if Sign.of_sort thy
@@ -970,8 +969,8 @@
         arities; FIXME activate when old instance command is gone*)
     val params_of = maps (these o try (#params o AxClass.get_info thy))
       o Sign.complete_sort thy;
-    val missing_params = arities
-      |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
+    val missing_params = tycos
+      |> maps (fn tyco => params_of sort |> map (rpair tyco))
       |> filter_out (can (inst thy) o apfst fst);
     fun declare_missing ((c, ty0), tyco) thy =
     (*fun declare_missing ((c, tyco), (_, ty)) thy =*)

--- a/src/Pure/Isar/instance.ML	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Wed Dec 05 14:15:51 2007 +0100
@@ -7,35 +7,38 @@
 
 signature INSTANCE =
 sig
-  val instantiate: arity list -> (local_theory -> local_theory)
-    -> (Proof.context -> tactic) -> theory -> theory
-  val instance: arity list -> ((bstring * Attrib.src list) * term) list
-    -> theory -> Proof.state
-  val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
-    -> theory -> thm list * theory
+  val instantiate: string list * sort list * sort -> (local_theory -> 'a * local_theory)
+    -> (Proof.context -> 'a -> tactic) -> theory -> theory
 
-  val instantiation_cmd: (xstring * sort * xstring) list
-    -> theory -> local_theory
-  val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
+  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
+  val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list
     -> theory -> Proof.state
 end;
 
 structure Instance : INSTANCE =
 struct
 
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+  let
+    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+    val tycos = map #1 all_arities;
+    val (_, sorts, sort) = hd all_arities;
+  in (tycos, sorts, sort) end;
+
 fun instantiation_cmd raw_arities thy =
-  TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy;
+  TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
 
 fun instantiate arities f tac =
   TheoryTarget.instantiation arities
   #> f
-  #> Class.prove_instantiation_instance tac
+  #-> (fn result => Class.prove_instantiation_instance (fn ctxt => tac ctxt result))
   #> LocalTheory.exit
   #> ProofContext.theory_of;
 
 fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
   let
-    val arities = map (prep_arity thy) raw_arities;
+    val (tyco, sorts, sort) = prep_arity thy raw_arities;
     fun export_defs ctxt = 
       let
         val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
@@ -53,32 +56,21 @@
       let
         val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
       in Specification.definition def' ctxt end;
-  in if not (null defs) orelse forall (fn (_, _, sort) =>
-      forall (Class.is_class thy) sort) arities
+  in if not (null defs) orelse forall (Class.is_class thy) sort
   then
     thy
-    |> TheoryTarget.instantiation arities
+    |> TheoryTarget.instantiation ([tyco], sorts, sort)
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
     ||> LocalTheory.reinit
-    (*||> ProofContext.theory_of
-    ||> TheoryTarget.instantiation arities*)
     |-> (fn defs => do_proof defs)
   else
     thy
-    |> do_proof' arities
+    |> do_proof' (tyco, sorts, sort)
   end;
 
-val instance = gen_instance Sign.cert_arity (K I) (K I)
-  (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
 val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
   (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
-fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
-  (fn defs => Class.prove_instantiation_instance (K tac)
-    #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs)
-   (pair [] o ProofContext.theory_of o Proof.global_terminal_proof
-      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
-      oo Class.instance_arity I) arities defs;
 
 end;

--- a/src/Pure/Isar/isar_syn.ML	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 05 14:15:51 2007 +0100
@@ -446,15 +446,15 @@
 
 val _ =
   OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
-   (P.and_list1 P.arity --| P.begin
+   (P.multi_arity --| P.begin
      >> (fn arities => Toplevel.print o
          Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
 
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-      >> (fn (arities, defs) => Instance.instance_cmd arities defs))
+    P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
+      >> (fn (arity, defs) => Instance.instance_cmd arity defs))
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 

--- a/src/Pure/Isar/overloading.ML	Wed Dec 05 14:15:48 2007 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Dec 05 14:15:51 2007 +0100
@@ -8,6 +8,7 @@
 signature OVERLOADING =
 sig
   val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
+  val prep_spec: local_theory -> term -> term
   val conclude: local_theory -> local_theory
   val declare: string * typ -> theory -> term * theory
   val confirm: string -> local_theory -> local_theory
@@ -45,14 +46,21 @@
 
 (* syntax *)
 
+fun subst_operation overloading = map_aterms (fn t as Const (c, ty) =>
+    (case AList.lookup (op =) overloading (c, ty)
+     of SOME (v, _) => Free (v, ty)
+      | NONE => t)
+  | t => t);
+
+fun prep_spec lthy =
+  let
+    val overloading = get_overloading lthy;
+  in subst_operation overloading end;
+
 fun term_check ts lthy =
   let
     val overloading = get_overloading lthy;
-    fun subst (t as Const (c, ty)) = (case AList.lookup (op =) overloading (c, ty)
-         of SOME (v, _) => Free (v, ty)
-          | NONE => t)
-      | subst t = t;
-    val ts' = (map o map_aterms) subst ts;
+    val ts' = map (subst_operation overloading) ts;
   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
 
 fun term_uncheck ts lthy =