# HG changeset patch
# User nipkow
# Date 966529872 -7200
# Node ID 8c6cf4f01644481d192b5cbe832d80ef89b750f6
# Parent  51107e8149a00f0ce8c17faac5a5bc8f6504c616
installed recdef congs data

diff -r 51107e8149a0 -r 8c6cf4f01644 TFL/post.sml
--- a/TFL/post.sml	Thu Aug 17 18:30:48 2000 +0200
+++ b/TFL/post.sml	Thu Aug 17 18:31:12 2000 +0200
@@ -191,7 +191,7 @@
 			  " would clash with the theory of the same name!")	(* FIXME !? *)
 	val def = freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
 	val {theory,rules,rows,TCs,full_pats_TCs} = 
-		 Prim.post_definition (Prim.congs tflCongs)
+		 Prim.post_definition (Prim.congs thy tflCongs)
 		    (thy, (def,pats))
 	val {lhs=f,rhs} = S.dest_eq(concl def)
 	val (_,[R,_]) = S.strip_comb rhs
diff -r 51107e8149a0 -r 8c6cf4f01644 TFL/tfl.sig
--- a/TFL/tfl.sig	Thu Aug 17 18:30:48 2000 +0200
+++ b/TFL/tfl.sig	Thu Aug 17 18:31:12 2000 +0200
@@ -13,7 +13,11 @@
 
    val default_simps : thm list      (*simprules used for deriving rules...*)
 
-   val congs : thm list -> thm list  (*fn to make congruent rules*)
+   val Add_recdef_congs: thm list -> unit
+   val Del_recdef_congs: thm list -> unit
+   val init: theory -> theory
+   val print_recdef_congs: theory -> unit
+   val congs : theory -> thm list -> thm list  (*fn to make congruence rules*)
 
    type pattern
 
diff -r 51107e8149a0 -r 8c6cf4f01644 TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Aug 17 18:30:48 2000 +0200
+++ b/TFL/tfl.sml	Thu Aug 17 18:31:12 2000 +0200
@@ -38,15 +38,72 @@
 
 
 (*---------------------------------------------------------------------------
-          handling of user-supplied congruence rules: lcp*)
+          handling of user-supplied congruence rules: tnn *)
 
 (*Convert conclusion from = to ==*)
 val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
 
-(*default congruence rules include those for LET and IF*)
-val default_congs = eq_reflect_list [Thms.LET_CONG, if_cong];
+val cong_hd = fst o dest_Const o head_of o fst o Logic.dest_equals o concl_of;
+
+fun add_cong(congs,thm) =
+  let val c = cong_hd thm
+  in case assoc(congs,c) of None => (c,thm)::congs
+     | _ => (warning ("Overwriting congruence rule for " ^ quote c);
+             overwrite (congs, (c,thm)))
+  end
+
+fun del_cong(congs,thm) =
+  let val c = cong_hd thm
+      val (del, rest) = partition (fn (n, _) => n = c) congs
+  in if null del
+     then (warning ("No congruence rule for " ^ quote c ^ " present"); congs)
+     else rest
+  end;
+
+fun add_congs(congs,thms) = foldl add_cong (congs, eq_reflect_list thms);
+fun del_congs(congs,thms) = foldl del_cong (congs, eq_reflect_list thms);
+
+(** recdef data **)
+
+(* theory data kind 'Provers/simpset' *)
+
+structure RecdefCongsArgs =
+struct
+  val name = "HOL/recdef-congs";
+  type T = (string * thm) list ref;
 
-fun congs ths = default_congs @ eq_reflect_list ths;
+  val empty = ref(add_congs([], [Thms.LET_CONG, if_cong]));
+  fun copy (ref congs) = (ref congs): T;            (*create new reference!*)
+  val prep_ext = copy;
+  fun merge (ref congs1, ref congs2) = ref (merge_alists congs1 congs2);
+  fun print _ (ref congs) = print_thms(map snd congs);
+end;
+
+structure RecdefCongs = TheoryDataFun(RecdefCongsArgs);
+val print_recdef_congs = RecdefCongs.print;
+val recdef_congs_ref_of_sg = RecdefCongs.get_sg;
+val recdef_congs_ref_of = RecdefCongs.get;
+val init = RecdefCongs.init;
+
+
+(* access global recdef_congs *)
+val recdef_congs_of_sg = ! o recdef_congs_ref_of_sg;
+val recdef_congs_of = recdef_congs_of_sg o Theory.sign_of;
+
+(* change global recdef_congs *)
+
+fun change_recdef_congs_of f x thy =
+  let val r = recdef_congs_ref_of thy
+  in r := f (! r, x); thy end;
+
+fun change_recdef_congs f x =
+ (change_recdef_congs_of f x (Context.the_context ()); ());
+
+val Add_recdef_congs = change_recdef_congs add_congs;
+val Del_recdef_congs = change_recdef_congs del_congs;
+
+
+fun congs thy ths = map snd (recdef_congs_of thy) @ eq_reflect_list ths;
 
 val default_simps =
     [less_Suc_eq RS iffD2, lex_prod_def, measure_def, inv_image_def];
@@ -512,7 +569,7 @@
 
 fun lazyR_def thy fid tflCongs eqns =
  let val {proto_def,WFR,pats,extracta,SV} =
-           wfrec_eqns thy fid (congs tflCongs) eqns
+           wfrec_eqns thy fid (congs thy tflCongs) eqns
      val R1 = S.rand WFR
      val f = #lhs(S.dest_eq proto_def)
      val (extractants,TCl) = ListPair.unzip extracta
diff -r 51107e8149a0 -r 8c6cf4f01644 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Aug 17 18:30:48 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Thu Aug 17 18:31:12 2000 +0200
@@ -137,7 +137,7 @@
 
 (* setup theory *)
 
-val setup = [RecdefData.init];
+val setup = [Prim.init,RecdefData.init];
 
 
 (* outer syntax *)