dropped preorders, unified syntax
authorhaftmann
Sun May 06 21:49:27 2007 +0200 (2007-05-06)
changeset 2284183b9f2d3fb3c
parent 22840 643bb625a2c3
child 22842 6d2fd4e0f984
dropped preorders, unified syntax
src/HOL/Orderings.thy
     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.42    by (simp add: less_le)
    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.80    by (simp add: less_le)
    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.172    apply (simp add: less_le)
   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.178    apply (simp add: less_le)
   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.251    by (simp add: min_def)
   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.256    by (simp add: max_def)
   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