src/HOL/Library/Fun_Lexorder.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68312 e9b5f25f6712 permissions -rw-r--r--
tuned equation
 haftmann@58196 ` 1` ```(* Author: Florian Haftmann, TU Muenchen *) ``` haftmann@58196 ` 2` nipkow@68312 ` 3` ```section \Lexicographic order on functions\ ``` haftmann@58196 ` 4` haftmann@58196 ` 5` ```theory Fun_Lexorder ``` haftmann@58196 ` 6` ```imports Main ``` haftmann@58196 ` 7` ```begin ``` haftmann@58196 ` 8` haftmann@58196 ` 9` ```definition less_fun :: "('a::linorder \ 'b::linorder) \ ('a \ 'b) \ bool" ``` haftmann@58196 ` 10` ```where ``` haftmann@58196 ` 11` ``` "less_fun f g \ (\k. f k < g k \ (\k' < k. f k' = g k'))" ``` haftmann@58196 ` 12` haftmann@58196 ` 13` ```lemma less_funI: ``` haftmann@58196 ` 14` ``` assumes "\k. f k < g k \ (\k' < k. f k' = g k')" ``` haftmann@58196 ` 15` ``` shows "less_fun f g" ``` haftmann@58196 ` 16` ``` using assms by (simp add: less_fun_def) ``` haftmann@58196 ` 17` haftmann@58196 ` 18` ```lemma less_funE: ``` haftmann@58196 ` 19` ``` assumes "less_fun f g" ``` haftmann@58196 ` 20` ``` obtains k where "f k < g k" and "\k'. k' < k \ f k' = g k'" ``` haftmann@58196 ` 21` ``` using assms unfolding less_fun_def by blast ``` haftmann@58196 ` 22` haftmann@58196 ` 23` ```lemma less_fun_asym: ``` haftmann@58196 ` 24` ``` assumes "less_fun f g" ``` haftmann@58196 ` 25` ``` shows "\ less_fun g f" ``` haftmann@58196 ` 26` ```proof ``` wenzelm@63060 ` 27` ``` from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \ f k' = g k'" for k' ``` haftmann@58196 ` 28` ``` by (blast elim!: less_funE) ``` wenzelm@63060 ` 29` ``` assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \ g k' = f k'" for k' ``` haftmann@58196 ` 30` ``` by (blast elim!: less_funE) ``` haftmann@58196 ` 31` ``` show False proof (cases k1 k2 rule: linorder_cases) ``` haftmann@58196 ` 32` ``` case equal with k1 k2 show False by simp ``` haftmann@58196 ` 33` ``` next ``` haftmann@58196 ` 34` ``` case less with k2 have "g k1 = f k1" by simp ``` haftmann@58196 ` 35` ``` with k1 show False by simp ``` haftmann@58196 ` 36` ``` next ``` haftmann@58196 ` 37` ``` case greater with k1 have "f k2 = g k2" by simp ``` haftmann@58196 ` 38` ``` with k2 show False by simp ``` haftmann@58196 ` 39` ``` qed ``` haftmann@58196 ` 40` ```qed ``` haftmann@58196 ` 41` haftmann@58196 ` 42` ```lemma less_fun_irrefl: ``` haftmann@58196 ` 43` ``` "\ less_fun f f" ``` haftmann@58196 ` 44` ```proof ``` haftmann@58196 ` 45` ``` assume "less_fun f f" ``` haftmann@58196 ` 46` ``` then obtain k where k: "f k < f k" ``` haftmann@58196 ` 47` ``` by (blast elim!: less_funE) ``` haftmann@58196 ` 48` ``` then show False by simp ``` haftmann@58196 ` 49` ```qed ``` haftmann@58196 ` 50` haftmann@58196 ` 51` ```lemma less_fun_trans: ``` haftmann@58196 ` 52` ``` assumes "less_fun f g" and "less_fun g h" ``` haftmann@58196 ` 53` ``` shows "less_fun f h" ``` haftmann@58196 ` 54` ```proof (rule less_funI) ``` wenzelm@63060 ` 55` ``` from \less_fun f g\ obtain k1 where k1: "f k1 < g k1" "k' < k1 \ f k' = g k'" for k' ``` wenzelm@63060 ` 56` ``` by (blast elim!: less_funE) ``` wenzelm@63060 ` 57` ``` from \less_fun g h\ obtain k2 where k2: "g k2 < h k2" "k' < k2 \ g k' = h k'" for k' ``` haftmann@58196 ` 58` ``` by (blast elim!: less_funE) ``` haftmann@58196 ` 59` ``` show "\k. f k < h k \ (\k'k'. k' < k1 \ g k' = h k'" by simp_all ``` haftmann@58196 ` 64` ``` with k1 show ?thesis by (auto intro: exI [of _ k1]) ``` haftmann@58196 ` 65` ``` next ``` haftmann@58196 ` 66` ``` case greater with k1 have "f k2 = g k2" "\k'. k' < k2 \ f k' = g k'" by simp_all ``` haftmann@58196 ` 67` ``` with k2 show ?thesis by (auto intro: exI [of _ k2]) ``` haftmann@58196 ` 68` ``` qed ``` haftmann@58196 ` 69` ```qed ``` haftmann@58196 ` 70` haftmann@58196 ` 71` ```lemma order_less_fun: ``` haftmann@58196 ` 72` ``` "class.order (\f g. less_fun f g \ f = g) less_fun" ``` haftmann@58196 ` 73` ``` by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym) ``` haftmann@58196 ` 74` haftmann@58196 ` 75` ```lemma less_fun_trichotomy: ``` haftmann@58196 ` 76` ``` assumes "finite {k. f k \ g k}" ``` haftmann@58196 ` 77` ``` shows "less_fun f g \ f = g \ less_fun g f" ``` haftmann@58196 ` 78` ```proof - ``` wenzelm@63040 ` 79` ``` { define K where "K = {k. f k \ g k}" ``` haftmann@58196 ` 80` ``` assume "f \ g" ``` haftmann@58196 ` 81` ``` then obtain k' where "f k' \ g k'" by auto ``` haftmann@58196 ` 82` ``` then have [simp]: "K \ {}" by (auto simp add: K_def) ``` haftmann@58196 ` 83` ``` with assms have [simp]: "finite K" by (simp add: K_def) ``` wenzelm@63040 ` 84` ``` define q where "q = Min K" ``` haftmann@58196 ` 85` ``` then have "q \ K" and "\k. k \ K \ k \ q" by auto ``` haftmann@58196 ` 86` ``` then have "\k. \ k \ q \ k \ K" by blast ``` haftmann@58196 ` 87` ``` then have *: "\k. k < q \ f k = g k" by (simp add: K_def) ``` wenzelm@60500 ` 88` ``` from \q \ K\ have "f q \ g q" by (simp add: K_def) ``` haftmann@58196 ` 89` ``` then have "f q < g q \ f q > g q" by auto ``` haftmann@58196 ` 90` ``` with * have "less_fun f g \ less_fun g f" ``` haftmann@58196 ` 91` ``` by (auto intro!: less_funI) ``` haftmann@58196 ` 92` ``` } then show ?thesis by blast ``` haftmann@58196 ` 93` ```qed ``` haftmann@58196 ` 94` haftmann@58196 ` 95` ```end ```