<commit_before>(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
    ID:          $Id$
    Author:      <NAME>, <NAME>

Method for termination proofs with lexicographic orderings.
*)

signature LEXICOGRAPHIC_ORDER =
sig
  val lexicographic_order : thm list -> Proof.context -> Method.method

  (* exported for debugging *)
  val setup: theory -> theory
end

structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
struct

open FundefLib

(** General stuff **)

fun mk_measures domT mfuns =
    let 
        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
        fun mk_ms [] = Const (@{const_name "{}"}, relT)
          | mk_ms (f::fs) = 
            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
    in
        mk_ms mfuns
    end

fun del_index n [] = []
  | del_index n (x :: xs) =
    if n > 0 then x :: del_index (n - 1) xs else xs
<commit_msg>export lexicographic_order_tac<commit_after>(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
    ID:          $Id$
    Author:      <NAME>, T<NAME>

Method for termination proofs with lexicographic orderings.
*)

signature LEXICOGRAPHIC_ORDER =
sig
  val lexicographic_order : thm list -> Proof.context -> Method.method
  val lexicographic_order_tac : Proof.context -> tactic -> tactic

  val setup: theory -> theory
end

structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
struct

open FundefLib

(** General stuff **)

fun mk_measures domT mfuns =
    let 
        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
        fun mk_ms [] = Const (@{const_name "{}"}, relT)
          | mk_ms (f::fs) = 
            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
    in
        mk_ms mfuns
    end

fun del_index n [] = []
  | del_index n (x :: xs) =
    if n > 0 then x :: del_index (n - 1) xs else xs

{'fraction_non_alphanumeric': 0.11710323574730354, 'fraction_numerical': 0.002054442732408834, 'mean_word_length': 2.6343283582089554, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2491137', 'n_tokens_mistral': 721, 'n_tokens_neox': 687, 'n_words': 189}