(* 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'<k. f k' = h 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