src/HOL/Library/Fun_Lexorder.thy
author haftmann
Sat, 06 Sep 2014 20:12:34 +0200
changeset 58196 1b3fbfb85980
child 58881 b9556a055632
permissions -rw-r--r--
theory about lexicographic ordering on functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58196
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     1
(* Author: Florian Haftmann, TU Muenchen *)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     2
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     3
header \<open>Lexical order on functions\<close>
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     4
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     5
theory Fun_Lexorder
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     6
imports Main
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     7
begin
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     8
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
     9
definition less_fun :: "('a::linorder \<Rightarrow> 'b::linorder) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    10
where
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    11
  "less_fun f g \<longleftrightarrow> (\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k'))"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    12
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    13
lemma less_funI:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    14
  assumes "\<exists>k. f k < g k \<and> (\<forall>k' < k. f k' = g k')"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    15
  shows "less_fun f g"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    16
  using assms by (simp add: less_fun_def)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    17
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    18
lemma less_funE:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    19
  assumes "less_fun f g"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    20
  obtains k where "f k < g k" and "\<And>k'. k' < k \<Longrightarrow> f k' = g k'"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    21
  using assms unfolding less_fun_def by blast
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    22
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    23
lemma less_fun_asym:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    24
  assumes "less_fun f g"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    25
  shows "\<not> less_fun g f"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    26
proof
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    27
  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    28
    by (blast elim!: less_funE) 
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    29
  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    30
    by (blast elim!: less_funE) 
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    31
  show False proof (cases k1 k2 rule: linorder_cases)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    32
    case equal with k1 k2 show False by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    33
  next
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    34
    case less with k2 have "g k1 = f k1" by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    35
    with k1 show False by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    36
  next
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    37
    case greater with k1 have "f k2 = g k2" by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    38
    with k2 show False by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    39
  qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    40
qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    41
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    42
lemma less_fun_irrefl:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    43
  "\<not> less_fun f f"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    44
proof
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    45
  assume "less_fun f f"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    46
  then obtain k where k: "f k < f k"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    47
    by (blast elim!: less_funE)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    48
  then show False by simp
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    49
qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    50
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    51
lemma less_fun_trans:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    52
  assumes "less_fun f g" and "less_fun g h"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    53
  shows "less_fun f h"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    54
proof (rule less_funI)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    55
  from `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    56
    by (blast elim!: less_funE) 
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    57
  from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    58
    by (blast elim!: less_funE) 
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    59
  show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    60
  proof (cases k1 k2 rule: linorder_cases)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    61
    case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    62
  next
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    63
    case less with k2 have "g k1 = h k1" "\<And>k'. k' < k1 \<Longrightarrow> g k' = h k'" by simp_all
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    64
    with k1 show ?thesis by (auto intro: exI [of _ k1])
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    65
  next
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    66
    case greater with k1 have "f k2 = g k2" "\<And>k'. k' < k2 \<Longrightarrow> f k' = g k'" by simp_all
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    67
    with k2 show ?thesis by (auto intro: exI [of _ k2])
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    68
  qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    69
qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    70
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    71
lemma order_less_fun:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    72
  "class.order (\<lambda>f g. less_fun f g \<or> f = g) less_fun"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    73
  by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    74
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    75
lemma less_fun_trichotomy:
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    76
  assumes "finite {k. f k \<noteq> g k}"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    77
  shows "less_fun f g \<or> f = g \<or> less_fun g f"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    78
proof -
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    79
  { def K \<equiv> "{k. f k \<noteq> g k}"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    80
    assume "f \<noteq> g"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    81
    then obtain k' where "f k' \<noteq> g k'" by auto
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    82
    then have [simp]: "K \<noteq> {}" by (auto simp add: K_def)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    83
    with assms have [simp]: "finite K" by (simp add: K_def)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    84
    def q \<equiv> "Min K"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    85
    then have "q \<in> K" and "\<And>k. k \<in> K \<Longrightarrow> k \<ge> q" by auto
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    86
    then have "\<And>k. \<not> k \<ge> q \<Longrightarrow> k \<notin> K" by blast
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    87
    then have *: "\<And>k. k < q \<Longrightarrow> f k = g k" by (simp add: K_def)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    88
    from `q \<in> K` have "f q \<noteq> g q" by (simp add: K_def)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    89
    then have "f q < g q \<or> f q > g q" by auto
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    90
    with * have "less_fun f g \<or> less_fun g f"
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    91
      by (auto intro!: less_funI)
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    92
  } then show ?thesis by blast
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    93
qed
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    94
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents:
diff changeset
    95
end