src/HOL/Library/Fun_Lexorder.thy
 changeset 58196 1b3fbfb85980 child 58881 b9556a055632
equal inserted replaced
58195:1fee63e0377d 58196:1b3fbfb85980

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