src/HOL/Tools/function_package/lexicographic_order.ML
changeset 25509 e537c91b043d
parent 24977 9f98751c9628
child 25538 58e8ba3b792b
equal deleted inserted replaced
25508:00b59b9c7c83 25509:e537c91b043d
    16   val setup: theory -> theory
    16   val setup: theory -> theory
    17 end
    17 end
    18 
    18 
    19 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    19 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    20 struct
    20 struct
       
    21 
       
    22 (** User-declared size functions **)
       
    23 
       
    24 structure SizeFunsData = GenericDataFun
       
    25 (
       
    26   type T = term NetRules.T;
       
    27   val empty = NetRules.init (op aconv) I
       
    28   val copy = I
       
    29   val extend = I
       
    30   fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
       
    31 );
       
    32 
       
    33 fun add_sfun f ctxt = 
       
    34   SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt
       
    35 val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f))))
       
    36 
       
    37 fun get_sfuns T thy =
       
    38     map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy)
       
    39                                                                 (domain_type (fastype_of f), T)
       
    40                                                                 Vartab.empty) 
       
    41                                                 f)
       
    42                    handle Type.TYPE_MATCH => NONE)
       
    43                (NetRules.rules (SizeFunsData.get (Context.Theory thy)))
    21 
    44 
    22 (** General stuff **)
    45 (** General stuff **)
    23 
    46 
    24 fun mk_measures domT mfuns =
    47 fun mk_measures domT mfuns =
    25     let 
    48     let 
    75       map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
    98       map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
    76     @ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT)
    99     @ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT)
    77 
   100 
    78   | mk_base_funs thy T = (* default: size function, if available *)
   101   | mk_base_funs thy T = (* default: size function, if available *)
    79     if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
   102     if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
    80     then [HOLogic.size_const T]
   103     then (HOLogic.size_const T) :: get_sfuns T thy
    81     else []
   104     else get_sfuns T thy
    82 
   105 
    83 fun mk_sum_case f1 f2 =
   106 fun mk_sum_case f1 f2 =
    84     let
   107     let
    85       val Type ("fun", [fT, Q]) = fastype_of f1
   108       val Type ("fun", [fT, Q]) = fastype_of f1
    86       val Type ("fun", [sT, _]) = fastype_of f2
   109       val Type ("fun", [sT, _]) = fastype_of f2
   304 fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
   327 fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
   305                                                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
   328                                                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
   306 
   329 
   307 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   330 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   308                                  "termination prover for lexicographic orderings")]
   331                                  "termination prover for lexicographic orderings")]
       
   332     #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
   309 
   333 
   310 end
   334 end