updated to named_theorems;
authorwenzelm
Sat Aug 16 19:20:11 2014 +0200 (2014-08-16)
changeset 579591bfed12a7646
parent 57958 045c96e3edf0
child 57960 ee1ba4848896
updated to named_theorems;
modernized module name and setup;
src/HOL/Fun_Def.thy
src/HOL/Fun_Def_Base.thy
src/HOL/Partial_Function.thy
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/Fun_Def.thy	Sat Aug 16 19:01:31 2014 +0200
     1.2 +++ b/src/HOL/Fun_Def.thy	Sat Aug 16 19:20:11 2014 +0200
     1.3 @@ -117,8 +117,8 @@
     1.4  inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
     1.5  where is_measure_trivial: "is_measure f"
     1.6  
     1.7 +named_theorems measure_function "rules that guide the heuristic generation of measure functions"
     1.8  ML_file "Tools/Function/measure_functions.ML"
     1.9 -setup MeasureFunctions.setup
    1.10  
    1.11  lemma measure_size[measure_function]: "is_measure size"
    1.12  by (rule is_measure_trivial)
     2.1 --- a/src/HOL/Fun_Def_Base.thy	Sat Aug 16 19:01:31 2014 +0200
     2.2 +++ b/src/HOL/Fun_Def_Base.thy	Sat Aug 16 19:20:11 2014 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  begin
     2.5  
     2.6  ML_file "Tools/Function/function_lib.ML"
     2.7 +named_theorems termination_simp "simplification rules for termination proofs"
     2.8  ML_file "Tools/Function/function_common.ML"
     2.9  ML_file "Tools/Function/context_tree.ML"
    2.10  setup Function_Ctx_Tree.setup
     3.1 --- a/src/HOL/Partial_Function.thy	Sat Aug 16 19:01:31 2014 +0200
     3.2 +++ b/src/HOL/Partial_Function.thy	Sat Aug 16 19:20:11 2014 +0200
     3.3 @@ -9,8 +9,9 @@
     3.4  keywords "partial_function" :: thy_decl
     3.5  begin
     3.6  
     3.7 +named_theorems partial_function_mono "monotonicity rules for partial function definitions"
     3.8  ML_file "Tools/Function/partial_function.ML"
     3.9 -setup Partial_Function.setup
    3.10 +
    3.11  
    3.12  subsection {* Axiomatic setup *}
    3.13  
     4.1 --- a/src/HOL/Tools/Function/function.ML	Sat Aug 16 19:01:31 2014 +0200
     4.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Aug 16 19:20:11 2014 +0200
     4.3 @@ -279,9 +279,7 @@
     4.4  
     4.5  (* setup *)
     4.6  
     4.7 -val setup =
     4.8 -  setup_case_cong
     4.9 -  #> Function_Common.Termination_Simps.setup
    4.10 +val setup = setup_case_cong
    4.11  
    4.12  val get_congs = Function_Ctx_Tree.get_function_congs
    4.13  
     5.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat Aug 16 19:01:31 2014 +0200
     5.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Aug 16 19:20:11 2014 +0200
     5.3 @@ -81,7 +81,6 @@
     5.4    val import_function_data : term -> Proof.context -> info option
     5.5    val import_last_function : Proof.context -> info option
     5.6    val add_function_data : info -> Context.generic -> Context.generic
     5.7 -  structure Termination_Simps: NAMED_THMS
     5.8    val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
     5.9    val get_termination_prover : Proof.context -> tactic
    5.10    val store_termination_rule : thm -> Context.generic -> Context.generic
    5.11 @@ -224,15 +223,6 @@
    5.12    #> store_termination_rule termination
    5.13  
    5.14  
    5.15 -(* Simp rules for termination proofs *)
    5.16 -
    5.17 -structure Termination_Simps = Named_Thms
    5.18 -(
    5.19 -  val name = @{binding termination_simp}
    5.20 -  val description = "simplification rules for termination proofs"
    5.21 -)
    5.22 -
    5.23 -
    5.24  (* Default Termination Prover *)
    5.25  
    5.26  (* FIXME just one data slot (record) per program unit *)
     6.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Aug 16 19:01:31 2014 +0200
     6.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Aug 16 19:20:11 2014 +0200
     6.3 @@ -182,7 +182,7 @@
     6.4      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
     6.5  
     6.6      val measure_funs = (* 1: generate measures *)
     6.7 -      MeasureFunctions.get_measure_functions ctxt domT
     6.8 +      Measure_Functions.get_measure_functions ctxt domT
     6.9  
    6.10      val table = (* 2: create table *)
    6.11        map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
    6.12 @@ -212,7 +212,7 @@
    6.13  fun lexicographic_order_tac quiet ctxt =
    6.14    TRY (Function_Common.apply_termination_rule ctxt 1) THEN
    6.15    lex_order_tac quiet ctxt
    6.16 -    (auto_tac (ctxt addsimps Function_Common.Termination_Simps.get ctxt))
    6.17 +    (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp})))
    6.18  
    6.19  val setup =
    6.20    Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
     7.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Sat Aug 16 19:01:31 2014 +0200
     7.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Sat Aug 16 19:20:11 2014 +0200
     7.3 @@ -7,25 +7,18 @@
     7.4  signature MEASURE_FUNCTIONS =
     7.5  sig
     7.6    val get_measure_functions : Proof.context -> typ -> term list
     7.7 -  val setup : theory -> theory
     7.8  end
     7.9  
    7.10 -structure MeasureFunctions : MEASURE_FUNCTIONS =
    7.11 +structure Measure_Functions : MEASURE_FUNCTIONS =
    7.12  struct
    7.13  
    7.14  (** User-declared size functions **)
    7.15 -structure Measure_Heuristic_Rules = Named_Thms
    7.16 -(
    7.17 -  val name = @{binding measure_function}
    7.18 -  val description =
    7.19 -    "rules that guide the heuristic generation of measure functions"
    7.20 -);
    7.21  
    7.22  fun mk_is_measure t =
    7.23    Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
    7.24  
    7.25  fun find_measures ctxt T =
    7.26 -  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
    7.27 +  DEPTH_SOLVE (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
    7.28      (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
    7.29       |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
    7.30    |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    7.31 @@ -53,6 +46,4 @@
    7.32  
    7.33  val get_measure_functions = mk_all_measure_funs
    7.34  
    7.35 -val setup = Measure_Heuristic_Rules.setup
    7.36 -
    7.37  end
     8.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sat Aug 16 19:01:31 2014 +0200
     8.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sat Aug 16 19:20:11 2014 +0200
     8.3 @@ -6,7 +6,6 @@
     8.4  
     8.5  signature PARTIAL_FUNCTION =
     8.6  sig
     8.7 -  val setup: theory -> theory
     8.8    val init: string -> term -> term -> thm -> thm -> thm option -> declaration
     8.9  
    8.10    val mono_tac: Proof.context -> int -> tactic
    8.11 @@ -54,13 +53,6 @@
    8.12  val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
    8.13  
    8.14  
    8.15 -structure Mono_Rules = Named_Thms
    8.16 -(
    8.17 -  val name = @{binding partial_function_mono};
    8.18 -  val description = "monotonicity rules for partial function definitions";
    8.19 -);
    8.20 -
    8.21 -
    8.22  (*** Automated monotonicity proofs ***)
    8.23  
    8.24  fun strip_cases ctac = ctac #> Seq.map snd;
    8.25 @@ -109,7 +101,7 @@
    8.26  fun mono_tac ctxt =
    8.27    K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
    8.28    THEN' (TRY o REPEAT_ALL_NEW
    8.29 -   (resolve_tac (Mono_Rules.get ctxt)
    8.30 +   (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
    8.31       ORELSE' split_cases_tac ctxt));
    8.32  
    8.33  
    8.34 @@ -321,7 +313,4 @@
    8.35      ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
    8.36        >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
    8.37  
    8.38 -
    8.39 -val setup = Mono_Rules.setup;
    8.40 -
    8.41  end
     9.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Aug 16 19:01:31 2014 +0200
     9.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Aug 16 19:20:11 2014 +0200
     9.3 @@ -331,7 +331,7 @@
     9.4  
     9.5  fun decomp_scnp_tac orders ctxt =
     9.6    let
     9.7 -    val extra_simps = Function_Common.Termination_Simps.get ctxt
     9.8 +    val extra_simps = Named_Theorems.get ctxt @{named_theorems termination_simp}
     9.9      val autom_tac = auto_tac (ctxt addsimps extra_simps)
    9.10    in
    9.11       gen_sizechange_tac orders autom_tac ctxt
    10.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Aug 16 19:01:31 2014 +0200
    10.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Aug 16 19:20:11 2014 +0200
    10.3 @@ -199,7 +199,7 @@
    10.4      val thy = Proof_Context.theory_of ctxt
    10.5      val sk = mk_sum_skel rel
    10.6      val Ts = node_types sk T
    10.7 -    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
    10.8 +    val M = Inttab.make (map_index (apsnd (Measure_Functions.get_measure_functions ctxt)) Ts)
    10.9      val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
   10.10        (prove_chain thy chain_tac)
   10.11      val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update