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`