src/HOL/Library/Fun_Lexorder.thy
 author wenzelm Sun Nov 02 17:20:45 2014 +0100 (2014-11-02) changeset 58881 b9556a055632 parent 58196 1b3fbfb85980 child 60500 903bb1495239 permissions -rw-r--r--
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 section \<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
```