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)"
   1.260 -by (simp add: min_def)
   1.261 -
   1.262 -lemma max_of_mono:
   1.263 -  "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   1.264 -by (simp add: max_def)
   1.265 -
   1.266 -
   1.267  subsection {* legacy ML bindings *}
   1.268  
   1.269  ML {*