1.1 --- a/NEWS Wed Oct 17 23:16:38 2007 +0200
1.2 +++ b/NEWS Thu Oct 18 09:20:55 2007 +0200
1.3 @@ -562,6 +562,10 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* localized monotonicity predicate in theory "Orderings";
1.8 +integrated lemmas max_of_mono and min_of_mono with this predicate.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 * class "div" now inherits from class "times" rather than "type".
1.12 INCOMPATIBILITY.
1.13
2.1 --- a/src/HOL/Library/Continuity.thy Wed Oct 17 23:16:38 2007 +0200
2.2 +++ b/src/HOL/Library/Continuity.thy Thu Oct 18 09:20:55 2007 +0200
2.3 @@ -153,7 +153,7 @@
2.4
2.5 lemma up_cont_mono: "up_cont f ==> mono f"
2.6 apply (rule monoI)
2.7 -apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
2.8 +apply (drule_tac F = "\<lambda>i. if i = 0 then x else y" in up_contD)
2.9 apply (rule up_chainI)
2.10 apply simp
2.11 apply (drule Un_absorb1)
2.12 @@ -181,10 +181,11 @@
2.13
2.14 lemma down_cont_mono: "down_cont f ==> mono f"
2.15 apply (rule monoI)
2.16 -apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
2.17 +apply (drule_tac F = "\<lambda>i. if i = 0 then y else x" in down_contD)
2.18 apply (rule down_chainI)
2.19 apply simp
2.20 apply (drule Int_absorb1)
2.21 +apply auto
2.22 apply (auto simp add: nat_not_singleton)
2.23 done
2.24
3.1 --- a/src/HOL/Nat.thy Wed Oct 17 23:16:38 2007 +0200
3.2 +++ b/src/HOL/Nat.thy Thu Oct 18 09:20:55 2007 +0200
3.3 @@ -549,6 +549,9 @@
3.4
3.5 subsection {* @{term min} and @{term max} *}
3.6
3.7 +lemma mono_Suc: "mono Suc"
3.8 + by (rule monoI) simp
3.9 +
3.10 lemma min_0L [simp]: "min 0 n = (0::nat)"
3.11 by (rule min_leastL) simp
3.12
3.13 @@ -556,7 +559,7 @@
3.14 by (rule min_leastR) simp
3.15
3.16 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
3.17 - by (simp add: min_of_mono)
3.18 + by (simp add: mono_Suc min_of_mono)
3.19
3.20 lemma min_Suc1:
3.21 "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
3.22 @@ -573,7 +576,7 @@
3.23 by (rule max_leastR) simp
3.24
3.25 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
3.26 - by (simp add: max_of_mono)
3.27 + by (simp add: mono_Suc max_of_mono)
3.28
3.29 lemma max_Suc1:
3.30 "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
4.1 --- a/src/HOL/Orderings.thy Wed Oct 17 23:16:38 2007 +0200
4.2 +++ b/src/HOL/Orderings.thy Thu Oct 18 09:20:55 2007 +0200
4.3 @@ -18,7 +18,6 @@
4.4 and order_refl [iff]: "x \<le> x"
4.5 and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
4.6 assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
4.7 -
4.8 begin
4.9
4.10 notation (input)
4.11 @@ -368,114 +367,126 @@
4.12
4.13 text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
4.14
4.15 +context order
4.16 +begin
4.17 +
4.18 (* The type constraint on @{term op =} below is necessary since the operation
4.19 is not a parameter of the locale. *)
4.20 -lemmas (in order)
4.21 - [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.22 +
4.23 +lemmas
4.24 + [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] =
4.25 less_irrefl [THEN notE]
4.26 -lemmas (in order)
4.27 +lemmas
4.28 [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.29 order_refl
4.30 -lemmas (in order)
4.31 +lemmas
4.32 [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.33 less_imp_le
4.34 -lemmas (in order)
4.35 +lemmas
4.36 [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.37 antisym
4.38 -lemmas (in order)
4.39 +lemmas
4.40 [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.41 eq_refl
4.42 -lemmas (in order)
4.43 +lemmas
4.44 [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.45 sym [THEN eq_refl]
4.46 -lemmas (in order)
4.47 +lemmas
4.48 [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.49 less_trans
4.50 -lemmas (in order)
4.51 +lemmas
4.52 [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.53 less_le_trans
4.54 -lemmas (in order)
4.55 +lemmas
4.56 [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.57 le_less_trans
4.58 -lemmas (in order)
4.59 +lemmas
4.60 [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.61 order_trans
4.62 -lemmas (in order)
4.63 +lemmas
4.64 [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.65 le_neq_trans
4.66 -lemmas (in order)
4.67 +lemmas
4.68 [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.69 neq_le_trans
4.70 -lemmas (in order)
4.71 +lemmas
4.72 [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.73 less_imp_neq
4.74 -lemmas (in order)
4.75 +lemmas
4.76 [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.77 eq_neq_eq_imp_neq
4.78 -lemmas (in order)
4.79 +lemmas
4.80 [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.81 not_sym
4.82
4.83 -lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
4.84 +end
4.85
4.86 -lemmas (in linorder)
4.87 +context linorder
4.88 +begin
4.89 +
4.90 +lemmas
4.91 + [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
4.92 +
4.93 +lemmas
4.94 [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.95 less_irrefl [THEN notE]
4.96 -lemmas (in linorder)
4.97 +lemmas
4.98 [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.99 order_refl
4.100 -lemmas (in linorder)
4.101 +lemmas
4.102 [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.103 less_imp_le
4.104 -lemmas (in linorder)
4.105 +lemmas
4.106 [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.107 not_less [THEN iffD2]
4.108 -lemmas (in linorder)
4.109 +lemmas
4.110 [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.111 not_le [THEN iffD2]
4.112 -lemmas (in linorder)
4.113 +lemmas
4.114 [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.115 not_less [THEN iffD1]
4.116 -lemmas (in linorder)
4.117 +lemmas
4.118 [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.119 not_le [THEN iffD1]
4.120 -lemmas (in linorder)
4.121 +lemmas
4.122 [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.123 antisym
4.124 -lemmas (in linorder)
4.125 +lemmas
4.126 [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.127 eq_refl
4.128 -lemmas (in linorder)
4.129 +lemmas
4.130 [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.131 sym [THEN eq_refl]
4.132 -lemmas (in linorder)
4.133 +lemmas
4.134 [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.135 less_trans
4.136 -lemmas (in linorder)
4.137 +lemmas
4.138 [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.139 less_le_trans
4.140 -lemmas (in linorder)
4.141 +lemmas
4.142 [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.143 le_less_trans
4.144 -lemmas (in linorder)
4.145 +lemmas
4.146 [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.147 order_trans
4.148 -lemmas (in linorder)
4.149 +lemmas
4.150 [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.151 le_neq_trans
4.152 -lemmas (in linorder)
4.153 +lemmas
4.154 [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.155 neq_le_trans
4.156 -lemmas (in linorder)
4.157 +lemmas
4.158 [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.159 less_imp_neq
4.160 -lemmas (in linorder)
4.161 +lemmas
4.162 [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.163 eq_neq_eq_imp_neq
4.164 -lemmas (in linorder)
4.165 +lemmas
4.166 [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
4.167 not_sym
4.168
4.169 +end
4.170 +
4.171
4.172 setup {*
4.173 let
4.174 @@ -537,17 +548,18 @@
4.175 subsection {* Dense orders *}
4.176
4.177 class dense_linear_order = linorder +
4.178 - assumes gt_ex: "\<exists>y. x \<sqsubset> y"
4.179 - and lt_ex: "\<exists>y. y \<sqsubset> x"
4.180 - and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
4.181 + assumes gt_ex: "\<exists>y. x < y"
4.182 + and lt_ex: "\<exists>y. y < x"
4.183 + and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
4.184 (*see further theory Dense_Linear_Order*)
4.185 -
4.186 +begin
4.187
4.188 lemma interval_empty_iff:
4.189 - fixes x y z :: "'a\<Colon>dense_linear_order"
4.190 - shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
4.191 + "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
4.192 by (auto dest: dense)
4.193
4.194 +end
4.195 +
4.196 subsection {* Name duplicates *}
4.197
4.198 lemmas order_less_le = less_le
4.199 @@ -860,7 +872,7 @@
4.200 "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
4.201 "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
4.202 "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
4.203 -by auto
4.204 + by auto
4.205
4.206 lemma xt2:
4.207 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
4.208 @@ -1027,12 +1039,40 @@
4.209
4.210 subsection {* Monotonicity, least value operator and min/max *}
4.211
4.212 -locale mono =
4.213 - fixes f
4.214 - assumes mono: "A \<le> B \<Longrightarrow> f A \<le> f B"
4.215 +context order
4.216 +begin
4.217
4.218 -lemmas monoI [intro?] = mono.intro
4.219 - and monoD [dest?] = mono.mono
4.220 +definition
4.221 + mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
4.222 +where
4.223 + "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
4.224 +
4.225 +lemma monoI [intro?]:
4.226 + fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
4.227 + shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
4.228 + unfolding mono_def by iprover
4.229 +
4.230 +lemma monoD [dest?]:
4.231 + fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
4.232 + shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
4.233 + unfolding mono_def by iprover
4.234 +
4.235 +end
4.236 +
4.237 +context linorder
4.238 +begin
4.239 +
4.240 +lemma min_of_mono:
4.241 + fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
4.242 + shows "mono f \<Longrightarrow> Orderings.min (f m) (f n) = f (min m n)"
4.243 + by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
4.244 +
4.245 +lemma max_of_mono:
4.246 + fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
4.247 + shows "mono f \<Longrightarrow> Orderings.max (f m) (f n) = f (max m n)"
4.248 + by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
4.249 +
4.250 +end
4.251
4.252 lemma LeastI2_order:
4.253 "[| P (x::'a::order);
4.254 @@ -1077,15 +1117,6 @@
4.255 apply (blast intro: order_antisym)
4.256 done
4.257
4.258 -lemma min_of_mono:
4.259 - "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
4.260 -by (simp add: min_def)
4.261 -
4.262 -lemma max_of_mono:
4.263 - "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
4.264 -by (simp add: max_def)
4.265 -
4.266 -
4.267 subsection {* legacy ML bindings *}
4.268
4.269 ML {*