--- 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 **)