haftmann@58196: (* Author: Florian Haftmann, TU Muenchen *)
haftmann@58196:
wenzelm@58881: section \Lexical order on functions\
haftmann@58196:
haftmann@58196: theory Fun_Lexorder
haftmann@58196: imports Main
haftmann@58196: begin
haftmann@58196:
haftmann@58196: definition less_fun :: "('a::linorder \ 'b::linorder) \ ('a \ 'b) \ bool"
haftmann@58196: where
haftmann@58196: "less_fun f g \ (\k. f k < g k \ (\k' < k. f k' = g k'))"
haftmann@58196:
haftmann@58196: lemma less_funI:
haftmann@58196: assumes "\k. f k < g k \ (\k' < k. f k' = g k')"
haftmann@58196: shows "less_fun f g"
haftmann@58196: using assms by (simp add: less_fun_def)
haftmann@58196:
haftmann@58196: lemma less_funE:
haftmann@58196: assumes "less_fun f g"
haftmann@58196: obtains k where "f k < g k" and "\k'. k' < k \ f k' = g k'"
haftmann@58196: using assms unfolding less_fun_def by blast
haftmann@58196:
haftmann@58196: lemma less_fun_asym:
haftmann@58196: assumes "less_fun f g"
haftmann@58196: shows "\ less_fun g f"
haftmann@58196: proof
wenzelm@63060: from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \ f k' = g k'" for k'
haftmann@58196: by (blast elim!: less_funE)
wenzelm@63060: assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \ g k' = f k'" for k'
haftmann@58196: by (blast elim!: less_funE)
haftmann@58196: show False proof (cases k1 k2 rule: linorder_cases)
haftmann@58196: case equal with k1 k2 show False by simp
haftmann@58196: next
haftmann@58196: case less with k2 have "g k1 = f k1" by simp
haftmann@58196: with k1 show False by simp
haftmann@58196: next
haftmann@58196: case greater with k1 have "f k2 = g k2" by simp
haftmann@58196: with k2 show False by simp
haftmann@58196: qed
haftmann@58196: qed
haftmann@58196:
haftmann@58196: lemma less_fun_irrefl:
haftmann@58196: "\ less_fun f f"
haftmann@58196: proof
haftmann@58196: assume "less_fun f f"
haftmann@58196: then obtain k where k: "f k < f k"
haftmann@58196: by (blast elim!: less_funE)
haftmann@58196: then show False by simp
haftmann@58196: qed
haftmann@58196:
haftmann@58196: lemma less_fun_trans:
haftmann@58196: assumes "less_fun f g" and "less_fun g h"
haftmann@58196: shows "less_fun f h"
haftmann@58196: proof (rule less_funI)
wenzelm@63060: from \less_fun f g\ obtain k1 where k1: "f k1 < g k1" "k' < k1 \ f k' = g k'" for k'
wenzelm@63060: by (blast elim!: less_funE)
wenzelm@63060: from \less_fun g h\ obtain k2 where k2: "g k2 < h k2" "k' < k2 \ g k' = h k'" for k'
haftmann@58196: by (blast elim!: less_funE)
haftmann@58196: show "\k. f k < h k \ (\k'k'. k' < k1 \ g k' = h k'" by simp_all
haftmann@58196: with k1 show ?thesis by (auto intro: exI [of _ k1])
haftmann@58196: next
haftmann@58196: case greater with k1 have "f k2 = g k2" "\k'. k' < k2 \ f k' = g k'" by simp_all
haftmann@58196: with k2 show ?thesis by (auto intro: exI [of _ k2])
haftmann@58196: qed
haftmann@58196: qed
haftmann@58196:
haftmann@58196: lemma order_less_fun:
haftmann@58196: "class.order (\f g. less_fun f g \ f = g) less_fun"
haftmann@58196: by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)
haftmann@58196:
haftmann@58196: lemma less_fun_trichotomy:
haftmann@58196: assumes "finite {k. f k \ g k}"
haftmann@58196: shows "less_fun f g \ f = g \ less_fun g f"
haftmann@58196: proof -
wenzelm@63040: { define K where "K = {k. f k \ g k}"
haftmann@58196: assume "f \ g"
haftmann@58196: then obtain k' where "f k' \ g k'" by auto
haftmann@58196: then have [simp]: "K \ {}" by (auto simp add: K_def)
haftmann@58196: with assms have [simp]: "finite K" by (simp add: K_def)
wenzelm@63040: define q where "q = Min K"
haftmann@58196: then have "q \ K" and "\k. k \ K \ k \ q" by auto
haftmann@58196: then have "\k. \ k \ q \ k \ K" by blast
haftmann@58196: then have *: "\k. k < q \ f k = g k" by (simp add: K_def)
wenzelm@60500: from \q \ K\ have "f q \ g q" by (simp add: K_def)
haftmann@58196: then have "f q < g q \ f q > g q" by auto
haftmann@58196: with * have "less_fun f g \ less_fun g f"
haftmann@58196: by (auto intro!: less_funI)
haftmann@58196: } then show ?thesis by blast
haftmann@58196: qed
haftmann@58196:
haftmann@58196: end