# HG changeset patch
# User haftmann
# Date 1163606742 -3600
# Node ID 17e6275e13f582598e50bee8bdceb548734cc37d
# Parent  d71aed9286d38f061c72cc0d43f0139df5e4f50d
added transitivity rules, reworking of min/max lemmas

diff -r d71aed9286d3 -r 17e6275e13f5 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Nov 15 17:05:41 2006 +0100
+++ b/src/HOL/Orderings.thy	Wed Nov 15 17:05:42 2006 +0100
@@ -70,7 +70,7 @@
 subsection {* Quasiorders (preorders) *}
 
 locale preorder =
-  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
   fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
   assumes refl [iff]: "x \<sqsubseteq> x"
   and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
@@ -256,6 +256,46 @@
 lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
   unfolding not_le .
 
+(* min/max *)
+
+definition
+  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "min a b = (if a \<sqsubseteq> b then a else b)"
+  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  "max a b = (if a \<sqsubseteq> b then b else a)"
+
+lemma min_le_iff_disj:
+  "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
+  unfolding min_def using linear by (auto intro: trans)
+
+lemma le_max_iff_disj:
+  "z \<sqsubseteq> max x y \<longleftrightarrow> z \<sqsubseteq> x \<or> z \<sqsubseteq> y"
+  unfolding max_def using linear by (auto intro: trans)
+
+lemma min_less_iff_disj:
+  "min x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<or> y \<sqsubset> z"
+  unfolding min_def le_less using trichotomy by (auto intro: less_trans)
+
+lemma less_max_iff_disj:
+  "z \<sqsubset> max x y \<longleftrightarrow> z \<sqsubset> x \<or> z \<sqsubset> y"
+  unfolding max_def le_less using trichotomy by (auto intro: less_trans)
+
+lemma min_less_iff_conj [simp]:
+  "z \<sqsubset> min x y \<longleftrightarrow> z \<sqsubset> x \<and> z \<sqsubset> y"
+  unfolding min_def le_less using trichotomy by (auto intro: less_trans)
+
+lemma max_less_iff_conj [simp]:
+  "max x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<and> y \<sqsubset> z"
+  unfolding max_def le_less using trichotomy by (auto intro: less_trans)
+
+lemma split_min:
+  "P (min i j) \<longleftrightarrow> (i \<sqsubseteq> j \<longrightarrow> P i) \<and> (\<not> i \<sqsubseteq> j \<longrightarrow> P j)"
+  by (simp add: min_def)
+
+lemma split_max:
+  "P (max i j) \<longleftrightarrow> (i \<sqsubseteq> j \<longrightarrow> P j) \<and> (\<not> i \<sqsubseteq> j \<longrightarrow> P i)"
+  by (simp add: max_def)
+
 end
 
 axclass linorder < order
@@ -532,7 +572,163 @@
 *}
 
 
-subsection {* Transitivity reasoning on decreasing inequalities *}
+subsection {* Transitivity reasoning *}
+
+lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
+  by (rule subst)
+
+lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
+  by (rule ssubst)
+
+lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
+  by (rule subst)
+
+lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
+  by (rule ssubst)
+
+lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
+  (!!x y. x < y ==> f x < f y) ==> f a < c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a < b" hence "f a < f b" by (rule r)
+  also assume "f b < c"
+  finally (order_less_trans) show ?thesis .
+qed
+
+lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
+  (!!x y. x < y ==> f x < f y) ==> a < f c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a < f b"
+  also assume "b < c" hence "f b < f c" by (rule r)
+  finally (order_less_trans) show ?thesis .
+qed
+
+lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
+  (!!x y. x <= y ==> f x <= f y) ==> f a < c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a <= b" hence "f a <= f b" by (rule r)
+  also assume "f b < c"
+  finally (order_le_less_trans) show ?thesis .
+qed
+
+lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
+  (!!x y. x < y ==> f x < f y) ==> a < f c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a <= f b"
+  also assume "b < c" hence "f b < f c" by (rule r)
+  finally (order_le_less_trans) show ?thesis .
+qed
+
+lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
+  (!!x y. x < y ==> f x < f y) ==> f a < c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a < b" hence "f a < f b" by (rule r)
+  also assume "f b <= c"
+  finally (order_less_le_trans) show ?thesis .
+qed
+
+lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
+  (!!x y. x <= y ==> f x <= f y) ==> a < f c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a < f b"
+  also assume "b <= c" hence "f b <= f c" by (rule r)
+  finally (order_less_le_trans) show ?thesis .
+qed
+
+lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
+  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a <= f b"
+  also assume "b <= c" hence "f b <= f c" by (rule r)
+  finally (order_trans) show ?thesis .
+qed
+
+lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
+  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a <= b" hence "f a <= f b" by (rule r)
+  also assume "f b <= c"
+  finally (order_trans) show ?thesis .
+qed
+
+lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
+  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a <= b" hence "f a <= f b" by (rule r)
+  also assume "f b = c"
+  finally (ord_le_eq_trans) show ?thesis .
+qed
+
+lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
+  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
+proof -
+  assume r: "!!x y. x <= y ==> f x <= f y"
+  assume "a = f b"
+  also assume "b <= c" hence "f b <= f c" by (rule r)
+  finally (ord_eq_le_trans) show ?thesis .
+qed
+
+lemma ord_less_eq_subst: "a < b ==> f b = c ==>
+  (!!x y. x < y ==> f x < f y) ==> f a < c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a < b" hence "f a < f b" by (rule r)
+  also assume "f b = c"
+  finally (ord_less_eq_trans) show ?thesis .
+qed
+
+lemma ord_eq_less_subst: "a = f b ==> b < c ==>
+  (!!x y. x < y ==> f x < f y) ==> a < f c"
+proof -
+  assume r: "!!x y. x < y ==> f x < f y"
+  assume "a = f b"
+  also assume "b < c" hence "f b < f c" by (rule r)
+  finally (ord_eq_less_trans) show ?thesis .
+qed
+
+text {*
+  Note that this list of rules is in reverse order of priorities.
+*}
+
+lemmas order_trans_rules [trans] =
+  order_less_subst2
+  order_less_subst1
+  order_le_less_subst2
+  order_le_less_subst1
+  order_less_le_subst2
+  order_less_le_subst1
+  order_subst2
+  order_subst1
+  ord_le_eq_subst
+  ord_eq_le_subst
+  ord_less_eq_subst
+  ord_eq_less_subst
+  forw_subst
+  back_subst
+  rev_mp
+  mp
+  order_neq_le_trans
+  order_le_neq_trans
+  order_less_trans
+  order_less_asym'
+  order_le_less_trans
+  order_less_le_trans
+  order_trans
+  order_antisym
+  ord_le_eq_trans
+  ord_eq_le_trans
+  ord_less_eq_trans
+  ord_eq_less_trans
+  trans
+
 
 (* FIXME cleanup *)
 
@@ -619,7 +815,7 @@
   leave out the "(xtrans)" above.
 *)
 
-subsection {* Monotonicity, syntactic least value operator and syntactic min/max *}
+subsection {* Monotonicity, syntactic least value operator and min/max *}
 
 locale mono =
   fixes f
@@ -633,10 +829,68 @@
   "Least P == THE x. P x & (ALL y. P y --> x <= y)"
     -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
 
+lemma LeastI2_order:
+  "[| P (x::'a::order);
+      !!y. P y ==> x <= y;
+      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
+   ==> Q (Least P)"
+  apply (unfold Least_def)
+  apply (rule theI2)
+    apply (blast intro: order_antisym)+
+  done
+
+lemma Least_equality:
+    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
+  apply (simp add: Least_def)
+  apply (rule the_equality)
+  apply (auto intro!: order_antisym)
+  done
+
 constdefs
   min :: "['a::ord, 'a] => 'a"
   "min a b == (if a <= b then a else b)"
   max :: "['a::ord, 'a] => 'a"
   "max a b == (if a <= b then b else a)"
 
+lemma min_linorder:
+  "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
+  by (rule+) (simp add: min_def linorder.min_def)
+
+lemma max_linorder:
+  "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
+  by (rule+) (simp add: max_def linorder.max_def)
+
+lemmas min_le_iff_disj = linorder.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
+lemmas le_max_iff_disj = linorder.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
+lemmas min_less_iff_disj = linorder.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
+lemmas less_max_iff_disj = linorder.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
+lemmas min_less_iff_conj [simp] = linorder.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder]
+lemmas max_less_iff_conj [simp] = linorder.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder]
+lemmas split_min = linorder.split_min [where 'b = "?'a::linorder", simplified min_linorder]
+lemmas split_max = linorder.split_max [where 'b = "?'a::linorder", simplified max_linorder]
+
+lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
+  by (simp add: min_def)
+
+lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
+  by (simp add: max_def)
+
+lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
+  apply (simp add: min_def)
+  apply (blast intro: order_antisym)
+  done
+
+lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
+  apply (simp add: max_def)
+  apply (blast intro: order_antisym)
+  done
+
+lemma min_of_mono:
+    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
+  by (simp add: min_def)
+
+lemma max_of_mono:
+    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
+  by (simp add: max_def)
+
 end