src/HOL/Orderings.thy
 changeset 22841 83b9f2d3fb3c parent 22738 4899f06effc6 child 22886 cdff6ef76009
```     1.1 --- a/src/HOL/Orderings.thy	Sun May 06 21:49:26 2007 +0200
1.2 +++ b/src/HOL/Orderings.thy	Sun May 06 21:49:27 2007 +0200
1.3 @@ -48,11 +48,11 @@
1.4
1.5  definition
1.6    min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.7 -  "min a b = (if a \<sqsubseteq> b then a else b)"
1.8 +  "min a b = (if a \<^loc>\<le> b then a else b)"
1.9
1.10  definition
1.11    max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.12 -  "max a b = (if a \<sqsubseteq> b then b else a)"
1.13 +  "max a b = (if a \<^loc>\<le> b then b else a)"
1.14
1.15  end
1.16
1.17 @@ -98,104 +98,99 @@
1.18    by rule+ (simp add: max_def ord_class.max_def)
1.19
1.20
1.21 -subsection {* Quasiorders (preorders) *}
1.22 +subsection {* Partial orders *}
1.23
1.24 -class preorder = ord +
1.25 +class order = ord +
1.26    assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
1.27    and order_refl [iff]: "x \<sqsubseteq> x"
1.28    and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
1.29 +  assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
1.30 +
1.31  begin
1.32
1.33  text {* Reflexivity. *}
1.34
1.35 -lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"
1.36 +lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
1.37      -- {* This form is useful with the classical reasoner. *}
1.38    by (erule ssubst) (rule order_refl)
1.39
1.40 -lemma less_irrefl [iff]: "\<not> x \<sqsubset> x"
1.41 +lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
1.43
1.44 -lemma le_less: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubset> y \<or> x = y"
1.45 +lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
1.46      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
1.47    by (simp add: less_le) blast
1.48
1.49 -lemma le_imp_less_or_eq: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubset> y \<or> x = y"
1.50 +lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
1.51    unfolding less_le by blast
1.52
1.53 -lemma less_imp_le: "x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y"
1.54 +lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
1.55    unfolding less_le by blast
1.56
1.57 -lemma less_imp_neq: "x \<sqsubset> y \<Longrightarrow> x \<noteq> y"
1.58 +lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
1.59    by (erule contrapos_pn, erule subst, rule less_irrefl)
1.60
1.61
1.62  text {* Useful for simplification, but too risky to include by default. *}
1.63
1.64 -lemma less_imp_not_eq: "x \<sqsubset> y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
1.65 +lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
1.66    by auto
1.67
1.68 -lemma less_imp_not_eq2: "x \<sqsubset> y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
1.69 +lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
1.70    by auto
1.71
1.72
1.73  text {* Transitivity rules for calculational reasoning *}
1.74
1.75 -lemma neq_le_trans: "\<lbrakk> a \<noteq> b; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b"
1.76 -  by (simp add: less_le)
1.77 -
1.78 -lemma le_neq_trans: "\<lbrakk> a \<sqsubseteq> b; a \<noteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b"
1.79 +lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
1.81
1.82 -end
1.83 -
1.84 -subsection {* Partial orderings *}
1.85 +lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
1.86 +  by (simp add: less_le)
1.87
1.88 -class order = preorder +
1.89 -  assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
1.90 -begin
1.91
1.92  text {* Asymmetry. *}
1.93
1.94 -lemma less_not_sym: "x \<sqsubset> y \<Longrightarrow> \<not> (y \<sqsubset> x)"
1.95 +lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
1.96    by (simp add: less_le antisym)
1.97
1.98 -lemma less_asym: "x \<sqsubset> y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<sqsubset> x) \<Longrightarrow> P"
1.99 +lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
1.100    by (drule less_not_sym, erule contrapos_np) simp
1.101
1.102 -lemma eq_iff: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
1.103 +lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
1.104    by (blast intro: antisym)
1.105
1.106 -lemma antisym_conv: "y \<sqsubseteq> x \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y"
1.107 +lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
1.108    by (blast intro: antisym)
1.109
1.110 -lemma less_imp_neq: "x \<sqsubset> y \<Longrightarrow> x \<noteq> y"
1.111 +lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
1.112    by (erule contrapos_pn, erule subst, rule less_irrefl)
1.113
1.114
1.115  text {* Transitivity. *}
1.116
1.117 -lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
1.118 +lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
1.119    by (simp add: less_le) (blast intro: order_trans antisym)
1.120
1.121 -lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
1.122 +lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
1.123    by (simp add: less_le) (blast intro: order_trans antisym)
1.124
1.125 -lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
1.126 +lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
1.127    by (simp add: less_le) (blast intro: order_trans antisym)
1.128
1.129
1.130  text {* Useful for simplification, but too risky to include by default. *}
1.131
1.132 -lemma less_imp_not_less: "x \<sqsubset> y \<Longrightarrow> (\<not> y \<sqsubset> x) \<longleftrightarrow> True"
1.133 +lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
1.134    by (blast elim: less_asym)
1.135
1.136 -lemma less_imp_triv: "x \<sqsubset> y \<Longrightarrow> (y \<sqsubset> x \<longrightarrow> P) \<longleftrightarrow> True"
1.137 +lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
1.138    by (blast elim: less_asym)
1.139
1.140
1.141  text {* Transitivity rules for calculational reasoning *}
1.142
1.143 -lemma less_asym': "\<lbrakk> a \<sqsubset> b; b \<sqsubset> a \<rbrakk> \<Longrightarrow> P"
1.144 +lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
1.145    by (rule less_asym)
1.146
1.147  end
1.148 @@ -207,88 +202,88 @@
1.149    assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
1.150  begin
1.151
1.152 -lemma less_linear: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
1.153 +lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
1.154    unfolding less_le using less_le linear by blast
1.155
1.156 -lemma le_less_linear: "x \<sqsubseteq> y \<or> y \<sqsubset> x"
1.157 +lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
1.158    by (simp add: le_less less_linear)
1.159
1.160  lemma le_cases [case_names le ge]:
1.161 -  "\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.162 +  "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
1.163    using linear by blast
1.164
1.165  lemma linorder_cases [case_names less equal greater]:
1.166 -    "\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.167 +    "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
1.168    using less_linear by blast
1.169
1.170 -lemma not_less: "\<not> x \<sqsubset> y \<longleftrightarrow> y \<sqsubseteq> x"
1.171 +lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
1.173    using linear apply (blast intro: antisym)
1.174    done
1.175
1.176 -lemma not_le: "\<not> x \<sqsubseteq> y \<longleftrightarrow> y \<sqsubset> x"
1.177 +lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
1.179    using linear apply (blast intro: antisym)
1.180    done
1.181
1.182 -lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<sqsubset> y \<or> y \<sqsubset> x"
1.183 +lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
1.184    by (cut_tac x = x and y = y in less_linear, auto)
1.185
1.186 -lemma neqE: "\<lbrakk> x \<noteq> y; x \<sqsubset> y \<Longrightarrow> R; y \<sqsubset> x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
1.187 +lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
1.188    by (simp add: neq_iff) blast
1.189
1.190 -lemma antisym_conv1: "\<not> x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y"
1.191 +lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
1.192    by (blast intro: antisym dest: not_less [THEN iffD1])
1.193
1.194 -lemma antisym_conv2: "x \<sqsubseteq> y \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y"
1.195 +lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
1.196    by (blast intro: antisym dest: not_less [THEN iffD1])
1.197
1.198 -lemma antisym_conv3: "\<not> y \<sqsubset> x \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y"
1.199 +lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
1.200    by (blast intro: antisym dest: not_less [THEN iffD1])
1.201
1.202  text{*Replacing the old Nat.leI*}
1.203 -lemma leI: "\<not> x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> x"
1.204 +lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
1.205    unfolding not_less .
1.206
1.207 -lemma leD: "y \<sqsubseteq> x \<Longrightarrow> \<not> x \<sqsubset> y"
1.208 +lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
1.209    unfolding not_less .
1.210
1.211  (*FIXME inappropriate name (or delete altogether)*)
1.212 -lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
1.213 +lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
1.214    unfolding not_le .
1.215
1.216  text {* min/max properties *}
1.217
1.218  lemma min_le_iff_disj:
1.219 -  "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
1.220 +  "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
1.221    unfolding min_def using linear by (auto intro: order_trans)
1.222
1.223  lemma le_max_iff_disj:
1.224 -  "z \<sqsubseteq> max x y \<longleftrightarrow> z \<sqsubseteq> x \<or> z \<sqsubseteq> y"
1.225 +  "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
1.226    unfolding max_def using linear by (auto intro: order_trans)
1.227
1.228  lemma min_less_iff_disj:
1.229 -  "min x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<or> y \<sqsubset> z"
1.230 +  "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
1.231    unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.232
1.233  lemma less_max_iff_disj:
1.234 -  "z \<sqsubset> max x y \<longleftrightarrow> z \<sqsubset> x \<or> z \<sqsubset> y"
1.235 +  "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
1.236    unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.237
1.238  lemma min_less_iff_conj [simp]:
1.239 -  "z \<sqsubset> min x y \<longleftrightarrow> z \<sqsubset> x \<and> z \<sqsubset> y"
1.240 +  "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
1.241    unfolding min_def le_less using less_linear by (auto intro: less_trans)
1.242
1.243  lemma max_less_iff_conj [simp]:
1.244 -  "max x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<and> y \<sqsubset> z"
1.245 +  "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
1.246    unfolding max_def le_less using less_linear by (auto intro: less_trans)
1.247
1.248  lemma split_min:
1.249 -  "P (min i j) \<longleftrightarrow> (i \<sqsubseteq> j \<longrightarrow> P i) \<and> (\<not> i \<sqsubseteq> j \<longrightarrow> P j)"
1.250 +  "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
1.252
1.253  lemma split_max:
1.254 -  "P (max i j) \<longleftrightarrow> (i \<sqsubseteq> j \<longrightarrow> P j) \<and> (\<not> i \<sqsubseteq> j \<longrightarrow> P i)"
1.255 +  "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
1.257
1.258  end
1.259 @@ -297,15 +292,15 @@
1.260  subsection {* Name duplicates *}
1.261
1.262  lemmas order_less_le = less_le
1.263 -lemmas order_eq_refl = preorder_class.eq_refl
1.264 -lemmas order_less_irrefl = preorder_class.less_irrefl
1.265 -lemmas order_le_less = preorder_class.le_less
1.266 -lemmas order_le_imp_less_or_eq = preorder_class.le_imp_less_or_eq
1.267 -lemmas order_less_imp_le = preorder_class.less_imp_le
1.268 -lemmas order_less_imp_not_eq = preorder_class.less_imp_not_eq
1.269 -lemmas order_less_imp_not_eq2 = preorder_class.less_imp_not_eq2
1.270 -lemmas order_neq_le_trans = preorder_class.neq_le_trans
1.271 -lemmas order_le_neq_trans = preorder_class.le_neq_trans
1.272 +lemmas order_eq_refl = order_class.eq_refl
1.273 +lemmas order_less_irrefl = order_class.less_irrefl
1.274 +lemmas order_le_less = order_class.le_less
1.275 +lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
1.276 +lemmas order_less_imp_le = order_class.less_imp_le
1.277 +lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
1.278 +lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
1.279 +lemmas order_neq_le_trans = order_class.neq_le_trans
1.280 +lemmas order_le_neq_trans = order_class.le_neq_trans
1.281
1.282  lemmas order_antisym = antisym
1.283  lemmas order_less_not_sym = order_class.less_not_sym
1.284 @@ -371,6 +366,7 @@
1.285
1.286  in
1.287
1.288 +(* sorry - there is no preorder class
1.289  structure Quasi_Tac = Quasi_Tac_Fun (
1.290  struct
1.291    val le_trans = thm "order_trans";
1.292 @@ -384,7 +380,7 @@
1.293    val less_imp_neq = thm "less_imp_neq";
1.294    val decomp_trans = decomp_gen ["Orderings.preorder"];
1.295    val decomp_quasi = decomp_gen ["Orderings.preorder"];
1.296 -end);
1.297 +end);*)
1.298
1.299  structure Order_Tac = Order_Tac_Fun (
1.300  struct
```