src/HOL/Tools/Function/measure_functions.ML
changeset 34232 36a2a3029fd3
parent 32603 e08fdd615333
child 37387 3581483cca6c
     1.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -8,26 +8,28 @@
     1.4  sig
     1.5  
     1.6    val get_measure_functions : Proof.context -> typ -> term list
     1.7 -  val setup : theory -> theory                                                      
     1.8 +  val setup : theory -> theory
     1.9  
    1.10  end
    1.11  
    1.12 -structure MeasureFunctions : MEASURE_FUNCTIONS = 
    1.13 -struct 
    1.14 +structure MeasureFunctions : MEASURE_FUNCTIONS =
    1.15 +struct
    1.16  
    1.17  (** User-declared size functions **)
    1.18  structure Measure_Heuristic_Rules = Named_Thms
    1.19  (
    1.20 -  val name = "measure_function" 
    1.21 -  val description = "Rules that guide the heuristic generation of measure functions"
    1.22 +  val name = "measure_function"
    1.23 +  val description =
    1.24 +    "Rules that guide the heuristic generation of measure functions"
    1.25  );
    1.26  
    1.27 -fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
    1.28 +fun mk_is_measure t =
    1.29 +  Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
    1.30  
    1.31  fun find_measures ctxt T =
    1.32 -  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) 
    1.33 -    (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
    1.34 -      |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
    1.35 +  DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)
    1.36 +    (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT)))
    1.37 +     |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
    1.38    |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    1.39    |> Seq.list_of
    1.40  
    1.41 @@ -38,13 +40,13 @@
    1.42  fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    1.43  
    1.44  fun mk_funorder_funs (Type ("+", [fT, sT])) =
    1.45 -      map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    1.46 -    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    1.47 +  map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    1.48 +  @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    1.49    | mk_funorder_funs T = [ constant_1 T ]
    1.50  
    1.51  fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
    1.52 -      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    1.53 -                  (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    1.54 +    map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    1.55 +      (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    1.56    | mk_ext_base_funs ctxt T = find_measures ctxt T
    1.57  
    1.58  fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
    1.59 @@ -56,4 +58,3 @@
    1.60  val setup = Measure_Heuristic_Rules.setup
    1.61  
    1.62  end
    1.63 -