src/HOL/Orderings.thy
 changeset 23212 82881b1ae9c6 parent 23182 01fa88b79ddc child 23247 b99dce43d252
```     1.1 --- a/src/HOL/Orderings.thy	Sun Jun 03 15:44:35 2007 +0200
1.2 +++ b/src/HOL/Orderings.thy	Sun Jun 03 16:57:51 2007 +0200
1.3 @@ -99,94 +99,94 @@
1.4
1.5  lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
1.6      -- {* This form is useful with the classical reasoner. *}
1.7 -  by (erule ssubst) (rule order_refl)
1.8 +by (erule ssubst) (rule order_refl)
1.9
1.10  lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
1.11 -  by (simp add: less_le)
1.13
1.14  lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
1.15      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
1.16 -  by (simp add: less_le) blast
1.17 +by (simp add: less_le) blast
1.18
1.19  lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
1.20 -  unfolding less_le by blast
1.21 +unfolding less_le by blast
1.22
1.23  lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
1.24 -  unfolding less_le by blast
1.25 +unfolding less_le by blast
1.26
1.27  lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
1.28 -  by (erule contrapos_pn, erule subst, rule less_irrefl)
1.29 +by (erule contrapos_pn, erule subst, rule less_irrefl)
1.30
1.31
1.32  text {* Useful for simplification, but too risky to include by default. *}
1.33
1.34  lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
1.35 -  by auto
1.36 +by auto
1.37
1.38  lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
1.39 -  by auto
1.40 +by auto
1.41
1.42
1.43  text {* Transitivity rules for calculational reasoning *}
1.44
1.45  lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
1.46 -  by (simp add: less_le)
1.48
1.49  lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
1.50 -  by (simp add: less_le)
1.52
1.53
1.54  text {* Asymmetry. *}
1.55
1.56  lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
1.57 -  by (simp add: less_le antisym)
1.58 +by (simp add: less_le antisym)
1.59
1.60  lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
1.61 -  by (drule less_not_sym, erule contrapos_np) simp
1.62 +by (drule less_not_sym, erule contrapos_np) simp
1.63
1.64  lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
1.65 -  by (blast intro: antisym)
1.66 +by (blast intro: antisym)
1.67
1.68  lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
1.69 -  by (blast intro: antisym)
1.70 +by (blast intro: antisym)
1.71
1.72  lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
1.73 -  by (erule contrapos_pn, erule subst, rule less_irrefl)
1.74 +by (erule contrapos_pn, erule subst, rule less_irrefl)
1.75
1.76
1.77  text {* Transitivity. *}
1.78
1.79  lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
1.80 -  by (simp add: less_le) (blast intro: order_trans antisym)
1.81 +by (simp add: less_le) (blast intro: order_trans antisym)
1.82
1.83  lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
1.84 -  by (simp add: less_le) (blast intro: order_trans antisym)
1.85 +by (simp add: less_le) (blast intro: order_trans antisym)
1.86
1.87  lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
1.88 -  by (simp add: less_le) (blast intro: order_trans antisym)
1.89 +by (simp add: less_le) (blast intro: order_trans antisym)
1.90
1.91
1.92  text {* Useful for simplification, but too risky to include by default. *}
1.93
1.94  lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
1.95 -  by (blast elim: less_asym)
1.96 +by (blast elim: less_asym)
1.97
1.98  lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
1.99 -  by (blast elim: less_asym)
1.100 +by (blast elim: less_asym)
1.101
1.102
1.103  text {* Transitivity rules for calculational reasoning *}
1.104
1.105  lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
1.106 -  by (rule less_asym)
1.107 +by (rule less_asym)
1.108
1.109
1.110  text {* Reverse order *}
1.111
1.112  lemma order_reverse:
1.113    "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
1.114 -  by unfold_locales
1.115 -    (simp add: less_le, auto intro: antisym order_trans)
1.116 +by unfold_locales
1.117 +   (simp add: less_le, auto intro: antisym order_trans)
1.118
1.119  end
1.120
1.121 @@ -198,97 +198,103 @@
1.122  begin
1.123
1.124  lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
1.125 -  unfolding less_le using less_le linear by blast
1.126 +unfolding less_le using less_le linear by blast
1.127
1.128  lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
1.129 -  by (simp add: le_less less_linear)
1.130 +by (simp add: le_less less_linear)
1.131
1.132  lemma le_cases [case_names le ge]:
1.133    "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
1.134 -  using linear by blast
1.135 +using linear by blast
1.136
1.137  lemma linorder_cases [case_names less equal greater]:
1.138 -    "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
1.139 -  using less_linear by blast
1.140 +  "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
1.141 +using less_linear by blast
1.142
1.143  lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
1.144 -  apply (simp add: less_le)
1.145 -  using linear apply (blast intro: antisym)
1.146 -  done
1.148 +using linear apply (blast intro: antisym)
1.149 +done
1.150 +
1.151 +lemma not_less_iff_gr_or_eq:
1.152 + "\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y | x = y)"
1.154 +apply blast
1.155 +done
1.156
1.157  lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
1.158 -  apply (simp add: less_le)
1.159 -  using linear apply (blast intro: antisym)
1.160 -  done
1.162 +using linear apply (blast intro: antisym)
1.163 +done
1.164
1.165  lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
1.166 -  by (cut_tac x = x and y = y in less_linear, auto)
1.167 +by (cut_tac x = x and y = y in less_linear, auto)
1.168
1.169  lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
1.170 -  by (simp add: neq_iff) blast
1.171 +by (simp add: neq_iff) blast
1.172
1.173  lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
1.174 -  by (blast intro: antisym dest: not_less [THEN iffD1])
1.175 +by (blast intro: antisym dest: not_less [THEN iffD1])
1.176
1.177  lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
1.178 -  by (blast intro: antisym dest: not_less [THEN iffD1])
1.179 +by (blast intro: antisym dest: not_less [THEN iffD1])
1.180
1.181  lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
1.182 -  by (blast intro: antisym dest: not_less [THEN iffD1])
1.183 +by (blast intro: antisym dest: not_less [THEN iffD1])
1.184
1.185  text{*Replacing the old Nat.leI*}
1.186  lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
1.187 -  unfolding not_less .
1.188 +unfolding not_less .
1.189
1.190  lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
1.191 -  unfolding not_less .
1.192 +unfolding not_less .
1.193
1.194  (*FIXME inappropriate name (or delete altogether)*)
1.195  lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
1.196 -  unfolding not_le .
1.197 +unfolding not_le .
1.198
1.199
1.200  text {* Reverse order *}
1.201
1.202  lemma linorder_reverse:
1.203    "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
1.204 -  by unfold_locales
1.205 -    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
1.206 +by unfold_locales
1.207 +  (simp add: less_le, auto intro: antisym order_trans simp add: linear)
1.208
1.209
1.210  text {* min/max properties *}
1.211
1.212  lemma min_le_iff_disj:
1.213    "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
1.214 -  unfolding min_def using linear by (auto intro: order_trans)
1.215 +unfolding min_def using linear by (auto intro: order_trans)
1.216
1.217  lemma le_max_iff_disj:
1.218    "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
1.219 -  unfolding max_def using linear by (auto intro: order_trans)
1.220 +unfolding max_def using linear by (auto intro: order_trans)
1.221
1.222  lemma min_less_iff_disj:
1.223    "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
1.224 -  unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.225 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.226
1.227  lemma less_max_iff_disj:
1.228    "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
1.229 -  unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.230 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.231
1.232  lemma min_less_iff_conj [simp]:
1.233    "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
1.234 -  unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.235 +unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.236
1.237  lemma max_less_iff_conj [simp]:
1.238    "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
1.239 -  unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.240 +unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.241
1.242  lemma split_min:
1.243    "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
1.244 -  by (simp add: min_def)
1.246
1.247  lemma split_max:
1.248    "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
1.249 -  by (simp add: max_def)
1.251
1.252  end
1.253
1.254 @@ -564,16 +570,16 @@
1.255  subsection {* Transitivity reasoning *}
1.256
1.257  lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
1.258 -  by (rule subst)
1.259 +by (rule subst)
1.260
1.261  lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
1.262 -  by (rule ssubst)
1.263 +by (rule ssubst)
1.264
1.265  lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
1.266 -  by (rule subst)
1.267 +by (rule subst)
1.268
1.269  lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
1.270 -  by (rule ssubst)
1.271 +by (rule ssubst)
1.272
1.273  lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
1.274    (!!x y. x < y ==> f x < f y) ==> f a < c"
1.275 @@ -812,16 +818,16 @@
1.276    by intro_classes (auto simp add: le_bool_def less_bool_def)
1.277
1.278  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
1.279 -  by (simp add: le_bool_def)
1.281
1.282  lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
1.283 -  by (simp add: le_bool_def)
1.285
1.286  lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
1.287 -  by (simp add: le_bool_def)
1.289
1.290  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
1.291 -  by (simp add: le_bool_def)
1.293
1.294  lemma [code func]:
1.295    "False \<le> b \<longleftrightarrow> True"
1.296 @@ -850,41 +856,41 @@
1.297        !!y. P y ==> x <= y;
1.298        !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
1.299     ==> Q (Least P)"
1.300 -  apply (unfold Least_def)
1.301 -  apply (rule theI2)
1.302 -    apply (blast intro: order_antisym)+
1.303 -  done
1.304 +apply (unfold Least_def)
1.305 +apply (rule theI2)
1.306 +  apply (blast intro: order_antisym)+
1.307 +done
1.308
1.309  lemma Least_equality:
1.310 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
1.311 -  apply (simp add: Least_def)
1.312 -  apply (rule the_equality)
1.313 -  apply (auto intro!: order_antisym)
1.314 -  done
1.315 +  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
1.317 +apply (rule the_equality)
1.318 +apply (auto intro!: order_antisym)
1.319 +done
1.320
1.321  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
1.322 -  by (simp add: min_def)
1.324
1.325  lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
1.326 -  by (simp add: max_def)
1.328
1.329  lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
1.330 -  apply (simp add: min_def)
1.331 -  apply (blast intro: order_antisym)
1.332 -  done
1.334 +apply (blast intro: order_antisym)
1.335 +done
1.336
1.337  lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
1.338 -  apply (simp add: max_def)
1.339 -  apply (blast intro: order_antisym)
1.340 -  done
1.342 +apply (blast intro: order_antisym)
1.343 +done
1.344
1.345  lemma min_of_mono:
1.346 -    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
1.347 -  by (simp add: min_def)
1.348 +  "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"