Quelle  Fun_Lexorder.thy

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Lexicographic order on functions›

theory Fun_Lexorder
imports Main
begin

definition less_fun :: "('a::linorder ==> 'b::linorder) ==> ('a ==> 'b) ==> bool"
where
  "less_fun f g ⟷ (∃k. f k < g k ∧ (∀k' < k. f k' = g k'))"

lemma less_funI:
  assumes "∃k. f k < g k ∧ (∀k' < k. f k' = g k')"
  shows "less_fun f g"
  using assms by (simp add: less_fun_def)

lemma less_funE:
  assumes "less_fun f g"
  obtains k where "f k < g k" and "∧k'. k' < k ==> f k' = g k'"
  using assms unfolding less_fun_def by blast

lemma less_fun_asym:
  assumes "less_fun f g"
  shows "¬ less_fun g f"
proof
  from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 ==> f k' = g k'" for k'
    by (blast elim!: less_funE) 
  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 ==> g k' = f k'" for k'
    by (blast elim!: less_funE) 
  show False proof (cases k1 k2 rule: linorder_cases)
    case equal with k1 k2 show False by simp
  next
    case less with k2 have "g k1 = f k1" by simp
    with k1 show False by simp
  next
    case greater with k1 have "f k2 = g k2" by simp
    with k2 show False by simp
  qed
qed

lemma less_fun_irrefl:
  "¬ less_fun f f"
proof
  assume "less_fun f f"
  then obtain k where k: "f k < f k"
    by (blast elim!: less_funE)
  then show False by simp
qed

lemma less_fun_trans:
  assumes "less_fun f g" and "less_fun g h"
  shows "less_fun f h"
proof (rule less_funI)
  from ‹less_fun f g› obtain k1 where k1: "f k1 < g k1" "k' < k1 ==> f k' = g k'" for k'
    by (blast elim!: less_funE)                          
  from ‹less_fun g h› obtain k2 where k2: "g k2 < h k2" "k' < k2 ==> g k' = h k'" for k'
    by (blast elim!: less_funE) 
  show "∃k. f k < h k ∧ (∀k'
  proof (cases k1 k2 rule: linorder_cases)
    case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])
  next
    case less with k2 have "g k1 = h k1" "∧k'. k' < k1 ==> g k' = h k'" by simp_all
    with k1 show ?thesis by (auto intro: exI [of _ k1])
  next
    case greater with k1 have "f k2 = g k2" "∧k'. k' < k2 ==> f k' = g k'" by simp_all
    with k2 show ?thesis by (auto intro: exI [of _ k2])
  qed
qed

lemma order_less_fun:
  "class.order (λf g. less_fun f g ∨ f = g) less_fun"
  by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)

lemma less_fun_trichotomy:
  assumes "finite {k. f k ≠ g k}"
  shows "less_fun f g ∨ f = g ∨ less_fun g f"
proof -
  { define K where "K = {k. f k ≠ g k}"
    assume "f ≠ g"
    then obtain k' where "f k' ≠ g k'" by auto
    then have [simp]: "K ≠ {}" by (auto simp add: K_def)
    with assms have [simp]: "finite K" by (simp add: K_def)
    define q where "q = Min K"
    then have "q ∈ K" and "∧k. k ∈ K ==> k ≥ q" by auto
    then have "∧k. ¬ k ≥ q ==> k ∉ K" by blast
    then have *: "∧k. k < q ==> f k = g k" by (simp add: K_def)
    from ‹q ∈ K› have "f q ≠ g q" by (simp add: K_def)
    then have "f q < g q ∨ f q > g q" by auto
    with * have "less_fun f g ∨ less_fun g f"
      by (auto intro!: less_funI)
  } then show ?thesis by blast
qed

end