src/HOL/Orderings.thy
changeset 27682 25aceefd4786
parent 27299 3447cd2e18e8
child 27689 268a7d02cf7a
     1.1 --- a/src/HOL/Orderings.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -11,13 +11,12 @@
     1.4    "~~/src/Provers/order.ML"
     1.5  begin
     1.6  
     1.7 -subsection {* Partial orders *}
     1.8 +subsection {* Quasi orders *}
     1.9  
    1.10 -class order = ord +
    1.11 -  assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.12 +class preorder = ord +
    1.13 +  assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"
    1.14    and order_refl [iff]: "x \<le> x"
    1.15    and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    1.16 -  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.17  begin
    1.18  
    1.19  text {* Reflexivity. *}
    1.20 @@ -27,7 +26,67 @@
    1.21  by (erule ssubst) (rule order_refl)
    1.22  
    1.23  lemma less_irrefl [iff]: "\<not> x < x"
    1.24 -by (simp add: less_le)
    1.25 +by (simp add: less_le_not_le)
    1.26 +
    1.27 +lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
    1.28 +unfolding less_le_not_le by blast
    1.29 +
    1.30 +
    1.31 +text {* Asymmetry. *}
    1.32 +
    1.33 +lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
    1.34 +by (simp add: less_le_not_le)
    1.35 +
    1.36 +lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
    1.37 +by (drule less_not_sym, erule contrapos_np) simp
    1.38 +
    1.39 +
    1.40 +text {* Transitivity. *}
    1.41 +
    1.42 +lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
    1.43 +by (auto simp add: less_le_not_le intro: order_trans) 
    1.44 +
    1.45 +lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
    1.46 +by (auto simp add: less_le_not_le intro: order_trans) 
    1.47 +
    1.48 +lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
    1.49 +by (auto simp add: less_le_not_le intro: order_trans) 
    1.50 +
    1.51 +
    1.52 +text {* Useful for simplification, but too risky to include by default. *}
    1.53 +
    1.54 +lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
    1.55 +by (blast elim: less_asym)
    1.56 +
    1.57 +lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
    1.58 +by (blast elim: less_asym)
    1.59 +
    1.60 +
    1.61 +text {* Transitivity rules for calculational reasoning *}
    1.62 +
    1.63 +lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
    1.64 +by (rule less_asym)
    1.65 +
    1.66 +
    1.67 +text {* Dual order *}
    1.68 +
    1.69 +lemma dual_preorder:
    1.70 +  "preorder (op \<ge>) (op >)"
    1.71 +by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
    1.72 +
    1.73 +end
    1.74 +
    1.75 +
    1.76 +subsection {* Partial orders *}
    1.77 +
    1.78 +class order = preorder +
    1.79 +  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.80 +begin
    1.81 +
    1.82 +text {* Reflexivity. *}
    1.83 +
    1.84 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.85 +by (auto simp add: less_le_not_le intro: antisym)
    1.86  
    1.87  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
    1.88      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    1.89 @@ -36,9 +95,6 @@
    1.90  lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
    1.91  unfolding less_le by blast
    1.92  
    1.93 -lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
    1.94 -unfolding less_le by blast
    1.95 -
    1.96  
    1.97  text {* Useful for simplification, but too risky to include by default. *}
    1.98  
    1.99 @@ -60,12 +116,6 @@
   1.100  
   1.101  text {* Asymmetry. *}
   1.102  
   1.103 -lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
   1.104 -by (simp add: less_le antisym)
   1.105 -
   1.106 -lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
   1.107 -by (drule less_not_sym, erule contrapos_np) simp
   1.108 -
   1.109  lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
   1.110  by (blast intro: antisym)
   1.111  
   1.112 @@ -76,33 +126,6 @@
   1.113  by (erule contrapos_pn, erule subst, rule less_irrefl)
   1.114  
   1.115  
   1.116 -text {* Transitivity. *}
   1.117 -
   1.118 -lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   1.119 -by (simp add: less_le) (blast intro: order_trans antisym)
   1.120 -
   1.121 -lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   1.122 -by (simp add: less_le) (blast intro: order_trans antisym)
   1.123 -
   1.124 -lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
   1.125 -by (simp add: less_le) (blast intro: order_trans antisym)
   1.126 -
   1.127 -
   1.128 -text {* Useful for simplification, but too risky to include by default. *}
   1.129 -
   1.130 -lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
   1.131 -by (blast elim: less_asym)
   1.132 -
   1.133 -lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
   1.134 -by (blast elim: less_asym)
   1.135 -
   1.136 -
   1.137 -text {* Transitivity rules for calculational reasoning *}
   1.138 -
   1.139 -lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
   1.140 -by (rule less_asym)
   1.141 -
   1.142 -
   1.143  text {* Least value operator *}
   1.144  
   1.145  definition (in ord)
   1.146 @@ -129,8 +152,7 @@
   1.147  
   1.148  lemma dual_order:
   1.149    "order (op \<ge>) (op >)"
   1.150 -by unfold_locales
   1.151 -   (simp add: less_le, auto intro: antisym order_trans)
   1.152 +by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
   1.153  
   1.154  end
   1.155  
   1.156 @@ -201,8 +223,7 @@
   1.157  
   1.158  lemma dual_linorder:
   1.159    "linorder (op \<ge>) (op >)"
   1.160 -by unfold_locales
   1.161 -  (simp add: less_le, auto intro: antisym order_trans simp add: linear)
   1.162 +by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
   1.163  
   1.164  
   1.165  text {* min/max *}
   1.166 @@ -557,27 +578,27 @@
   1.167  subsection {* Name duplicates *}
   1.168  
   1.169  lemmas order_less_le = less_le
   1.170 -lemmas order_eq_refl = order_class.eq_refl
   1.171 -lemmas order_less_irrefl = order_class.less_irrefl
   1.172 +lemmas order_eq_refl = preorder_class.eq_refl
   1.173 +lemmas order_less_irrefl = preorder_class.less_irrefl
   1.174  lemmas order_le_less = order_class.le_less
   1.175  lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
   1.176 -lemmas order_less_imp_le = order_class.less_imp_le
   1.177 +lemmas order_less_imp_le = preorder_class.less_imp_le
   1.178  lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
   1.179  lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
   1.180  lemmas order_neq_le_trans = order_class.neq_le_trans
   1.181  lemmas order_le_neq_trans = order_class.le_neq_trans
   1.182  
   1.183  lemmas order_antisym = antisym
   1.184 -lemmas order_less_not_sym = order_class.less_not_sym
   1.185 -lemmas order_less_asym = order_class.less_asym
   1.186 +lemmas order_less_not_sym = preorder_class.less_not_sym
   1.187 +lemmas order_less_asym = preorder_class.less_asym
   1.188  lemmas order_eq_iff = order_class.eq_iff
   1.189  lemmas order_antisym_conv = order_class.antisym_conv
   1.190 -lemmas order_less_trans = order_class.less_trans
   1.191 -lemmas order_le_less_trans = order_class.le_less_trans
   1.192 -lemmas order_less_le_trans = order_class.less_le_trans
   1.193 -lemmas order_less_imp_not_less = order_class.less_imp_not_less
   1.194 -lemmas order_less_imp_triv = order_class.less_imp_triv
   1.195 -lemmas order_less_asym' = order_class.less_asym'
   1.196 +lemmas order_less_trans = preorder_class.less_trans
   1.197 +lemmas order_le_less_trans = preorder_class.le_less_trans
   1.198 +lemmas order_less_le_trans = preorder_class.less_le_trans
   1.199 +lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
   1.200 +lemmas order_less_imp_triv = preorder_class.less_imp_triv
   1.201 +lemmas order_less_asym' = preorder_class.less_asym'
   1.202  
   1.203  lemmas linorder_linear = linear
   1.204  lemmas linorder_less_linear = linorder_class.less_linear
   1.205 @@ -808,7 +829,7 @@
   1.206    Note that this list of rules is in reverse order of priorities.
   1.207  *}
   1.208  
   1.209 -lemmas order_trans_rules [trans] =
   1.210 +lemmas [trans] =
   1.211    order_less_subst2
   1.212    order_less_subst1
   1.213    order_le_less_subst2
   1.214 @@ -825,21 +846,61 @@
   1.215    back_subst
   1.216    rev_mp
   1.217    mp
   1.218 -  order_neq_le_trans
   1.219 -  order_le_neq_trans
   1.220 -  order_less_trans
   1.221 -  order_less_asym'
   1.222 -  order_le_less_trans
   1.223 -  order_less_le_trans
   1.224 +
   1.225 +lemmas (in order) [trans] =
   1.226 +  neq_le_trans
   1.227 +  le_neq_trans
   1.228 +
   1.229 +lemmas (in preorder) [trans] =
   1.230 +  less_trans
   1.231 +  less_asym'
   1.232 +  le_less_trans
   1.233 +  less_le_trans
   1.234    order_trans
   1.235 -  order_antisym
   1.236 +
   1.237 +lemmas (in order) [trans] =
   1.238 +  antisym
   1.239 +
   1.240 +lemmas (in ord) [trans] =
   1.241 +  ord_le_eq_trans
   1.242 +  ord_eq_le_trans
   1.243 +  ord_less_eq_trans
   1.244 +  ord_eq_less_trans
   1.245 +
   1.246 +lemmas [trans] =
   1.247 +  trans
   1.248 +
   1.249 +lemmas order_trans_rules =
   1.250 +  order_less_subst2
   1.251 +  order_less_subst1
   1.252 +  order_le_less_subst2
   1.253 +  order_le_less_subst1
   1.254 +  order_less_le_subst2
   1.255 +  order_less_le_subst1
   1.256 +  order_subst2
   1.257 +  order_subst1
   1.258 +  ord_le_eq_subst
   1.259 +  ord_eq_le_subst
   1.260 +  ord_less_eq_subst
   1.261 +  ord_eq_less_subst
   1.262 +  forw_subst
   1.263 +  back_subst
   1.264 +  rev_mp
   1.265 +  mp
   1.266 +  neq_le_trans
   1.267 +  le_neq_trans
   1.268 +  less_trans
   1.269 +  less_asym'
   1.270 +  le_less_trans
   1.271 +  less_le_trans
   1.272 +  order_trans
   1.273 +  antisym
   1.274    ord_le_eq_trans
   1.275    ord_eq_le_trans
   1.276    ord_less_eq_trans
   1.277    ord_eq_less_trans
   1.278    trans
   1.279  
   1.280 -
   1.281  (* FIXME cleanup *)
   1.282  
   1.283  text {* These support proving chains of decreasing inequalities