src/HOL/Tools/Function/measure_functions.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 67149 e61557884799
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
     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   val get_measure_functions : Proof.context -> typ -> term list
    10 end
    11 
    12 structure Measure_Functions : MEASURE_FUNCTIONS =
    13 struct
    14 
    15 (** User-declared size functions **)
    16 
    17 fun mk_is_measure t =
    18   Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
    19 
    20 fun find_measures ctxt T =
    21   DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
    22     (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
    23      |> Thm.cterm_of ctxt |> Goal.init)
    24   |> Seq.map (Thm.prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    25   |> Seq.list_of
    26 
    27 
    28 (** Generating Measure Functions **)
    29 
    30 fun constant_0 T = Abs ("x", T, HOLogic.zero)
    31 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    32 
    33 fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    34   map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    35   @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    36   | mk_funorder_funs T = [ constant_1 T ]
    37 
    38 fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
    39     map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
    40       (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    41   | mk_ext_base_funs ctxt T = find_measures ctxt T
    42 
    43 fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
    44     mk_ext_base_funs ctxt T @ mk_funorder_funs T
    45   | mk_all_measure_funs ctxt T = find_measures ctxt T
    46 
    47 val get_measure_functions = mk_all_measure_funs
    48 
    49 end