# HG changeset patch # User wenzelm # Date 1408181733 -7200 # Node ID cacb00a569e0d27d7cee63862abbfc4c51719605 # Parent fff8d328da5665d0bc199c28bf6134282b83f12b prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order; diff -r fff8d328da56 -r cacb00a569e0 src/CCL/Wfd.thy --- 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)) diff -r fff8d328da56 -r cacb00a569e0 src/Cube/Cube.thy --- 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" diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Cfun.thy --- 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 *} diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Cont.thy --- 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 *} diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Domain.thy --- 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 diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Domain_Aux.thy --- 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" diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.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 diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- 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 **************************) diff -r fff8d328da56 -r cacb00a569e0 src/HOL/HOLCF/Tools/fixrec.ML --- 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 diff -r fff8d328da56 -r cacb00a569e0 src/ZF/UNITY/Constrains.thy --- 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 \ 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" diff -r fff8d328da56 -r cacb00a569e0 src/ZF/UNITY/SubstAx.thy --- 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,