--- a/src/HOL/Tools/Function/measure_functions.ML Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/measure_functions.ML Sat Jan 02 23:18:58 2010 +0100
@@ -8,26 +8,28 @@
sig
val get_measure_functions : Proof.context -> typ -> term list
- val setup : theory -> theory
+ val setup : theory -> theory
end
-structure MeasureFunctions : MEASURE_FUNCTIONS =
-struct
+structure MeasureFunctions : MEASURE_FUNCTIONS =
+struct
(** User-declared size functions **)
structure Measure_Heuristic_Rules = Named_Thms
(
- val name = "measure_function"
- val description = "Rules that guide the heuristic generation of measure functions"
+ val name = "measure_function"
+ val description =
+ "Rules that guide the heuristic generation of measure functions"
);
-fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measure t =
+ Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
fun find_measures ctxt T =
- DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
- (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
- |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
+ DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
+ (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
+ |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
|> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
|> Seq.list_of
@@ -38,13 +40,13 @@
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
fun mk_funorder_funs (Type ("+", [fT, sT])) =
- map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
- @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
+ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
+ @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
| mk_funorder_funs T = [ constant_1 T ]
fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
- map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
- (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
+ map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
+ (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
| mk_ext_base_funs ctxt T = find_measures ctxt T
fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
@@ -56,4 +58,3 @@
val setup = Measure_Heuristic_Rules.setup
end
-