src/Pure/axclass.ML

     (Thm.binding * term list) list -> theory -> class * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
   val prove_arity: string * sort list * sort -> tactic -> theory -> theory
-  val get_info: theory -> class ->
-    {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+  val get_info: theory -> class -> info
   val class_intros: theory -> thm list
   val class_of_param: theory -> string -> class option
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
   val axiomatize_class: binding * class list -> theory -> theory

 fun merge_params _ ([], qs) = qs
   | merge_params pp (ps, qs) =
       fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
 
 
-(* axclasses *)
-
-datatype axclass = AxClass of
+(* axclass info *)
+
+type info =
  {def: thm,
   intro: thm,
   axioms: thm list,
   params: (string * typ) list};
 
-type axclasses = axclass Symtab.table * param list;
-
-fun make_axclass ((def, intro, axioms), params) = AxClass
+type axclasses = info Symtab.table * param list;
+
+fun make_axclass ((def, intro, axioms), params): info =
   {def = def, intro = intro, axioms = axioms, params = params};
 
 fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
   (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
 

     Symtab.merge (K true) (param_const1, param_const2));
 
 
 (* setup data *)
 
-structure AxClassData = Theory_Data_PP
+structure Data = Theory_Data_PP
 (
   type T = axclasses * ((instances * inst_params) * (class * class) list);
   val empty = ((Symtab.empty, []), (((Symreltab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), []));
   val extend = I;
   fun merge pp ((axclasses1, ((instances1, inst_params1), diff_merge_classrels1)),
     (axclasses2, ((instances2, inst_params2), diff_merge_classrels2))) =
     let
-      val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2)
-      val diff_merge_classrels = subtract (op =) classrels1 classrels2
-        @ subtract (op =) classrels2 classrels1
-        @ diff_merge_classrels1 @ diff_merge_classrels2
+      val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2);
+      val diff_merge_classrels =
+        subtract (op =) classrels1 classrels2 @
+        subtract (op =) classrels2 classrels1 @
+        diff_merge_classrels1 @ diff_merge_classrels2;
     in
       (merge_axclasses pp (axclasses1, axclasses2),
         ((merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)),
           diff_merge_classrels))
     end;
 );
 
 
 (* maintain axclasses *)
 
-val get_axclasses = #1 o AxClassData.get;
-val map_axclasses = AxClassData.map o apfst;
-
-val lookup_def = Symtab.lookup o #1 o get_axclasses;
+val get_axclasses = #1 o Data.get;
+val map_axclasses = Data.map o apfst;
 
 fun get_info thy c =
-  (case lookup_def thy c of
-    SOME (AxClass info) => info
+  (case Symtab.lookup (#1 (get_axclasses thy)) c of
+    SOME info => info
   | NONE => error ("No such axclass: " ^ quote c));
 
 fun class_intros thy =
   let
-    fun add_intro c =
-      (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
+    fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
     val classes = Sign.all_classes thy;
   in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
 
-
-fun get_params thy pred =
+fun all_params_of thy S =
   let val params = #2 (get_axclasses thy);
-  in fold (fn (x, c) => if pred c then cons x else I) params [] end;
-
-fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
+  in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
 
 fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
 
 
 (* maintain instances *)
 
 fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
 
-val get_instances = #1 o #1 o #2 o AxClassData.get;
-val map_instances = AxClassData.map o apsnd o apfst o apfst;
-
-val get_diff_merge_classrels = #2 o #2 o AxClassData.get;
-val clear_diff_merge_classrels = AxClassData.map (apsnd (apsnd (K [])));
+val get_instances = #1 o #1 o #2 o Data.get;
+val map_instances = Data.map o apsnd o apfst o apfst;
+
+val get_diff_merge_classrels = #2 o #2 o Data.get;
+val clear_diff_merge_classrels = Data.map (apsnd (apsnd (K [])));
 
 
 fun the_classrel thy (c1, c2) =
   (case Symreltab.lookup (#1 (get_instances thy)) (c1, c2) of
     SOME classrel => classrel

 fun the_classrel_thm thy = Thm.transfer thy o fst o the_classrel thy;
 fun the_classrel_prf thy = snd o the_classrel thy;
 
 fun put_trancl_classrel ((c1, c2), th) thy =
   let
-    val classrels = fst (get_instances thy)
-    val alg = Sign.classes_of thy
-    val {classes, ...} = alg |> Sorts.rep_algebra
+    val cert = Thm.cterm_of thy;
+    val certT = Thm.ctyp_of thy;
+
+    val classrels = fst (get_instances thy);
+    val classes = #classes (Sorts.rep_algebra (Sign.classes_of thy));
 
     fun reflcl_classrel (c1', c2') =
-      if c1' = c2' then Thm.trivial (Logic.mk_of_class (TVar(("'a",0),[]), c1') |> cterm_of thy)
-      else the_classrel_thm thy (c1', c2')
+      if c1' = c2'
+      then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
+      else the_classrel_thm thy (c1', c2');
     fun gen_classrel (c1_pred, c2_succ) =
       let
         val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
-          |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] []
-          |> Thm.close_derivation
-        val prf' = th' |> Thm.proof_of
-      in ((c1_pred, c2_succ), (th',prf')) end
-
-    val new_classrels = Library.map_product pair
-        (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+          |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
+          |> Thm.close_derivation;
+        val prf' = th' |> Thm.proof_of;
+      in ((c1_pred, c2_succ), (th', prf')) end;
+
+    val new_classrels =
+      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
       |> filter_out (Symreltab.defined classrels)
-      |> map gen_classrel
-    val needed = length new_classrels > 0
+      |> map gen_classrel;
+    val needed = not (null new_classrels);
   in
     (needed,
      if needed then
        thy |> map_instances (fn (classrels, arities) =>
          (classrels |> fold Symreltab.update new_classrels, arities))
      else thy)
   end;
 
 fun complete_classrels thy =
   let
-    val diff_merge_classrels = get_diff_merge_classrels thy
-    val classrels = fst (get_instances thy)
+    val diff_merge_classrels = get_diff_merge_classrels thy;
+    val classrels = fst (get_instances thy);
     val (needed, thy') = (false, thy) |>
       fold (fn c12 => fn (needed, thy) =>
           put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> fst) thy
           |>> (fn b => needed orelse b))
-        diff_merge_classrels
+        diff_merge_classrels;
   in
     if null diff_merge_classrels then NONE
     else thy' |> clear_diff_merge_classrels |> SOME
   end;
 

     val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
     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) []
-          |> Thm.close_derivation
-        val prf1 = Thm.proof_of th1
-      in (((th1,thy_name), prf1), c1) end)
+          |> Thm.close_derivation;
+        val prf1 = Thm.proof_of th1;
+      in (((th1, thy_name), prf1), c1) end);
     val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
       completions arities;
   in (null completions, arities') end;
 
 fun put_arity ((t, Ss, c), th) thy =

   (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities))
 
 
 (* maintain instance parameters *)
 
-val get_inst_params = #2 o #1 o #2 o AxClassData.get;
-val map_inst_params = AxClassData.map o apsnd o apfst o apsnd;
+val get_inst_params = #2 o #1 o #2 o Data.get;
+val map_inst_params = Data.map o apsnd o apfst o apsnd;
 
 fun get_inst_param thy (c, tyco) =
-  case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
-   of SOME c' => c'
-    | NONE => error ("No instance parameter for constant " ^ quote c
-        ^ " on type constructor " ^ quote tyco);
-
-fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
-      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
+  (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (get_inst_params thy)) c)) tyco of
+    SOME c' => c'
+  | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
+
+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)));
 
 val inst_of_param = Symtab.lookup o snd o get_inst_params;
 val param_of_inst = fst oo get_inst_param;
 
-fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
-  (get_inst_params thy) [];
+fun inst_thms thy =
+  (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) (get_inst_params thy) [];
 
 fun get_inst_tyco consts = try (fst 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));
 
 fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
 fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
 
-fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
- of SOME tyco => AList.lookup (op =) params (c, tyco)
-  | NONE => NONE;
+fun lookup_inst_param consts params (c, T) =
+  (case get_inst_tyco consts (c, T) of
+    SOME tyco => AList.lookup (op =) params (c, tyco)
+  | NONE => NONE);
 
 fun unoverload_const thy (c_ty as (c, _)) =
-  if is_some (class_of_param thy c)
-  then case get_inst_tyco (Sign.consts_of thy) c_ty
-   of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
-    | NONE => c
+  if is_some (class_of_param thy c) then
+    (case get_inst_tyco (Sign.consts_of thy) c_ty of
+      SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+    | NONE => c)
   else c;
+
 
 
 (** instances **)
 
 (* class relations *)

 
 fun read_classrel thy raw_rel =
   cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
     handle TYPE (msg, _, _) => error msg;
 
-fun check_shyps_topped th errmsg =
-  let val {shyps, ...} = Thm.rep_thm th
-  in
-    forall null shyps orelse raise Fail errmsg
-  end;
+val shyps_topped = forall null o #shyps o Thm.rep_thm;
+
 
 (* declaration and definition of instances of overloaded constants *)
 
 fun inst_tyco_of thy (c, T) =
   (case get_inst_tyco (Sign.consts_of thy) (c, T) of

     val rel = Logic.dest_classrel prop handle TERM _ => err ();
     val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
     val th' = th
       |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
       |> Drule.unconstrainTs;
-    val _ = check_shyps_topped th' "add_classrel: nontop shyps after unconstrain"
+    val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
   in
     thy
     |> Sign.primitive_classrel (c1, c2)
     |> (snd oo put_trancl_classrel) ((c1, c2), th')
     |> perhaps complete_arities

       |> (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.unconstrainTs;
-    val _ = check_shyps_topped th' "add_arity: nontop shyps after unconstrain"
+    val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
   in
     thy
     |> fold (snd oo declare_overloaded) missing_params
     |> Sign.primitive_arity (t, Ss, [c])
     |> put_arity ((t, Ss, c), th')