src/HOL/Tools/Function/measure_functions.ML
author blanchet
Fri Mar 07 14:21:15 2014 +0100 (2014-03-07)
changeset 55968 94242fa87638
parent 45294 3c5d3d286055
child 57959 1bfed12a7646
permissions -rw-r--r--
tuning
haftmann@31775
     1
(*  Title:       HOL/Tools/Function/measure_functions.ML
krauss@26875
     2
    Author:      Alexander Krauss, TU Muenchen
krauss@26875
     3
wenzelm@31902
     4
Measure functions, generated heuristically.
krauss@26875
     5
*)
krauss@26875
     6
krauss@26875
     7
signature MEASURE_FUNCTIONS =
krauss@26875
     8
sig
krauss@26875
     9
  val get_measure_functions : Proof.context -> typ -> term list
krauss@34232
    10
  val setup : theory -> theory
krauss@26875
    11
end
krauss@26875
    12
krauss@34232
    13
structure MeasureFunctions : MEASURE_FUNCTIONS =
krauss@34232
    14
struct
krauss@26875
    15
krauss@26875
    16
(** User-declared size functions **)
wenzelm@31902
    17
structure Measure_Heuristic_Rules = Named_Thms
wenzelm@31902
    18
(
wenzelm@45294
    19
  val name = @{binding measure_function}
krauss@34232
    20
  val description =
wenzelm@38764
    21
    "rules that guide the heuristic generation of measure functions"
krauss@26875
    22
);
krauss@26875
    23
krauss@34232
    24
fun mk_is_measure t =
krauss@34232
    25
  Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
krauss@26875
    26
krauss@26875
    27
fun find_measures ctxt T =
krauss@34232
    28
  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
krauss@34232
    29
    (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
wenzelm@42361
    30
     |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
krauss@26875
    31
  |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
krauss@26875
    32
  |> Seq.list_of
krauss@26875
    33
krauss@26875
    34
krauss@26875
    35
(** Generating Measure Functions **)
krauss@26875
    36
krauss@26875
    37
fun constant_0 T = Abs ("x", T, HOLogic.zero)
krauss@26875
    38
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
krauss@26875
    39
haftmann@37678
    40
fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
blanchet@55968
    41
  map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
blanchet@55968
    42
  @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
krauss@26875
    43
  | mk_funorder_funs T = [ constant_1 T ]
krauss@26875
    44
haftmann@37678
    45
fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
blanchet@55968
    46
    map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
krauss@34232
    47
      (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
krauss@26875
    48
  | mk_ext_base_funs ctxt T = find_measures ctxt T
krauss@26875
    49
haftmann@37678
    50
fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
krauss@26875
    51
    mk_ext_base_funs ctxt T @ mk_funorder_funs T
krauss@26875
    52
  | mk_all_measure_funs ctxt T = find_measures ctxt T
krauss@26875
    53
krauss@26875
    54
val get_measure_functions = mk_all_measure_funs
krauss@26875
    55
wenzelm@31902
    56
val setup = Measure_Heuristic_Rules.setup
krauss@26875
    57
krauss@26875
    58
end