prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
--- a/src/CCL/Wfd.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/CCL/Wfd.thy Sat Aug 16 11:35:33 2014 +0200
@@ -483,15 +483,14 @@
subsection {* Evaluation *}
+named_theorems eval "evaluation rules"
+
ML {*
-structure Eval_Rules =
- Named_Thms(val name = @{binding eval} val description = "evaluation rules");
-
fun eval_tac ths =
- Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
- DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
+ Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} =>
+ let val eval_rules = Named_Theorems.get ctxt @{named_theorems eval}
+ in DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ rev eval_rules) 1) end)
*}
-setup Eval_Rules.setup
method_setup eval = {*
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
--- a/src/Cube/Cube.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/Cube/Cube.thy Sat Aug 16 11:35:33 2014 +0200
@@ -10,14 +10,7 @@
setup Pure_Thy.old_appl_syntax_setup
-ML {*
- structure Rules = Named_Thms
- (
- val name = @{binding rules}
- val description = "Cube inference rules"
- )
-*}
-setup Rules.setup
+named_theorems rules "Cube inference rules"
typedecl "term"
typedecl "context"
--- a/src/HOL/HOLCF/Cfun.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Sat Aug 16 11:35:33 2014 +0200
@@ -147,7 +147,7 @@
val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
val tr = instantiate' [SOME T, SOME U] [SOME f]
(mk_meta_eq @{thm Abs_cfun_inverse2});
- val rules = Cont2ContData.get ctxt;
+ val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
in SOME (perhaps (SINGLE (tac 1)) tr) end
*}
--- a/src/HOL/HOLCF/Cont.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Cont.thy Sat Aug 16 11:35:33 2014 +0200
@@ -120,15 +120,8 @@
subsection {* Collection of continuity rules *}
-ML {*
-structure Cont2ContData = Named_Thms
-(
- val name = @{binding cont2cont}
- val description = "continuity intro rule"
-)
-*}
+named_theorems cont2cont "continuity intro rule"
-setup Cont2ContData.setup
subsection {* Continuity of basic functions *}
--- a/src/HOL/HOLCF/Domain.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain.thy Sat Aug 16 11:35:33 2014 +0200
@@ -316,12 +316,13 @@
subsection {* Setting up the domain package *}
+named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
+named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
+
ML_file "Tools/Domain/domain_isomorphism.ML"
ML_file "Tools/Domain/domain_axioms.ML"
ML_file "Tools/Domain/domain.ML"
-setup Domain_Isomorphism.setup
-
lemmas [domain_defl_simps] =
DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of
--- a/src/HOL/HOLCF/Domain_Aux.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy Sat Aug 16 11:35:33 2014 +0200
@@ -344,6 +344,9 @@
subsection {* ML setup *}
+named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
+named_theorems domain_map_ID "theorems like foo_map$ID = ID"
+
ML_file "Tools/Domain/domain_take_proofs.ML"
ML_file "Tools/cont_consts.ML"
ML_file "Tools/cont_proc.ML"
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Aug 16 11:35:33 2014 +0200
@@ -28,8 +28,6 @@
val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
-
- val setup : theory -> theory
end
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
@@ -41,24 +39,6 @@
fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
-(******************************************************************************)
-(******************************** theory data *********************************)
-(******************************************************************************)
-
-structure RepData = Named_Thms
-(
- val name = @{binding domain_defl_simps}
- val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
-)
-
-structure IsodeflData = Named_Thms
-(
- val name = @{binding domain_isodefl}
- val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
-)
-
-val setup = RepData.setup #> IsodeflData.setup
-
(******************************************************************************)
(************************** building types and terms **************************)
@@ -170,7 +150,7 @@
val cont_thm =
let
val prop = mk_trp (mk_cont functional)
- val rules = Cont2ContData.get (Proof_Context.init_global thy)
+ val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
val tac = REPEAT_ALL_NEW (match_tac rules) 1
in
Goal.prove_global thy [] [] prop (K tac)
@@ -207,7 +187,8 @@
(tab2 : (typ * term) list)
(T : typ) : term =
let
- val defl_simps = RepData.get (Proof_Context.init_global thy)
+ val defl_simps =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
fun proc1 t =
@@ -522,7 +503,8 @@
val ((_, _, _, {DEFL, ...}), thy) =
Domaindef.add_domaindef spec defl NONE thy
(* declare domain_defl_simps rules *)
- val thy = Context.theory_map (RepData.add_thm DEFL) thy
+ val thy =
+ Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy
in
(DEFL, thy)
end
@@ -532,7 +514,8 @@
fun mk_DEFL_eq_thm (lhsT, rhsT) =
let
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
- val DEFL_simps = RepData.get (Proof_Context.init_global thy)
+ val DEFL_simps =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
fun tac ctxt =
rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
THEN TRY (resolve_tac defl_unfold_thms 1)
@@ -637,7 +620,7 @@
val isodefl_rules =
@{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
@ isodefl_abs_rep_thms
- @ IsodeflData.get (Proof_Context.init_global thy)
+ @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
@@ -661,7 +644,9 @@
val (isodefl_thms, thy) = thy |>
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts isodefl_binds isodefl_thm)
- val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy
+ val thy =
+ fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl})
+ isodefl_thms thy
(* prove map_ID theorems *)
fun prove_map_ID_thm
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Aug 16 11:35:33 2014 +0200
@@ -123,31 +123,20 @@
fun merge data = Symtab.merge (K true) data
)
-structure DeflMapData = Named_Thms
-(
- val name = @{binding domain_deflation}
- val description = "theorems like deflation a ==> deflation (foo_map$a)"
-)
-
-structure Map_Id_Data = Named_Thms
-(
- val name = @{binding domain_map_ID}
- val description = "theorems like foo_map$ID = ID"
-)
-
fun add_rec_type (tname, bs) =
Rec_Data.map (Symtab.insert (K true) (tname, bs))
fun add_deflation_thm thm =
- Context.theory_map (DeflMapData.add_thm thm)
+ Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm)
val get_rec_tab = Rec_Data.get
-fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy)
+fun get_deflation_thms thy =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
-val map_ID_add = Map_Id_Data.add
-val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
+val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
+fun get_map_ID_thms thy =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
-val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
(******************************************************************************)
(************************** building types and terms **************************)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Sat Aug 16 11:35:33 2014 +0200
@@ -130,7 +130,7 @@
"or simp rules are configured for all non-HOLCF constants.\n" ^
"The error occurred for the goal statement:\n" ^
Syntax.string_of_term lthy prop)
- val rules = Cont2ContData.get lthy
+ val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
val slow_tac = SOLVED' (simp_tac lthy)
val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
--- a/src/ZF/UNITY/Constrains.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/ZF/UNITY/Constrains.thy Sat Aug 16 11:35:33 2014 +0200
@@ -453,6 +453,9 @@
used by Always_Int_I) *)
lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
+(*To allow expansion of the program's definition when appropriate*)
+named_theorems program "program definitions"
+
ML
{*
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
@@ -461,13 +464,6 @@
(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
-(*To allow expansion of the program's definition when appropriate*)
-structure Program_Defs = Named_Thms
-(
- val name = @{binding program}
- val description = "program definitions"
-);
-
(*proves "co" properties when the program is specified*)
fun constrains_tac ctxt =
@@ -481,7 +477,7 @@
(* Three subgoals *)
rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
REPEAT (force_tac ctxt 2),
- full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
+ full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1,
ALLGOALS (clarify_tac ctxt),
REPEAT (FIRSTGOAL (etac @{thm disjE})),
ALLGOALS (clarify_tac ctxt),
@@ -495,8 +491,6 @@
rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
*}
-setup Program_Defs.setup
-
method_setup safety = {*
Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
"for proving safety properties"
--- a/src/ZF/UNITY/SubstAx.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Sat Aug 16 11:35:33 2014 +0200
@@ -358,7 +358,7 @@
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
- simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 2,
+ simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps [@{thm domain_def}]) 3,