src/HOL/Tools/function_package/measure_functions.ML
author krauss
Mon May 12 22:11:06 2008 +0200 (2008-05-12)
changeset 26875 e18574413bc4
permissions -rw-r--r--
Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.
krauss@26875
     1
(*  Title:       HOL/Tools/function_package/measure_functions.ML
krauss@26875
     2
    ID:          $Id$
krauss@26875
     3
    Author:      Alexander Krauss, TU Muenchen
krauss@26875
     4
krauss@26875
     5
Measure functions, generated heuristically
krauss@26875
     6
*)
krauss@26875
     7
krauss@26875
     8
signature MEASURE_FUNCTIONS =
krauss@26875
     9
sig
krauss@26875
    10
krauss@26875
    11
  val get_measure_functions : Proof.context -> typ -> term list
krauss@26875
    12
  val setup : theory -> theory                                                      
krauss@26875
    13
krauss@26875
    14
end
krauss@26875
    15
krauss@26875
    16
structure MeasureFunctions : MEASURE_FUNCTIONS = 
krauss@26875
    17
struct 
krauss@26875
    18
krauss@26875
    19
(** User-declared size functions **)
krauss@26875
    20
structure MeasureHeuristicRules = NamedThmsFun(
krauss@26875
    21
  val name = "measure_function" 
krauss@26875
    22
  val description = "Rules that guide the heuristic generation of measure functions"
krauss@26875
    23
);
krauss@26875
    24
krauss@26875
    25
fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
krauss@26875
    26
krauss@26875
    27
fun find_measures ctxt T =
krauss@26875
    28
  DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) 
krauss@26875
    29
    (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
krauss@26875
    30
      |> cterm_of (ProofContext.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
krauss@26875
    40
fun mk_funorder_funs (Type ("+", [fT, sT])) =
krauss@26875
    41
      map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
krauss@26875
    42
    @ map (fn m => SumTree.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
krauss@26875
    45
fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
krauss@26875
    46
      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
krauss@26875
    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
krauss@26875
    50
fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
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
krauss@26875
    56
val setup = MeasureHeuristicRules.setup
krauss@26875
    57
krauss@26875
    58
end
krauss@26875
    59