src/HOL/Tools/Function/measure_functions.ML
author wenzelm
Tue Feb 10 14:48:26 2015 +0100 (2015-02-10)
changeset 59498 50b60f501b05
parent 57959 1bfed12a7646
child 59580 cbc38731d42f
permissions -rw-r--r--
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
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@26875
    10
end
krauss@26875
    11
wenzelm@57959
    12
structure Measure_Functions : MEASURE_FUNCTIONS =
krauss@34232
    13
struct
krauss@26875
    14
krauss@26875
    15
(** User-declared size functions **)
krauss@26875
    16
krauss@34232
    17
fun mk_is_measure t =
krauss@34232
    18
  Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
krauss@26875
    19
krauss@26875
    20
fun find_measures ctxt T =
wenzelm@59498
    21
  DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1)
krauss@34232
    22
    (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
wenzelm@42361
    23
     |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init)
krauss@26875
    24
  |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
krauss@26875
    25
  |> Seq.list_of
krauss@26875
    26
krauss@26875
    27
krauss@26875
    28
(** Generating Measure Functions **)
krauss@26875
    29
krauss@26875
    30
fun constant_0 T = Abs ("x", T, HOLogic.zero)
krauss@26875
    31
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
krauss@26875
    32
haftmann@37678
    33
fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
blanchet@55968
    34
  map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
blanchet@55968
    35
  @ map (fn m => Sum_Tree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
krauss@26875
    36
  | mk_funorder_funs T = [ constant_1 T ]
krauss@26875
    37
haftmann@37678
    38
fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
blanchet@55968
    39
    map_product (Sum_Tree.mk_sumcase fT sT HOLogic.natT)
krauss@34232
    40
      (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
krauss@26875
    41
  | mk_ext_base_funs ctxt T = find_measures ctxt T
krauss@26875
    42
haftmann@37678
    43
fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
krauss@26875
    44
    mk_ext_base_funs ctxt T @ mk_funorder_funs T
krauss@26875
    45
  | mk_all_measure_funs ctxt T = find_measures ctxt T
krauss@26875
    46
krauss@26875
    47
val get_measure_functions = mk_all_measure_funs
krauss@26875
    48
krauss@26875
    49
end