--- a/src/HOL/Tools/datatype_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -350,10 +350,10 @@
weak_case_congs cong_att =
(snd o PureThy.add_thmss [(("simps", simps), []),
(("", List.concat case_thms @ size_thms @
- List.concat distinct @ rec_thms), [Simplifier.simp_add_global]),
+ List.concat distinct @ rec_thms), [Attrib.theory Simplifier.simp_add]),
(("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
- (("", List.concat inject), [iff_add_global]),
- (("", map name_notE (List.concat distinct)), [Classical.safe_elim_global]),
+ (("", List.concat inject), [Attrib.theory iff_add]),
+ (("", map name_notE (List.concat distinct)), [Attrib.theory Classical.safe_elim]),
(("", weak_case_congs), [cong_att])]);
@@ -747,7 +747,7 @@
|> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names' (hd descr), [])
|> Theory.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs Simplifier.cong_add_global
+ weak_case_congs (Attrib.theory Simplifier.cong_add)
|> put_datatypes (fold Symtab.update dt_infos dt_info)
|> add_cases_induct dt_infos induct
|> Theory.parent_path
@@ -806,7 +806,7 @@
|> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), [])
|> Theory.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Simplifier.change_global_ss (op addcongs))
+ weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs)))
|> put_datatypes (fold Symtab.update dt_infos dt_info)
|> add_cases_induct dt_infos induct
|> Theory.parent_path
@@ -913,7 +913,7 @@
val thy11 = thy10 |>
Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Simplifier.change_global_ss (op addcongs)) |>
+ weak_case_congs (Attrib.theory (Simplifier.attrib (op addcongs))) |>
put_datatypes (fold Symtab.update dt_infos dt_info) |>
add_cases_induct dt_infos induction' |>
Theory.parent_path |>
--- a/src/HOL/Tools/primrec_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -258,7 +258,7 @@
val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
|> (snd o PureThy.add_thmss [(("simps", simps'),
- [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
+ [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
|> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
|> Theory.parent_path
in
--- a/src/HOL/Tools/recdef_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -11,18 +11,12 @@
val print_recdefs: theory -> unit
val get_recdef: theory -> string
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
- val simp_add_global: theory attribute
- val simp_del_global: theory attribute
- val cong_add_global: theory attribute
- val cong_del_global: theory attribute
- val wf_add_global: theory attribute
- val wf_del_global: theory attribute
- val simp_add_local: Proof.context attribute
- val simp_del_local: Proof.context attribute
- val cong_add_local: Proof.context attribute
- val cong_del_local: Proof.context attribute
- val wf_add_local: Proof.context attribute
- val wf_del_local: Proof.context attribute
+ val simp_add: Context.generic attribute
+ val simp_del: Context.generic attribute
+ val cong_add: Context.generic attribute
+ val cong_del: Context.generic attribute
+ val wf_add: Context.generic attribute
+ val wf_del: Context.generic attribute
val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
Attrib.src option -> theory -> theory
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
@@ -41,7 +35,6 @@
structure RecdefPackage: RECDEF_PACKAGE =
struct
-
val quiet_mode = Tfl.quiet_mode;
val message = Tfl.message;
@@ -152,29 +145,17 @@
(* attributes *)
-local
+fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
+ | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
-fun global_local f g =
- (fn (thy, thm) => (map_global_hints (f (g thm)) thy, thm),
- fn (ctxt, thm) => (map_local_hints (f (g thm)) ctxt, thm));
-
-fun mk_attr (add1, add2) (del1, del2) =
- (Attrib.add_del_args add1 del1, Attrib.add_del_args add2 del2);
-
-in
+fun attrib f = Attrib.declaration (map_hints o f);
-val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
-val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
-val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
-val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
-val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
-val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
-
-val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
-val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
-val wf_attr = mk_attr (wf_add_global, wf_add_local) (wf_del_global, wf_del_local);
-
-end;
+val simp_add = attrib (map_simps o Drule.add_rule);
+val simp_del = attrib (map_simps o Drule.del_rule);
+val cong_add = attrib (map_congs o add_cong);
+val cong_del = attrib (map_congs o del_cong);
+val wf_add = attrib (map_wfs o Drule.add_rule);
+val wf_del = attrib (map_wfs o Drule.del_rule);
(* modifiers *)
@@ -184,15 +165,15 @@
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
- Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
- Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
- Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
- Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
- Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
- Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
- Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
- Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K ((I, Attrib.context simp_add): Method.modifier),
+ Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+ Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+ Args.$$$ recdef_congN -- Args.colon >> K (I, Attrib.context cong_add),
+ Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
+ Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del),
+ Args.$$$ recdef_wfN -- Args.colon >> K (I, Attrib.context wf_add),
+ Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, Attrib.context wf_add),
+ Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, Attrib.context wf_del)] @
Clasimp.clasimp_modifiers;
@@ -243,12 +224,13 @@
congs wfs name R eqs;
val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
val simp_att = if null tcs then
- [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
+ [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE] else [];
val ((simps' :: rules', [induct']), thy) =
thy
|> Theory.add_path bname
- |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+ |> PureThy.add_thmss
+ ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> PureThy.add_thms [(("induct", induct), [])];
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
@@ -314,9 +296,12 @@
val setup =
[GlobalRecdefData.init, LocalRecdefData.init,
Attrib.add_attributes
- [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
- (recdef_congN, cong_attr, "declaration of recdef cong rule"),
- (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
+ [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
+ "declaration of recdef simp rule"),
+ (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
+ "declaration of recdef cong rule"),
+ (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
+ "declaration of recdef wf rule")]];
(* outer syntax *)
--- a/src/HOL/Tools/record_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -1993,8 +1993,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
- (("iffs",iffs), [iff_add_global])]
+ [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
+ (("iffs",iffs), [Attrib.theory iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
|> add_record_equalities extension_id equality'
--- a/src/HOLCF/domain/theorems.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Jan 14 22:25:34 2006 +0100
@@ -368,7 +368,7 @@
("inverts" , inverts ),
("injects" , injects ),
("copy_rews", copy_rews)])))
- |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
+ |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Attrib.theory Simplifier.simp_add])])
|> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
end; (* let *)
--- a/src/HOLCF/fixrec_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/HOLCF/fixrec_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -250,7 +250,7 @@
val (simp_thms, thy'') = PureThy.add_thms simps thy';
val simp_names = map (fn name => name^"_simps") cnames;
- val simp_attribute = rpair [Simplifier.simp_add_global];
+ val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
in
(snd o PureThy.add_thmss simps') thy''
--- a/src/Provers/clasimp.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/clasimp.ML Sat Jan 14 22:25:34 2006 +0100
@@ -56,16 +56,12 @@
val fast_simp_tac: clasimpset -> int -> tactic
val slow_simp_tac: clasimpset -> int -> tactic
val best_simp_tac: clasimpset -> int -> tactic
- val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
- val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
+ val attrib: (clasimpset * thm list -> clasimpset) -> Context.generic attribute
val get_local_clasimpset: Proof.context -> clasimpset
val local_clasimpset_of: Proof.context -> clasimpset
- val iff_add_global: theory attribute
- val iff_add_global': theory attribute
- val iff_del_global: theory attribute
- val iff_add_local: Proof.context attribute
- val iff_add_local': Proof.context attribute
- val iff_del_local: Proof.context attribute
+ val iff_add: Context.generic attribute
+ val iff_add': Context.generic attribute
+ val iff_del: Context.generic attribute
val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val setup: (theory -> theory) list
@@ -138,18 +134,18 @@
val (elim, intro) = if n = 0 then decls1 else decls2;
val zero_rotate = zero_var_indexes o rotate_prems n;
in
- (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
- [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))])
- handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
+ (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]),
+ [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS iffD1)))])
+ handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS notE))])
handle THM _ => intro (cs, [th])),
simp (ss, [th]))
end;
fun delIff delcs delss ((cs, ss), th) =
let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
- (delcs (cs, [zero_rotate (th RS Data.iffD2),
- Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
- handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
+ (delcs (cs, [zero_rotate (th RS iffD2),
+ Tactic.make_elim (zero_rotate (th RS iffD1))])
+ handle THM _ => (delcs (cs, [zero_rotate (th RS notE)])
handle THM _ => delcs (cs, [th])),
delss (ss, [th]))
end;
@@ -157,10 +153,10 @@
fun modifier att (x, ths) =
fst (Thm.applys_attributes [att] (x, rev ths));
-fun addXIs which = modifier (which (ContextRules.intro_query NONE));
-fun addXEs which = modifier (which (ContextRules.elim_query NONE));
-fun addXDs which = modifier (which (ContextRules.dest_query NONE));
-fun delXs which = modifier (which ContextRules.rule_del);
+val addXIs = modifier (ContextRules.intro_query NONE);
+val addXEs = modifier (ContextRules.elim_query NONE);
+val addXDs = modifier (ContextRules.dest_query NONE);
+val delXs = modifier ContextRules.rule_del;
in
@@ -174,23 +170,11 @@
fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
-fun addIffs_global (thy, ths) =
- Library.foldl (addIff
- (addXEs Attrib.theory, addXIs Attrib.theory)
- (addXEs Attrib.theory, addXIs Attrib.theory) #1)
- ((thy, ()), ths) |> #1;
+fun addIffs_generic (x, ths) =
+ Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
-fun addIffs_local (ctxt, ths) =
- Library.foldl (addIff
- (addXEs Attrib.context, addXIs Attrib.context)
- (addXEs Attrib.context, addXIs Attrib.context) #1)
- ((ctxt, ()), ths) |> #1;
-
-fun delIffs_global (thy, ths) =
- Library.foldl (delIff (delXs Attrib.theory) #1) ((thy, ()), ths) |> #1;
-
-fun delIffs_local (ctxt, ths) =
- Library.foldl (delIff (delXs Attrib.context) #1) ((ctxt, ()), ths) |> #1;
+fun delIffs_generic (x, ths) =
+ Library.foldl (delIff delXs #1) ((x, ()), ths) |> #1;
end;
@@ -272,20 +256,6 @@
(* access clasimpset *)
-fun change_global_css f (thy, th) =
- (change_clasimpset_of thy (fn css => f (css, [th])); (thy, th));
-
-fun change_local_css f (ctxt, th) =
- let
- val cs = Classical.get_local_claset ctxt;
- val ss = Simplifier.get_local_simpset ctxt;
- val (cs', ss') = f ((cs, ss), [th]);
- val ctxt' =
- ctxt
- |> Classical.put_local_claset cs'
- |> Simplifier.put_local_simpset ss';
- in (ctxt', th) end;
-
fun get_local_clasimpset ctxt =
(Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
@@ -295,23 +265,29 @@
(* attributes *)
-fun change_rules f (x, th) = (f (x, [th]), th);
-
-val iff_add_global = change_global_css (op addIffs);
-val iff_add_global' = change_rules addIffs_global;
-val iff_del_global = change_global_css (op delIffs) o change_rules delIffs_global;
-val iff_add_local = change_local_css (op addIffs);
-val iff_add_local' = change_rules addIffs_local;
-val iff_del_local = change_local_css (op delIffs) o change_rules delIffs_local;
+fun attrib f = Attrib.declaration (fn th =>
+ fn Context.Theory thy => (change_clasimpset_of thy (fn css => f (css, [th])); Context.Theory thy)
+ | Context.Proof ctxt =>
+ let
+ val cs = Classical.get_local_claset ctxt;
+ val ss = Simplifier.get_local_simpset ctxt;
+ val (cs', ss') = f ((cs, ss), [th]);
+ val ctxt' =
+ ctxt
+ |> Classical.put_local_claset cs'
+ |> Simplifier.put_local_simpset ss';
+ in Context.Proof ctxt' end);
-fun iff_att add add' del = Attrib.syntax (Scan.lift
- (Args.del >> K del ||
- Scan.option Args.add -- Args.query >> K add' ||
- Scan.option Args.add >> K add));
+fun attrib' f (x, th) = (f (x, [th]), th);
-val iff_attr =
- (iff_att iff_add_global iff_add_global' iff_del_global,
- iff_att iff_add_local iff_add_local' iff_del_local);
+val iff_add = attrib (op addIffs);
+val iff_add' = attrib' addIffs_generic;
+val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
+
+val iff_att = Attrib.syntax (Scan.lift
+ (Args.del >> K iff_del ||
+ Scan.option Args.add -- Args.query >> K iff_add' ||
+ Scan.option Args.add >> K iff_add));
(* method modifiers *)
@@ -319,9 +295,10 @@
val iffN = "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add_local): Method.modifier),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add_local'),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del_local)];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon
+ >> K ((I, Attrib.context iff_add): Method.modifier),
+ Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, Attrib.context iff_add'),
+ Args.$$$ iffN -- Args.del -- Args.colon >> K (I, Attrib.context iff_del)];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
@@ -351,7 +328,7 @@
val setup =
[Attrib.add_attributes
- [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
+ [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")],
Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
--- a/src/Provers/classical.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/classical.ML Sat Jan 14 22:25:34 2006 +0100
@@ -143,20 +143,13 @@
val print_local_claset: Proof.context -> unit
val get_local_claset: Proof.context -> claset
val put_local_claset: claset -> Proof.context -> Proof.context
- val safe_dest_global: theory attribute
- val safe_elim_global: theory attribute
- val safe_intro_global: theory attribute
- val haz_dest_global: theory attribute
- val haz_elim_global: theory attribute
- val haz_intro_global: theory attribute
- val rule_del_global: theory attribute
- val safe_dest_local: Proof.context attribute
- val safe_elim_local: Proof.context attribute
- val safe_intro_local: Proof.context attribute
- val haz_dest_local: Proof.context attribute
- val haz_elim_local: Proof.context attribute
- val haz_intro_local: Proof.context attribute
- val rule_del_local: Proof.context attribute
+ val safe_dest: Context.generic attribute
+ val safe_elim: Context.generic attribute
+ val safe_intro: Context.generic attribute
+ val haz_dest: Context.generic attribute
+ val haz_elim: Context.generic attribute
+ val haz_intro: Context.generic attribute
+ val rule_del: Context.generic attribute
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
@@ -959,24 +952,17 @@
(* attributes *)
-fun change_global_cs f (thy, th) = (change_claset_of thy (fn cs => f (cs, [th])); (thy, th));
-fun change_local_cs f (ctxt, th) = (LocalClaset.map (fn cs => f (cs, [th])) ctxt, th);
+fun attrib f = Attrib.declaration (fn th =>
+ fn Context.Theory thy => (change_claset_of thy (fn cs => f (cs, [th])); Context.Theory thy)
+ | Context.Proof ctxt => Context.Proof (LocalClaset.map (fn cs => f (cs, [th])) ctxt));
-val safe_dest_global = change_global_cs (op addSDs);
-val safe_elim_global = change_global_cs (op addSEs);
-val safe_intro_global = change_global_cs (op addSIs);
-val haz_dest_global = change_global_cs (op addDs);
-val haz_elim_global = change_global_cs (op addEs);
-val haz_intro_global = change_global_cs (op addIs);
-val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del;
-
-val safe_dest_local = change_local_cs (op addSDs);
-val safe_elim_local = change_local_cs (op addSEs);
-val safe_intro_local = change_local_cs (op addSIs);
-val haz_dest_local = change_local_cs (op addDs);
-val haz_elim_local = change_local_cs (op addEs);
-val haz_intro_local = change_local_cs (op addIs);
-val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del;
+val safe_dest = attrib (op addSDs);
+val safe_elim = attrib (op addSEs);
+val safe_intro = attrib (op addSIs);
+val haz_dest = attrib (op addDs);
+val haz_elim = attrib (op addEs);
+val haz_intro = attrib (op addIs);
+val rule_del = attrib (op delrules) o ContextRules.rule_del;
(* tactics referring to the implicit claset *)
@@ -1018,19 +1004,13 @@
val setup_attrs = Attrib.add_attributes
[("swapped", (swapped, swapped), "classical swap of introduction rule"),
- (destN,
- (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global,
- add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local),
- "declaration of destruction rule"),
- (elimN,
- (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global,
- add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local),
- "declaration of elimination rule"),
- (introN,
- (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global,
- add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local),
- "declaration of introduction rule"),
- (ruleN, (del_rule rule_del_global, del_rule rule_del_local),
+ (destN, Attrib.common (add_rule ContextRules.dest_query haz_dest safe_dest),
+ "declaration of Classical destruction rule"),
+ (elimN, Attrib.common (add_rule ContextRules.elim_query haz_elim safe_elim),
+ "declaration of Classical elimination rule"),
+ (introN, Attrib.common (add_rule ContextRules.intro_query haz_intro safe_intro),
+ "declaration of Classical introduction rule"),
+ (ruleN, Attrib.common (del_rule rule_del),
"remove declaration of intro/elim/dest rule")];
@@ -1078,13 +1058,13 @@
(* automatic methods *)
val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest_local): Method.modifier),
- Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
- Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
- Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
- Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
- Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
- Args.del -- Args.colon >> K (I, rule_del_local)];
+ [Args.$$$ destN -- Args.bang_colon >> K ((I, Attrib.context safe_dest): Method.modifier),
+ Args.$$$ destN -- Args.colon >> K (I, Attrib.context haz_dest),
+ Args.$$$ elimN -- Args.bang_colon >> K (I, Attrib.context safe_elim),
+ Args.$$$ elimN -- Args.colon >> K (I, Attrib.context haz_elim),
+ Args.$$$ introN -- Args.bang_colon >> K (I, Attrib.context safe_intro),
+ Args.$$$ introN -- Args.colon >> K (I, Attrib.context haz_intro),
+ Args.del -- Args.colon >> K (I, Attrib.context rule_del)];
fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
--- a/src/Provers/splitter.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Provers/splitter.ML Sat Jan 14 22:25:34 2006 +0100
@@ -32,10 +32,8 @@
val delsplits : simpset * thm list -> simpset
val Addsplits : thm list -> unit
val Delsplits : thm list -> unit
- val split_add_global: theory attribute
- val split_del_global: theory attribute
- val split_add_local: Proof.context attribute
- val split_del_local: Proof.context attribute
+ val split_add: Context.generic attribute
+ val split_del: Context.generic attribute
val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
val setup: (theory -> theory) list
end;
@@ -405,6 +403,7 @@
gen_split_tac splits
end;
+
(** declare split rules **)
(* addsplits / delsplits *)
@@ -437,33 +436,28 @@
val splitN = "split";
-val split_add_global = Simplifier.change_global_ss (op addsplits);
-val split_del_global = Simplifier.change_global_ss (op delsplits);
-val split_add_local = Simplifier.change_local_ss (op addsplits);
-val split_del_local = Simplifier.change_local_ss (op delsplits);
-
-val split_attr =
- (Attrib.add_del_args split_add_global split_del_global,
- Attrib.add_del_args split_add_local split_del_local);
+val split_add = Simplifier.attrib (op addsplits);
+val split_del = Simplifier.attrib (op delsplits);
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
- Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
- Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
+ [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
+ Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
+ Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
-val split_args = #2 oo Method.syntax Attrib.local_thms;
-
-fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
+fun split_meth src =
+ Method.syntax Attrib.local_thms src
+ #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
-
-(** theory setup **)
+(* theory setup *)
val setup =
- [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
- Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
+ [Attrib.add_attributes
+ [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
+ "declaration of case split rule")],
+ Method.add_methods [(splitN, split_meth, "apply case split rule")]];
end;
--- a/src/Pure/simplifier.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/Pure/simplifier.ML Sat Jan 14 22:25:34 2006 +0100
@@ -64,16 +64,11 @@
val print_local_simpset: Proof.context -> unit
val get_local_simpset: Proof.context -> simpset
val put_local_simpset: simpset -> Proof.context -> Proof.context
- val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
- val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
- val simp_add_global: theory attribute
- val simp_del_global: theory attribute
- val simp_add_local: Proof.context attribute
- val simp_del_local: Proof.context attribute
- val cong_add_global: theory attribute
- val cong_del_global: theory attribute
- val cong_add_local: Proof.context attribute
- val cong_del_local: Proof.context attribute
+ val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
+ val simp_add: Context.generic attribute
+ val simp_del: Context.generic attribute
+ val cong_add: Context.generic attribute
+ val cong_del: Context.generic attribute
val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
@@ -143,18 +138,14 @@
(* attributes *)
-fun change_global_ss f (thy, th) = (change_simpset_of thy (fn ss => f (ss, [th])); (thy, th));
-fun change_local_ss f (ctxt, th) = (LocalSimpset.map (fn ss => f (ss, [th])) ctxt, th);
+fun attrib f = Attrib.declaration (fn th =>
+ fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
+ | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
-val simp_add_global = change_global_ss (op addsimps);
-val simp_del_global = change_global_ss (op delsimps);
-val simp_add_local = change_local_ss (op addsimps);
-val simp_del_local = change_local_ss (op delsimps);
-
-val cong_add_global = change_global_ss (op addcongs);
-val cong_del_global = change_global_ss (op delcongs);
-val cong_add_local = change_local_ss (op addcongs);
-val cong_del_local = change_local_ss (op delcongs);
+val simp_add = attrib (op addsimps);
+val simp_del = attrib (op delsimps);
+val cong_add = attrib (op addcongs);
+val cong_del = attrib (op delcongs);
@@ -243,14 +234,6 @@
val no_asm_simpN = "no_asm_simp";
val asm_lrN = "asm_lr";
-val simp_attr =
- (Attrib.add_del_args simp_add_global simp_del_global,
- Attrib.add_del_args simp_add_local simp_del_local);
-
-val cong_attr =
- (Attrib.add_del_args cong_add_global cong_del_global,
- Attrib.add_del_args cong_add_local cong_del_local);
-
(* conversions *)
@@ -262,15 +245,14 @@
Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
Scan.succeed asm_full_simplify) |> Scan.lift) x;
-fun simplified_att get args =
- Attrib.syntax (conv_mode -- args >> (fn (f, ths) => Attrib.rule (fn x =>
- f ((if null ths then I else MetaSimplifier.clear_ss) (get x) addsimps ths))));
+fun get_ss (Context.Theory thy) = simpset_of thy
+ | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
in
-val simplified_attr =
- (simplified_att simpset_of Attrib.global_thmss,
- simplified_att local_simpset_of Attrib.local_thmss);
+val simplified =
+ Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
+ f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
end;
@@ -279,9 +261,11 @@
val _ = Context.add_setup
[Attrib.add_attributes
- [(simpN, simp_attr, "declaration of simplification rule"),
- (congN, cong_attr, "declaration of Simplifier congruence rule"),
- ("simplified", simplified_attr, "simplified rule")]];
+ [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
+ "declaration of Simplifier rule"),
+ (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
+ "declaration of Simplifier congruence rule"),
+ ("simplified", Attrib.common simplified, "simplified rule")]];
@@ -302,22 +286,23 @@
>> (curry (Library.foldl op o) I o rev)) x;
val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local): Method.modifier),
- Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
- Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
+ [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
+ Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
+ Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
- Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
- Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
+ [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
+ Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+ Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
- >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
+ >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
@ cong_modifiers;
val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, simp_add_local),
- Args.del -- Args.colon >> K (I, simp_del_local),
- Args.$$$ onlyN -- Args.colon >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add_local)]
+ [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
+ Args.del -- Args.colon >> K (I, Attrib.context simp_del),
+ Args.$$$ onlyN -- Args.colon
+ >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
@ cong_modifiers;
fun simp_args more_mods =
--- a/src/ZF/Tools/datatype_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -367,8 +367,8 @@
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
|> PureThy.add_thmss
- [(("simps", simps), [Simplifier.simp_add_global]),
- (("", intrs), [Classical.safe_intro_global]),
+ [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
+ (("", intrs), [Attrib.theory Classical.safe_intro]),
(("con_defs", con_defs), []),
(("case_eqns", case_eqns), []),
(("recursor_eqns", recursor_eqns), []),
--- a/src/ZF/Tools/induct_tacs.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sat Jan 14 22:25:34 2006 +0100
@@ -165,7 +165,7 @@
in
thy
|> Theory.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
+ |> PureThy.add_thmss [(("simps", simps), [Attrib.theory Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Theory.parent_path
--- a/src/ZF/Tools/primrec_package.ML Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML Sat Jan 14 22:25:34 2006 +0100
@@ -191,7 +191,7 @@
|> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
- |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]
+ |> PureThy.add_thmss [(("simps", eqn_thms'), [Attrib.theory Simplifier.simp_add])]
||> Theory.parent_path;
in (thy3, eqn_thms') end;