src/HOL/Tools/Function/measure_functions.ML
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32603 e08fdd615333
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
     1 (*  Title:       HOL/Tools/Function/measure_functions.ML
     2     Author:      Alexander Krauss, TU Muenchen
     3 
     4 Measure functions, generated heuristically.
     5 *)
     6 
     7 signature MEASURE_FUNCTIONS =
     8 sig
     9 
    10   val get_measure_functions : Proof.context -> typ -> term list
    11   val setup : theory -> theory                                                      
    12 
    13 end
    14 
    15 structure MeasureFunctions : MEASURE_FUNCTIONS = 
    16 struct 
    17 
    18 (** User-declared size functions **)
    19 structure Measure_Heuristic_Rules = Named_Thms
    20 (
    21   val name = "measure_function" 
    22   val description = "Rules that guide the heuristic generation of measure functions"
    23 );
    24 
    25 fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
    26 
    27 fun find_measures ctxt T =
    28   DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
    29     (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
    30       |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
    31   |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    32   |> Seq.list_of
    33 
    34 
    35 (** Generating Measure Functions **)
    36 
    37 fun constant_0 T = Abs ("x", T, HOLogic.zero)
    38 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    39 
    40 fun mk_funorder_funs (Type ("+", [fT, sT])) =
    41       map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    42     @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    43   | mk_funorder_funs T = [ constant_1 T ]
    44 
    45 fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
    46       map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    47                   (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    48   | mk_ext_base_funs ctxt T = find_measures ctxt T
    49 
    50 fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
    51     mk_ext_base_funs ctxt T @ mk_funorder_funs T
    52   | mk_all_measure_funs ctxt T = find_measures ctxt T
    53 
    54 val get_measure_functions = mk_all_measure_funs
    55 
    56 val setup = Measure_Heuristic_Rules.setup
    57 
    58 end
    59