summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Fun_Lexorder.thy

author | blanchet |

Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) | |

changeset 58425 | 246985c6b20b |

parent 58196 | 1b3fbfb85980 |

child 58881 | b9556a055632 |

permissions | -rw-r--r-- |

simpler proof

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

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

5 theory Fun_Lexorder

6 imports Main

7 begin

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'))"

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)

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

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

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

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

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)

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

95 end