--- a/src/Pure/axclass.ML Sun Apr 30 22:50:03 2006 +0200
+++ b/src/Pure/axclass.ML Sun Apr 30 22:50:05 2006 +0200
@@ -2,27 +2,34 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Axiomatic type classes: managing predicates and parameter collections.
+Type classes as parameter records and predicates, with explicit
+definitions and proofs.
*)
signature AX_CLASS =
sig
- val print_axclasses: theory -> unit
- val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list}
+ val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list}
val class_intros: theory -> thm list
val params_of: theory -> class -> string list
val all_params_of: theory -> sort -> string list
+ val print_axclasses: theory -> unit
val cert_classrel: theory -> class * class -> class * class
val read_classrel: theory -> xstring * xstring -> class * class
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 of_sort: theory -> typ * sort -> thm list
- val add_axclass: bstring * xstring list -> string list ->
+ val define_class: bstring * xstring list -> string list ->
((bstring * Attrib.src list) * string list) list -> theory -> class * theory
- val add_axclass_i: bstring * class list -> string list ->
+ val define_class_i: bstring * class list -> string list ->
((bstring * attribute list) * term list) list -> theory -> class * theory
+ val axiomatize_class: bstring * xstring list -> theory -> theory
+ val axiomatize_class_i: bstring * class list -> theory -> theory
+ val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
+ val axiomatize_classrel_i: (class * class) list -> theory -> theory
+ val axiomatize_arity: xstring * string list * string -> theory -> theory
+ val axiomatize_arity_i: arity -> theory -> theory
+ val of_sort: theory -> typ * sort -> thm list
end;
structure AxClass: AX_CLASS =
@@ -46,9 +53,10 @@
fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
-(* axclass *)
+(* axclasses *)
val introN = "intro";
+val superN = "super";
val axiomsN = "axioms";
datatype axclass = AxClass of
@@ -67,6 +75,9 @@
(* instances *)
+val classrelN = "classrel";
+val arityN = "arity";
+
datatype instances = Instances of
{classes: unit Graph.T, (*raw relation -- no closure!*)
classrel: ((class * class) * thm) list,
@@ -89,7 +100,7 @@
Typtab.join (K (merge (eq_fst op =))) (types1, types2));
-(* data *)
+(* setup data *)
structure AxClassData = TheoryDataFun
(struct
@@ -107,24 +118,24 @@
val _ = Context.add_setup AxClassData.init;
-(* classes *)
+(* retrieve axclasses *)
-val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get;
+val lookup_def = Symtab.lookup o #1 o #1 o AxClassData.get;
-fun get_info thy c =
- (case lookup_info thy c of
+fun get_definition thy c =
+ (case lookup_def thy c of
SOME (AxClass info) => info
- | NONE => error ("Unknown axclass " ^ quote c));
+ | NONE => error ("Undefined type class " ^ quote c));
fun class_intros thy =
let
fun add_intro c =
- (case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
+ (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
val classes = Sign.classes thy;
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-(* parameters *)
+(* retrieve parameters *)
fun get_params thy pred =
let val params = #2 (#1 (AxClassData.get thy))
@@ -134,7 +145,7 @@
fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
-(* instances *)
+(* maintain instances *)
val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts);
@@ -158,7 +169,7 @@
(classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th))));
-(* print_axclasses *)
+(* print data *)
fun print_axclasses thy =
let
@@ -168,7 +179,7 @@
fun pretty_axclass (class, AxClass {def, intro, axioms}) =
Pretty.block (Pretty.fbreaks
[Pretty.block
- [Pretty.str "axclass ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
+ [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
Pretty.strs ("parameters:" :: params_of thy class),
ProofContext.pretty_fact ctxt ("def", [def]),
ProofContext.pretty_fact ctxt (introN, [intro]),
@@ -177,14 +188,14 @@
-(** instance proofs **)
+(** instances **)
(* class relations *)
fun cert_classrel thy raw_rel =
let
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
- val _ = Type.add_classrel (Sign.pp thy) [(c1, c2)] (Sign.tsig_of thy);
+ val _ = Type.add_classrel (Sign.pp thy) (c1, c2) (Sign.tsig_of thy);
val _ =
(case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
[] => ()
@@ -205,7 +216,7 @@
val prop = Drule.plain_prop_of (Thm.transfer thy th);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val thy' = thy |> Theory.add_classrel_i [(c1, c2)];
+ val thy' = thy |> Sign.primitive_classrel (c1, c2);
val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th);
in thy' end;
@@ -214,7 +225,7 @@
val prop = Drule.plain_prop_of (Thm.transfer thy th);
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ =>
raise THM ("add_arity: malformed type arity", 0, [th]);
- val thy' = thy |> Theory.add_arities_i [(t, Ss, [c])];
+ val thy' = thy |> Sign.primitive_arity (t, Ss, [c]);
val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th);
in thy' end;
@@ -227,7 +238,11 @@
val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
quote (Sign.string_of_classrel thy [c1, c2]));
- in add_classrel th thy end;
+ in
+ thy
+ |> PureThy.add_thms [((classrelN ^ "_" ^ serial_string (), th), [])]
+ |-> (fn [th'] => add_classrel th')
+ end;
fun prove_arity raw_arity tac thy =
let
@@ -237,10 +252,135 @@
(fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
quote (Sign.string_of_arity thy arity));
- in fold add_arity ths thy end;
+ in
+ thy
+ |> PureThy.add_thms (ths |> map (fn th => ((arityN ^ "_" ^ serial_string (), th), [])))
+ |-> fold add_arity
+ end;
+
+
+
+(** class definitions **)
+
+local
+
+fun def_class prep_class prep_att prep_propp
+ (bclass, raw_super) params raw_specs thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val pp = ProofContext.pp ctxt;
+
+
+ (* prepare specification *)
+
+ val bconst = Logic.const_of_class bclass;
+ val class = Sign.full_name thy bclass;
+ val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
+
+ fun prep_axiom t =
+ (case Term.add_tfrees t [] of
+ [(a, S)] =>
+ if Sign.subsort thy (super, S) then t
+ else error ("Sort constraint of type variable " ^
+ setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
+ " needs to be weaker than " ^ Pretty.string_of_sort pp super)
+ | [] => t
+ | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t))
+ |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
+ |> Logic.close_form;
+
+ val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs)
+ |> snd |> map (map (prep_axiom o fst));
+ val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
+
+
+ (* definition *)
+
+ val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
+ val class_eq =
+ Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs);
+
+ val ([def], def_thy) =
+ thy
+ |> Sign.primitive_class (bclass, super)
+ |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
+ val (raw_intro, (raw_classrel, raw_axioms)) =
+ (Conjunction.split_defined (length conjs) def) ||> chop (length super);
-(* derived instances -- cached *)
+ (* facts *)
+
+ val class_triv = Thm.class_triv def_thy class;
+ val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
+ def_thy
+ |> PureThy.note_thmss_qualified "" bconst
+ [((introN, []), [([Drule.standard raw_intro], [])]),
+ ((superN, []), [(map Drule.standard raw_classrel, [])]),
+ ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])];
+ val _ = map (store_classrel facts_thy) (map (pair class) super ~~ classrel);
+
+
+ (* result *)
+
+ val result_thy =
+ facts_thy
+ |> Sign.add_path bconst
+ |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
+ |> Sign.restore_naming facts_thy
+ |> AxClassData.map (apfst (fn (axclasses, parameters) =>
+ (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses,
+ fold (fn x => add_param pp (x, class)) params parameters)));
+
+ in (class, result_thy) end;
+
+in
+
+val define_class = def_class Sign.read_class Attrib.attribute ProofContext.read_propp;
+val define_class_i = def_class Sign.certify_class (K I) ProofContext.cert_propp;
+
+end;
+
+
+(** axiomatizations **)
+
+local
+
+fun axiomatize kind add prep arg thy =
+ let val specs = arg |> prep thy |> map (fn prop => ((kind ^ "_" ^ serial_string (), prop), []))
+ in thy |> PureThy.add_axioms_i specs |-> fold add end;
+
+fun ax_classrel prep =
+ axiomatize classrelN add_classrel (fn thy => map (prep thy #> Logic.mk_classrel));
+
+fun ax_arity prep =
+ axiomatize arityN add_arity (fn thy => prep thy #> Logic.mk_arities);
+
+fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
+ let
+ val class = Sign.full_name thy bclass;
+ val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
+ in
+ thy
+ |> Sign.primitive_class (bclass, super)
+ |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
+ end;
+
+in
+
+val axiomatize_class = ax_class Sign.read_class read_classrel;
+val axiomatize_class_i = ax_class Sign.certify_class cert_classrel;
+val axiomatize_classrel = ax_classrel read_classrel;
+val axiomatize_classrel_i = ax_classrel cert_classrel;
+val axiomatize_arity = ax_arity Sign.read_arity;
+val axiomatize_arity_i = ax_arity Sign.cert_arity;
+
+end;
+
+
+
+(** explicit derivations -- cached **)
+
+local
fun derive_classrel thy (c1, c2) =
let
@@ -291,6 +431,8 @@
setmp show_sorts true (Sign.string_of_typ thy) T);
in derive end;
+in
+
fun of_sort thy (typ, sort) =
let
fun lookup () = AList.lookup (op =) (Typtab.lookup_list (#types (get_instances thy)) typ);
@@ -316,82 +458,6 @@
in () end);
in map (the o lookup ()) sort end;
-
-
-(** axclass definitions **)
-
-(* add_axclass(_i) *)
-
-fun gen_axclass prep_class prep_att prep_propp
- (bclass, raw_super) params raw_specs thy =
- let
- val ctxt = ProofContext.init thy;
- val pp = ProofContext.pp ctxt;
-
-
- (* prepare specification *)
-
- val bconst = Logic.const_of_class bclass;
- val class = Sign.full_name thy bclass;
- val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
-
- fun prep_axiom t =
- (case Term.add_tfrees t [] of
- [(a, S)] =>
- if Sign.subsort thy (super, S) then t
- else error ("Sort constraint of type variable " ^
- setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
- " needs to be weaker than " ^ Pretty.string_of_sort pp super)
- | [] => t
- | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t))
- |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
- |> Logic.close_form;
-
- val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs)
- |> snd |> map (map (prep_axiom o fst));
- val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
-
-
- (* definition *)
-
- val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
- val class_eq =
- Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs);
-
- val ([def], def_thy) =
- thy
- |> Theory.add_classes_i [(bclass, super)]
- |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
- val (raw_intro, (raw_classrel, raw_axioms)) =
- (Conjunction.split_defined (length conjs) def) ||> chop (length super);
-
-
- (* facts *)
-
- val class_triv = Thm.class_triv def_thy class;
- val ([(_, [intro]), (_, axioms)], facts_thy) =
- def_thy
- |> PureThy.note_thmss_qualified "" bconst
- [((introN, []), [([Drule.standard raw_intro], [])]),
- ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])];
- val _ = map (store_classrel facts_thy)
- (map (pair class) super ~~ map Drule.standard raw_classrel);
-
-
- (* result *)
-
- val result_thy =
- facts_thy
- |> Sign.add_path bconst
- |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
- |> Sign.restore_naming facts_thy
- |> AxClassData.map (apfst (fn (axclasses, parameters) =>
- (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses,
- fold (fn x => add_param pp (x, class)) params parameters)));
-
- in (class, result_thy) end;
-
-val add_axclass = gen_axclass Sign.read_class Attrib.attribute ProofContext.read_propp;
-val add_axclass_i = gen_axclass Sign.certify_class (K I) ProofContext.cert_propp;
+end;
end;