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
 haftmann@58196 ` 1` ```(* Author: Florian Haftmann, TU Muenchen *) ``` haftmann@58196 ` 2` haftmann@58196 ` 3` ```header \Lexical 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 ``` haftmann@58196 ` 27` ``` from assms obtain k1 where k1: "f k1 < g k1" "\k'. k' < k1 \ f k' = g k'" ``` haftmann@58196 ` 28` ``` by (blast elim!: less_funE) ``` haftmann@58196 ` 29` ``` assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\k'. k' < k2 \ g k' = f 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) ``` haftmann@58196 ` 55` ``` from `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\k'. k' < k1 \ f k' = g k'" ``` haftmann@58196 ` 56` ``` by (blast elim!: less_funE) ``` haftmann@58196 ` 57` ``` from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\k'. k' < k2 \ g k' = h 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 - ``` haftmann@58196 ` 79` ``` { def 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) ``` haftmann@58196 ` 84` ``` def 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) ``` haftmann@58196 ` 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 ```