# HG changeset patch
# User wenzelm
# Date 1272370787 -7200
# Node ID 54bc1a44967dfc794e8108213466e4132c9d84f8
# Parent  9459be72b89eb293c7d9fee4f073d5d547ad42a6
misc tuning and simplification;

diff -r 9459be72b89e -r 54bc1a44967d src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Apr 27 10:42:41 2010 +0200
+++ b/src/Pure/axclass.ML	Tue Apr 27 14:19:47 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Type classes defined as predicates, associated with a record of
-parameters.
+parameters.  Proven class relations and type arities.
 *)
 
 signature AX_CLASS =
@@ -104,7 +104,7 @@
       val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
       val params' =
         if null params1 then params2
-        else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
+        else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
 
       (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
       val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
@@ -232,8 +232,8 @@
     val classrels = proven_classrels_of thy;
     val diff_merge_classrels = diff_merge_classrels_of thy;
     val (needed, thy') = (false, thy) |>
-      fold (fn c12 => fn (needed, thy) =>
-          put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
+      fold (fn rel => fn (needed, thy) =>
+          put_trancl_classrel (rel, Symreltab.lookup classrels rel |> the |> #1) thy
           |>> (fn b => needed orelse b))
         diff_merge_classrels;
   in
@@ -253,21 +253,25 @@
 
 fun thynames_of_arity thy (c, a) =
   Symtab.lookup_list (proven_arities_of thy) a
-  |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
+  |> map_filter (fn ((c', _), ((_, name), _)) => if c = c' then SOME name else NONE)
   |> rev;
 
 fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
   let
     val algebra = Sign.classes_of thy;
+    val ars = Symtab.lookup_list arities t;
     val super_class_completions =
       Sign.super_classes thy c
-      |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
-          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
-    val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
+      |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
+            c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
+
+    val names = Name.invents Name.context Name.aT (length Ss);
+    val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
+
     val completions = super_class_completions |> map (fn c1 =>
       let
         val th1 = (th RS the_classrel_thm thy (c, c1))
-          |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
+          |> Drule.instantiate' std_vars []
           |> Thm.close_derivation;
         val prf1 = Thm.proof_of th1;
       in (((th1, thy_name), prf1), c1) end);
@@ -277,12 +281,11 @@
 
 fun put_arity ((t, Ss, c), th) thy =
   let
-    val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
+    val arity = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
   in
     thy
     |> map_proven_arities
-      (Symtab.insert_list (eq_fst op =) arity' #>
-        insert_arity_completions thy arity' #> snd)
+      (Symtab.insert_list (eq_fst op =) arity #> insert_arity_completions thy arity #> #2)
   end;
 
 fun complete_arities thy =
@@ -309,15 +312,15 @@
 
 fun add_inst_param (c, tyco) inst =
   (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
-  #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
+  #> (map_inst_params o apsnd) (Symtab.update_new (#1 inst, (c, tyco)));
 
 val inst_of_param = Symtab.lookup o #2 o inst_params_of;
-val param_of_inst = fst oo get_inst_param;
+val param_of_inst = #1 oo get_inst_param;
 
 fun inst_thms thy =
   Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
 
-fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
+fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
 
 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
@@ -376,7 +379,7 @@
       | NONE => error ("Not a class parameter: " ^ quote c));
     val tyco = inst_tyco_of thy (c, T);
     val name_inst = instance_name (tyco, class) ^ "_inst";
-    val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
+    val c' = instance_name (tyco, c);
     val T' = Type.strip_sorts T;
   in
     thy
@@ -388,7 +391,7 @@
       #>> apsnd Thm.varifyT_global
       #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
         #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
-        #> snd
+        #> #2
         #> pair (Const (c, T))))
     ||> Sign.restore_naming thy
   end;
@@ -399,8 +402,7 @@
     val tyco = inst_tyco_of thy (c, T);
     val (c', eq) = get_inst_param thy (c, tyco);
     val prop = Logic.mk_equals (Const (c', T), t);
-    val b' = Thm.def_binding_optional
-      (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
+    val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   in
     thy
     |> Thm.add_def false false (b', prop)
@@ -426,7 +428,7 @@
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
-    |> (snd oo put_trancl_classrel) ((c1, c2), th')
+    |> (#2 oo put_trancl_classrel) ((c1, c2), th')
     |> perhaps complete_arities
   end;
 
@@ -436,20 +438,23 @@
     val prop = Thm.plain_prop_of th;
     fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
-    val names = Name.names Name.context Name.aT Ss;
-    val T = Type (t, map TFree names);
+
+    val args = Name.names Name.context Name.aT Ss;
+    val T = Type (t, map TFree args);
+    val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), S)))) args;
+
     val missing_params = Sign.complete_sort thy [c]
       |> maps (these o Option.map #params o try (get_info thy))
       |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
       |> (map o apsnd o map_atyps) (K T);
     val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     val th' = th
-      |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
+      |> Drule.instantiate' std_vars []
       |> Thm.unconstrain_allTs;
     val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
-    |> fold (snd oo declare_overloaded) missing_params
+    |> fold (#2 oo declare_overloaded) missing_params
     |> Sign.primitive_arity (t, Ss, [c])
     |> put_arity ((t, Ss, c), th')
   end;
@@ -585,9 +590,9 @@
     val axclass = make_axclass (def, intro, axioms, params);
     val result_thy =
       facts_thy
-      |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
+      |> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel)
       |> Sign.qualified_path false bconst
-      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
+      |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
       |> Sign.restore_naming facts_thy
       |> map_axclasses (Symtab.update (class, axclass))
       |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
@@ -600,8 +605,7 @@
 
 local
 
-(* old-style axioms *)
-
+(*old-style axioms*)
 fun add_axiom (b, prop) =
   Thm.add_axiom (b, prop) #->
   (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));