Theory Fun_Util

theory Fun_Util
  imports Main
begin

section ‹Monotonic Functions›

lemma strict_mono_leD: "strict_mono r ⟹ m ≤ n ⟹ r m ≤ r n"
  by (erule (1) monoD [OF strict_mono_mono])

definition map_to_nat :: "('a :: linorder list) ⇒ ('a ⇒ nat)"
  where
"map_to_nat xs = (λx. card {y|y. y ∈ set xs ∧ y < x})"

lemma map_to_nat_strict_mono_on:
  "strict_mono_on (set xs) (map_to_nat xs)"
  unfolding strict_mono_on_def map_to_nat_def
proof safe
 fix x y :: 'a
  assume "x < y" "x ∈ set xs" "y ∈ set xs"
  have "finite {a |a. a ∈ set xs ∧ a < y}"
    by auto
  moreover
  have "{a |a. a ∈ set xs ∧ a < x} ⊂ {a |a. a ∈ set xs ∧ a < y}"
  proof (intro psubsetI subsetI notI)
    fix k
    assume "k ∈ {a |a. a ∈ set xs ∧ a < x}"
    hence "k < x" "k ∈ set xs"
      by simp_all
    hence "k < y" "k ∈ set xs"
      using ‹x < y› by auto
    then show "k ∈ {a |a. a ∈ set xs ∧ a < y}"
      by simp
  next
    assume "{a |a. a ∈ set xs ∧ a < x} = {a |a. a ∈ set xs ∧ a < y}"
    moreover
    have "x ∈ {a |a. a ∈ set xs ∧ a < y}"
      using ‹x < y› `x ∈ set xs` by auto
    moreover
    have "x ∉ {a |a. a ∈ set xs ∧ a < x}"
      by auto
    ultimately show False
      by simp
  qed
  ultimately show "card {a |a. a ∈ set xs ∧ a < x} < card {a |a. a ∈ set xs ∧ a < y}"
    using psubset_card_mono[of "{a |a. a ∈ set xs ∧ a < y}" "{a |a. a ∈ set xs ∧ a < x}"]
    by blast
qed

lemma strict_mono_on_map_set_ex:
  "∃(f :: ('a :: linorder ⇒ nat)). strict_mono_on (set xs) f"
  using map_to_nat_strict_mono_on by blast

locale Linorder_to_Nat_List =
  fixes map_to_nat :: "'a :: linorder list ⇒ 'a ⇒ nat"
  and   xs :: "'a :: linorder list"
  assumes map_to_nat_strict_mono_on: "strict_mono_on (set xs) (map_to_nat xs)"

context Linorder_to_Nat_List begin

lemma strict_mono_on_Suc_map_to_nat:
  "strict_mono_on (set xs) (λx. Suc (map_to_nat xs x))"
  by (metis (mono_tags, lifting) Suc_mono ord.strict_mono_on_def map_to_nat_strict_mono_on)

end (* of context *)

lemma Linorder_to_Nat_List_ex:
  "∃α. Linorder_to_Nat_List α xs"
  by (meson Linorder_to_Nat_List.intro strict_mono_on_map_set_ex)


end