# HG changeset patch # User wenzelm # Date 1246548854 -7200 # Node ID 862ae16a799db7cc36b390c730ccf30064228de0 # Parent e280491f36b8dda11b040012ee0d7b754f6bd03c renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms; diff -r e280491f36b8 -r 862ae16a799d src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/CCL/Wfd.thy Thu Jul 02 17:34:14 2009 +0200 @@ -495,7 +495,7 @@ ML {* local - structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules"); + structure Data = Named_Thms(val name = "eval" val description = "evaluation rules"); in fun eval_tac ctxt ths = diff -r e280491f36b8 -r 862ae16a799d src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Deriv.thy Thu Jul 02 17:34:14 2009 +0200 @@ -315,14 +315,14 @@ text {* @{text "DERIV_intros"} *} ML {* -structure DerivIntros = NamedThmsFun +structure Deriv_Intros = Named_Thms ( val name = "DERIV_intros" val description = "DERIV introduction rules" ) *} -setup DerivIntros.setup +setup Deriv_Intros.setup lemma DERIV_cong: "\ DERIV f x :> X ; X = Y \ \ DERIV f x :> Y" by simp diff -r e280491f36b8 -r 862ae16a799d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/HOL.thy Thu Jul 02 17:34:14 2009 +0200 @@ -923,9 +923,11 @@ ML_Antiquote.value "claset" (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())"); -structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules"); +structure ResAtpset = Named_Thms + (val name = "atp" val description = "ATP rules"); -structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP"); +structure ResBlacklist = Named_Thms + (val name = "noatp" val description = "theorems blacklisted for ATP"); *} text {*ResBlacklist holds theorems blacklisted to sledgehammer. @@ -1982,19 +1984,18 @@ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))))) *} "solve goal by normalization" + subsubsection {* Quickcheck *} ML {* -structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun +structure Quickcheck_RecFun_Simps = Named_Thms ( val name = "quickcheck_recfun_simp" val description = "simplification rules of recursive functions as needed by Quickcheck" ) *} -setup {* - Quickcheck_RecFun_Simp_Thms.setup -*} +setup Quickcheck_RecFun_Simps.setup setup {* Quickcheck.add_generator ("SML", Codegen.test_term) @@ -2008,22 +2009,22 @@ text {* This will be relocated once Nitpick is moved to HOL. *} ML {* -structure Nitpick_Const_Def_Thms = NamedThmsFun +structure Nitpick_Const_Defs = Named_Thms ( val name = "nitpick_const_def" val description = "alternative definitions of constants as needed by Nitpick" ) -structure Nitpick_Const_Simp_Thms = NamedThmsFun +structure Nitpick_Const_Simps = Named_Thms ( val name = "nitpick_const_simp" val description = "equational specification of constants as needed by Nitpick" ) -structure Nitpick_Const_Psimp_Thms = NamedThmsFun +structure Nitpick_Const_Psimps = Named_Thms ( val name = "nitpick_const_psimp" val description = "partial equational specification of constants as needed by Nitpick" ) -structure Nitpick_Ind_Intro_Thms = NamedThmsFun +structure Nitpick_Ind_Intros = Named_Thms ( val name = "nitpick_ind_intro" val description = "introduction rules for (co)inductive predicates as needed by Nitpick" @@ -2031,10 +2032,10 @@ *} setup {* - Nitpick_Const_Def_Thms.setup - #> Nitpick_Const_Simp_Thms.setup - #> Nitpick_Const_Psimp_Thms.setup - #> Nitpick_Ind_Intro_Thms.setup + Nitpick_Const_Defs.setup + #> Nitpick_Const_Simps.setup + #> Nitpick_Const_Psimps.setup + #> Nitpick_Ind_Intros.setup *} diff -r e280491f36b8 -r 862ae16a799d src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Limits.thy Thu Jul 02 17:34:14 2009 +0200 @@ -350,7 +350,7 @@ lemmas Zfun_mult_left = mult.Zfun_left -subsection{* Limits *} +subsection {* Limits *} definition tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" @@ -358,13 +358,15 @@ where [code del]: "(f ---> l) net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" -ML{* -structure TendstoIntros = - NamedThmsFun(val name = "tendsto_intros" - val description = "introduction rules for tendsto"); +ML {* +structure Tendsto_Intros = Named_Thms +( + val name = "tendsto_intros" + val description = "introduction rules for tendsto" +) *} -setup TendstoIntros.setup +setup Tendsto_Intros.setup lemma topological_tendstoI: "(\S. open S \ l \ S \ eventually (\x. f x \ S) net) diff -r e280491f36b8 -r 862ae16a799d src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 17:34:14 2009 +0200 @@ -373,7 +373,7 @@ lthy'' |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"), map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add]), maps snd simps') |> snd end) diff -r e280491f36b8 -r 862ae16a799d src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/OrderedGroup.thy Thu Jul 02 17:34:14 2009 +0200 @@ -22,13 +22,15 @@ \end{itemize} *} -ML{* -structure AlgebraSimps = - NamedThmsFun(val name = "algebra_simps" - val description = "algebra simplification rules"); +ML {* +structure Algebra_Simps = Named_Thms +( + val name = "algebra_simps" + val description = "algebra simplification rules" +) *} -setup AlgebraSimps.setup +setup Algebra_Simps.setup text{* The rewrites accumulated in @{text algebra_simps} deal with the classical algebraic structures of groups, rings and family. They simplify diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 17:34:14 2009 +0200 @@ -264,7 +264,7 @@ thy2 |> Sign.add_path (space_implode "_" new_type_names) |> PureThy.add_thmss [((Binding.name "recs", rec_thms), - [Nitpick_Const_Simp_Thms.add])] + [Nitpick_Const_Simps.add])] ||> Sign.parent_path ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, Library.flat thms)) @@ -337,7 +337,7 @@ (DatatypeProp.make_cases new_type_names descr sorts thy2) in thy2 - |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms + |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms o Context.Theory |> parent_path (#flat_names config) |> store_thmss "cases" new_type_names case_thms diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/fundef.ML --- a/src/HOL/Tools/Function/fundef.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/fundef.ML Thu Jul 02 17:34:14 2009 +0200 @@ -37,12 +37,12 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, Code.add_default_eqn_attribute, - Nitpick_Const_Simp_Thms.add, - Quickcheck_RecFun_Simp_Thms.add] + Nitpick_Const_Simps.add, + Quickcheck_RecFun_Simps.add] val psimp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, - Nitpick_Const_Psimp_Thms.add] + Nitpick_Const_Psimps.add] fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) @@ -202,7 +202,7 @@ "declaration of congruence rule for function definitions" #> setup_case_cong #> FundefRelation.setup - #> FundefCommon.TerminationSimps.setup + #> FundefCommon.Termination_Simps.setup val get_congs = FundefCtxTree.get_fundef_congs diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/fundef_common.ML --- a/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 17:34:14 2009 +0200 @@ -144,7 +144,7 @@ (* Simp rules for termination proofs *) -structure TerminationSimps = NamedThmsFun +structure Termination_Simps = Named_Thms ( val name = "termination_simp" val description = "Simplification rule for termination proofs" diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 17:34:14 2009 +0200 @@ -216,7 +216,8 @@ fun lexicographic_order_tac ctxt = TRY (FundefCommon.apply_termination_rule ctxt 1) - THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) + THEN lex_order_tac ctxt + (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt)) val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 17:34:14 2009 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/Function/measure_functions.ML Author: Alexander Krauss, TU Muenchen -Measure functions, generated heuristically +Measure functions, generated heuristically. *) signature MEASURE_FUNCTIONS = @@ -16,7 +16,8 @@ struct (** User-declared size functions **) -structure MeasureHeuristicRules = NamedThmsFun( +structure Measure_Heuristic_Rules = Named_Thms +( val name = "measure_function" val description = "Rules that guide the heuristic generation of measure functions" ); @@ -24,7 +25,7 @@ fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t fun find_measures ctxt T = - DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) + DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT))) |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) @@ -41,7 +42,7 @@ @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) | mk_funorder_funs T = [ constant_1 T ] -fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) = +fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) = map_product (SumTree.mk_sumcase fT sT HOLogic.natT) (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) | mk_ext_base_funs ctxt T = find_measures ctxt T @@ -52,7 +53,7 @@ val get_measure_functions = mk_all_measure_funs -val setup = MeasureHeuristicRules.setup +val setup = Measure_Heuristic_Rules.setup end diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:34:14 2009 +0200 @@ -405,7 +405,7 @@ fun decomp_scnp orders ctxt = let - val extra_simps = FundefCommon.TerminationSimps.get ctxt + val extra_simps = FundefCommon.Termination_Simps.get ctxt val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps) in SIMPLE_METHOD diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/size.ML Thu Jul 02 17:34:14 2009 +0200 @@ -209,7 +209,7 @@ val ([size_thms], thy'') = PureThy.add_thmss [((Binding.name "size", size_eqns), - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, + [Simplifier.simp_add, Nitpick_Const_Simps.add, Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy' diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/arith_data.ML Thu Jul 02 17:34:14 2009 +0200 @@ -28,7 +28,8 @@ (* slots for plugging in arithmetic facts and tactics *) -structure Arith_Facts = NamedThmsFun( +structure Arith_Facts = Named_Thms +( val name = "arith" val description = "arith facts - only ground formulas" ); diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Thu Jul 02 17:34:14 2009 +0200 @@ -694,7 +694,7 @@ LocalTheory.notes kind (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE)), - Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>> + Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), ctxt2) = ctxt1 |> diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Thu Jul 02 17:34:14 2009 +0200 @@ -283,8 +283,8 @@ val simps'' = maps snd simps'; in thy'' - |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, - Code.add_default_eqn_attribute]), simps'') + |> note (("simps", + [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'') |> snd |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/primrec.ML Thu Jul 02 17:34:14 2009 +0200 @@ -272,7 +272,7 @@ (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"), map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]); + [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]); in lthy |> set_group ? LocalTheory.set_group (serial_string ()) diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 17:34:14 2009 +0200 @@ -244,7 +244,7 @@ |-> (fn proto_simps => prove_simps proto_simps) |-> (fn simps => LocalTheory.note Thm.generatedK ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]), simps)) |> snd end diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/recdef.ML Thu Jul 02 17:34:14 2009 +0200 @@ -207,8 +207,8 @@ tfl_fn not_permissive thy cs (ss delcongs [imp_cong]) congs wfs name R eqs; val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); - val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, - Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else []; + val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add, + Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else []; val ((simps' :: rules', [induct']), thy) = thy diff -r e280491f36b8 -r 862ae16a799d src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Jul 02 17:34:14 2009 +0200 @@ -2192,7 +2192,7 @@ thms_thy |> (snd oo PureThy.add_thmss) [((Binding.name "simps", sel_upd_simps), - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add]), ((Binding.name "iffs", iffs), [iff_add])] |> put_record name (make_record_info args parent fields extension induct_scheme') |> put_sel_upd (names @ [full_moreN]) sel_upd_simps diff -r e280491f36b8 -r 862ae16a799d src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/ex/Numeral.thy Thu Jul 02 17:34:14 2009 +0200 @@ -93,11 +93,14 @@ subsection {* Numeral operations *} ML {* -structure DigSimps = - NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals") +structure Dig_Simps = Named_Thms +( + val name = "numeral" + val description = "Simplification rules for numerals" +) *} -setup DigSimps.setup +setup Dig_Simps.setup instantiation num :: "{plus,times,ord}" begin diff -r e280491f36b8 -r 862ae16a799d src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOLCF/Cont.thy Thu Jul 02 17:34:14 2009 +0200 @@ -140,8 +140,11 @@ subsection {* Continuity simproc *} ML {* -structure Cont2ContData = NamedThmsFun - ( val name = "cont2cont" val description = "continuity intro rule" ) +structure Cont2ContData = Named_Thms +( + val name = "cont2cont" + val description = "continuity intro rule" +) *} setup Cont2ContData.setup diff -r e280491f36b8 -r 862ae16a799d src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/Tools/atomize_elim.ML Thu Jul 02 17:34:14 2009 +0200 @@ -20,7 +20,9 @@ struct (* theory data *) -structure AtomizeElimData = NamedThmsFun( + +structure AtomizeElimData = Named_Thms +( val name = "atomize_elim"; val description = "atomize_elim rewrite rule"; ); diff -r e280491f36b8 -r 862ae16a799d src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/ZF/UNITY/Constrains.thy Thu Jul 02 17:34:14 2009 +0200 @@ -462,7 +462,11 @@ 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 ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions"); +structure Program_Defs = Named_Thms +( + val name = "program" + val description = "program definitions" +); (*proves "co" properties when the program is specified*) @@ -478,7 +482,7 @@ (* Three subgoals *) rewrite_goal_tac [@{thm st_set_def}] 3, REPEAT (force_tac css 2), - full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1, + full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1, ALLGOALS (clarify_tac cs), REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS (clarify_tac cs), @@ -493,7 +497,7 @@ rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i; *} -setup ProgramDefs.setup +setup Program_Defs.setup method_setup safety = {* Scan.succeed (SIMPLE_METHOD' o constrains_tac) *} diff -r e280491f36b8 -r 862ae16a799d src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:33:36 2009 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:34:14 2009 +0200 @@ -359,7 +359,7 @@ REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) - simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2, + simp_tac (ss addsimps (Program_Defs.get ctxt)) 2, res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ss addsimps [@{thm domain_def}]) 3,