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