--- a/src/Pure/axclass.ML Thu Jun 16 12:04:33 1994 +0200
+++ b/src/Pure/axclass.ML Thu Jun 16 12:05:53 1994 +0200
@@ -2,23 +2,33 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-User interface for axiomatic type classes.
-
-TODO:
- arity_tac: FILTER is_arity (?), assume_tac (?) (no?)
+Higher level user interfaces for axiomatic type classes.
*)
signature AX_CLASS =
sig
structure Tactical: TACTICAL
- local open Tactical Tactical.Thm in
+ local open Tactical Tactical.Thm Tactical.Thm.Sign.Syntax.Mixfix in
+ val add_thms_as_axms: (string * thm) list -> theory -> theory
+ val add_classrel_thms: thm list -> theory -> theory
+ val add_arity_thms: thm list -> theory -> theory
val add_axclass: class * class list -> (string * string) list
-> theory -> theory
val add_axclass_i: class * class list -> (string * term) list
-> theory -> theory
- val add_instance: string * sort list * class -> string list -> thm list
+ val add_sigclass: class * class list -> (string * string * mixfix) list
+ -> theory -> theory
+ val add_sigclass_i: class * class list -> (string * typ * mixfix) list
+ -> theory -> theory
+ val axclass_tac: theory -> thm list -> tactic
+ val prove_classrel: theory -> class * class -> thm list
+ -> tactic option -> thm
+ val prove_arity: theory -> string * sort list * class -> thm list
+ -> tactic option -> thm
+ val add_subclass: class * class -> string list -> thm list
-> tactic option -> theory -> theory
- val axclass_tac: theory -> tactic
+ val add_instance: string * sort list * class list -> string list
+ -> thm list -> tactic option -> theory -> theory
end
end;
@@ -34,30 +44,13 @@
open Logic Thm Tactical Tactic Goals;
-(* FIXME -> type.ML *)
-
-structure Type =
-struct
- open Type;
-
- fun str_of_sort [c] = c
- | str_of_sort cs = parents "{" "}" (commas cs);
+(* FIXME fake! - remove *)
- fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom));
-
- fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
- | str_of_arity (t, SS, S) =
- t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
-end;
-
-
-(** add constant definitions **) (* FIXME -> drule.ML (?) *)
-
-(* FIXME fake! *)
val add_defns = add_axioms;
val add_defns_i = add_axioms_i;
+
(** utilities **)
(* type vars *)
@@ -88,7 +81,99 @@
-(** add axiomatic type class **)
+(** abstract syntax operations **) (* FIXME -> logic.ML (?) *)
+
+(* subclass relations as terms *)
+
+fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2);
+
+fun dest_classrel tm =
+ let
+ fun err () = raise_term "dest_classrel" [tm];
+
+ val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
+ val c1 = (case ty of TFree (_, [c]) => c | _ => err ());
+ in
+ (c1, c2)
+ end;
+
+
+(* arities as terms *)
+
+fun mk_arity (t, ss, c) =
+ let
+ val names = variantlist (replicate (length ss) "'a", []);
+ val tfrees = map TFree (names ~~ ss);
+ in
+ mk_inclass (Type (t, tfrees), c)
+ end;
+
+fun dest_arity tm =
+ let
+ fun err () = raise_term "dest_arity" [tm];
+
+ val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
+ val (t, tfrees) =
+ (case ty of
+ Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys)
+ | _ => err ());
+ val ss =
+ if null (gen_duplicates eq_fst tfrees)
+ then map snd tfrees else err ();
+ in
+ (t, ss, c)
+ end;
+
+
+
+(** add theorems as axioms **) (* FIXME -> drule.ML (?) *)
+
+fun prep_thm_axm thy thm =
+ let
+ fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
+
+ val {sign, hyps, prop, ...} = rep_thm thm;
+ in
+ if not (Sign.subsig (sign, sign_of thy)) then
+ err "theorem not of same theory"
+ else if not (null hyps) then
+ err "theorem may not contain hypotheses"
+ else prop
+ end;
+
+(*general theorems*)
+fun add_thms_as_axms thms thy =
+ add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
+
+(*theorems expressing class relations*)
+fun add_classrel_thms thms thy =
+ let
+ fun prep_thm thm =
+ let
+ val prop = prep_thm_axm thy thm;
+ val (c1, c2) = dest_classrel prop handle TERM _ =>
+ raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
+ in (c1, c2) end;
+ in
+ add_classrel (map prep_thm thms) thy
+ end;
+
+(*theorems expressing arities*)
+fun add_arity_thms thms thy =
+ let
+ fun prep_thm thm =
+ let
+ val prop = prep_thm_axm thy thm;
+ val (t, ss, c) = dest_arity prop handle TERM _ =>
+ raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
+ in (t, ss, [c]) end;
+ in
+ add_arities (map prep_thm thms) thy
+ end;
+
+
+
+(** add axiomatic type classes **)
(* errors *)
@@ -154,40 +239,23 @@
val add_axclass_i = ext_axclass cert_axm;
-
-(** add class instance **)
-
-(* arities as terms *)
-
-fun mk_arity (t, ss, c) =
- let
- val names = variantlist (replicate (length ss) "'a", []);
- val tvars = map (fn a => TVar ((a, 0), logicS)) names;
- in
- mk_inclass (Type (t, tvars), c)
- end;
+(* add signature classes *)
-fun dest_arity tm =
- let
- fun err () = raise_term "dest_arity" [tm];
+fun ext_sigclass add_cnsts (class, super_classes) consts old_thy =
+ old_thy
+ |> add_axclass (class, super_classes) []
+ |> add_defsort [class]
+ |> add_cnsts consts
+ |> add_defsort (Type.defaultS (#tsig (Sign.rep_sg (sign_of old_thy))));
- val (ty, c) = dest_inclass tm handle TERM _ => err ();
- val (t, tvars) =
- (case ty of
- Type (t, tys) => (t, map (fn TVar x => x | _ => err ()) tys)
- | _ => err ());
- val ss =
- if null (gen_duplicates eq_fst tvars)
- then map snd tvars else err ();
- in
- (t, ss, c)
- end;
+val add_sigclass = ext_sigclass add_consts;
+val add_sigclass_i = ext_sigclass add_consts_i;
-(* axclass_tac *)
-(*repeatedly resolve subgoals of form "(| ty : c_class |)";
- try "cI" axioms first and use class_triv as last resort*)
+(** prove class relations and type arities **)
+
+(* class_axms *)
fun class_axms thy =
let
@@ -198,49 +266,64 @@
map (class_triv thy) classes
end;
-fun axclass_tac thy =
- REPEAT_FIRST (resolve_tac (class_axms thy));
+
+(* axclass_tac *)
+
+(*(1) repeatedly resolve goals of form "(| ty : c_class |)",
+ try "cI" axioms first and use class_triv as last resort
+ (2) rewrite goals using user supplied definitions
+ (3) repeatedly resolve goals with user supplied non-definitions*)
+
+fun axclass_tac thy thms =
+ TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
+ TRY (rewrite_goals_tac (filter is_defn thms)) THEN
+ TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms)));
-(* prove_arity *)
+(* provers *)
-(*(* FIXME *)
-(* FIXME state sign vs sign (!?) *)
-fun weaker_arity state =
- all_subsort (ss, #2 (dest_arity (concl_of state)))
- handle TERM _ => false;
-*)
-
-fun prove_arity thy (arity as (t, ss, c)) thms usr_tac =
+fun prove term_of str_of thy sig_prop thms usr_tac =
let
val sign = sign_of thy;
- val all_subsort = forall2 (Sign.subsort sign);
-
- val arity_goal = cterm_of sign (mk_arity arity);
-
- val arity_tac =
- axclass_tac thy THEN
- TRY (rewrite_goals_tac (filter is_defn thms)) THEN
- TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))) THEN
- (if_none usr_tac all_tac);
+ val goal = cterm_of sign (term_of sig_prop);
+ val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac);
+ in
+ prove_goalw_cterm [] goal (K [tac])
+ end
+ handle ERROR => error ("The error(s) above occurred while trying to prove "
+ ^ quote (str_of sig_prop));
- val arity_thm = prove_goalw_cterm [] arity_goal (K [arity_tac]);
+val prove_classrel =
+ prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2);
- val (t', ss', c') = dest_arity (#prop (rep_thm arity_thm))
- handle TERM _ => error "Result is not an arity";
- in
- if t = t' andalso all_subsort (ss, ss') andalso c = c' then ()
- else error ("Proved different arity: " ^ Type.str_of_arity (t', ss', [c']))
- end
- handle ERROR => error ("The error(s) above occurred while trying to prove: " ^
- Type.str_of_arity (t, ss, [c]));
+val prove_arity =
+ prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c]));
-(* external interface *)
+(* make goals (for interactive use) *)
+
+fun mk_goal term_of thy sig_prop =
+ goalw_cterm [] (cterm_of (sign_of thy) (term_of sig_prop));
+
+val goal_subclass = mk_goal mk_classrel;
+val goal_arity = mk_goal mk_arity;
+
+
+
+(** add proved class relations and instances **)
-fun add_instance (t, ss, c) axms thms usr_tac thy =
- (prove_arity thy (t, ss, c) (get_axioms thy axms @ thms) usr_tac;
- add_arities [(t, ss, [c])] thy);
+fun add_subclass (c1, c2) axms thms usr_tac thy =
+ add_classrel_thms
+ [prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
+
+fun add_instance (t, ss, cs) axms thms usr_tac thy =
+ let
+ val usr_thms = get_axioms thy axms @ thms;
+ fun prove c =
+ prove_arity thy (t, ss, c) usr_thms usr_tac;
+ in
+ add_arity_thms (map prove cs) thy
+ end;
end;