# HG changeset patch # User wenzelm # Date 771761153 -7200 # Node ID a42892e72854c962e8f7d73c0fbd799a6096d870 # Parent 8f194014a9c8a1c0a134f97cba28298e25844512 (beta release) diff -r 8f194014a9c8 -r a42892e72854 src/Pure/axclass.ML --- 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;