# HG changeset patch # User wenzelm # Date 1408209611 -7200 # Node ID 1bfed12a7646854a79237d6c11c78580876c7a98 # Parent 045c96e3edf0fb00d0429a37b2f29224e61afa50 updated to named_theorems; modernized module name and setup; diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Fun_Def.thy --- a/src/HOL/Fun_Def.thy Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Fun_Def.thy Sat Aug 16 19:20:11 2014 +0200 @@ -117,8 +117,8 @@ inductive is_measure :: "('a \ nat) \ bool" where is_measure_trivial: "is_measure f" +named_theorems measure_function "rules that guide the heuristic generation of measure functions" ML_file "Tools/Function/measure_functions.ML" -setup MeasureFunctions.setup lemma measure_size[measure_function]: "is_measure size" by (rule is_measure_trivial) diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Fun_Def_Base.thy --- a/src/HOL/Fun_Def_Base.thy Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Fun_Def_Base.thy Sat Aug 16 19:20:11 2014 +0200 @@ -9,6 +9,7 @@ begin ML_file "Tools/Function/function_lib.ML" +named_theorems termination_simp "simplification rules for termination proofs" ML_file "Tools/Function/function_common.ML" ML_file "Tools/Function/context_tree.ML" setup Function_Ctx_Tree.setup diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Partial_Function.thy Sat Aug 16 19:20:11 2014 +0200 @@ -9,8 +9,9 @@ keywords "partial_function" :: thy_decl begin +named_theorems partial_function_mono "monotonicity rules for partial function definitions" ML_file "Tools/Function/partial_function.ML" -setup Partial_Function.setup + subsection {* Axiomatic setup *} diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/function.ML Sat Aug 16 19:20:11 2014 +0200 @@ -279,9 +279,7 @@ (* setup *) -val setup = - setup_case_cong - #> Function_Common.Termination_Simps.setup +val setup = setup_case_cong val get_congs = Function_Ctx_Tree.get_function_congs diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Sat Aug 16 19:20:11 2014 +0200 @@ -81,7 +81,6 @@ val import_function_data : term -> Proof.context -> info option val import_last_function : Proof.context -> info option val add_function_data : info -> Context.generic -> Context.generic - structure Termination_Simps: NAMED_THMS val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic val get_termination_prover : Proof.context -> tactic val store_termination_rule : thm -> Context.generic -> Context.generic @@ -224,15 +223,6 @@ #> store_termination_rule termination -(* Simp rules for termination proofs *) - -structure Termination_Simps = Named_Thms -( - val name = @{binding termination_simp} - val description = "simplification rules for termination proofs" -) - - (* Default Termination Prover *) (* FIXME just one data slot (record) per program unit *) diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Aug 16 19:20:11 2014 +0200 @@ -182,7 +182,7 @@ val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) val measure_funs = (* 1: generate measures *) - MeasureFunctions.get_measure_functions ctxt domT + Measure_Functions.get_measure_functions ctxt domT val table = (* 2: create table *) map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl @@ -212,7 +212,7 @@ fun lexicographic_order_tac quiet ctxt = TRY (Function_Common.apply_termination_rule ctxt 1) THEN lex_order_tac quiet ctxt - (auto_tac (ctxt addsimps Function_Common.Termination_Simps.get ctxt)) + (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp}))) val setup = Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Sat Aug 16 19:20:11 2014 +0200 @@ -7,25 +7,18 @@ signature MEASURE_FUNCTIONS = sig val get_measure_functions : Proof.context -> typ -> term list - val setup : theory -> theory end -structure MeasureFunctions : MEASURE_FUNCTIONS = +structure Measure_Functions : MEASURE_FUNCTIONS = struct (** User-declared size functions **) -structure Measure_Heuristic_Rules = Named_Thms -( - val name = @{binding measure_function} - val description = - "rules that guide the heuristic generation of measure functions" -); fun mk_is_measure t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t fun find_measures ctxt T = - DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) + DEPTH_SOLVE (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1) (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) @@ -53,6 +46,4 @@ val get_measure_functions = mk_all_measure_funs -val setup = Measure_Heuristic_Rules.setup - end diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sat Aug 16 19:20:11 2014 +0200 @@ -6,7 +6,6 @@ signature PARTIAL_FUNCTION = sig - val setup: theory -> theory val init: string -> term -> term -> thm -> thm -> thm option -> declaration val mono_tac: Proof.context -> int -> tactic @@ -54,13 +53,6 @@ val lookup_mode = Symtab.lookup o Modes.get o Context.Proof; -structure Mono_Rules = Named_Thms -( - val name = @{binding partial_function_mono}; - val description = "monotonicity rules for partial function definitions"; -); - - (*** Automated monotonicity proofs ***) fun strip_cases ctac = ctac #> Seq.map snd; @@ -109,7 +101,7 @@ fun mono_tac ctxt = K (Local_Defs.unfold_tac ctxt [@{thm curry_def}]) THEN' (TRY o REPEAT_ALL_NEW - (resolve_tac (Mono_Rules.get ctxt) + (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono})) ORELSE' split_cases_tac ctxt)); @@ -321,7 +313,4 @@ ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec))) >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec)); - -val setup = Mono_Rules.setup; - end diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Aug 16 19:20:11 2014 +0200 @@ -331,7 +331,7 @@ fun decomp_scnp_tac orders ctxt = let - val extra_simps = Function_Common.Termination_Simps.get ctxt + val extra_simps = Named_Theorems.get ctxt @{named_theorems termination_simp} val autom_tac = auto_tac (ctxt addsimps extra_simps) in gen_sizechange_tac orders autom_tac ctxt diff -r 045c96e3edf0 -r 1bfed12a7646 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Sat Aug 16 19:01:31 2014 +0200 +++ b/src/HOL/Tools/Function/termination.ML Sat Aug 16 19:20:11 2014 +0200 @@ -199,7 +199,7 @@ val thy = Proof_Context.theory_of ctxt val sk = mk_sum_skel rel val Ts = node_types sk T - val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts) + val M = Inttab.make (map_index (apsnd (Measure_Functions.get_measure_functions ctxt)) Ts) val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update (prove_chain thy chain_tac) val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update