Quelle Fun_Lexorder.thy Sprache: Isabelle

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Lexicographic order on functions\<close>

theory Fun_Lexorder
imports Main
begin

definition less_fun :: "('a::linorder \ 'b::linorder) \ ('a \ 'b) \ bool"
where
  "less_fun f g \ (\k. f k < g k \ (\k' < k. f k' = g k'))"

lemma less_funI:
  assumes "\k. f k < g k \ (\k' < k. f k' = g k')"
  shows "less_fun f g"
  using assms by (simp add: less_fun_def)

lemma less_funE:
  assumes "less_fun f g"
  obtains k where "f k < g k" and "\k'. k' < k \ f k' = g k'"
  using assms unfolding less_fun_def by blast

lemma less_fun_asym:
  assumes "less_fun f g"
  shows "\ less_fun g f"
proof
  from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \ f k' = g k'" for k'
    by (blast elim!: less_funE)
  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \ g k' = f k'" for k'
    by (blast elim!: less_funE)
  show False proof (cases k1 k2 rule: linorder_cases)
    case equal with k1 k2 show False by simp
  next
    case less with k2 have "g k1 = f k1" by simp
    with k1 show False by simp
  next
    case greater with k1 have "f k2 = g k2" by simp
    with k2 show False by simp
  qed
qed

lemma less_fun_irrefl:
  "\ less_fun f f"
proof
  assume "less_fun f f"
  then obtain k where k: "f k < f k"
    by (blast elim!: less_funE)
  then show False by simp
qed

lemma less_fun_trans:
  assumes "less_fun f g" and "less_fun g h"
  shows "less_fun f h"
proof (rule less_funI)
  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
    by (blast elim!: less_funE)
  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
    by (blast elim!: less_funE)
  show "\k. f k < h k \ (\k'
  proof (cases k1 k2 rule: linorder_cases)
    case equal with k1 k2 show ?thesis by (auto simp add: exI [of _ k2])
  next
    case less with k2 have "g k1 = h k1" "\k'. k' < k1 \ g k' = h k'" by simp_all
    with k1 show ?thesis by (auto intro: exI [of _ k1])
  next
    case greater with k1 have "f k2 = g k2" "\k'. k' < k2 \ f k' = g k'" by simp_all
    with k2 show ?thesis by (auto intro: exI [of _ k2])
  qed
qed

lemma order_less_fun:
  "class.order (\f g. less_fun f g \ f = g) less_fun"
  by (rule order_strictI) (auto intro: less_fun_trans intro!: less_fun_irrefl less_fun_asym)

lemma less_fun_trichotomy:
  assumes "finite {k. f k \ g k}"
  shows "less_fun f g \ f = g \ less_fun g f"
proof -
  { define K where "K = {k. f k \ g k}"
    assume "f \ g"
    then obtain k' where "f k' \<noteq> g k'" by auto
    then have [simp]: "K \ {}" by (auto simp add: K_def)
    with assms have [simp]: "finite K" by (simp add: K_def)
    define q where "q = Min K"
    then have "q \ K" and "\k. k \ K \ k \ q" by auto
    then have "\k. \ k \ q \ k \ K" by blast
    then have *: "\k. k < q \ f k = g k" by (simp add: K_def)
    from \<open>q \<in> K\<close> have "f q \<noteq> g q" by (simp add: K_def)
    then have "f q < g q \ f q > g q" by auto
    with * have "less_fun f g \ less_fun g f"
      by (auto intro!: less_funI)
  } then show ?thesis by blast
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.