--- 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 \<Rightarrow> nat) \<Rightarrow> 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)
--- 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
--- 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 *}
--- 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
--- 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 *)
--- 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))
--- 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
--- 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
--- 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
--- 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