--- a/NEWS Wed Oct 17 23:16:38 2007 +0200
+++ b/NEWS Thu Oct 18 09:20:55 2007 +0200
@@ -562,6 +562,10 @@
*** HOL ***
+* localized monotonicity predicate in theory "Orderings";
+integrated lemmas max_of_mono and min_of_mono with this predicate.
+INCOMPATIBILITY.
+
* class "div" now inherits from class "times" rather than "type".
INCOMPATIBILITY.
--- a/src/HOL/Library/Continuity.thy Wed Oct 17 23:16:38 2007 +0200
+++ b/src/HOL/Library/Continuity.thy Thu Oct 18 09:20:55 2007 +0200
@@ -153,7 +153,7 @@
lemma up_cont_mono: "up_cont f ==> mono f"
apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
+apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD)
apply (rule up_chainI)
apply simp
apply (drule Un_absorb1)
@@ -181,10 +181,11 @@
lemma down_cont_mono: "down_cont f ==> mono f"
apply (rule monoI)
-apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
+apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD)
apply (rule down_chainI)
apply simp
apply (drule Int_absorb1)
+apply auto
apply (auto simp add: nat_not_singleton)
done
--- a/src/HOL/Nat.thy Wed Oct 17 23:16:38 2007 +0200
+++ b/src/HOL/Nat.thy Thu Oct 18 09:20:55 2007 +0200
@@ -549,6 +549,9 @@
subsection {* @{term min} and @{term max} *}
+lemma mono_Suc: "mono Suc"
+ by (rule monoI) simp
+
lemma min_0L [simp]: "min 0 n = (0::nat)"
by (rule min_leastL) simp
@@ -556,7 +559,7 @@
by (rule min_leastR) simp
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
- by (simp add: min_of_mono)
+ by (simp add: mono_Suc min_of_mono)
lemma min_Suc1:
"min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
@@ -573,7 +576,7 @@
by (rule max_leastR) simp
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
- by (simp add: max_of_mono)
+ by (simp add: mono_Suc max_of_mono)
lemma max_Suc1:
"max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
--- a/src/HOL/Orderings.thy Wed Oct 17 23:16:38 2007 +0200
+++ b/src/HOL/Orderings.thy Thu Oct 18 09:20:55 2007 +0200
@@ -18,7 +18,6 @@
and order_refl [iff]: "x \<le> x"
and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
-
begin
notation (input)
@@ -368,114 +367,126 @@
text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
+context order
+begin
+
(* The type constraint on @{term op =} below is necessary since the operation
is not a parameter of the locale. *)
-lemmas (in order)
- [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
+
+lemmas
+ [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] =
less_irrefl [THEN notE]
-lemmas (in order)
+lemmas
[order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_refl
-lemmas (in order)
+lemmas
[order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_le
-lemmas (in order)
+lemmas
[order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
antisym
-lemmas (in order)
+lemmas
[order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_refl
-lemmas (in order)
+lemmas
[order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
sym [THEN eq_refl]
-lemmas (in order)
+lemmas
[order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_trans
-lemmas (in order)
+lemmas
[order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_le_trans
-lemmas (in order)
+lemmas
[order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_less_trans
-lemmas (in order)
+lemmas
[order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_trans
-lemmas (in order)
+lemmas
[order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_neq_trans
-lemmas (in order)
+lemmas
[order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
neq_le_trans
-lemmas (in order)
+lemmas
[order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_neq
-lemmas (in order)
+lemmas
[order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_neq_eq_imp_neq
-lemmas (in order)
+lemmas
[order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_sym
-lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
+end
+
+context linorder
+begin
-lemmas (in linorder)
+lemmas
+ [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
+
+lemmas
[order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_irrefl [THEN notE]
-lemmas (in linorder)
+lemmas
[order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_refl
-lemmas (in linorder)
+lemmas
[order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_le
-lemmas (in linorder)
+lemmas
[order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_less [THEN iffD2]
-lemmas (in linorder)
+lemmas
[order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_le [THEN iffD2]
-lemmas (in linorder)
+lemmas
[order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_less [THEN iffD1]
-lemmas (in linorder)
+lemmas
[order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_le [THEN iffD1]
-lemmas (in linorder)
+lemmas
[order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
antisym
-lemmas (in linorder)
+lemmas
[order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_refl
-lemmas (in linorder)
+lemmas
[order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
sym [THEN eq_refl]
-lemmas (in linorder)
+lemmas
[order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_trans
-lemmas (in linorder)
+lemmas
[order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_le_trans
-lemmas (in linorder)
+lemmas
[order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_less_trans
-lemmas (in linorder)
+lemmas
[order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
order_trans
-lemmas (in linorder)
+lemmas
[order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
le_neq_trans
-lemmas (in linorder)
+lemmas
[order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
neq_le_trans
-lemmas (in linorder)
+lemmas
[order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
less_imp_neq
-lemmas (in linorder)
+lemmas
[order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
eq_neq_eq_imp_neq
-lemmas (in linorder)
+lemmas
[order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
not_sym
+end
+
setup {*
let
@@ -537,17 +548,18 @@
subsection {* Dense orders *}
class dense_linear_order = linorder +
- assumes gt_ex: "\<exists>y. x \<sqsubset> y"
- and lt_ex: "\<exists>y. y \<sqsubset> x"
- and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+ assumes gt_ex: "\<exists>y. x < y"
+ and lt_ex: "\<exists>y. y < x"
+ and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
(*see further theory Dense_Linear_Order*)
-
+begin
lemma interval_empty_iff:
- fixes x y z :: "'a\<Colon>dense_linear_order"
- shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+ "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
by (auto dest: dense)
+end
+
subsection {* Name duplicates *}
lemmas order_less_le = less_le
@@ -860,7 +872,7 @@
"a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
"a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
-by auto
+ by auto
lemma xt2:
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
@@ -1027,12 +1039,40 @@
subsection {* Monotonicity, least value operator and min/max *}
-locale mono =
- fixes f
- assumes mono: "A \<le> B \<Longrightarrow> f A \<le> f B"
+context order
+begin
+
+definition
+ mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
+where
+ "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
+
+lemma monoI [intro?]:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+ shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
+ unfolding mono_def by iprover
-lemmas monoI [intro?] = mono.intro
- and monoD [dest?] = mono.mono
+lemma monoD [dest?]:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+ shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+ unfolding mono_def by iprover
+
+end
+
+context linorder
+begin
+
+lemma min_of_mono:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
+ shows "mono f \<Longrightarrow> Orderings.min (f m) (f n) = f (min m n)"
+ by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
+
+lemma max_of_mono:
+ fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
+ shows "mono f \<Longrightarrow> Orderings.max (f m) (f n) = f (max m n)"
+ by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
+
+end
lemma LeastI2_order:
"[| P (x::'a::order);
@@ -1077,15 +1117,6 @@
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)
-
-
subsection {* legacy ML bindings *}
ML {*