new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
authorkrauss
Fri Nov 30 16:23:52 2007 +0100 (2007-11-30)
changeset 25509e537c91b043d
parent 25508 00b59b9c7c83
child 25510 38c15efe603b
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
src/HOL/Tools/function_package/lexicographic_order.ML
     1.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Nov 30 15:40:14 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Nov 30 16:23:52 2007 +0100
     1.3 @@ -19,6 +19,29 @@
     1.4  structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
     1.5  struct
     1.6  
     1.7 +(** User-declared size functions **)
     1.8 +
     1.9 +structure SizeFunsData = GenericDataFun
    1.10 +(
    1.11 +  type T = term NetRules.T;
    1.12 +  val empty = NetRules.init (op aconv) I
    1.13 +  val copy = I
    1.14 +  val extend = I
    1.15 +  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
    1.16 +);
    1.17 +
    1.18 +fun add_sfun f ctxt = 
    1.19 +  SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt
    1.20 +val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f))))
    1.21 +
    1.22 +fun get_sfuns T thy =
    1.23 +    map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy)
    1.24 +                                                                (domain_type (fastype_of f), T)
    1.25 +                                                                Vartab.empty) 
    1.26 +                                                f)
    1.27 +                   handle Type.TYPE_MATCH => NONE)
    1.28 +               (NetRules.rules (SizeFunsData.get (Context.Theory thy)))
    1.29 +
    1.30  (** General stuff **)
    1.31  
    1.32  fun mk_measures domT mfuns =
    1.33 @@ -77,8 +100,8 @@
    1.34  
    1.35    | mk_base_funs thy T = (* default: size function, if available *)
    1.36      if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
    1.37 -    then [HOLogic.size_const T]
    1.38 -    else []
    1.39 +    then (HOLogic.size_const T) :: get_sfuns T thy
    1.40 +    else get_sfuns T thy
    1.41  
    1.42  fun mk_sum_case f1 f2 =
    1.43      let
    1.44 @@ -306,5 +329,6 @@
    1.45  
    1.46  val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
    1.47                                   "termination prover for lexicographic orderings")]
    1.48 +    #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
    1.49  
    1.50  end