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