src/HOL/Tools/recdef_package.ML
changeset 18688 abf0f018b5ec
parent 18418 bf448d999b7e
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -11,18 +11,12 @@
     1.4    val print_recdefs: theory -> unit
     1.5    val get_recdef: theory -> string
     1.6      -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     1.7 -  val simp_add_global: theory attribute
     1.8 -  val simp_del_global: theory attribute
     1.9 -  val cong_add_global: theory attribute
    1.10 -  val cong_del_global: theory attribute
    1.11 -  val wf_add_global: theory attribute
    1.12 -  val wf_del_global: theory attribute
    1.13 -  val simp_add_local: Proof.context attribute
    1.14 -  val simp_del_local: Proof.context attribute
    1.15 -  val cong_add_local: Proof.context attribute
    1.16 -  val cong_del_local: Proof.context attribute
    1.17 -  val wf_add_local: Proof.context attribute
    1.18 -  val wf_del_local: Proof.context attribute
    1.19 +  val simp_add: Context.generic attribute
    1.20 +  val simp_del: Context.generic attribute
    1.21 +  val cong_add: Context.generic attribute
    1.22 +  val cong_del: Context.generic attribute
    1.23 +  val wf_add: Context.generic attribute
    1.24 +  val wf_del: Context.generic attribute
    1.25    val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
    1.26      Attrib.src option -> theory -> theory
    1.27        * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.28 @@ -41,7 +35,6 @@
    1.29  structure RecdefPackage: RECDEF_PACKAGE =
    1.30  struct
    1.31  
    1.32 -
    1.33  val quiet_mode = Tfl.quiet_mode;
    1.34  val message = Tfl.message;
    1.35  
    1.36 @@ -152,29 +145,17 @@
    1.37  
    1.38  (* attributes *)
    1.39  
    1.40 -local
    1.41 +fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
    1.42 +  | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
    1.43  
    1.44 -fun global_local f g =
    1.45 - (fn (thy, thm) => (map_global_hints (f (g thm)) thy, thm),
    1.46 -  fn (ctxt, thm) => (map_local_hints (f (g thm)) ctxt, thm));
    1.47 -
    1.48 -fun mk_attr (add1, add2) (del1, del2) =
    1.49 - (Attrib.add_del_args add1 del1, Attrib.add_del_args add2 del2);
    1.50 -
    1.51 -in
    1.52 +fun attrib f = Attrib.declaration (map_hints o f);
    1.53  
    1.54 -val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
    1.55 -val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
    1.56 -val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
    1.57 -val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
    1.58 -val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
    1.59 -val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
    1.60 -
    1.61 -val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
    1.62 -val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
    1.63 -val wf_attr = mk_attr (wf_add_global, wf_add_local) (wf_del_global, wf_del_local);
    1.64 -
    1.65 -end;
    1.66 +val simp_add = attrib (map_simps o Drule.add_rule);
    1.67 +val simp_del = attrib (map_simps o Drule.del_rule);
    1.68 +val cong_add = attrib (map_congs o add_cong);
    1.69 +val cong_del = attrib (map_congs o del_cong);
    1.70 +val wf_add = attrib (map_wfs o Drule.add_rule);
    1.71 +val wf_del = attrib (map_wfs o Drule.del_rule);
    1.72  
    1.73  
    1.74  (* modifiers *)
    1.75 @@ -184,15 +165,15 @@
    1.76  val recdef_wfN = "recdef_wf";
    1.77  
    1.78  val recdef_modifiers =
    1.79 - [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
    1.80 -  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
    1.81 -  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
    1.82 -  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
    1.83 -  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
    1.84 -  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
    1.85 -  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
    1.86 -  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
    1.87 -  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
    1.88 + [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
    1.89 +  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
    1.90 +  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
    1.91 +  Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
    1.92 +  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
    1.93 +  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
    1.94 +  Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
    1.95 +  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
    1.96 +  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
    1.97    Clasimp.clasimp_modifiers;
    1.98  
    1.99  
   1.100 @@ -243,12 +224,13 @@
   1.101                 congs wfs name R eqs;
   1.102      val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
   1.103      val simp_att = if null tcs then
   1.104 -      [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
   1.105 +      [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
   1.106  
   1.107      val ((simps' :: rules', [induct']), thy) =
   1.108        thy
   1.109        |> Theory.add_path bname
   1.110 -      |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   1.111 +      |> PureThy.add_thmss
   1.112 +        ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   1.113        ||>> PureThy.add_thms [(("induct", induct), [])];
   1.114      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   1.115      val thy =
   1.116 @@ -314,9 +296,12 @@
   1.117  val setup =
   1.118   [GlobalRecdefData.init, LocalRecdefData.init,
   1.119    Attrib.add_attributes
   1.120 -   [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
   1.121 -    (recdef_congN, cong_attr, "declaration of recdef cong rule"),
   1.122 -    (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
   1.123 +   [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   1.124 +      "declaration of recdef simp rule"),
   1.125 +    (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   1.126 +      "declaration of recdef cong rule"),
   1.127 +    (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
   1.128 +      "declaration of recdef wf rule")]];
   1.129  
   1.130  
   1.131  (* outer syntax *)