
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 