# HG changeset patch
# User haftmann
# Date 1192692055 -7200
# Node ID a50b36401c616468e2ac87e1e115647034eddc11
# Parent  8717d93b0fe2217766d0b4b83afc7ebd184bb346
localized mono predicate

diff -r 8717d93b0fe2 -r a50b36401c61 NEWS
--- 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.
 
diff -r 8717d93b0fe2 -r a50b36401c61 src/HOL/Library/Continuity.thy
--- 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
 
diff -r 8717d93b0fe2 -r a50b36401c61 src/HOL/Nat.thy
--- 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'))"
diff -r 8717d93b0fe2 -r a50b36401c61 src/HOL/Orderings.thy
--- 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 {*