theory about lexicographic ordering on functions
authorhaftmann
Sat Sep 06 20:12:34 2014 +0200 (2014-09-06)
changeset 581961b3fbfb85980
parent 58195 1fee63e0377d
child 58197 4fd7f47ead6c
theory about lexicographic ordering on functions
CONTRIBUTORS
src/HOL/Library/Fun_Lexorder.thy
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Sat Sep 06 20:12:32 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Sat Sep 06 20:12:34 2014 +0200
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2014: Florian Haftmann, TUM
     1.8 +  Lexicographic order on functions and
     1.9 +  sum/product over function bodies.
    1.10 +
    1.11  * August 2014: Manuel Eberl, TUM
    1.12    Generic euclidean algorithms for gcd et al.
    1.13  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Fun_Lexorder.thy	Sat Sep 06 20:12:34 2014 +0200
     2.3 @@ -0,0 +1,95 @@
     2.4 +(* Author: Florian Haftmann, TU Muenchen *)
     2.5 +
     2.6 +header \<open>Lexical order on functions\<close>
     2.7 +
     2.8 +theory Fun_Lexorder
     2.9 +imports Main
    2.10 +begin
    2.11 +
    2.12 +definition less_fun :: "('a::linorder \<Rightarrow> 'b::linorder) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    2.13 +where
    2.14 +  "less_fun f g \<longleftrightarrow> (\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k'))"
    2.15 +
    2.16 +lemma less_funI:
    2.17 +  assumes "\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k')"
    2.18 +  shows "less_fun f g"
    2.19 +  using assms by (simp add: less_fun_def)
    2.20 +
    2.21 +lemma less_funE:
    2.22 +  assumes "less_fun f g"
    2.23 +  obtains k where "f k < g k" and "\<And>k'. k' < k \<Longrightarrow> f k' = g k'"
    2.24 +  using assms unfolding less_fun_def by blast
    2.25 +
    2.26 +lemma less_fun_asym:
    2.27 +  assumes "less_fun f g"
    2.28 +  shows "\<not> less_fun g f"
    2.29 +proof
    2.30 +  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
    2.31 +    by (blast elim!: less_funE) 
    2.32 +  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
    2.33 +    by (blast elim!: less_funE) 
    2.34 +  show False proof (cases k1 k2 rule: linorder_cases)
    2.35 +    case equal with k1 k2 show False by simp
    2.36 +  next
    2.37 +    case less with k2 have "g k1 = f k1" by simp
    2.38 +    with k1 show False by simp
    2.39 +  next
    2.40 +    case greater with k1 have "f k2 = g k2" by simp
    2.41 +    with k2 show False by simp
    2.42 +  qed
    2.43 +qed
    2.44 +
    2.45 +lemma less_fun_irrefl:
    2.46 +  "\<not> less_fun f f"
    2.47 +proof
    2.48 +  assume "less_fun f f"
    2.49 +  then obtain k where k: "f k < f k"
    2.50 +    by (blast elim!: less_funE)
    2.51 +  then show False by simp
    2.52 +qed
    2.53 +
    2.54 +lemma less_fun_trans:
    2.55 +  assumes "less_fun f g" and "less_fun g h"
    2.56 +  shows "less_fun f h"
    2.57 +proof (rule less_funI)
    2.58 +  from `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
    2.59 +    by (blast elim!: less_funE) 
    2.60 +  from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
    2.61 +    by (blast elim!: less_funE) 
    2.62 +  show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
    2.63 +  proof (cases k1 k2 rule: linorder_cases)
    2.64 +    case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])
    2.65 +  next
    2.66 +    case less with k2 have "g k1 = h k1" "\<And>k'. k' < k1 \<Longrightarrow> g k' = h k'" by simp_all
    2.67 +    with k1 show ?thesis by (auto intro: exI [of _ k1])
    2.68 +  next
    2.69 +    case greater with k1 have "f k2 = g k2" "\<And>k'. k' < k2 \<Longrightarrow> f k' = g k'" by simp_all
    2.70 +    with k2 show ?thesis by (auto intro: exI [of _ k2])
    2.71 +  qed
    2.72 +qed
    2.73 +
    2.74 +lemma order_less_fun:
    2.75 +  "class.order (\<lambda>f g. less_fun f g \<or> f = g) less_fun"
    2.76 +  by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)
    2.77 +
    2.78 +lemma less_fun_trichotomy:
    2.79 +  assumes "finite {k. f k \<noteq> g k}"
    2.80 +  shows "less_fun f g \<or> f = g \<or> less_fun g f"
    2.81 +proof -
    2.82 +  { def K \<equiv> "{k. f k \<noteq> g k}"
    2.83 +    assume "f \<noteq> g"
    2.84 +    then obtain k' where "f k' \<noteq> g k'" by auto
    2.85 +    then have [simp]: "K \<noteq> {}" by (auto simp add: K_def)
    2.86 +    with assms have [simp]: "finite K" by (simp add: K_def)
    2.87 +    def q \<equiv> "Min K"
    2.88 +    then have "q \<in> K" and "\<And>k. k \<in> K \<Longrightarrow> k \<ge> q" by auto
    2.89 +    then have "\<And>k. \<not> k \<ge> q \<Longrightarrow> k \<notin> K" by blast
    2.90 +    then have *: "\<And>k. k < q \<Longrightarrow> f k = g k" by (simp add: K_def)
    2.91 +    from `q \<in> K` have "f q \<noteq> g q" by (simp add: K_def)
    2.92 +    then have "f q < g q \<or> f q > g q" by auto
    2.93 +    with * have "less_fun f g \<or> less_fun g f"
    2.94 +      by (auto intro!: less_funI)
    2.95 +  } then show ?thesis by blast
    2.96 +qed
    2.97 +
    2.98 +end
     3.1 --- a/src/HOL/Library/Library.thy	Sat Sep 06 20:12:32 2014 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Sat Sep 06 20:12:34 2014 +0200
     3.3 @@ -26,6 +26,7 @@
     3.4    Function_Division
     3.5    Function_Growth
     3.6    Fundamental_Theorem_Algebra
     3.7 +  Fun_Lexorder
     3.8    Indicator_Function
     3.9    Infinite_Set
    3.10    Inner_Product