src/HOL/Orderings.thy
changeset 15524 2ef571f80a55
child 15531 08c8dad8e399
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Orderings.thy	Thu Feb 10 18:51:12 2005 +0100
     1.3 @@ -0,0 +1,612 @@
     1.4 +(*  Title:      HOL/Orderings.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     1.7 +
     1.8 +FIXME: derive more of the min/max laws generically via semilattices
     1.9 +*)
    1.10 +
    1.11 +header {* Type classes for $\le$ *}
    1.12 +
    1.13 +theory Orderings
    1.14 +imports Lattice_Locales
    1.15 +files ("antisym_setup.ML")
    1.16 +begin
    1.17 +
    1.18 +subsection {* Order signatures and orders *}
    1.19 +
    1.20 +axclass
    1.21 +  ord < type
    1.22 +
    1.23 +syntax
    1.24 +  "op <"        :: "['a::ord, 'a] => bool"             ("op <")
    1.25 +  "op <="       :: "['a::ord, 'a] => bool"             ("op <=")
    1.26 +
    1.27 +global
    1.28 +
    1.29 +consts
    1.30 +  "op <"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
    1.31 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
    1.32 +
    1.33 +local
    1.34 +
    1.35 +syntax (xsymbols)
    1.36 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.37 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.38 +
    1.39 +syntax (HTML output)
    1.40 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    1.41 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    1.42 +
    1.43 +text{* Syntactic sugar: *}
    1.44 +
    1.45 +consts
    1.46 +  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    1.47 +  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    1.48 +translations
    1.49 +  "x > y"  => "y < x"
    1.50 +  "x >= y" => "y <= x"
    1.51 +
    1.52 +syntax (xsymbols)
    1.53 +  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    1.54 +
    1.55 +syntax (HTML output)
    1.56 +  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    1.57 +
    1.58 +
    1.59 +subsection {* Monotonicity *}
    1.60 +
    1.61 +locale mono =
    1.62 +  fixes f
    1.63 +  assumes mono: "A <= B ==> f A <= f B"
    1.64 +
    1.65 +lemmas monoI [intro?] = mono.intro
    1.66 +  and monoD [dest?] = mono.mono
    1.67 +
    1.68 +constdefs
    1.69 +  min :: "['a::ord, 'a] => 'a"
    1.70 +  "min a b == (if a <= b then a else b)"
    1.71 +  max :: "['a::ord, 'a] => 'a"
    1.72 +  "max a b == (if a <= b then b else a)"
    1.73 +
    1.74 +lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    1.75 +  by (simp add: min_def)
    1.76 +
    1.77 +lemma min_of_mono:
    1.78 +    "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
    1.79 +  by (simp add: min_def)
    1.80 +
    1.81 +lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    1.82 +  by (simp add: max_def)
    1.83 +
    1.84 +lemma max_of_mono:
    1.85 +    "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
    1.86 +  by (simp add: max_def)
    1.87 +
    1.88 +
    1.89 +subsection "Orders"
    1.90 +
    1.91 +axclass order < ord
    1.92 +  order_refl [iff]: "x <= x"
    1.93 +  order_trans: "x <= y ==> y <= z ==> x <= z"
    1.94 +  order_antisym: "x <= y ==> y <= x ==> x = y"
    1.95 +  order_less_le: "(x < y) = (x <= y & x ~= y)"
    1.96 +
    1.97 +text{* Connection to locale: *}
    1.98 +
    1.99 +lemma partial_order_order:
   1.100 + "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
   1.101 +apply(rule partial_order.intro)
   1.102 +apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
   1.103 +done
   1.104 +
   1.105 +text {* Reflexivity. *}
   1.106 +
   1.107 +lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y"
   1.108 +    -- {* This form is useful with the classical reasoner. *}
   1.109 +  apply (erule ssubst)
   1.110 +  apply (rule order_refl)
   1.111 +  done
   1.112 +
   1.113 +lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   1.114 +  by (simp add: order_less_le)
   1.115 +
   1.116 +lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
   1.117 +    -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   1.118 +  apply (simp add: order_less_le, blast)
   1.119 +  done
   1.120 +
   1.121 +lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
   1.122 +
   1.123 +lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"
   1.124 +  by (simp add: order_less_le)
   1.125 +
   1.126 +
   1.127 +text {* Asymmetry. *}
   1.128 +
   1.129 +lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
   1.130 +  by (simp add: order_less_le order_antisym)
   1.131 +
   1.132 +lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
   1.133 +  apply (drule order_less_not_sym)
   1.134 +  apply (erule contrapos_np, simp)
   1.135 +  done
   1.136 +
   1.137 +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
   1.138 +by (blast intro: order_antisym)
   1.139 +
   1.140 +lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
   1.141 +by(blast intro:order_antisym)
   1.142 +
   1.143 +text {* Transitivity. *}
   1.144 +
   1.145 +lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z"
   1.146 +  apply (simp add: order_less_le)
   1.147 +  apply (blast intro: order_trans order_antisym)
   1.148 +  done
   1.149 +
   1.150 +lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z"
   1.151 +  apply (simp add: order_less_le)
   1.152 +  apply (blast intro: order_trans order_antisym)
   1.153 +  done
   1.154 +
   1.155 +lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z"
   1.156 +  apply (simp add: order_less_le)
   1.157 +  apply (blast intro: order_trans order_antisym)
   1.158 +  done
   1.159 +
   1.160 +
   1.161 +text {* Useful for simplification, but too risky to include by default. *}
   1.162 +
   1.163 +lemma order_less_imp_not_less: "(x::'a::order) < y ==>  (~ y < x) = True"
   1.164 +  by (blast elim: order_less_asym)
   1.165 +
   1.166 +lemma order_less_imp_triv: "(x::'a::order) < y ==>  (y < x --> P) = True"
   1.167 +  by (blast elim: order_less_asym)
   1.168 +
   1.169 +lemma order_less_imp_not_eq: "(x::'a::order) < y ==>  (x = y) = False"
   1.170 +  by auto
   1.171 +
   1.172 +lemma order_less_imp_not_eq2: "(x::'a::order) < y ==>  (y = x) = False"
   1.173 +  by auto
   1.174 +
   1.175 +
   1.176 +text {* Other operators. *}
   1.177 +
   1.178 +lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least"
   1.179 +  apply (simp add: min_def)
   1.180 +  apply (blast intro: order_antisym)
   1.181 +  done
   1.182 +
   1.183 +lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x"
   1.184 +  apply (simp add: max_def)
   1.185 +  apply (blast intro: order_antisym)
   1.186 +  done
   1.187 +
   1.188 +
   1.189 +subsection {* Transitivity rules for calculational reasoning *}
   1.190 +
   1.191 +
   1.192 +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
   1.193 +  by (simp add: order_less_le)
   1.194 +
   1.195 +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   1.196 +  by (simp add: order_less_le)
   1.197 +
   1.198 +lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   1.199 +  by (rule order_less_asym)
   1.200 +
   1.201 +
   1.202 +subsection {* Least value operator *}
   1.203 +
   1.204 +constdefs
   1.205 +  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   1.206 +  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   1.207 +    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
   1.208 +
   1.209 +lemma LeastI2:
   1.210 +  "[| P (x::'a::order);
   1.211 +      !!y. P y ==> x <= y;
   1.212 +      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   1.213 +   ==> Q (Least P)"
   1.214 +  apply (unfold Least_def)
   1.215 +  apply (rule theI2)
   1.216 +    apply (blast intro: order_antisym)+
   1.217 +  done
   1.218 +
   1.219 +lemma Least_equality:
   1.220 +    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   1.221 +  apply (simp add: Least_def)
   1.222 +  apply (rule the_equality)
   1.223 +  apply (auto intro!: order_antisym)
   1.224 +  done
   1.225 +
   1.226 +
   1.227 +subsection "Linear / total orders"
   1.228 +
   1.229 +axclass linorder < order
   1.230 +  linorder_linear: "x <= y | y <= x"
   1.231 +
   1.232 +lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   1.233 +  apply (simp add: order_less_le)
   1.234 +  apply (insert linorder_linear, blast)
   1.235 +  done
   1.236 +
   1.237 +lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
   1.238 +  by (simp add: order_le_less linorder_less_linear)
   1.239 +
   1.240 +lemma linorder_le_cases [case_names le ge]:
   1.241 +    "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
   1.242 +  by (insert linorder_linear, blast)
   1.243 +
   1.244 +lemma linorder_cases [case_names less equal greater]:
   1.245 +    "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
   1.246 +  by (insert linorder_less_linear, blast)
   1.247 +
   1.248 +lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
   1.249 +  apply (simp add: order_less_le)
   1.250 +  apply (insert linorder_linear)
   1.251 +  apply (blast intro: order_antisym)
   1.252 +  done
   1.253 +
   1.254 +lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)"
   1.255 +  apply (simp add: order_less_le)
   1.256 +  apply (insert linorder_linear)
   1.257 +  apply (blast intro: order_antisym)
   1.258 +  done
   1.259 +
   1.260 +lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
   1.261 +by (cut_tac x = x and y = y in linorder_less_linear, auto)
   1.262 +
   1.263 +lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   1.264 +by (simp add: linorder_neq_iff, blast)
   1.265 +
   1.266 +lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
   1.267 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   1.268 +
   1.269 +lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   1.270 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   1.271 +
   1.272 +lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   1.273 +by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   1.274 +
   1.275 +use "antisym_setup.ML";
   1.276 +setup antisym_setup
   1.277 +
   1.278 +subsection {* Setup of transitivity reasoner as Solver *}
   1.279 +
   1.280 +lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
   1.281 +  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
   1.282 +
   1.283 +lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   1.284 +  by (erule subst, erule ssubst, assumption)
   1.285 +
   1.286 +ML_setup {*
   1.287 +
   1.288 +(* The setting up of Quasi_Tac serves as a demo.  Since there is no
   1.289 +   class for quasi orders, the tactics Quasi_Tac.trans_tac and
   1.290 +   Quasi_Tac.quasi_tac are not of much use. *)
   1.291 +
   1.292 +fun decomp_gen sort sign (Trueprop $ t) =
   1.293 +  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
   1.294 +  fun dec (Const ("Not", _) $ t) = (
   1.295 +	  case dec t of
   1.296 +	    None => None
   1.297 +	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
   1.298 +	| dec (Const ("op =",  _) $ t1 $ t2) =
   1.299 +	    if of_sort t1
   1.300 +	    then Some (t1, "=", t2)
   1.301 +	    else None
   1.302 +	| dec (Const ("op <=",  _) $ t1 $ t2) =
   1.303 +	    if of_sort t1
   1.304 +	    then Some (t1, "<=", t2)
   1.305 +	    else None
   1.306 +	| dec (Const ("op <",  _) $ t1 $ t2) =
   1.307 +	    if of_sort t1
   1.308 +	    then Some (t1, "<", t2)
   1.309 +	    else None
   1.310 +	| dec _ = None
   1.311 +  in dec t end;
   1.312 +
   1.313 +structure Quasi_Tac = Quasi_Tac_Fun (
   1.314 +  struct
   1.315 +    val le_trans = thm "order_trans";
   1.316 +    val le_refl = thm "order_refl";
   1.317 +    val eqD1 = thm "order_eq_refl";
   1.318 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
   1.319 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   1.320 +    val less_imp_le = thm "order_less_imp_le";
   1.321 +    val le_neq_trans = thm "order_le_neq_trans";
   1.322 +    val neq_le_trans = thm "order_neq_le_trans";
   1.323 +    val less_imp_neq = thm "less_imp_neq";
   1.324 +    val decomp_trans = decomp_gen ["Orderings.order"];
   1.325 +    val decomp_quasi = decomp_gen ["Orderings.order"];
   1.326 +
   1.327 +  end);  (* struct *)
   1.328 +
   1.329 +structure Order_Tac = Order_Tac_Fun (
   1.330 +  struct
   1.331 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
   1.332 +    val le_refl = thm "order_refl";
   1.333 +    val less_imp_le = thm "order_less_imp_le";
   1.334 +    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   1.335 +    val not_leI = thm "linorder_not_le" RS thm "iffD2";
   1.336 +    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   1.337 +    val not_leD = thm "linorder_not_le" RS thm "iffD1";
   1.338 +    val eqI = thm "order_antisym";
   1.339 +    val eqD1 = thm "order_eq_refl";
   1.340 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
   1.341 +    val less_trans = thm "order_less_trans";
   1.342 +    val less_le_trans = thm "order_less_le_trans";
   1.343 +    val le_less_trans = thm "order_le_less_trans";
   1.344 +    val le_trans = thm "order_trans";
   1.345 +    val le_neq_trans = thm "order_le_neq_trans";
   1.346 +    val neq_le_trans = thm "order_neq_le_trans";
   1.347 +    val less_imp_neq = thm "less_imp_neq";
   1.348 +    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
   1.349 +    val decomp_part = decomp_gen ["Orderings.order"];
   1.350 +    val decomp_lin = decomp_gen ["Orderings.linorder"];
   1.351 +
   1.352 +  end);  (* struct *)
   1.353 +
   1.354 +simpset_ref() := simpset ()
   1.355 +    addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
   1.356 +    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
   1.357 +  (* Adding the transitivity reasoners also as safe solvers showed a slight
   1.358 +     speed up, but the reasoning strength appears to be not higher (at least
   1.359 +     no breaking of additional proofs in the entire HOL distribution, as
   1.360 +     of 5 March 2004, was observed). *)
   1.361 +*}
   1.362 +
   1.363 +(* Optional setup of methods *)
   1.364 +
   1.365 +(*
   1.366 +method_setup trans_partial =
   1.367 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
   1.368 +  {* transitivity reasoner for partial orders *}	
   1.369 +method_setup trans_linear =
   1.370 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   1.371 +  {* transitivity reasoner for linear orders *}
   1.372 +*)
   1.373 +
   1.374 +(*
   1.375 +declare order.order_refl [simp del] order_less_irrefl [simp del]
   1.376 +
   1.377 +can currently not be removed, abel_cancel relies on it.
   1.378 +*)
   1.379 +
   1.380 +
   1.381 +subsection "Min and max on (linear) orders"
   1.382 +
   1.383 +lemma min_same [simp]: "min (x::'a::order) x = x"
   1.384 +  by (simp add: min_def)
   1.385 +
   1.386 +lemma max_same [simp]: "max (x::'a::order) x = x"
   1.387 +  by (simp add: max_def)
   1.388 +
   1.389 +text{* Instantiate locales: *}
   1.390 +
   1.391 +lemma lower_semilattice_lin_min:
   1.392 +  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.393 +apply(rule lower_semilattice.intro)
   1.394 +apply(rule partial_order_order)
   1.395 +apply(rule lower_semilattice_axioms.intro)
   1.396 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   1.397 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   1.398 +apply(simp add:min_def linorder_not_le order_less_imp_le)
   1.399 +done
   1.400 +
   1.401 +lemma upper_semilattice_lin_max:
   1.402 +  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.403 +apply(rule upper_semilattice.intro)
   1.404 +apply(rule partial_order_order)
   1.405 +apply(rule upper_semilattice_axioms.intro)
   1.406 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   1.407 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   1.408 +apply(simp add: max_def linorder_not_le order_less_imp_le)
   1.409 +done
   1.410 +
   1.411 +lemma lattice_min_max: "lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
   1.412 +apply(rule lattice.intro)
   1.413 +apply(rule partial_order_order)
   1.414 +apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
   1.415 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
   1.416 +done
   1.417 +
   1.418 +lemma distrib_lattice_min_max:
   1.419 + "distrib_lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
   1.420 +apply(rule distrib_lattice.intro)
   1.421 +apply(rule partial_order_order)
   1.422 +apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
   1.423 +apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
   1.424 +apply(rule distrib_lattice_axioms.intro)
   1.425 +apply(rule_tac x=x and y=y in linorder_le_cases)
   1.426 +apply(rule_tac x=x and y=z in linorder_le_cases)
   1.427 +apply(rule_tac x=y and y=z in linorder_le_cases)
   1.428 +apply(simp add:min_def max_def)
   1.429 +apply(simp add:min_def max_def)
   1.430 +apply(rule_tac x=y and y=z in linorder_le_cases)
   1.431 +apply(simp add:min_def max_def)
   1.432 +apply(simp add:min_def max_def)
   1.433 +apply(rule_tac x=x and y=z in linorder_le_cases)
   1.434 +apply(rule_tac x=y and y=z in linorder_le_cases)
   1.435 +apply(simp add:min_def max_def)
   1.436 +apply(simp add:min_def max_def)
   1.437 +apply(rule_tac x=y and y=z in linorder_le_cases)
   1.438 +apply(simp add:min_def max_def)
   1.439 +apply(simp add:min_def max_def)
   1.440 +done
   1.441 +
   1.442 +lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   1.443 +  apply(simp add:max_def)
   1.444 +  apply (insert linorder_linear)
   1.445 +  apply (blast intro: order_trans)
   1.446 +  done
   1.447 +
   1.448 +lemma le_maxI1: "(x::'a::linorder) <= max x y"
   1.449 +by(rule upper_semilattice.sup_ge1[OF upper_semilattice_lin_max])
   1.450 +
   1.451 +lemma le_maxI2: "(y::'a::linorder) <= max x y"
   1.452 +    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
   1.453 +by(rule upper_semilattice.sup_ge2[OF upper_semilattice_lin_max])
   1.454 +
   1.455 +lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   1.456 +  apply (simp add: max_def order_le_less)
   1.457 +  apply (insert linorder_less_linear)
   1.458 +  apply (blast intro: order_less_trans)
   1.459 +  done
   1.460 +
   1.461 +lemma max_le_iff_conj [simp]:
   1.462 +    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
   1.463 +by (rule upper_semilattice.above_sup_conv[OF upper_semilattice_lin_max])
   1.464 +
   1.465 +lemma max_less_iff_conj [simp]:
   1.466 +    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   1.467 +  apply (simp add: order_le_less max_def)
   1.468 +  apply (insert linorder_less_linear)
   1.469 +  apply (blast intro: order_less_trans)
   1.470 +  done
   1.471 +
   1.472 +lemma le_min_iff_conj [simp]:
   1.473 +    "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
   1.474 +    -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
   1.475 +by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
   1.476 +
   1.477 +lemma min_less_iff_conj [simp]:
   1.478 +    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   1.479 +  apply (simp add: order_le_less min_def)
   1.480 +  apply (insert linorder_less_linear)
   1.481 +  apply (blast intro: order_less_trans)
   1.482 +  done
   1.483 +
   1.484 +lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   1.485 +  apply (simp add: min_def)
   1.486 +  apply (insert linorder_linear)
   1.487 +  apply (blast intro: order_trans)
   1.488 +  done
   1.489 +
   1.490 +lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   1.491 +  apply (simp add: min_def order_le_less)
   1.492 +  apply (insert linorder_less_linear)
   1.493 +  apply (blast intro: order_less_trans)
   1.494 +  done
   1.495 +
   1.496 +lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
   1.497 +by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
   1.498 +
   1.499 +lemma max_commute: "!!x::'a::linorder. max x y = max y x"
   1.500 +by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
   1.501 +
   1.502 +lemmas max_ac = max_assoc max_commute
   1.503 +                mk_left_commute[of max,OF max_assoc max_commute]
   1.504 +
   1.505 +lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
   1.506 +by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
   1.507 +
   1.508 +lemma min_commute: "!!x::'a::linorder. min x y = min y x"
   1.509 +by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
   1.510 +
   1.511 +lemmas min_ac = min_assoc min_commute
   1.512 +                mk_left_commute[of min,OF min_assoc min_commute]
   1.513 +
   1.514 +lemma split_min:
   1.515 +    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   1.516 +  by (simp add: min_def)
   1.517 +
   1.518 +lemma split_max:
   1.519 +    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   1.520 +  by (simp add: max_def)
   1.521 +
   1.522 +
   1.523 +subsection "Bounded quantifiers"
   1.524 +
   1.525 +syntax
   1.526 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   1.527 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
   1.528 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   1.529 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
   1.530 +
   1.531 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   1.532 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
   1.533 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   1.534 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
   1.535 +
   1.536 +syntax (xsymbols)
   1.537 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   1.538 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   1.539 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   1.540 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   1.541 +
   1.542 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   1.543 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   1.544 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   1.545 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   1.546 +
   1.547 +syntax (HOL)
   1.548 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   1.549 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   1.550 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   1.551 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   1.552 +
   1.553 +syntax (HTML output)
   1.554 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   1.555 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   1.556 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   1.557 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   1.558 +
   1.559 +  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   1.560 +  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   1.561 +  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   1.562 +  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   1.563 +
   1.564 +translations
   1.565 + "ALL x<y. P"   =>  "ALL x. x < y --> P"
   1.566 + "EX x<y. P"    =>  "EX x. x < y  & P"
   1.567 + "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
   1.568 + "EX x<=y. P"   =>  "EX x. x <= y & P"
   1.569 + "ALL x>y. P"   =>  "ALL x. x > y --> P"
   1.570 + "EX x>y. P"    =>  "EX x. x > y  & P"
   1.571 + "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
   1.572 + "EX x>=y. P"   =>  "EX x. x >= y & P"
   1.573 +
   1.574 +print_translation {*
   1.575 +let
   1.576 +  fun mk v v' q n P =
   1.577 +    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
   1.578 +    then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   1.579 +  fun all_tr' [Const ("_bound",_) $ Free (v,_),
   1.580 +               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.581 +    mk v v' "_lessAll" n P
   1.582 +
   1.583 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.584 +               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.585 +    mk v v' "_leAll" n P
   1.586 +
   1.587 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.588 +               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.589 +    mk v v' "_gtAll" n P
   1.590 +
   1.591 +  | all_tr' [Const ("_bound",_) $ Free (v,_),
   1.592 +               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.593 +    mk v v' "_geAll" n P;
   1.594 +
   1.595 +  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.596 +               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.597 +    mk v v' "_lessEx" n P
   1.598 +
   1.599 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.600 +               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   1.601 +    mk v v' "_leEx" n P
   1.602 +
   1.603 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.604 +               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.605 +    mk v v' "_gtEx" n P
   1.606 +
   1.607 +  | ex_tr' [Const ("_bound",_) $ Free (v,_),
   1.608 +               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   1.609 +    mk v v' "_geEx" n P
   1.610 +in
   1.611 +[("ALL ", all_tr'), ("EX ", ex_tr')]
   1.612 +end
   1.613 +*}
   1.614 +
   1.615 +end