src/HOL/Library/Fun_Lexorder.thy
changeset 58196 1b3fbfb85980
child 58881 b9556a055632
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Fun_Lexorder.thy	Sat Sep 06 20:12:34 2014 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header \<open>Lexical order on functions\<close>
     1.7 +
     1.8 +theory Fun_Lexorder
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +definition less_fun :: "('a::linorder \<Rightarrow> 'b::linorder) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.13 +where
    1.14 +  "less_fun f g \<longleftrightarrow> (\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k'))"
    1.15 +
    1.16 +lemma less_funI:
    1.17 +  assumes "\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k')"
    1.18 +  shows "less_fun f g"
    1.19 +  using assms by (simp add: less_fun_def)
    1.20 +
    1.21 +lemma less_funE:
    1.22 +  assumes "less_fun f g"
    1.23 +  obtains k where "f k < g k" and "\<And>k'. k' < k \<Longrightarrow> f k' = g k'"
    1.24 +  using assms unfolding less_fun_def by blast
    1.25 +
    1.26 +lemma less_fun_asym:
    1.27 +  assumes "less_fun f g"
    1.28 +  shows "\<not> less_fun g f"
    1.29 +proof
    1.30 +  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
    1.31 +    by (blast elim!: less_funE) 
    1.32 +  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
    1.33 +    by (blast elim!: less_funE) 
    1.34 +  show False proof (cases k1 k2 rule: linorder_cases)
    1.35 +    case equal with k1 k2 show False by simp
    1.36 +  next
    1.37 +    case less with k2 have "g k1 = f k1" by simp
    1.38 +    with k1 show False by simp
    1.39 +  next
    1.40 +    case greater with k1 have "f k2 = g k2" by simp
    1.41 +    with k2 show False by simp
    1.42 +  qed
    1.43 +qed
    1.44 +
    1.45 +lemma less_fun_irrefl:
    1.46 +  "\<not> less_fun f f"
    1.47 +proof
    1.48 +  assume "less_fun f f"
    1.49 +  then obtain k where k: "f k < f k"
    1.50 +    by (blast elim!: less_funE)
    1.51 +  then show False by simp
    1.52 +qed
    1.53 +
    1.54 +lemma less_fun_trans:
    1.55 +  assumes "less_fun f g" and "less_fun g h"
    1.56 +  shows "less_fun f h"
    1.57 +proof (rule less_funI)
    1.58 +  from `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
    1.59 +    by (blast elim!: less_funE) 
    1.60 +  from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
    1.61 +    by (blast elim!: less_funE) 
    1.62 +  show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
    1.63 +  proof (cases k1 k2 rule: linorder_cases)
    1.64 +    case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])
    1.65 +  next
    1.66 +    case less with k2 have "g k1 = h k1" "\<And>k'. k' < k1 \<Longrightarrow> g k' = h k'" by simp_all
    1.67 +    with k1 show ?thesis by (auto intro: exI [of _ k1])
    1.68 +  next
    1.69 +    case greater with k1 have "f k2 = g k2" "\<And>k'. k' < k2 \<Longrightarrow> f k' = g k'" by simp_all
    1.70 +    with k2 show ?thesis by (auto intro: exI [of _ k2])
    1.71 +  qed
    1.72 +qed
    1.73 +
    1.74 +lemma order_less_fun:
    1.75 +  "class.order (\<lambda>f g. less_fun f g \<or> f = g) less_fun"
    1.76 +  by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)
    1.77 +
    1.78 +lemma less_fun_trichotomy:
    1.79 +  assumes "finite {k. f k \<noteq> g k}"
    1.80 +  shows "less_fun f g \<or> f = g \<or> less_fun g f"
    1.81 +proof -
    1.82 +  { def K \<equiv> "{k. f k \<noteq> g k}"
    1.83 +    assume "f \<noteq> g"
    1.84 +    then obtain k' where "f k' \<noteq> g k'" by auto
    1.85 +    then have [simp]: "K \<noteq> {}" by (auto simp add: K_def)
    1.86 +    with assms have [simp]: "finite K" by (simp add: K_def)
    1.87 +    def q \<equiv> "Min K"
    1.88 +    then have "q \<in> K" and "\<And>k. k \<in> K \<Longrightarrow> k \<ge> q" by auto
    1.89 +    then have "\<And>k. \<not> k \<ge> q \<Longrightarrow> k \<notin> K" by blast
    1.90 +    then have *: "\<And>k. k < q \<Longrightarrow> f k = g k" by (simp add: K_def)
    1.91 +    from `q \<in> K` have "f q \<noteq> g q" by (simp add: K_def)
    1.92 +    then have "f q < g q \<or> f q > g q" by auto
    1.93 +    with * have "less_fun f g \<or> less_fun g f"
    1.94 +      by (auto intro!: less_funI)
    1.95 +  } then show ?thesis by blast
    1.96 +qed
    1.97 +
    1.98 +end