Moved oderings from HOL into the new Orderings.thy
authornipkow
Thu Feb 10 18:51:12 2005 +0100 (2005-02-10)
changeset 155242ef571f80a55
parent 15523 617996110388
child 15525 396268ad58b3
Moved oderings from HOL into the new Orderings.thy
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/LOrder.thy
src/HOL/Lattice_Locales.thy
src/HOL/Orderings.ML
src/HOL/Orderings.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.ML	Thu Feb 10 17:09:15 2005 +0100
     1.2 +++ b/src/HOL/HOL.ML	Thu Feb 10 18:51:12 2005 +0100
     1.3 @@ -1,58 +1,5 @@
     1.4 -
     1.5  (* legacy ML bindings *)
     1.6  
     1.7 -val Least_def = thm "Least_def";
     1.8 -val Least_equality = thm "Least_equality";
     1.9 -val mono_def = thm "mono_def";
    1.10 -val monoI = thm "monoI";
    1.11 -val monoD = thm "monoD";
    1.12 -val min_def = thm "min_def";
    1.13 -val min_of_mono = thm "min_of_mono";
    1.14 -val max_def = thm "max_def";
    1.15 -val max_of_mono = thm "max_of_mono";
    1.16 -val min_leastL = thm "min_leastL";
    1.17 -val max_leastL = thm "max_leastL";
    1.18 -val min_leastR = thm "min_leastR";
    1.19 -val max_leastR = thm "max_leastR";
    1.20 -val order_eq_refl = thm "order_eq_refl";
    1.21 -val order_less_irrefl = thm "order_less_irrefl";
    1.22 -val order_le_less = thm "order_le_less";
    1.23 -val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
    1.24 -val order_less_imp_le = thm "order_less_imp_le";
    1.25 -val order_less_not_sym = thm "order_less_not_sym";
    1.26 -val order_less_asym = thm "order_less_asym";
    1.27 -val order_less_trans = thm "order_less_trans";
    1.28 -val order_le_less_trans = thm "order_le_less_trans";
    1.29 -val order_less_le_trans = thm "order_less_le_trans";
    1.30 -val order_less_imp_not_less = thm "order_less_imp_not_less";
    1.31 -val order_less_imp_triv = thm "order_less_imp_triv";
    1.32 -val order_less_imp_not_eq = thm "order_less_imp_not_eq";
    1.33 -val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
    1.34 -val linorder_less_linear = thm "linorder_less_linear";
    1.35 -val linorder_cases = thm "linorder_cases";
    1.36 -val linorder_not_less = thm "linorder_not_less";
    1.37 -val linorder_not_le = thm "linorder_not_le";
    1.38 -val linorder_neq_iff = thm "linorder_neq_iff";
    1.39 -val linorder_neqE = thm "linorder_neqE";
    1.40 -val min_same = thm "min_same";
    1.41 -val max_same = thm "max_same";
    1.42 -val le_max_iff_disj = thm "le_max_iff_disj";
    1.43 -val le_maxI1 = thm "le_maxI1";
    1.44 -val le_maxI2 = thm "le_maxI2";
    1.45 -val less_max_iff_disj = thm "less_max_iff_disj";
    1.46 -val max_le_iff_conj = thm "max_le_iff_conj";
    1.47 -val max_less_iff_conj = thm "max_less_iff_conj";
    1.48 -val le_min_iff_conj = thm "le_min_iff_conj";
    1.49 -val min_less_iff_conj = thm "min_less_iff_conj";
    1.50 -val min_le_iff_disj = thm "min_le_iff_disj";
    1.51 -val min_less_iff_disj = thm "min_less_iff_disj";
    1.52 -val split_min = thm "split_min";
    1.53 -val split_max = thm "split_max";
    1.54 -val order_refl = thm "order_refl";
    1.55 -val order_trans = thm "order_trans";
    1.56 -val order_antisym = thm "order_antisym";
    1.57 -val order_less_le = thm "order_less_le";
    1.58 -val linorder_linear = thm "linorder_linear";
    1.59  val choice_eq = thm "choice_eq";
    1.60  
    1.61  structure HOL =
     2.1 --- a/src/HOL/HOL.thy	Thu Feb 10 17:09:15 2005 +0100
     2.2 +++ b/src/HOL/HOL.thy	Thu Feb 10 18:51:12 2005 +0100
     2.3 @@ -7,8 +7,7 @@
     2.4  
     2.5  theory HOL
     2.6  imports CPure
     2.7 -files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("antisym_setup.ML")
     2.8 -      ("eqrule_HOL_data.ML")
     2.9 +files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
    2.10        ("~~/src/Provers/eqsubst.ML")
    2.11  begin
    2.12  
    2.13 @@ -248,6 +247,14 @@
    2.14  apply assumption+
    2.15  done
    2.16  
    2.17 +text {* For calculational reasoning: *}
    2.18 +
    2.19 +lemma forw_subst: "a = b ==> P b ==> P a"
    2.20 +  by (rule ssubst)
    2.21 +
    2.22 +lemma back_subst: "P a ==> a = b ==> P b"
    2.23 +  by (rule subst)
    2.24 +
    2.25  
    2.26  subsection {*Congruence rules for application*}
    2.27  
    2.28 @@ -1224,563 +1231,5 @@
    2.29  setup InductMethod.setup
    2.30  
    2.31  
    2.32 -subsection {* Order signatures and orders *}
    2.33 -
    2.34 -axclass
    2.35 -  ord < type
    2.36 -
    2.37 -syntax
    2.38 -  "op <"        :: "['a::ord, 'a] => bool"             ("op <")
    2.39 -  "op <="       :: "['a::ord, 'a] => bool"             ("op <=")
    2.40 -
    2.41 -global
    2.42 -
    2.43 -consts
    2.44 -  "op <"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
    2.45 -  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
    2.46 -
    2.47 -local
    2.48 -
    2.49 -syntax (xsymbols)
    2.50 -  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    2.51 -  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    2.52 -
    2.53 -syntax (HTML output)
    2.54 -  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    2.55 -  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    2.56 -
    2.57 -text{* Syntactic sugar: *}
    2.58 -
    2.59 -consts
    2.60 -  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    2.61 -  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    2.62 -translations
    2.63 -  "x > y"  => "y < x"
    2.64 -  "x >= y" => "y <= x"
    2.65 -
    2.66 -syntax (xsymbols)
    2.67 -  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    2.68 -
    2.69 -syntax (HTML output)
    2.70 -  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    2.71 -
    2.72 -
    2.73 -subsubsection {* Monotonicity *}
    2.74 -
    2.75 -locale mono =
    2.76 -  fixes f
    2.77 -  assumes mono: "A <= B ==> f A <= f B"
    2.78 -
    2.79 -lemmas monoI [intro?] = mono.intro
    2.80 -  and monoD [dest?] = mono.mono
    2.81 -
    2.82 -constdefs
    2.83 -  min :: "['a::ord, 'a] => 'a"
    2.84 -  "min a b == (if a <= b then a else b)"
    2.85 -  max :: "['a::ord, 'a] => 'a"
    2.86 -  "max a b == (if a <= b then b else a)"
    2.87 -
    2.88 -lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    2.89 -  by (simp add: min_def)
    2.90 -
    2.91 -lemma min_of_mono:
    2.92 -    "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
    2.93 -  by (simp add: min_def)
    2.94 -
    2.95 -lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    2.96 -  by (simp add: max_def)
    2.97 -
    2.98 -lemma max_of_mono:
    2.99 -    "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
   2.100 -  by (simp add: max_def)
   2.101 -
   2.102 -
   2.103 -subsubsection "Orders"
   2.104 -
   2.105 -axclass order < ord
   2.106 -  order_refl [iff]: "x <= x"
   2.107 -  order_trans: "x <= y ==> y <= z ==> x <= z"
   2.108 -  order_antisym: "x <= y ==> y <= x ==> x = y"
   2.109 -  order_less_le: "(x < y) = (x <= y & x ~= y)"
   2.110 -
   2.111 -
   2.112 -text {* Reflexivity. *}
   2.113 -
   2.114 -lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y"
   2.115 -    -- {* This form is useful with the classical reasoner. *}
   2.116 -  apply (erule ssubst)
   2.117 -  apply (rule order_refl)
   2.118 -  done
   2.119 -
   2.120 -lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   2.121 -  by (simp add: order_less_le)
   2.122 -
   2.123 -lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
   2.124 -    -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   2.125 -  apply (simp add: order_less_le, blast)
   2.126 -  done
   2.127 -
   2.128 -lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
   2.129 -
   2.130 -lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"
   2.131 -  by (simp add: order_less_le)
   2.132 -
   2.133 -
   2.134 -text {* Asymmetry. *}
   2.135 -
   2.136 -lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
   2.137 -  by (simp add: order_less_le order_antisym)
   2.138 -
   2.139 -lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
   2.140 -  apply (drule order_less_not_sym)
   2.141 -  apply (erule contrapos_np, simp)
   2.142 -  done
   2.143 -
   2.144 -lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
   2.145 -by (blast intro: order_antisym)
   2.146 -
   2.147 -lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
   2.148 -by(blast intro:order_antisym)
   2.149 -
   2.150 -text {* Transitivity. *}
   2.151 -
   2.152 -lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z"
   2.153 -  apply (simp add: order_less_le)
   2.154 -  apply (blast intro: order_trans order_antisym)
   2.155 -  done
   2.156 -
   2.157 -lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z"
   2.158 -  apply (simp add: order_less_le)
   2.159 -  apply (blast intro: order_trans order_antisym)
   2.160 -  done
   2.161 -
   2.162 -lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z"
   2.163 -  apply (simp add: order_less_le)
   2.164 -  apply (blast intro: order_trans order_antisym)
   2.165 -  done
   2.166 -
   2.167 -
   2.168 -text {* Useful for simplification, but too risky to include by default. *}
   2.169 -
   2.170 -lemma order_less_imp_not_less: "(x::'a::order) < y ==>  (~ y < x) = True"
   2.171 -  by (blast elim: order_less_asym)
   2.172 -
   2.173 -lemma order_less_imp_triv: "(x::'a::order) < y ==>  (y < x --> P) = True"
   2.174 -  by (blast elim: order_less_asym)
   2.175 -
   2.176 -lemma order_less_imp_not_eq: "(x::'a::order) < y ==>  (x = y) = False"
   2.177 -  by auto
   2.178 -
   2.179 -lemma order_less_imp_not_eq2: "(x::'a::order) < y ==>  (y = x) = False"
   2.180 -  by auto
   2.181 -
   2.182 -
   2.183 -text {* Other operators. *}
   2.184 -
   2.185 -lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least"
   2.186 -  apply (simp add: min_def)
   2.187 -  apply (blast intro: order_antisym)
   2.188 -  done
   2.189 -
   2.190 -lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x"
   2.191 -  apply (simp add: max_def)
   2.192 -  apply (blast intro: order_antisym)
   2.193 -  done
   2.194 -
   2.195 -
   2.196 -subsubsection {* Least value operator *}
   2.197 -
   2.198 -constdefs
   2.199 -  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   2.200 -  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   2.201 -    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
   2.202 -
   2.203 -lemma LeastI2:
   2.204 -  "[| P (x::'a::order);
   2.205 -      !!y. P y ==> x <= y;
   2.206 -      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   2.207 -   ==> Q (Least P)"
   2.208 -  apply (unfold Least_def)
   2.209 -  apply (rule theI2)
   2.210 -    apply (blast intro: order_antisym)+
   2.211 -  done
   2.212 -
   2.213 -lemma Least_equality:
   2.214 -    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   2.215 -  apply (simp add: Least_def)
   2.216 -  apply (rule the_equality)
   2.217 -  apply (auto intro!: order_antisym)
   2.218 -  done
   2.219 -
   2.220 -
   2.221 -subsubsection "Linear / total orders"
   2.222 -
   2.223 -axclass linorder < order
   2.224 -  linorder_linear: "x <= y | y <= x"
   2.225 -
   2.226 -lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   2.227 -  apply (simp add: order_less_le)
   2.228 -  apply (insert linorder_linear, blast)
   2.229 -  done
   2.230 -
   2.231 -lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
   2.232 -  by (simp add: order_le_less linorder_less_linear)
   2.233 -
   2.234 -lemma linorder_le_cases [case_names le ge]:
   2.235 -    "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
   2.236 -  by (insert linorder_linear, blast)
   2.237 -
   2.238 -lemma linorder_cases [case_names less equal greater]:
   2.239 -    "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
   2.240 -  by (insert linorder_less_linear, blast)
   2.241 -
   2.242 -lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
   2.243 -  apply (simp add: order_less_le)
   2.244 -  apply (insert linorder_linear)
   2.245 -  apply (blast intro: order_antisym)
   2.246 -  done
   2.247 -
   2.248 -lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)"
   2.249 -  apply (simp add: order_less_le)
   2.250 -  apply (insert linorder_linear)
   2.251 -  apply (blast intro: order_antisym)
   2.252 -  done
   2.253 -
   2.254 -lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
   2.255 -by (cut_tac x = x and y = y in linorder_less_linear, auto)
   2.256 -
   2.257 -lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   2.258 -by (simp add: linorder_neq_iff, blast)
   2.259 -
   2.260 -lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
   2.261 -by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   2.262 -
   2.263 -lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   2.264 -by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   2.265 -
   2.266 -lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   2.267 -by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   2.268 -
   2.269 -use "antisym_setup.ML";
   2.270 -setup antisym_setup
   2.271 -
   2.272 -subsubsection "Min and max on (linear) orders"
   2.273 -
   2.274 -lemma min_same [simp]: "min (x::'a::order) x = x"
   2.275 -  by (simp add: min_def)
   2.276 -
   2.277 -lemma max_same [simp]: "max (x::'a::order) x = x"
   2.278 -  by (simp add: max_def)
   2.279 -
   2.280 -lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   2.281 -  apply (simp add: max_def)
   2.282 -  apply (insert linorder_linear)
   2.283 -  apply (blast intro: order_trans)
   2.284 -  done
   2.285 -
   2.286 -lemma le_maxI1: "(x::'a::linorder) <= max x y"
   2.287 -  by (simp add: le_max_iff_disj)
   2.288 -
   2.289 -lemma le_maxI2: "(y::'a::linorder) <= max x y"
   2.290 -    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
   2.291 -  by (simp add: le_max_iff_disj)
   2.292 -
   2.293 -lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   2.294 -  apply (simp add: max_def order_le_less)
   2.295 -  apply (insert linorder_less_linear)
   2.296 -  apply (blast intro: order_less_trans)
   2.297 -  done
   2.298 -
   2.299 -lemma max_le_iff_conj [simp]:
   2.300 -    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
   2.301 -  apply (simp add: max_def)
   2.302 -  apply (insert linorder_linear)
   2.303 -  apply (blast intro: order_trans)
   2.304 -  done
   2.305 -
   2.306 -lemma max_less_iff_conj [simp]:
   2.307 -    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   2.308 -  apply (simp add: order_le_less max_def)
   2.309 -  apply (insert linorder_less_linear)
   2.310 -  apply (blast intro: order_less_trans)
   2.311 -  done
   2.312 -
   2.313 -lemma le_min_iff_conj [simp]:
   2.314 -    "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
   2.315 -    -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
   2.316 -  apply (simp add: min_def)
   2.317 -  apply (insert linorder_linear)
   2.318 -  apply (blast intro: order_trans)
   2.319 -  done
   2.320 -
   2.321 -lemma min_less_iff_conj [simp]:
   2.322 -    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   2.323 -  apply (simp add: order_le_less min_def)
   2.324 -  apply (insert linorder_less_linear)
   2.325 -  apply (blast intro: order_less_trans)
   2.326 -  done
   2.327 -
   2.328 -lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   2.329 -  apply (simp add: min_def)
   2.330 -  apply (insert linorder_linear)
   2.331 -  apply (blast intro: order_trans)
   2.332 -  done
   2.333 -
   2.334 -lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   2.335 -  apply (simp add: min_def order_le_less)
   2.336 -  apply (insert linorder_less_linear)
   2.337 -  apply (blast intro: order_less_trans)
   2.338 -  done
   2.339 -
   2.340 -lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
   2.341 -apply(simp add:max_def)
   2.342 -apply(rule conjI)
   2.343 -apply(blast intro:order_trans)
   2.344 -apply(simp add:linorder_not_le)
   2.345 -apply(blast dest: order_less_trans order_le_less_trans)
   2.346 -done
   2.347 -
   2.348 -lemma max_commute: "!!x::'a::linorder. max x y = max y x"
   2.349 -apply(simp add:max_def)
   2.350 -apply(simp add:linorder_not_le)
   2.351 -apply(blast dest: order_less_trans)
   2.352 -done
   2.353 -
   2.354 -lemmas max_ac = max_assoc max_commute
   2.355 -                mk_left_commute[of max,OF max_assoc max_commute]
   2.356 -
   2.357 -lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
   2.358 -apply(simp add:min_def)
   2.359 -apply(rule conjI)
   2.360 -apply(blast intro:order_trans)
   2.361 -apply(simp add:linorder_not_le)
   2.362 -apply(blast dest: order_less_trans order_le_less_trans)
   2.363 -done
   2.364 -
   2.365 -lemma min_commute: "!!x::'a::linorder. min x y = min y x"
   2.366 -apply(simp add:min_def)
   2.367 -apply(simp add:linorder_not_le)
   2.368 -apply(blast dest: order_less_trans)
   2.369 -done
   2.370 -
   2.371 -lemmas min_ac = min_assoc min_commute
   2.372 -                mk_left_commute[of min,OF min_assoc min_commute]
   2.373 -
   2.374 -lemma split_min:
   2.375 -    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   2.376 -  by (simp add: min_def)
   2.377 -
   2.378 -lemma split_max:
   2.379 -    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   2.380 -  by (simp add: max_def)
   2.381 -
   2.382 -
   2.383 -subsubsection {* Transitivity rules for calculational reasoning *}
   2.384 -
   2.385 -
   2.386 -lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
   2.387 -  by (simp add: order_less_le)
   2.388 -
   2.389 -lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   2.390 -  by (simp add: order_less_le)
   2.391 -
   2.392 -lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   2.393 -  by (rule order_less_asym)
   2.394 -
   2.395 -
   2.396 -subsubsection {* Setup of transitivity reasoner as Solver *}
   2.397 -
   2.398 -lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
   2.399 -  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
   2.400 -
   2.401 -lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   2.402 -  by (erule subst, erule ssubst, assumption)
   2.403 -
   2.404 -ML_setup {*
   2.405 -
   2.406 -(* The setting up of Quasi_Tac serves as a demo.  Since there is no
   2.407 -   class for quasi orders, the tactics Quasi_Tac.trans_tac and
   2.408 -   Quasi_Tac.quasi_tac are not of much use. *)
   2.409 -
   2.410 -fun decomp_gen sort sign (Trueprop $ t) =
   2.411 -  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
   2.412 -  fun dec (Const ("Not", _) $ t) = (
   2.413 -	  case dec t of
   2.414 -	    None => None
   2.415 -	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   2.416 -	| dec (Const ("op =",  _) $ t1 $ t2) =
   2.417 -	    if of_sort t1
   2.418 -	    then Some (t1, "=", t2)
   2.419 -	    else None
   2.420 -	| dec (Const ("op <=",  _) $ t1 $ t2) =
   2.421 -	    if of_sort t1
   2.422 -	    then Some (t1, "<=", t2)
   2.423 -	    else None
   2.424 -	| dec (Const ("op <",  _) $ t1 $ t2) =
   2.425 -	    if of_sort t1
   2.426 -	    then Some (t1, "<", t2)
   2.427 -	    else None
   2.428 -	| dec _ = None
   2.429 -  in dec t end;
   2.430 -
   2.431 -structure Quasi_Tac = Quasi_Tac_Fun (
   2.432 -  struct
   2.433 -    val le_trans = thm "order_trans";
   2.434 -    val le_refl = thm "order_refl";
   2.435 -    val eqD1 = thm "order_eq_refl";
   2.436 -    val eqD2 = thm "sym" RS thm "order_eq_refl";
   2.437 -    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   2.438 -    val less_imp_le = thm "order_less_imp_le";
   2.439 -    val le_neq_trans = thm "order_le_neq_trans";
   2.440 -    val neq_le_trans = thm "order_neq_le_trans";
   2.441 -    val less_imp_neq = thm "less_imp_neq";
   2.442 -    val decomp_trans = decomp_gen ["HOL.order"];
   2.443 -    val decomp_quasi = decomp_gen ["HOL.order"];
   2.444 -
   2.445 -  end);  (* struct *)
   2.446 -
   2.447 -structure Order_Tac = Order_Tac_Fun (
   2.448 -  struct
   2.449 -    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   2.450 -    val le_refl = thm "order_refl";
   2.451 -    val less_imp_le = thm "order_less_imp_le";
   2.452 -    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   2.453 -    val not_leI = thm "linorder_not_le" RS thm "iffD2";
   2.454 -    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   2.455 -    val not_leD = thm "linorder_not_le" RS thm "iffD1";
   2.456 -    val eqI = thm "order_antisym";
   2.457 -    val eqD1 = thm "order_eq_refl";
   2.458 -    val eqD2 = thm "sym" RS thm "order_eq_refl";
   2.459 -    val less_trans = thm "order_less_trans";
   2.460 -    val less_le_trans = thm "order_less_le_trans";
   2.461 -    val le_less_trans = thm "order_le_less_trans";
   2.462 -    val le_trans = thm "order_trans";
   2.463 -    val le_neq_trans = thm "order_le_neq_trans";
   2.464 -    val neq_le_trans = thm "order_neq_le_trans";
   2.465 -    val less_imp_neq = thm "less_imp_neq";
   2.466 -    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
   2.467 -    val decomp_part = decomp_gen ["HOL.order"];
   2.468 -    val decomp_lin = decomp_gen ["HOL.linorder"];
   2.469 -
   2.470 -  end);  (* struct *)
   2.471 -
   2.472 -simpset_ref() := simpset ()
   2.473 -    addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
   2.474 -    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
   2.475 -  (* Adding the transitivity reasoners also as safe solvers showed a slight
   2.476 -     speed up, but the reasoning strength appears to be not higher (at least
   2.477 -     no breaking of additional proofs in the entire HOL distribution, as
   2.478 -     of 5 March 2004, was observed). *)
   2.479 -*}
   2.480 -
   2.481 -(* Optional setup of methods *)
   2.482 -
   2.483 -(*
   2.484 -method_setup trans_partial =
   2.485 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
   2.486 -  {* transitivity reasoner for partial orders *}	
   2.487 -method_setup trans_linear =
   2.488 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   2.489 -  {* transitivity reasoner for linear orders *}
   2.490 -*)
   2.491 -
   2.492 -(*
   2.493 -declare order.order_refl [simp del] order_less_irrefl [simp del]
   2.494 -
   2.495 -can currently not be removed, abel_cancel relies on it.
   2.496 -*)
   2.497 -
   2.498 -subsubsection "Bounded quantifiers"
   2.499 -
   2.500 -syntax
   2.501 -  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   2.502 -  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
   2.503 -  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   2.504 -  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
   2.505 -
   2.506 -  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   2.507 -  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
   2.508 -  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   2.509 -  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
   2.510 -
   2.511 -syntax (xsymbols)
   2.512 -  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   2.513 -  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   2.514 -  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   2.515 -  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   2.516 -
   2.517 -  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   2.518 -  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   2.519 -  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   2.520 -  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   2.521 -
   2.522 -syntax (HOL)
   2.523 -  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   2.524 -  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   2.525 -  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   2.526 -  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   2.527 -
   2.528 -syntax (HTML output)
   2.529 -  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   2.530 -  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   2.531 -  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   2.532 -  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   2.533 -
   2.534 -  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   2.535 -  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   2.536 -  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   2.537 -  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   2.538 -
   2.539 -translations
   2.540 - "ALL x<y. P"   =>  "ALL x. x < y --> P"
   2.541 - "EX x<y. P"    =>  "EX x. x < y  & P"
   2.542 - "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
   2.543 - "EX x<=y. P"   =>  "EX x. x <= y & P"
   2.544 - "ALL x>y. P"   =>  "ALL x. x > y --> P"
   2.545 - "EX x>y. P"    =>  "EX x. x > y  & P"
   2.546 - "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
   2.547 - "EX x>=y. P"   =>  "EX x. x >= y & P"
   2.548 -
   2.549 -print_translation {*
   2.550 -let
   2.551 -  fun mk v v' q n P =
   2.552 -    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
   2.553 -    then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   2.554 -  fun all_tr' [Const ("_bound",_) $ Free (v,_),
   2.555 -               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   2.556 -    mk v v' "_lessAll" n P
   2.557 -
   2.558 -  | all_tr' [Const ("_bound",_) $ Free (v,_),
   2.559 -               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   2.560 -    mk v v' "_leAll" n P
   2.561 -
   2.562 -  | all_tr' [Const ("_bound",_) $ Free (v,_),
   2.563 -               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   2.564 -    mk v v' "_gtAll" n P
   2.565 -
   2.566 -  | all_tr' [Const ("_bound",_) $ Free (v,_),
   2.567 -               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   2.568 -    mk v v' "_geAll" n P;
   2.569 -
   2.570 -  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
   2.571 -               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   2.572 -    mk v v' "_lessEx" n P
   2.573 -
   2.574 -  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   2.575 -               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   2.576 -    mk v v' "_leEx" n P
   2.577 -
   2.578 -  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   2.579 -               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   2.580 -    mk v v' "_gtEx" n P
   2.581 -
   2.582 -  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   2.583 -               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   2.584 -    mk v v' "_geEx" n P
   2.585 -in
   2.586 -[("ALL ", all_tr'), ("EX ", ex_tr')]
   2.587 -end
   2.588 -*}
   2.589 -
   2.590  end
   2.591  
     3.1 --- a/src/HOL/LOrder.thy	Thu Feb 10 17:09:15 2005 +0100
     3.2 +++ b/src/HOL/LOrder.thy	Thu Feb 10 18:51:12 2005 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Lattice Orders *}
     3.5  
     3.6  theory LOrder
     3.7 -imports HOL
     3.8 +imports Orderings
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Lattice_Locales.thy	Thu Feb 10 17:09:15 2005 +0100
     4.2 +++ b/src/HOL/Lattice_Locales.thy	Thu Feb 10 18:51:12 2005 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Lattices via Locales *}
     4.5  
     4.6  theory Lattice_Locales
     4.7 -imports Set
     4.8 +imports HOL
     4.9  begin
    4.10  
    4.11  subsection{* Lattices *}
    4.12 @@ -64,6 +64,16 @@
    4.13  lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
    4.14  by(blast intro: antisym sup_ge2 sup_greatest refl)
    4.15  
    4.16 +
    4.17 +lemma (in lower_semilattice) below_inf_conv[simp]:
    4.18 + "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    4.19 +by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
    4.20 +
    4.21 +lemma (in upper_semilattice) above_sup_conv[simp]:
    4.22 + "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    4.23 +by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
    4.24 +
    4.25 +
    4.26  text{* Towards distributivity: if you have one of them, you have them all. *}
    4.27  
    4.28  lemma (in lattice) distrib_imp1:
    4.29 @@ -97,7 +107,7 @@
    4.30    have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
    4.31    also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
    4.32    also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
    4.33 -  finally show ?thesis .
    4.34 +  finally(back_subst) show ?thesis .
    4.35  qed
    4.36  
    4.37  lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    4.38 @@ -105,7 +115,7 @@
    4.39    have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
    4.40    also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
    4.41    also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
    4.42 -  finally show ?thesis .
    4.43 +  finally(back_subst) show ?thesis .
    4.44  qed
    4.45  
    4.46  lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Orderings.ML	Thu Feb 10 18:51:12 2005 +0100
     5.3 @@ -0,0 +1,54 @@
     5.4 +(* legacy ML bindings *)
     5.5 +
     5.6 +val Least_def = thm "Least_def";
     5.7 +val Least_equality = thm "Least_equality";
     5.8 +val mono_def = thm "mono_def";
     5.9 +val monoI = thm "monoI";
    5.10 +val monoD = thm "monoD";
    5.11 +val min_def = thm "min_def";
    5.12 +val min_of_mono = thm "min_of_mono";
    5.13 +val max_def = thm "max_def";
    5.14 +val max_of_mono = thm "max_of_mono";
    5.15 +val min_leastL = thm "min_leastL";
    5.16 +val max_leastL = thm "max_leastL";
    5.17 +val min_leastR = thm "min_leastR";
    5.18 +val max_leastR = thm "max_leastR";
    5.19 +val order_eq_refl = thm "order_eq_refl";
    5.20 +val order_less_irrefl = thm "order_less_irrefl";
    5.21 +val order_le_less = thm "order_le_less";
    5.22 +val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
    5.23 +val order_less_imp_le = thm "order_less_imp_le";
    5.24 +val order_less_not_sym = thm "order_less_not_sym";
    5.25 +val order_less_asym = thm "order_less_asym";
    5.26 +val order_less_trans = thm "order_less_trans";
    5.27 +val order_le_less_trans = thm "order_le_less_trans";
    5.28 +val order_less_le_trans = thm "order_less_le_trans";
    5.29 +val order_less_imp_not_less = thm "order_less_imp_not_less";
    5.30 +val order_less_imp_triv = thm "order_less_imp_triv";
    5.31 +val order_less_imp_not_eq = thm "order_less_imp_not_eq";
    5.32 +val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
    5.33 +val linorder_less_linear = thm "linorder_less_linear";
    5.34 +val linorder_cases = thm "linorder_cases";
    5.35 +val linorder_not_less = thm "linorder_not_less";
    5.36 +val linorder_not_le = thm "linorder_not_le";
    5.37 +val linorder_neq_iff = thm "linorder_neq_iff";
    5.38 +val linorder_neqE = thm "linorder_neqE";
    5.39 +val min_same = thm "min_same";
    5.40 +val max_same = thm "max_same";
    5.41 +val le_max_iff_disj = thm "le_max_iff_disj";
    5.42 +val le_maxI1 = thm "le_maxI1";
    5.43 +val le_maxI2 = thm "le_maxI2";
    5.44 +val less_max_iff_disj = thm "less_max_iff_disj";
    5.45 +val max_le_iff_conj = thm "max_le_iff_conj";
    5.46 +val max_less_iff_conj = thm "max_less_iff_conj";
    5.47 +val le_min_iff_conj = thm "le_min_iff_conj";
    5.48 +val min_less_iff_conj = thm "min_less_iff_conj";
    5.49 +val min_le_iff_disj = thm "min_le_iff_disj";
    5.50 +val min_less_iff_disj = thm "min_less_iff_disj";
    5.51 +val split_min = thm "split_min";
    5.52 +val split_max = thm "split_max";
    5.53 +val order_refl = thm "order_refl";
    5.54 +val order_trans = thm "order_trans";
    5.55 +val order_antisym = thm "order_antisym";
    5.56 +val order_less_le = thm "order_less_le";
    5.57 +val linorder_linear = thm "linorder_linear";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Orderings.thy	Thu Feb 10 18:51:12 2005 +0100
     6.3 @@ -0,0 +1,612 @@
     6.4 +(*  Title:      HOL/Orderings.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     6.7 +
     6.8 +FIXME: derive more of the min/max laws generically via semilattices
     6.9 +*)
    6.10 +
    6.11 +header {* Type classes for $\le$ *}
    6.12 +
    6.13 +theory Orderings
    6.14 +imports Lattice_Locales
    6.15 +files ("antisym_setup.ML")
    6.16 +begin
    6.17 +
    6.18 +subsection {* Order signatures and orders *}
    6.19 +
    6.20 +axclass
    6.21 +  ord < type
    6.22 +
    6.23 +syntax
    6.24 +  "op <"        :: "['a::ord, 'a] => bool"             ("op <")
    6.25 +  "op <="       :: "['a::ord, 'a] => bool"             ("op <=")
    6.26 +
    6.27 +global
    6.28 +
    6.29 +consts
    6.30 +  "op <"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
    6.31 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
    6.32 +
    6.33 +local
    6.34 +
    6.35 +syntax (xsymbols)
    6.36 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    6.37 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    6.38 +
    6.39 +syntax (HTML output)
    6.40 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    6.41 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    6.42 +
    6.43 +text{* Syntactic sugar: *}
    6.44 +
    6.45 +consts
    6.46 +  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    6.47 +  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    6.48 +translations
    6.49 +  "x > y"  => "y < x"
    6.50 +  "x >= y" => "y <= x"
    6.51 +
    6.52 +syntax (xsymbols)
    6.53 +  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    6.54 +
    6.55 +syntax (HTML output)
    6.56 +  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    6.57 +
    6.58 +
    6.59 +subsection {* Monotonicity *}
    6.60 +
    6.61 +locale mono =
    6.62 +  fixes f
    6.63 +  assumes mono: "A <= B ==> f A <= f B"
    6.64 +
    6.65 +lemmas monoI [intro?] = mono.intro
    6.66 +  and monoD [dest?] = mono.mono
    6.67 +
    6.68 +constdefs
    6.69 +  min :: "['a::ord, 'a] => 'a"
    6.70 +  "min a b == (if a <= b then a else b)"
    6.71 +  max :: "['a::ord, 'a] => 'a"
    6.72 +  "max a b == (if a <= b then b else a)"
    6.73 +
    6.74 +lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    6.75 +  by (simp add: min_def)
    6.76 +
    6.77 +lemma min_of_mono:
    6.78 +    "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
    6.79 +  by (simp add: min_def)
    6.80 +
    6.81 +lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    6.82 +  by (simp add: max_def)
    6.83 +
    6.84 +lemma max_of_mono:
    6.85 +    "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
    6.86 +  by (simp add: max_def)
    6.87 +
    6.88 +
    6.89 +subsection "Orders"
    6.90 +
    6.91 +axclass order < ord
    6.92 +  order_refl [iff]: "x <= x"
    6.93 +  order_trans: "x <= y ==> y <= z ==> x <= z"
    6.94 +  order_antisym: "x <= y ==> y <= x ==> x = y"
    6.95 +  order_less_le: "(x < y) = (x <= y & x ~= y)"
    6.96 +
    6.97 +text{* Connection to locale: *}
    6.98 +
    6.99 +lemma partial_order_order:
   6.100 + "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
   6.101 +apply(rule partial_order.intro)
   6.102 +apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
   6.103 +done
   6.104 +
   6.105 +text {* Reflexivity. *}
   6.106 +
   6.107 +lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y"
   6.108 +    -- {* This form is useful with the classical reasoner. *}
   6.109 +  apply (erule ssubst)
   6.110 +  apply (rule order_refl)
   6.111 +  done
   6.112 +
   6.113 +lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   6.114 +  by (simp add: order_less_le)
   6.115 +
   6.116 +lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
   6.117 +    -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   6.118 +  apply (simp add: order_less_le, blast)
   6.119 +  done
   6.120 +
   6.121 +lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
   6.122 +
   6.123 +lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"
   6.124 +  by (simp add: order_less_le)
   6.125 +
   6.126 +
   6.127 +text {* Asymmetry. *}
   6.128 +
   6.129 +lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
   6.130 +  by (simp add: order_less_le order_antisym)
   6.131 +
   6.132 +lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
   6.133 +  apply (drule order_less_not_sym)
   6.134 +  apply (erule contrapos_np, simp)
   6.135 +  done
   6.136 +
   6.137 +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
   6.138 +by (blast intro: order_antisym)
   6.139 +
   6.140 +lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
   6.141 +by(blast intro:order_antisym)
   6.142 +
   6.143 +text {* Transitivity. *}
   6.144 +
   6.145 +lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z"
   6.146 +  apply (simp add: order_less_le)
   6.147 +  apply (blast intro: order_trans order_antisym)
   6.148 +  done
   6.149 +
   6.150 +lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z"
   6.151 +  apply (simp add: order_less_le)
   6.152 +  apply (blast intro: order_trans order_antisym)
   6.153 +  done
   6.154 +
   6.155 +lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z"
   6.156 +  apply (simp add: order_less_le)
   6.157 +  apply (blast intro: order_trans order_antisym)
   6.158 +  done
   6.159 +
   6.160 +
   6.161 +text {* Useful for simplification, but too risky to include by default. *}
   6.162 +
   6.163 +lemma order_less_imp_not_less: "(x::'a::order) < y ==>  (~ y < x) = True"
   6.164 +  by (blast elim: order_less_asym)
   6.165 +
   6.166 +lemma order_less_imp_triv: "(x::'a::order) < y ==>  (y < x --> P) = True"
   6.167 +  by (blast elim: order_less_asym)
   6.168 +
   6.169 +lemma order_less_imp_not_eq: "(x::'a::order) < y ==>  (x = y) = False"
   6.170 +  by auto
   6.171 +
   6.172 +lemma order_less_imp_not_eq2: "(x::'a::order) < y ==>  (y = x) = False"
   6.173 +  by auto
   6.174 +
   6.175 +
   6.176 +text {* Other operators. *}
   6.177 +
   6.178 +lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least"
   6.179 +  apply (simp add: min_def)
   6.180 +  apply (blast intro: order_antisym)
   6.181 +  done
   6.182 +
   6.183 +lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x"
   6.184 +  apply (simp add: max_def)
   6.185 +  apply (blast intro: order_antisym)
   6.186 +  done
   6.187 +
   6.188 +
   6.189 +subsection {* Transitivity rules for calculational reasoning *}
   6.190 +
   6.191 +
   6.192 +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
   6.193 +  by (simp add: order_less_le)
   6.194 +
   6.195 +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   6.196 +  by (simp add: order_less_le)
   6.197 +
   6.198 +lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   6.199 +  by (rule order_less_asym)
   6.200 +
   6.201 +
   6.202 +subsection {* Least value operator *}
   6.203 +
   6.204 +constdefs
   6.205 +  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   6.206 +  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   6.207 +    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
   6.208 +
   6.209 +lemma LeastI2:
   6.210 +  "[| P (x::'a::order);
   6.211 +      !!y. P y ==> x <= y;
   6.212 +      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   6.213 +   ==> Q (Least P)"
   6.214 +  apply (unfold Least_def)
   6.215 +  apply (rule theI2)
   6.216 +    apply (blast intro: order_antisym)+
   6.217 +  done
   6.218 +
   6.219 +lemma Least_equality:
   6.220 +    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   6.221 +  apply (simp add: Least_def)
   6.222 +  apply (rule the_equality)
   6.223 +  apply (auto intro!: order_antisym)
   6.224 +  done
   6.225 +
   6.226 +
   6.227 +subsection "Linear / total orders"
   6.228 +
   6.229 +axclass linorder < order
   6.230 +  linorder_linear: "x <= y | y <= x"
   6.231 +
   6.232 +lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   6.233 +  apply (simp add: order_less_le)
   6.234 +  apply (insert linorder_linear, blast)
   6.235 +  done
   6.236 +
   6.237 +lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
   6.238 +  by (simp add: order_le_less linorder_less_linear)
   6.239 +
   6.240 +lemma linorder_le_cases [case_names le ge]:
   6.241 +    "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
   6.242 +  by (insert linorder_linear, blast)
   6.243 +
   6.244 +lemma linorder_cases [case_names less equal greater]:
   6.245 +    "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
   6.246 +  by (insert linorder_less_linear, blast)
   6.247 +
   6.248 +lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
   6.249 +  apply (simp add: order_less_le)
   6.250 +  apply (insert linorder_linear)
   6.251 +  apply (blast intro: order_antisym)
   6.252 +  done
   6.253 +
   6.254 +lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)"
   6.255 +  apply (simp add: order_less_le)
   6.256 +  apply (insert linorder_linear)
   6.257 +  apply (blast intro: order_antisym)
   6.258 +  done
   6.259 +
   6.260 +lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
   6.261 +by (cut_tac x = x and y = y in linorder_less_linear, auto)
   6.262 +
   6.263 +lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   6.264 +by (simp add: linorder_neq_iff, blast)
   6.265 +
   6.266 +lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
   6.267 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   6.268 +
   6.269 +lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   6.270 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   6.271 +
   6.272 +lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   6.273 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   6.274 +
   6.275 +use "antisym_setup.ML";
   6.276 +setup antisym_setup
   6.277 +
   6.278 +subsection {* Setup of transitivity reasoner as Solver *}
   6.279 +
   6.280 +lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
   6.281 +  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
   6.282 +
   6.283 +lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   6.284 +  by (erule subst, erule ssubst, assumption)
   6.285 +
   6.286 +ML_setup {*
   6.287 +
   6.288 +(* The setting up of Quasi_Tac serves as a demo.  Since there is no
   6.289 +   class for quasi orders, the tactics Quasi_Tac.trans_tac and
   6.290 +   Quasi_Tac.quasi_tac are not of much use. *)
   6.291 +
   6.292 +fun decomp_gen sort sign (Trueprop $ t) =
   6.293 +  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
   6.294 +  fun dec (Const ("Not", _) $ t) = (
   6.295 +	  case dec t of
   6.296 +	    None => None
   6.297 +	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   6.298 +	| dec (Const ("op =",  _) $ t1 $ t2) =
   6.299 +	    if of_sort t1
   6.300 +	    then Some (t1, "=", t2)
   6.301 +	    else None
   6.302 +	| dec (Const ("op <=",  _) $ t1 $ t2) =
   6.303 +	    if of_sort t1
   6.304 +	    then Some (t1, "<=", t2)
   6.305 +	    else None
   6.306 +	| dec (Const ("op <",  _) $ t1 $ t2) =
   6.307 +	    if of_sort t1
   6.308 +	    then Some (t1, "<", t2)
   6.309 +	    else None
   6.310 +	| dec _ = None
   6.311 +  in dec t end;
   6.312 +
   6.313 +structure Quasi_Tac = Quasi_Tac_Fun (
   6.314 +  struct
   6.315 +    val le_trans = thm "order_trans";
   6.316 +    val le_refl = thm "order_refl";
   6.317 +    val eqD1 = thm "order_eq_refl";
   6.318 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
   6.319 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   6.320 +    val less_imp_le = thm "order_less_imp_le";
   6.321 +    val le_neq_trans = thm "order_le_neq_trans";
   6.322 +    val neq_le_trans = thm "order_neq_le_trans";
   6.323 +    val less_imp_neq = thm "less_imp_neq";
   6.324 +    val decomp_trans = decomp_gen ["Orderings.order"];
   6.325 +    val decomp_quasi = decomp_gen ["Orderings.order"];
   6.326 +
   6.327 +  end);  (* struct *)
   6.328 +
   6.329 +structure Order_Tac = Order_Tac_Fun (
   6.330 +  struct
   6.331 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   6.332 +    val le_refl = thm "order_refl";
   6.333 +    val less_imp_le = thm "order_less_imp_le";
   6.334 +    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   6.335 +    val not_leI = thm "linorder_not_le" RS thm "iffD2";
   6.336 +    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   6.337 +    val not_leD = thm "linorder_not_le" RS thm "iffD1";
   6.338 +    val eqI = thm "order_antisym";
   6.339 +    val eqD1 = thm "order_eq_refl";
   6.340 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
   6.341 +    val less_trans = thm "order_less_trans";
   6.342 +    val less_le_trans = thm "order_less_le_trans";
   6.343 +    val le_less_trans = thm "order_le_less_trans";
   6.344 +    val le_trans = thm "order_trans";
   6.345 +    val le_neq_trans = thm "order_le_neq_trans";
   6.346 +    val neq_le_trans = thm "order_neq_le_trans";
   6.347 +    val less_imp_neq = thm "less_imp_neq";
   6.348 +    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
   6.349 +    val decomp_part = decomp_gen ["Orderings.order"];
   6.350 +    val decomp_lin = decomp_gen ["Orderings.linorder"];
   6.351 +
   6.352 +  end);  (* struct *)
   6.353 +
   6.354 +simpset_ref() := simpset ()
   6.355 +    addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
   6.356 +    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
   6.357 +  (* Adding the transitivity reasoners also as safe solvers showed a slight
   6.358 +     speed up, but the reasoning strength appears to be not higher (at least
   6.359 +     no breaking of additional proofs in the entire HOL distribution, as
   6.360 +     of 5 March 2004, was observed). *)
   6.361 +*}
   6.362 +
   6.363 +(* Optional setup of methods *)
   6.364 +
   6.365 +(*
   6.366 +method_setup trans_partial =
   6.367 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
   6.368 +  {* transitivity reasoner for partial orders *}	
   6.369 +method_setup trans_linear =
   6.370 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   6.371 +  {* transitivity reasoner for linear orders *}
   6.372 +*)
   6.373 +
   6.374 +(*
   6.375 +declare order.order_refl [simp del] order_less_irrefl [simp del]
   6.376 +
   6.377 +can currently not be removed, abel_cancel relies on it.
   6.378 +*)
   6.379 +
   6.380 +
   6.381 +subsection "Min and max on (linear) orders"
   6.382 +
   6.383 +lemma min_same [simp]: "min (x::'a::order) x = x"
   6.384 +  by (simp add: min_def)
   6.385 +
   6.386 +lemma max_same [simp]: "max (x::'a::order) x = x"
   6.387 +  by (simp add: max_def)
   6.388 +
   6.389 +text{* Instantiate locales: *}
   6.390 +
   6.391 +lemma lower_semilattice_lin_min:
   6.392 +  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
   6.393 +apply(rule lower_semilattice.intro)
   6.394 +apply(rule partial_order_order)
   6.395 +apply(rule lower_semilattice_axioms.intro)
   6.396 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   6.397 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   6.398 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   6.399 +done
   6.400 +
   6.401 +lemma upper_semilattice_lin_max:
   6.402 +  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
   6.403 +apply(rule upper_semilattice.intro)
   6.404 +apply(rule partial_order_order)
   6.405 +apply(rule upper_semilattice_axioms.intro)
   6.406 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   6.407 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   6.408 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   6.409 +done
   6.410 +
   6.411 +lemma lattice_min_max: "lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
   6.412 +apply(rule lattice.intro)
   6.413 +apply(rule partial_order_order)
   6.414 +apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
   6.415 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
   6.416 +done
   6.417 +
   6.418 +lemma distrib_lattice_min_max:
   6.419 + "distrib_lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
   6.420 +apply(rule distrib_lattice.intro)
   6.421 +apply(rule partial_order_order)
   6.422 +apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
   6.423 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
   6.424 +apply(rule distrib_lattice_axioms.intro)
   6.425 +apply(rule_tac x=x and y=y in linorder_le_cases)
   6.426 +apply(rule_tac x=x and y=z in linorder_le_cases)
   6.427 +apply(rule_tac x=y and y=z in linorder_le_cases)
   6.428 +apply(simp add:min_def max_def)
   6.429 +apply(simp add:min_def max_def)
   6.430 +apply(rule_tac x=y and y=z in linorder_le_cases)
   6.431 +apply(simp add:min_def max_def)
   6.432 +apply(simp add:min_def max_def)
   6.433 +apply(rule_tac x=x and y=z in linorder_le_cases)
   6.434 +apply(rule_tac x=y and y=z in linorder_le_cases)
   6.435 +apply(simp add:min_def max_def)
   6.436 +apply(simp add:min_def max_def)
   6.437 +apply(rule_tac x=y and y=z in linorder_le_cases)
   6.438 +apply(simp add:min_def max_def)
   6.439 +apply(simp add:min_def max_def)
   6.440 +done
   6.441 +
   6.442 +lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   6.443 +  apply(simp add:max_def)
   6.444 +  apply (insert linorder_linear)
   6.445 +  apply (blast intro: order_trans)
   6.446 +  done
   6.447 +
   6.448 +lemma le_maxI1: "(x::'a::linorder) <= max x y"
   6.449 +by(rule upper_semilattice.sup_ge1[OF upper_semilattice_lin_max])
   6.450 +
   6.451 +lemma le_maxI2: "(y::'a::linorder) <= max x y"
   6.452 +    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
   6.453 +by(rule upper_semilattice.sup_ge2[OF upper_semilattice_lin_max])
   6.454 +
   6.455 +lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   6.456 +  apply (simp add: max_def order_le_less)
   6.457 +  apply (insert linorder_less_linear)
   6.458 +  apply (blast intro: order_less_trans)
   6.459 +  done
   6.460 +
   6.461 +lemma max_le_iff_conj [simp]:
   6.462 +    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
   6.463 +by (rule upper_semilattice.above_sup_conv[OF upper_semilattice_lin_max])
   6.464 +
   6.465 +lemma max_less_iff_conj [simp]:
   6.466 +    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   6.467 +  apply (simp add: order_le_less max_def)
   6.468 +  apply (insert linorder_less_linear)
   6.469 +  apply (blast intro: order_less_trans)
   6.470 +  done
   6.471 +
   6.472 +lemma le_min_iff_conj [simp]:
   6.473 +    "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
   6.474 +    -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
   6.475 +by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
   6.476 +
   6.477 +lemma min_less_iff_conj [simp]:
   6.478 +    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   6.479 +  apply (simp add: order_le_less min_def)
   6.480 +  apply (insert linorder_less_linear)
   6.481 +  apply (blast intro: order_less_trans)
   6.482 +  done
   6.483 +
   6.484 +lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   6.485 +  apply (simp add: min_def)
   6.486 +  apply (insert linorder_linear)
   6.487 +  apply (blast intro: order_trans)
   6.488 +  done
   6.489 +
   6.490 +lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   6.491 +  apply (simp add: min_def order_le_less)
   6.492 +  apply (insert linorder_less_linear)
   6.493 +  apply (blast intro: order_less_trans)
   6.494 +  done
   6.495 +
   6.496 +lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
   6.497 +by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
   6.498 +
   6.499 +lemma max_commute: "!!x::'a::linorder. max x y = max y x"
   6.500 +by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
   6.501 +
   6.502 +lemmas max_ac = max_assoc max_commute
   6.503 +                mk_left_commute[of max,OF max_assoc max_commute]
   6.504 +
   6.505 +lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
   6.506 +by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
   6.507 +
   6.508 +lemma min_commute: "!!x::'a::linorder. min x y = min y x"
   6.509 +by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
   6.510 +
   6.511 +lemmas min_ac = min_assoc min_commute
   6.512 +                mk_left_commute[of min,OF min_assoc min_commute]
   6.513 +
   6.514 +lemma split_min:
   6.515 +    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   6.516 +  by (simp add: min_def)
   6.517 +
   6.518 +lemma split_max:
   6.519 +    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   6.520 +  by (simp add: max_def)
   6.521 +
   6.522 +
   6.523 +subsection "Bounded quantifiers"
   6.524 +
   6.525 +syntax
   6.526 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   6.527 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
   6.528 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   6.529 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
   6.530 +
   6.531 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   6.532 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
   6.533 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   6.534 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
   6.535 +
   6.536 +syntax (xsymbols)
   6.537 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   6.538 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   6.539 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   6.540 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   6.541 +
   6.542 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   6.543 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   6.544 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   6.545 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   6.546 +
   6.547 +syntax (HOL)
   6.548 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   6.549 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   6.550 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   6.551 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   6.552 +
   6.553 +syntax (HTML output)
   6.554 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   6.555 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   6.556 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   6.557 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   6.558 +
   6.559 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   6.560 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   6.561 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   6.562 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   6.563 +
   6.564 +translations
   6.565 + "ALL x<y. P"   =>  "ALL x. x < y --> P"
   6.566 + "EX x<y. P"    =>  "EX x. x < y  & P"
   6.567 + "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
   6.568 + "EX x<=y. P"   =>  "EX x. x <= y & P"
   6.569 + "ALL x>y. P"   =>  "ALL x. x > y --> P"
   6.570 + "EX x>y. P"    =>  "EX x. x > y  & P"
   6.571 + "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
   6.572 + "EX x>=y. P"   =>  "EX x. x >= y & P"
   6.573 +
   6.574 +print_translation {*
   6.575 +let
   6.576 +  fun mk v v' q n P =
   6.577 +    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
   6.578 +    then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   6.579 +  fun all_tr' [Const ("_bound",_) $ Free (v,_),
   6.580 +               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   6.581 +    mk v v' "_lessAll" n P
   6.582 +
   6.583 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   6.584 +               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   6.585 +    mk v v' "_leAll" n P
   6.586 +
   6.587 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   6.588 +               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   6.589 +    mk v v' "_gtAll" n P
   6.590 +
   6.591 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   6.592 +               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   6.593 +    mk v v' "_geAll" n P;
   6.594 +
   6.595 +  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
   6.596 +               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   6.597 +    mk v v' "_lessEx" n P
   6.598 +
   6.599 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   6.600 +               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   6.601 +    mk v v' "_leEx" n P
   6.602 +
   6.603 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   6.604 +               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   6.605 +    mk v v' "_gtEx" n P
   6.606 +
   6.607 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   6.608 +               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   6.609 +    mk v v' "_geEx" n P
   6.610 +in
   6.611 +[("ALL ", all_tr'), ("EX ", ex_tr')]
   6.612 +end
   6.613 +*}
   6.614 +
   6.615 +end
     7.1 --- a/src/HOL/Set.thy	Thu Feb 10 17:09:15 2005 +0100
     7.2 +++ b/src/HOL/Set.thy	Thu Feb 10 18:51:12 2005 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Set theory for higher-order logic *}
     7.5  
     7.6  theory Set
     7.7 -imports HOL
     7.8 +imports Orderings
     7.9  begin
    7.10  
    7.11  text {* A set in HOL is simply a predicate. *}
    7.12 @@ -2057,12 +2057,6 @@
    7.13  
    7.14  subsection {* Transitivity rules for calculational reasoning *}
    7.15  
    7.16 -lemma forw_subst: "a = b ==> P b ==> P a"
    7.17 -  by (rule ssubst)
    7.18 -
    7.19 -lemma back_subst: "P a ==> a = b ==> P b"
    7.20 -  by (rule subst)
    7.21 -
    7.22  lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
    7.23    by (rule subsetD)
    7.24