# HG changeset patch # User wenzelm # Date 777303592 -7200 # Node ID 6702a715281d0bd7a7cf63e09b72b4d51ea970c2 # Parent 00365d2e0c501091258f4d2a5c74166df1302f68 cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes; diff -r 00365d2e0c50 -r 6702a715281d src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri Aug 19 15:39:19 1994 +0200 +++ b/src/Pure/axclass.ML Fri Aug 19 15:39:52 1994 +0200 @@ -2,18 +2,13 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Higher level user interfaces for axiomatic type classes. - -TODO: - remove add_sigclass (?) - remove goal_... (?) - clean signature +User interfaces for axiomatic type classes. *) signature AX_CLASS = sig structure Tactical: TACTICAL - local open Tactical Tactical.Thm Tactical.Thm.Sign.Syntax.Mixfix in + local open Tactical Tactical.Thm 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 @@ -21,25 +16,10 @@ -> theory -> theory val add_axclass_i: class * class list -> (string * term) list -> theory -> theory - 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 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_inst_subclass: class * class -> string list -> thm list -> tactic option -> theory -> theory val add_inst_arity: string * sort list * class list -> string list -> thm list -> tactic option -> theory -> theory - val add_defns: (string * string) list -> theory -> theory - val add_defns_i: (string * term) list -> theory -> theory - val mk_classrel: class * class -> term - val dest_classrel: term -> class * class - val mk_arity: string * sort list * class -> term - val dest_arity: term -> string * sort list * class - val class_axms: theory -> thm list val axclass_tac: theory -> thm list -> tactic val goal_subclass: theory -> class * class -> thm list val goal_arity: theory -> string * sort list * class -> thm list @@ -59,116 +39,6 @@ open Logic Thm Tactical Tactic Goals; -(** add constant definitions **) (* FIXME -> drule.ML (?) *) - -(* all_axioms_of *) - -(*results may contain duplicates!*) - -fun ancestry_of thy = - thy :: flat (map ancestry_of (parents_of thy)); - -val all_axioms_of = flat o map axioms_of o ancestry_of; - - -(* clash_types, clash_consts *) - -(*check if types have common instance (ignoring sorts)*) - -fun clash_types ty1 ty2 = - let - val ty1' = Type.varifyT ty1; - val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); - in - Type.raw_unify (ty1', ty2') - end; - -fun clash_consts (c1, ty1) (c2, ty2) = - c1 = c2 andalso clash_types ty1 ty2; - - -(* clash_defns *) - -fun clash_defn c_ty (name, tm) = - let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in - if clash_consts c_ty (c, ty') then Some (name, ty') else None - end handle TERM _ => None; - -fun clash_defns c_ty axms = - distinct (mapfilter (clash_defn c_ty) axms); - - -(* dest_defn *) - -fun dest_defn tm = - let - fun err msg = raise_term msg [tm]; - - val (lhs, rhs) = Logic.dest_equals tm - handle TERM _ => err "Not a meta-equality (==)"; - val (head, args) = strip_comb lhs; - val (c, ty) = dest_Const head - handle TERM _ => err "Head of lhs not a constant"; - - fun occs_const (Const c_ty') = clash_consts (c, ty) c_ty' - | occs_const (Abs (_, _, t)) = occs_const t - | occs_const (t $ u) = occs_const t orelse occs_const u - | occs_const _ = false; - in - if not (forall is_Free args) then - err "Arguments of lhs have to be variables" - else if not (null (duplicates args)) then - err "Duplicate variables on lhs" - else if not (term_frees rhs subset args) then - err "Extra variables on rhs" - else if not (term_tfrees rhs subset typ_tfrees ty) then - err "Extra type variables on rhs" - else if occs_const rhs then - err "Constant to be defined clashes with occurrence(s) on rhs" - else (c, ty) - end; - - -(* check_defn *) - -fun err_in_axm name msg = - (writeln msg; error ("The error(s) above occurred in axiom " ^ quote name)); - -fun check_defn sign (axms, (name, tm)) = - let - fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block - [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty])); - - fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; - fun show_defns c = commas o map (show_defn c); - - val (c, ty) = dest_defn tm - handle TERM (msg, _) => err_in_axm name msg; - val defns = clash_defns (c, ty) axms; - in - if not (null defns) then - err_in_axm name ("Definition of " ^ show_const (c, ty) ^ - " clashes with " ^ show_defns c defns) - else (name, tm) :: axms - end; - - -(* add_defns *) - -fun ext_defns prep_axm raw_axms thy = - let - val axms = map (prep_axm (sign_of thy)) raw_axms; - val all_axms = all_axioms_of thy; - in - foldl (check_defn (sign_of thy)) (all_axms, axms); - add_axioms_i axms thy - end; - -val add_defns_i = ext_defns cert_axm; -val add_defns = ext_defns read_axm; - - - (** utilities **) (* type vars *) @@ -199,7 +69,7 @@ -(** abstract syntax operations **) (* FIXME -> logic.ML (?) *) +(** abstract syntax operations **) (* subclass relations as terms *) @@ -244,7 +114,7 @@ -(** add theorems as axioms **) (* FIXME -> drule.ML (?) *) +(** add theorems as axioms **) fun prep_thm_axm thy thm = let @@ -310,7 +180,7 @@ fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy = let val axioms = map (prep_axm (sign_of old_thy)) raw_axioms; - val thy = add_classes [([], class, super_classes)] old_thy; + val thy = add_classes [(class, super_classes)] old_thy; val sign = sign_of thy; @@ -357,19 +227,6 @@ val add_axclass_i = ext_axclass cert_axm; -(* add signature classes *) - -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 add_sigclass = ext_sigclass add_consts; -val add_sigclass_i = ext_sigclass add_consts_i; - - (** prove class relations and type arities **)