# 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 \<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)
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