1(*  Title:       HOL/Tools/Function/measure_functions.ML
2    Author:      Alexander Krauss, TU Muenchen
3
4Measure functions, generated heuristically.
5*)
6
7signature MEASURE_FUNCTIONS =
8sig
9  val get_measure_functions : Proof.context -> typ -> term list
10end
11
12structure Measure_Functions : MEASURE_FUNCTIONS =
13struct
14
15(** User-declared size functions **)
16
17fun mk_is_measure t =
18  Const (\<^const_name>\<open>is_measure\<close>, fastype_of t --> HOLogic.boolT) $ t
19
20fun find_measures ctxt T =
21  DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>measure_function\<close>)) 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
30fun constant_0 T = Abs ("x", T, HOLogic.zero)
31fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
32
33fun mk_funorder_funs (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [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
38fun mk_ext_base_funs ctxt (Type (\<^type_name>\<open>Sum_Type.sum\<close>, [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
43fun mk_all_measure_funs ctxt (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, _)) =
44    mk_ext_base_funs ctxt T @ mk_funorder_funs T
45  | mk_all_measure_funs ctxt T = find_measures ctxt T
46
47val get_measure_functions = mk_all_measure_funs
48
49end
50