src/Pure/axclass.ML
author wenzelm
Tue Aug 23 19:31:05 1994 +0200 (1994-08-23)
changeset 573 2fa5ef27bd0a
parent 560 6702a715281d
child 638 7f25cc9067e7
permissions -rw-r--r--
removed constant _constrain from Pure sig;
     1 (*  Title:      Pure/axclass.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 User interfaces for axiomatic type classes.
     6 *)
     7 
     8 signature AX_CLASS =
     9 sig
    10   structure Tactical: TACTICAL
    11   local open Tactical Tactical.Thm in
    12     val add_thms_as_axms: (string * thm) list -> theory -> theory
    13     val add_classrel_thms: thm list -> theory -> theory
    14     val add_arity_thms: thm list -> theory -> theory
    15     val add_axclass: class * class list -> (string * string) list
    16       -> theory -> theory
    17     val add_axclass_i: class * class list -> (string * term) list
    18       -> theory -> theory
    19     val add_inst_subclass: class * class -> string list -> thm list
    20       -> tactic option -> theory -> theory
    21     val add_inst_arity: string * sort list * class list -> string list
    22       -> thm list -> tactic option -> theory -> theory
    23     val axclass_tac: theory -> thm list -> tactic
    24     val goal_subclass: theory -> class * class -> thm list
    25     val goal_arity: theory -> string * sort list * class -> thm list
    26   end
    27 end;
    28 
    29 functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC
    30   sharing Goals.Tactical = Tactic.Tactical): AX_CLASS =
    31 struct
    32 
    33 structure Tactical = Goals.Tactical;
    34 structure Thm = Tactical.Thm;
    35 structure Sign = Thm.Sign;
    36 structure Type = Sign.Type;
    37 structure Pretty = Sign.Syntax.Pretty;
    38 
    39 open Logic Thm Tactical Tactic Goals;
    40 
    41 
    42 (** utilities **)
    43 
    44 (* type vars *)
    45 
    46 fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys)
    47   | map_typ_frees f (TFree a) = f a
    48   | map_typ_frees _ a = a;
    49 
    50 val map_term_tfrees = map_term_types o map_typ_frees;
    51 
    52 fun aT S = TFree ("'a", S);
    53 
    54 
    55 (* get axioms *)
    56 
    57 fun get_ax thy name =
    58   Some (get_axiom thy name) handle THEORY _ => None;
    59 
    60 val get_axioms = mapfilter o get_ax;
    61 
    62 
    63 (* is_defn *)
    64 
    65 fun is_defn thm =
    66   (case #prop (rep_thm thm) of
    67     Const ("==", _) $ _ $ _ => true
    68   | _ => false);
    69 
    70 
    71 
    72 (** abstract syntax operations **)
    73 
    74 (* subclass relations as terms *)
    75 
    76 fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2);
    77 
    78 fun dest_classrel tm =
    79   let
    80     fun err () = raise_term "dest_classrel" [tm];
    81 
    82     val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
    83     val c1 = (case ty of TFree (_, [c]) => c | _ => err ());
    84   in
    85     (c1, c2)
    86   end;
    87 
    88 
    89 (* arities as terms *)
    90 
    91 fun mk_arity (t, ss, c) =
    92   let
    93     val names = tl (variantlist (replicate (length ss + 1) "'", []));
    94     val tfrees = map TFree (names ~~ ss);
    95   in
    96     mk_inclass (Type (t, tfrees), c)
    97   end;
    98 
    99 fun dest_arity tm =
   100   let
   101     fun err () = raise_term "dest_arity" [tm];
   102 
   103     val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
   104     val (t, tfrees) =
   105       (case ty of
   106         Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys)
   107       | _ => err ());
   108     val ss =
   109       if null (gen_duplicates eq_fst tfrees)
   110       then map snd tfrees else err ();
   111   in
   112     (t, ss, c)
   113   end;
   114 
   115 
   116 
   117 (** add theorems as axioms **)
   118 
   119 fun prep_thm_axm thy thm =
   120   let
   121     fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
   122 
   123     val {sign, hyps, prop, ...} = rep_thm thm;
   124   in
   125     if not (Sign.subsig (sign, sign_of thy)) then
   126       err "theorem not of same theory"
   127     else if not (null hyps) then
   128       err "theorem may not contain hypotheses"
   129     else prop
   130   end;
   131 
   132 (*general theorems*)
   133 fun add_thms_as_axms thms thy =
   134   add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
   135 
   136 (*theorems expressing class relations*)
   137 fun add_classrel_thms thms thy =
   138   let
   139     fun prep_thm thm =
   140       let
   141         val prop = prep_thm_axm thy thm;
   142         val (c1, c2) = dest_classrel prop handle TERM _ =>
   143           raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
   144       in (c1, c2) end;
   145   in
   146     add_classrel (map prep_thm thms) thy
   147   end;
   148 
   149 (*theorems expressing arities*)
   150 fun add_arity_thms thms thy =
   151   let
   152     fun prep_thm thm =
   153       let
   154         val prop = prep_thm_axm thy thm;
   155         val (t, ss, c) = dest_arity prop handle TERM _ =>
   156           raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
   157       in (t, ss, [c]) end;
   158   in
   159     add_arities (map prep_thm thms) thy
   160   end;
   161 
   162 
   163 
   164 (** add axiomatic type classes **)
   165 
   166 (* errors *)
   167 
   168 fun err_not_logic c =
   169   error ("Axiomatic class " ^ quote c ^ " not subclass of \"logic\"");
   170 
   171 fun err_bad_axsort ax c =
   172   error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
   173 
   174 fun err_bad_tfrees ax =
   175   error ("More than one type variable in axiom " ^ quote ax);
   176 
   177 
   178 (* ext_axclass *)
   179 
   180 fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy =
   181   let
   182     val axioms = map (prep_axm (sign_of old_thy)) raw_axioms;
   183     val thy = add_classes [(class, super_classes)] old_thy;
   184     val sign = sign_of thy;
   185 
   186 
   187     (* prepare abstract axioms *)
   188 
   189     fun abs_axm ax =
   190       if null (term_tfrees ax) then
   191         mk_implies (mk_inclass (aT logicS, class), ax)
   192       else
   193         map_term_tfrees (K (aT [class])) ax;
   194 
   195     val abs_axioms = map (apsnd abs_axm) axioms;
   196 
   197 
   198     (* prepare introduction orule *)
   199 
   200     val _ =
   201       if Sign.subsort sign ([class], logicS) then ()
   202       else err_not_logic class;
   203 
   204     fun axm_sort (name, ax) =
   205       (case term_tfrees ax of
   206         [] => []
   207       | [(_, S)] =>
   208           if Sign.subsort sign ([class], S) then S
   209           else err_bad_axsort name class
   210       | _ => err_bad_tfrees name);
   211 
   212     val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
   213 
   214     val int_axm = close_form o map_term_tfrees (K (aT axS));
   215     fun inclass c = mk_inclass (aT axS, c);
   216 
   217     val intro_axm = list_implies
   218       (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   219   in
   220     add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
   221   end;
   222 
   223 
   224 (* external interfaces *)
   225 
   226 val add_axclass = ext_axclass read_axm;
   227 val add_axclass_i = ext_axclass cert_axm;
   228 
   229 
   230 
   231 (** prove class relations and type arities **)
   232 
   233 (* class_axms *)
   234 
   235 fun class_axms thy =
   236   let
   237     val classes = Sign.classes (sign_of thy);
   238     val intros = map (fn c => c ^ "I") classes;
   239   in
   240     get_axioms thy intros @
   241     map (class_triv thy) classes
   242   end;
   243 
   244 
   245 (* axclass_tac *)
   246 
   247 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
   248       try "cI" axioms first and use class_triv as last resort
   249   (2) rewrite goals using user supplied definitions
   250   (3) repeatedly resolve goals with user supplied non-definitions*)
   251 
   252 fun axclass_tac thy thms =
   253   TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
   254   TRY (rewrite_goals_tac (filter is_defn thms)) THEN
   255   TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms)));
   256 
   257 
   258 (* provers *)
   259 
   260 fun prove term_of str_of thy sig_prop thms usr_tac =
   261   let
   262     val sign = sign_of thy;
   263     val goal = cterm_of sign (term_of sig_prop);
   264     val tac = axclass_tac thy thms THEN (if_none usr_tac all_tac);
   265   in
   266     prove_goalw_cterm [] goal (K [tac])
   267   end
   268   handle ERROR => error ("The error(s) above occurred while trying to prove "
   269     ^ quote (str_of sig_prop));
   270 
   271 val prove_classrel =
   272   prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2);
   273 
   274 val prove_arity =
   275   prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c]));
   276 
   277 
   278 (* make goals (for interactive use) *)
   279 
   280 fun mk_goal term_of thy sig_prop =
   281   goalw_cterm [] (cterm_of (sign_of thy) (term_of sig_prop));
   282 
   283 val goal_subclass = mk_goal mk_classrel;
   284 val goal_arity = mk_goal mk_arity;
   285 
   286 
   287 
   288 (** add proved subclass relations and arities **)
   289 
   290 fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
   291   add_classrel_thms
   292   [prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
   293 
   294 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
   295   let
   296     val usr_thms = get_axioms thy axms @ thms;
   297     fun prove c =
   298       prove_arity thy (t, ss, c) usr_thms usr_tac;
   299   in
   300     add_arity_thms (map prove cs) thy
   301   end;
   302 
   303 
   304 end;
   305