58196

1 
(* Author: Florian Haftmann, TU Muenchen *)


2 


3 
header \<open>Lexical order on functions\<close>


4 


5 
theory Fun_Lexorder


6 
imports Main


7 
begin


8 


9 
definition less_fun :: "('a::linorder \<Rightarrow> 'b::linorder) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"


10 
where


11 
"less_fun f g \<longleftrightarrow> (\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k'))"


12 


13 
lemma less_funI:


14 
assumes "\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k')"


15 
shows "less_fun f g"


16 
using assms by (simp add: less_fun_def)


17 


18 
lemma less_funE:


19 
assumes "less_fun f g"


20 
obtains k where "f k < g k" and "\<And>k'. k' < k \<Longrightarrow> f k' = g k'"


21 
using assms unfolding less_fun_def by blast


22 


23 
lemma less_fun_asym:


24 
assumes "less_fun f g"


25 
shows "\<not> less_fun g f"


26 
proof


27 
from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"


28 
by (blast elim!: less_funE)


29 
assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"


30 
by (blast elim!: less_funE)


31 
show False proof (cases k1 k2 rule: linorder_cases)


32 
case equal with k1 k2 show False by simp


33 
next


34 
case less with k2 have "g k1 = f k1" by simp


35 
with k1 show False by simp


36 
next


37 
case greater with k1 have "f k2 = g k2" by simp


38 
with k2 show False by simp


39 
qed


40 
qed


41 


42 
lemma less_fun_irrefl:


43 
"\<not> less_fun f f"


44 
proof


45 
assume "less_fun f f"


46 
then obtain k where k: "f k < f k"


47 
by (blast elim!: less_funE)


48 
then show False by simp


49 
qed


50 


51 
lemma less_fun_trans:


52 
assumes "less_fun f g" and "less_fun g h"


53 
shows "less_fun f h"


54 
proof (rule less_funI)


55 
from `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"


56 
by (blast elim!: less_funE)


57 
from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"


58 
by (blast elim!: less_funE)


59 
show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"


60 
proof (cases k1 k2 rule: linorder_cases)


61 
case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])


62 
next


63 
case less with k2 have "g k1 = h k1" "\<And>k'. k' < k1 \<Longrightarrow> g k' = h k'" by simp_all


64 
with k1 show ?thesis by (auto intro: exI [of _ k1])


65 
next


66 
case greater with k1 have "f k2 = g k2" "\<And>k'. k' < k2 \<Longrightarrow> f k' = g k'" by simp_all


67 
with k2 show ?thesis by (auto intro: exI [of _ k2])


68 
qed


69 
qed


70 


71 
lemma order_less_fun:


72 
"class.order (\<lambda>f g. less_fun f g \<or> f = g) less_fun"


73 
by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)


74 


75 
lemma less_fun_trichotomy:


76 
assumes "finite {k. f k \<noteq> g k}"


77 
shows "less_fun f g \<or> f = g \<or> less_fun g f"


78 
proof 


79 
{ def K \<equiv> "{k. f k \<noteq> g k}"


80 
assume "f \<noteq> g"


81 
then obtain k' where "f k' \<noteq> g k'" by auto


82 
then have [simp]: "K \<noteq> {}" by (auto simp add: K_def)


83 
with assms have [simp]: "finite K" by (simp add: K_def)


84 
def q \<equiv> "Min K"


85 
then have "q \<in> K" and "\<And>k. k \<in> K \<Longrightarrow> k \<ge> q" by auto


86 
then have "\<And>k. \<not> k \<ge> q \<Longrightarrow> k \<notin> K" by blast


87 
then have *: "\<And>k. k < q \<Longrightarrow> f k = g k" by (simp add: K_def)


88 
from `q \<in> K` have "f q \<noteq> g q" by (simp add: K_def)


89 
then have "f q < g q \<or> f q > g q" by auto


90 
with * have "less_fun f g \<or> less_fun g f"


91 
by (auto intro!: less_funI)


92 
} then show ?thesis by blast


93 
qed


94 


95 
end
