# HG changeset patch
# User haftmann
# Date 1410027154 -7200
# Node ID 1b3fbfb859804c250100b817bf82d1bb35ab04b9
# Parent 1fee63e0377df048932a4d517642f86a95187813
theory about lexicographic ordering on functions
diff -r 1fee63e0377d -r 1b3fbfb85980 CONTRIBUTORS
--- a/CONTRIBUTORS Sat Sep 06 20:12:32 2014 +0200
+++ b/CONTRIBUTORS Sat Sep 06 20:12:34 2014 +0200
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+* September 2014: Florian Haftmann, TUM
+ Lexicographic order on functions and
+ sum/product over function bodies.
+
* August 2014: Manuel Eberl, TUM
Generic euclidean algorithms for gcd et al.
diff -r 1fee63e0377d -r 1b3fbfb85980 src/HOL/Library/Fun_Lexorder.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Fun_Lexorder.thy Sat Sep 06 20:12:34 2014 +0200
@@ -0,0 +1,95 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header \Lexical order on functions\
+
+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'. k' < k1 \ f k' = g k'"
+ by (blast elim!: less_funE)
+ assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\k'. k' < k2 \ g k' = f 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 `less_fun f g` obtain k1 where k1: "f k1 < g k1" "\k'. k' < k1 \ f k' = g k'"
+ by (blast elim!: less_funE)
+ from `less_fun g h` obtain k2 where k2: "g k2 < h k2" "\k'. k' < k2 \ g k' = h k'"
+ by (blast elim!: less_funE)
+ show "\k. f k < h k \ (\k'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 -
+ { def K \ "{k. f k \ g k}"
+ assume "f \ g"
+ then obtain k' where "f k' \ 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)
+ def 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 `q \ K` have "f q \ 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
diff -r 1fee63e0377d -r 1b3fbfb85980 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy Sat Sep 06 20:12:32 2014 +0200
+++ b/src/HOL/Library/Library.thy Sat Sep 06 20:12:34 2014 +0200
@@ -26,6 +26,7 @@
Function_Division
Function_Growth
Fundamental_Theorem_Algebra
+ Fun_Lexorder
Indicator_Function
Infinite_Set
Inner_Product