src/HOL/Tools/Function/measure_functions.ML
author wenzelm
Wed Dec 06 20:43:09 2017 +0100 (18 months ago)
changeset 67149 e61557884799
parent 59621 291934bac95e
permissions -rw-r--r--
prefer control symbol antiquotations;
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 =
wenzelm@67149
    18
  Const (\<^const_name>\<open>is_measure\<close>, fastype_of t --> HOLogic.boolT) $ t
krauss@26875
    19
krauss@26875
    20
fun find_measures ctxt T =
wenzelm@67149
    21
  DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>measure_function\<close>)) 1)
krauss@34232
    22
    (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
wenzelm@59621
    23
     |> Thm.cterm_of ctxt |> Goal.init)
wenzelm@59582
    24
  |> Seq.map (Thm.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
wenzelm@67149
    33
fun mk_funorder_funs (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [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
wenzelm@67149
    38
fun mk_ext_base_funs ctxt (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [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
wenzelm@67149
    43
fun mk_all_measure_funs ctxt (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, _)) =
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