--- 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), []));