# HG changeset patch
# User wenzelm
# Date 777303610 -7200
# Node ID 95225e63ef02ac50272e0f474a545c61aa337923
# Parent  6702a715281d0bd7a7cf63e09b72b4d51ea970c2
added add_defs, add_defs_i;

diff -r 6702a715281d -r 95225e63ef02 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Aug 19 15:39:52 1994 +0200
+++ b/src/Pure/drule.ML	Fri Aug 19 15:40:10 1994 +0200
@@ -12,6 +12,8 @@
   sig
   structure Thm : THM
   local open Thm  in
+  val add_defs: (string * string) list -> theory -> theory
+  val add_defs_i: (string * term) list -> theory -> theory
   val asm_rl: thm
   val assume_ax: theory -> string -> thm
   val COMP: thm * thm -> thm
@@ -90,6 +92,118 @@
 local open Thm
 in
 
+(**** Extend Theories ****)
+
+(** add constant definitions **)
+
+(* 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_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 ****)
 
 (** reading of instantiations **)