--- a/src/Pure/drule.ML Wed Oct 01 17:41:20 1997 +0200
+++ b/src/Pure/drule.ML Wed Oct 01 17:42:32 1997 +0200
@@ -3,15 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Derived rules and other operations on theorems and theories
+Derived rules and other operations on theorems.
*)
infix 0 RS RSN RL RLN MRS MRL COMP;
signature DRULE =
- sig
- val add_defs : (string * string) list -> theory -> theory
- val add_defs_i : (string * term) list -> theory -> theory
+sig
val asm_rl : thm
val assume_ax : theory -> string -> thm
val COMP : thm * thm -> thm
@@ -68,134 +66,12 @@
val triv_forall_equality: thm
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
val zero_var_indexes : thm -> thm
- end;
+end;
structure Drule : DRULE =
struct
-(**** Extend Theories ****)
-
-(** add constant definitions **)
-
-(* all_axioms_of *)
-
-(*results may contain duplicates!*)
-
-fun ancestry_of thy =
- thy :: List.concat (map ancestry_of (parents_of thy));
-
-val all_axioms_of =
- List.concat o map (Symtab.dest o #new_axioms o rep_theory) 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 (Logic.strip_imp_concl 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') = (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;
-
- val show_frees = commas_quote o map (fst o dest_Free);
- val show_tfrees = commas_quote o map fst;
-
- val lhs_dups = duplicates args;
- val rhs_extras = gen_rems (op =) (term_frees rhs, args);
- val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
- in
- if not (forall is_Free args) then
- err "Arguments (on lhs) must be variables"
- else if not (null lhs_dups) then
- err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
- else if not (null rhs_extras) then
- err ("Extra variables on rhs: " ^ show_frees rhs_extras)
- else if not (null rhs_extrasT) then
- err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
- else if occs_const rhs then
- err ("Constant to be defined occurs on rhs")
- else (c, ty)
- end;
-
-
-(* check_defn *)
-
-fun err_in_defn name msg =
- (writeln msg; error ("The error(s) above occurred in definition " ^ 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 = cat_lines o map (show_defn c);
-
- val (c, ty) = dest_defn tm
- handle TERM (msg, _) => err_in_defn name msg;
- val defns = clash_defns (c, ty) axms;
- in
- if not (null defns) then
- err_in_defn name ("Definition of " ^ show_const (c, ty) ^
- "\nclashes with " ^ show_defns c defns)
- else (name, tm) :: axms
- end;
-
-
-(* add_defs *)
-
-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_defs_i = ext_defns cert_axm;
-val add_defs = ext_defns read_axm;
-
-
-
-(**** More derived rules and operations on theorems ****)
-
(** some cterm->cterm operations: much faster than calling cterm_of! **)
(** SAME NAMES as in structure Logic: use compound identifiers! **)