src/HOL/Orderings.thy
 changeset 25076 a50b36401c61 parent 25062 af5ef0d4d655 child 25103 1ee419a5a30f
```     1.1 --- a/src/HOL/Orderings.thy	Wed Oct 17 23:16:38 2007 +0200
1.2 +++ b/src/HOL/Orderings.thy	Thu Oct 18 09:20:55 2007 +0200
1.3 @@ -18,7 +18,6 @@
1.4    and order_refl [iff]: "x \<le> x"
1.5    and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
1.6    assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
1.7 -
1.8  begin
1.9
1.10  notation (input)
1.11 @@ -368,114 +367,126 @@
1.12
1.13  text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
1.14
1.15 +context order
1.16 +begin
1.17 +
1.18  (* The type constraint on @{term op =} below is necessary since the operation
1.19     is not a parameter of the locale. *)
1.20 -lemmas (in order)
1.21 -  [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.22 +
1.23 +lemmas
1.24 +  [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] =
1.25    less_irrefl [THEN notE]
1.26 -lemmas (in order)
1.27 +lemmas
1.28    [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.29    order_refl
1.30 -lemmas (in order)
1.31 +lemmas
1.32    [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.33    less_imp_le
1.34 -lemmas (in order)
1.35 +lemmas
1.36    [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.37    antisym
1.38 -lemmas (in order)
1.39 +lemmas
1.40    [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.41    eq_refl
1.42 -lemmas (in order)
1.43 +lemmas
1.44    [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.45    sym [THEN eq_refl]
1.46 -lemmas (in order)
1.47 +lemmas
1.48    [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.49    less_trans
1.50 -lemmas (in order)
1.51 +lemmas
1.52    [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.53    less_le_trans
1.54 -lemmas (in order)
1.55 +lemmas
1.56    [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.57    le_less_trans
1.58 -lemmas (in order)
1.59 +lemmas
1.60    [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.61    order_trans
1.62 -lemmas (in order)
1.63 +lemmas
1.64    [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.65    le_neq_trans
1.66 -lemmas (in order)
1.67 +lemmas
1.68    [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.69    neq_le_trans
1.70 -lemmas (in order)
1.71 +lemmas
1.72    [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.73    less_imp_neq
1.74 -lemmas (in order)
1.75 +lemmas
1.76    [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.77     eq_neq_eq_imp_neq
1.78 -lemmas (in order)
1.79 +lemmas
1.80    [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.81    not_sym
1.82
1.83 -lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
1.84 +end
1.85 +
1.86 +context linorder
1.87 +begin
1.88
1.89 -lemmas (in linorder)
1.90 +lemmas
1.91 +  [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
1.92 +
1.93 +lemmas
1.94    [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.95    less_irrefl [THEN notE]
1.96 -lemmas (in linorder)
1.97 +lemmas
1.98    [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.99    order_refl
1.100 -lemmas (in linorder)
1.101 +lemmas
1.102    [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.103    less_imp_le
1.104 -lemmas (in linorder)
1.105 +lemmas
1.106    [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.107    not_less [THEN iffD2]
1.108 -lemmas (in linorder)
1.109 +lemmas
1.110    [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.111    not_le [THEN iffD2]
1.112 -lemmas (in linorder)
1.113 +lemmas
1.114    [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.115    not_less [THEN iffD1]
1.116 -lemmas (in linorder)
1.117 +lemmas
1.118    [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.119    not_le [THEN iffD1]
1.120 -lemmas (in linorder)
1.121 +lemmas
1.122    [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.123    antisym
1.124 -lemmas (in linorder)
1.125 +lemmas
1.126    [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.127    eq_refl
1.128 -lemmas (in linorder)
1.129 +lemmas
1.130    [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.131    sym [THEN eq_refl]
1.132 -lemmas (in linorder)
1.133 +lemmas
1.134    [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.135    less_trans
1.136 -lemmas (in linorder)
1.137 +lemmas
1.138    [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.139    less_le_trans
1.140 -lemmas (in linorder)
1.141 +lemmas
1.142    [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.143    le_less_trans
1.144 -lemmas (in linorder)
1.145 +lemmas
1.146    [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.147    order_trans
1.148 -lemmas (in linorder)
1.149 +lemmas
1.150    [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.151    le_neq_trans
1.152 -lemmas (in linorder)
1.153 +lemmas
1.154    [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.155    neq_le_trans
1.156 -lemmas (in linorder)
1.157 +lemmas
1.158    [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.159    less_imp_neq
1.160 -lemmas (in linorder)
1.161 +lemmas
1.162    [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.163    eq_neq_eq_imp_neq
1.164 -lemmas (in linorder)
1.165 +lemmas
1.166    [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.167    not_sym
1.168
1.169 +end
1.170 +
1.171
1.172  setup {*
1.173  let
1.174 @@ -537,17 +548,18 @@
1.175  subsection {* Dense orders *}
1.176
1.177  class dense_linear_order = linorder +
1.178 -  assumes gt_ex: "\<exists>y. x \<sqsubset> y"
1.179 -  and lt_ex: "\<exists>y. y \<sqsubset> x"
1.180 -  and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
1.181 +  assumes gt_ex: "\<exists>y. x < y"
1.182 +  and lt_ex: "\<exists>y. y < x"
1.183 +  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
1.184    (*see further theory Dense_Linear_Order*)
1.185 -
1.186 +begin
1.187
1.188  lemma interval_empty_iff:
1.189 -  fixes x y z :: "'a\<Colon>dense_linear_order"
1.190 -  shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.191 +  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.192    by (auto dest: dense)
1.193
1.194 +end
1.195 +
1.196  subsection {* Name duplicates *}
1.197
1.198  lemmas order_less_le = less_le
1.199 @@ -860,7 +872,7 @@
1.200    "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
1.201    "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
1.202    "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
1.203 -by auto
1.204 +  by auto
1.205
1.206  lemma xt2:
1.207    "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
1.208 @@ -1027,12 +1039,40 @@
1.209
1.210  subsection {* Monotonicity, least value operator and min/max *}
1.211
1.212 -locale mono =
1.213 -  fixes f
1.214 -  assumes mono: "A \<le> B \<Longrightarrow> f A \<le> f B"
1.215 +context order
1.216 +begin
1.217 +
1.218 +definition
1.219 +  mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool"
1.220 +where
1.221 +  "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
1.222 +
1.223 +lemma monoI [intro?]:
1.224 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
1.225 +  shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
1.226 +  unfolding mono_def by iprover
1.227
1.228 -lemmas monoI [intro?] = mono.intro
1.229 -  and monoD [dest?] = mono.mono
1.230 +lemma monoD [dest?]:
1.231 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
1.232 +  shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
1.233 +  unfolding mono_def by iprover
1.234 +
1.235 +end
1.236 +
1.237 +context linorder
1.238 +begin
1.239 +
1.240 +lemma min_of_mono:
1.241 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1.242 +  shows "mono f \<Longrightarrow> Orderings.min (f m) (f n) = f (min m n)"
1.243 +  by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
1.244 +
1.245 +lemma max_of_mono:
1.246 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1.247 +  shows "mono f \<Longrightarrow> Orderings.max (f m) (f n) = f (max m n)"
1.248 +  by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
1.249 +
1.250 +end
1.251
1.252  lemma LeastI2_order:
1.253    "[| P (x::'a::order);
1.254 @@ -1077,15 +1117,6 @@
1.255  apply (blast intro: order_antisym)
1.256  done
1.257
1.258 -lemma min_of_mono:
1.259 -  "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"