src/HOL/Orderings.thy
author haftmann
Fri Mar 17 09:34:23 2006 +0100 (2006-03-17)
changeset 19277 f7602e74d948
parent 19039 8eae46249628
child 19527 9b5c38e8e780
permissions -rw-r--r--
renamed op < <= to Orderings.less(_eq)
     1 (*  Title:      HOL/Orderings.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     4 
     5 FIXME: derive more of the min/max laws generically via semilattices
     6 *)
     7 
     8 header {* Type classes for $\le$ *}
     9 
    10 theory Orderings
    11 imports Lattice_Locales
    12 uses ("antisym_setup.ML")
    13 begin
    14 
    15 subsection {* Order signatures and orders *}
    16 
    17 axclass
    18   ord < type
    19 
    20 syntax
    21   "less"        :: "['a::ord, 'a] => bool"             ("op <")
    22   "less_eq"     :: "['a::ord, 'a] => bool"             ("op <=")
    23 
    24 consts
    25   "less"        :: "['a::ord, 'a] => bool"             ("(_/ < _)"  [50, 51] 50)
    26   "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ <= _)" [50, 51] 50)
    27 
    28 syntax (xsymbols)
    29   "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
    30   "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    31 
    32 syntax (HTML output)
    33   "less_eq"     :: "['a::ord, 'a] => bool"             ("op \<le>")
    34   "less_eq"     :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    35 
    36 text{* Syntactic sugar: *}
    37 
    38 syntax
    39   "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    40   "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    41 translations
    42   "x > y"  => "y < x"
    43   "x >= y" => "y <= x"
    44 
    45 syntax (xsymbols)
    46   "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
    47 
    48 syntax (HTML output)
    49   "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
    50 
    51 
    52 subsection {* Monotonicity *}
    53 
    54 locale mono =
    55   fixes f
    56   assumes mono: "A <= B ==> f A <= f B"
    57 
    58 lemmas monoI [intro?] = mono.intro
    59   and monoD [dest?] = mono.mono
    60 
    61 constdefs
    62   min :: "['a::ord, 'a] => 'a"
    63   "min a b == (if a <= b then a else b)"
    64   max :: "['a::ord, 'a] => 'a"
    65   "max a b == (if a <= b then b else a)"
    66 
    67 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    68   by (simp add: min_def)
    69 
    70 lemma min_of_mono:
    71     "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
    72   by (simp add: min_def)
    73 
    74 lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
    75   by (simp add: max_def)
    76 
    77 lemma max_of_mono:
    78     "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
    79   by (simp add: max_def)
    80 
    81 
    82 subsection "Orders"
    83 
    84 axclass order < ord
    85   order_refl [iff]: "x <= x"
    86   order_trans: "x <= y ==> y <= z ==> x <= z"
    87   order_antisym: "x <= y ==> y <= x ==> x = y"
    88   order_less_le: "(x < y) = (x <= y & x ~= y)"
    89 
    90 text{* Connection to locale: *}
    91 
    92 interpretation order:
    93   partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
    94 apply(rule partial_order.intro)
    95 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    96 done
    97 
    98 text {* Reflexivity. *}
    99 
   100 lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y"
   101     -- {* This form is useful with the classical reasoner. *}
   102   apply (erule ssubst)
   103   apply (rule order_refl)
   104   done
   105 
   106 lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   107   by (simp add: order_less_le)
   108 
   109 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
   110     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   111   apply (simp add: order_less_le, blast)
   112   done
   113 
   114 lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
   115 
   116 lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"
   117   by (simp add: order_less_le)
   118 
   119 
   120 text {* Asymmetry. *}
   121 
   122 lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
   123   by (simp add: order_less_le order_antisym)
   124 
   125 lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
   126   apply (drule order_less_not_sym)
   127   apply (erule contrapos_np, simp)
   128   done
   129 
   130 lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
   131 by (blast intro: order_antisym)
   132 
   133 lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)"
   134 by(blast intro:order_antisym)
   135 
   136 text {* Transitivity. *}
   137 
   138 lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z"
   139   apply (simp add: order_less_le)
   140   apply (blast intro: order_trans order_antisym)
   141   done
   142 
   143 lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z"
   144   apply (simp add: order_less_le)
   145   apply (blast intro: order_trans order_antisym)
   146   done
   147 
   148 lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z"
   149   apply (simp add: order_less_le)
   150   apply (blast intro: order_trans order_antisym)
   151   done
   152 
   153 
   154 text {* Useful for simplification, but too risky to include by default. *}
   155 
   156 lemma order_less_imp_not_less: "(x::'a::order) < y ==>  (~ y < x) = True"
   157   by (blast elim: order_less_asym)
   158 
   159 lemma order_less_imp_triv: "(x::'a::order) < y ==>  (y < x --> P) = True"
   160   by (blast elim: order_less_asym)
   161 
   162 lemma order_less_imp_not_eq: "(x::'a::order) < y ==>  (x = y) = False"
   163   by auto
   164 
   165 lemma order_less_imp_not_eq2: "(x::'a::order) < y ==>  (y = x) = False"
   166   by auto
   167 
   168 
   169 text {* Other operators. *}
   170 
   171 lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least"
   172   apply (simp add: min_def)
   173   apply (blast intro: order_antisym)
   174   done
   175 
   176 lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x"
   177   apply (simp add: max_def)
   178   apply (blast intro: order_antisym)
   179   done
   180 
   181 
   182 subsection {* Transitivity rules for calculational reasoning *}
   183 
   184 
   185 lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
   186   by (simp add: order_less_le)
   187 
   188 lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
   189   by (simp add: order_less_le)
   190 
   191 lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
   192   by (rule order_less_asym)
   193 
   194 
   195 subsection {* Least value operator *}
   196 
   197 constdefs
   198   Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   199   "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   200     -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
   201 
   202 lemma LeastI2_order:
   203   "[| P (x::'a::order);
   204       !!y. P y ==> x <= y;
   205       !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
   206    ==> Q (Least P)"
   207   apply (unfold Least_def)
   208   apply (rule theI2)
   209     apply (blast intro: order_antisym)+
   210   done
   211 
   212 lemma Least_equality:
   213     "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   214   apply (simp add: Least_def)
   215   apply (rule the_equality)
   216   apply (auto intro!: order_antisym)
   217   done
   218 
   219 
   220 subsection "Linear / total orders"
   221 
   222 axclass linorder < order
   223   linorder_linear: "x <= y | y <= x"
   224 
   225 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   226   apply (simp add: order_less_le)
   227   apply (insert linorder_linear, blast)
   228   done
   229 
   230 lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x"
   231   by (simp add: order_le_less linorder_less_linear)
   232 
   233 lemma linorder_le_cases [case_names le ge]:
   234     "((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P"
   235   by (insert linorder_linear, blast)
   236 
   237 lemma linorder_cases [case_names less equal greater]:
   238     "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
   239   by (insert linorder_less_linear, blast)
   240 
   241 lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
   242   apply (simp add: order_less_le)
   243   apply (insert linorder_linear)
   244   apply (blast intro: order_antisym)
   245   done
   246 
   247 lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)"
   248   apply (simp add: order_less_le)
   249   apply (insert linorder_linear)
   250   apply (blast intro: order_antisym)
   251   done
   252 
   253 lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
   254 by (cut_tac x = x and y = y in linorder_less_linear, auto)
   255 
   256 lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   257 by (simp add: linorder_neq_iff, blast)
   258 
   259 lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)"
   260 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   261 
   262 lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   263 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   264 
   265 lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   266 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   267 
   268 text{*Replacing the old Nat.leI*}
   269 lemma leI: "~ x < y ==> y <= (x::'a::linorder)"
   270   by (simp only: linorder_not_less)
   271 
   272 lemma leD: "y <= (x::'a::linorder) ==> ~ x < y"
   273   by (simp only: linorder_not_less)
   274 
   275 (*FIXME inappropriate name (or delete altogether)*)
   276 lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y"
   277   by (simp only: linorder_not_le)
   278 
   279 use "antisym_setup.ML";
   280 setup antisym_setup
   281 
   282 subsection {* Setup of transitivity reasoner as Solver *}
   283 
   284 lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
   285   by (erule contrapos_pn, erule subst, rule order_less_irrefl)
   286 
   287 lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
   288   by (erule subst, erule ssubst, assumption)
   289 
   290 ML_setup {*
   291 
   292 (* The setting up of Quasi_Tac serves as a demo.  Since there is no
   293    class for quasi orders, the tactics Quasi_Tac.trans_tac and
   294    Quasi_Tac.quasi_tac are not of much use. *)
   295 
   296 fun decomp_gen sort sign (Trueprop $ t) =
   297   let fun of_sort t = let val T = type_of t in
   298         (* exclude numeric types: linear arithmetic subsumes transitivity *)
   299         T <> HOLogic.natT andalso T <> HOLogic.intT andalso
   300         T <> HOLogic.realT andalso Sign.of_sort sign (T, sort) end
   301   fun dec (Const ("Not", _) $ t) = (
   302 	  case dec t of
   303 	    NONE => NONE
   304 	  | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
   305 	| dec (Const ("op =",  _) $ t1 $ t2) =
   306 	    if of_sort t1
   307 	    then SOME (t1, "=", t2)
   308 	    else NONE
   309 	| dec (Const ("Orderings.less_eq",  _) $ t1 $ t2) =
   310 	    if of_sort t1
   311 	    then SOME (t1, "<=", t2)
   312 	    else NONE
   313 	| dec (Const ("Orderings.less",  _) $ t1 $ t2) =
   314 	    if of_sort t1
   315 	    then SOME (t1, "<", t2)
   316 	    else NONE
   317 	| dec _ = NONE
   318   in dec t end;
   319 
   320 structure Quasi_Tac = Quasi_Tac_Fun (
   321   struct
   322     val le_trans = thm "order_trans";
   323     val le_refl = thm "order_refl";
   324     val eqD1 = thm "order_eq_refl";
   325     val eqD2 = thm "sym" RS thm "order_eq_refl";
   326     val less_reflE = thm "order_less_irrefl" RS thm "notE";
   327     val less_imp_le = thm "order_less_imp_le";
   328     val le_neq_trans = thm "order_le_neq_trans";
   329     val neq_le_trans = thm "order_neq_le_trans";
   330     val less_imp_neq = thm "less_imp_neq";
   331     val decomp_trans = decomp_gen ["Orderings.order"];
   332     val decomp_quasi = decomp_gen ["Orderings.order"];
   333 
   334   end);  (* struct *)
   335 
   336 structure Order_Tac = Order_Tac_Fun (
   337   struct
   338     val less_reflE = thm "order_less_irrefl" RS thm "notE";
   339     val le_refl = thm "order_refl";
   340     val less_imp_le = thm "order_less_imp_le";
   341     val not_lessI = thm "linorder_not_less" RS thm "iffD2";
   342     val not_leI = thm "linorder_not_le" RS thm "iffD2";
   343     val not_lessD = thm "linorder_not_less" RS thm "iffD1";
   344     val not_leD = thm "linorder_not_le" RS thm "iffD1";
   345     val eqI = thm "order_antisym";
   346     val eqD1 = thm "order_eq_refl";
   347     val eqD2 = thm "sym" RS thm "order_eq_refl";
   348     val less_trans = thm "order_less_trans";
   349     val less_le_trans = thm "order_less_le_trans";
   350     val le_less_trans = thm "order_le_less_trans";
   351     val le_trans = thm "order_trans";
   352     val le_neq_trans = thm "order_le_neq_trans";
   353     val neq_le_trans = thm "order_neq_le_trans";
   354     val less_imp_neq = thm "less_imp_neq";
   355     val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
   356     val not_sym = thm "not_sym";
   357     val decomp_part = decomp_gen ["Orderings.order"];
   358     val decomp_lin = decomp_gen ["Orderings.linorder"];
   359 
   360   end);  (* struct *)
   361 
   362 change_simpset (fn ss => ss
   363     addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
   364     addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac)));
   365   (* Adding the transitivity reasoners also as safe solvers showed a slight
   366      speed up, but the reasoning strength appears to be not higher (at least
   367      no breaking of additional proofs in the entire HOL distribution, as
   368      of 5 March 2004, was observed). *)
   369 *}
   370 
   371 (* Optional setup of methods *)
   372 
   373 (*
   374 method_setup trans_partial =
   375   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
   376   {* transitivity reasoner for partial orders *}	
   377 method_setup trans_linear =
   378   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
   379   {* transitivity reasoner for linear orders *}
   380 *)
   381 
   382 (*
   383 declare order.order_refl [simp del] order_less_irrefl [simp del]
   384 
   385 can currently not be removed, abel_cancel relies on it.
   386 *)
   387 
   388 
   389 subsection "Min and max on (linear) orders"
   390 
   391 text{* Instantiate locales: *}
   392 
   393 interpretation min_max:
   394   lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   395 apply(rule lower_semilattice_axioms.intro)
   396 apply(simp add:min_def linorder_not_le order_less_imp_le)
   397 apply(simp add:min_def linorder_not_le order_less_imp_le)
   398 apply(simp add:min_def linorder_not_le order_less_imp_le)
   399 done
   400 
   401 interpretation min_max:
   402   upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
   403 apply -
   404 apply(rule upper_semilattice_axioms.intro)
   405 apply(simp add: max_def linorder_not_le order_less_imp_le)
   406 apply(simp add: max_def linorder_not_le order_less_imp_le)
   407 apply(simp add: max_def linorder_not_le order_less_imp_le)
   408 done
   409 
   410 interpretation min_max:
   411   lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   412 .
   413 
   414 interpretation min_max:
   415   distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
   416 apply(rule distrib_lattice_axioms.intro)
   417 apply(rule_tac x=x and y=y in linorder_le_cases)
   418 apply(rule_tac x=x and y=z in linorder_le_cases)
   419 apply(rule_tac x=y and y=z in linorder_le_cases)
   420 apply(simp add:min_def max_def)
   421 apply(simp add:min_def max_def)
   422 apply(rule_tac x=y and y=z in linorder_le_cases)
   423 apply(simp add:min_def max_def)
   424 apply(simp add:min_def max_def)
   425 apply(rule_tac x=x and y=z in linorder_le_cases)
   426 apply(rule_tac x=y and y=z in linorder_le_cases)
   427 apply(simp add:min_def max_def)
   428 apply(simp add:min_def max_def)
   429 apply(rule_tac x=y and y=z in linorder_le_cases)
   430 apply(simp add:min_def max_def)
   431 apply(simp add:min_def max_def)
   432 done
   433 
   434 lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
   435   apply(simp add:max_def)
   436   apply (insert linorder_linear)
   437   apply (blast intro: order_trans)
   438   done
   439 
   440 lemmas le_maxI1 = min_max.sup_ge1
   441 lemmas le_maxI2 = min_max.sup_ge2
   442 
   443 lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   444   apply (simp add: max_def order_le_less)
   445   apply (insert linorder_less_linear)
   446   apply (blast intro: order_less_trans)
   447   done
   448 
   449 lemma max_less_iff_conj [simp]:
   450     "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   451   apply (simp add: order_le_less max_def)
   452   apply (insert linorder_less_linear)
   453   apply (blast intro: order_less_trans)
   454   done
   455 
   456 lemma min_less_iff_conj [simp]:
   457     "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   458   apply (simp add: order_le_less min_def)
   459   apply (insert linorder_less_linear)
   460   apply (blast intro: order_less_trans)
   461   done
   462 
   463 lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
   464   apply (simp add: min_def)
   465   apply (insert linorder_linear)
   466   apply (blast intro: order_trans)
   467   done
   468 
   469 lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
   470   apply (simp add: min_def order_le_less)
   471   apply (insert linorder_less_linear)
   472   apply (blast intro: order_less_trans)
   473   done
   474 
   475 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   476                mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   477 
   478 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   479                mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   480 
   481 lemma split_min:
   482     "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
   483   by (simp add: min_def)
   484 
   485 lemma split_max:
   486     "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
   487   by (simp add: max_def)
   488 
   489 
   490 subsection "Bounded quantifiers"
   491 
   492 syntax
   493   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   494   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
   495   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   496   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
   497 
   498   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   499   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
   500   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   501   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
   502 
   503 syntax (xsymbols)
   504   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   505   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   506   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   507   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   508 
   509   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   510   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   511   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   512   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   513 
   514 syntax (HOL)
   515   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   516   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   517   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   518   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   519 
   520 syntax (HTML output)
   521   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   522   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   523   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   524   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   525 
   526   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   527   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   528   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   529   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   530 
   531 translations
   532  "ALL x<y. P"   =>  "ALL x. x < y --> P"
   533  "EX x<y. P"    =>  "EX x. x < y  & P"
   534  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
   535  "EX x<=y. P"   =>  "EX x. x <= y & P"
   536  "ALL x>y. P"   =>  "ALL x. x > y --> P"
   537  "EX x>y. P"    =>  "EX x. x > y  & P"
   538  "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
   539  "EX x>=y. P"   =>  "EX x. x >= y & P"
   540 
   541 print_translation {*
   542 let
   543   fun mk v v' q n P =
   544     if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
   545     then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   546   fun all_tr' [Const ("_bound",_) $ Free (v,_),
   547                Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   548     mk v v' "_lessAll" n P
   549 
   550   | all_tr' [Const ("_bound",_) $ Free (v,_),
   551                Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   552     mk v v' "_leAll" n P
   553 
   554   | all_tr' [Const ("_bound",_) $ Free (v,_),
   555                Const("op -->",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   556     mk v v' "_gtAll" n P
   557 
   558   | all_tr' [Const ("_bound",_) $ Free (v,_),
   559                Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   560     mk v v' "_geAll" n P;
   561 
   562   fun ex_tr' [Const ("_bound",_) $ Free (v,_),
   563                Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   564     mk v v' "_lessEx" n P
   565 
   566   | ex_tr' [Const ("_bound",_) $ Free (v,_),
   567                Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
   568     mk v v' "_leEx" n P
   569 
   570   | ex_tr' [Const ("_bound",_) $ Free (v,_),
   571                Const("op &",_) $ (Const ("Orderings.less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   572     mk v v' "_gtEx" n P
   573 
   574   | ex_tr' [Const ("_bound",_) $ Free (v,_),
   575                Const("op &",_) $ (Const ("Orderings.less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
   576     mk v v' "_geEx" n P
   577 in
   578 [("ALL ", all_tr'), ("EX ", ex_tr')]
   579 end
   580 *}
   581 
   582 subsection {* Extra transitivity rules *}
   583 
   584 text {* These support proving chains of decreasing inequalities
   585     a >= b >= c ... in Isar proofs. *}
   586 
   587 lemma xt1: "a = b ==> b > c ==> a > c"
   588 by simp
   589 
   590 lemma xt2: "a > b ==> b = c ==> a > c"
   591 by simp
   592 
   593 lemma xt3: "a = b ==> b >= c ==> a >= c"
   594 by simp
   595 
   596 lemma xt4: "a >= b ==> b = c ==> a >= c"
   597 by simp
   598 
   599 lemma xt5: "(x::'a::order) >= y ==> y >= x ==> x = y"
   600 by simp
   601 
   602 lemma xt6: "(x::'a::order) >= y ==> y >= z ==> x >= z"
   603 by simp
   604 
   605 lemma xt7: "(x::'a::order) > y ==> y >= z ==> x > z"
   606 by simp
   607 
   608 lemma xt8: "(x::'a::order) >= y ==> y > z ==> x > z"
   609 by simp
   610 
   611 lemma xt9: "(a::'a::order) > b ==> b > a ==> ?P"
   612 by simp
   613 
   614 lemma xt10: "(x::'a::order) > y ==> y > z ==> x > z"
   615 by simp
   616 
   617 lemma xt11: "(a::'a::order) >= b ==> a ~= b ==> a > b"
   618 by simp
   619 
   620 lemma xt12: "(a::'a::order) ~= b ==> a >= b ==> a > b"
   621 by simp
   622 
   623 lemma xt13: "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==>
   624     a > f c" 
   625 by simp
   626 
   627 lemma xt14: "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==>
   628     f a > c"
   629 by auto
   630 
   631 lemma xt15: "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==>
   632     a >= f c"
   633 by simp
   634 
   635 lemma xt16: "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==>
   636     f a >= c"
   637 by auto
   638 
   639 lemma xt17: "(a::'a::order) >= f b ==> b >= c ==> 
   640     (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
   641 by (subgoal_tac "f b >= f c", force, force)
   642 
   643 lemma xt18: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> 
   644     (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
   645 by (subgoal_tac "f a >= f b", force, force)
   646 
   647 lemma xt19: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
   648   (!!x y. x >= y ==> f x >= f y) ==> a > f c"
   649 by (subgoal_tac "f b >= f c", force, force)
   650 
   651 lemma xt20: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
   652     (!!x y. x > y ==> f x > f y) ==> f a > c"
   653 by (subgoal_tac "f a > f b", force, force)
   654 
   655 lemma xt21: "(a::'a::order) >= f b ==> b > c ==>
   656     (!!x y. x > y ==> f x > f y) ==> a > f c"
   657 by (subgoal_tac "f b > f c", force, force)
   658 
   659 lemma xt22: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
   660     (!!x y. x >= y ==> f x >= f y) ==> f a > c"
   661 by (subgoal_tac "f a >= f b", force, force)
   662 
   663 lemma xt23: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
   664     (!!x y. x > y ==> f x > f y) ==> a > f c"
   665 by (subgoal_tac "f b > f c", force, force)
   666 
   667 lemma xt24: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
   668     (!!x y. x > y ==> f x > f y) ==> f a > c"
   669 by (subgoal_tac "f a > f b", force, force)
   670 
   671 
   672 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 xt10 xt11 xt12
   673     xt13 xt14 xt15 xt15 xt17 xt18 xt19 xt20 xt21 xt22 xt23 xt24
   674 
   675 (* 
   676   Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
   677   for the wrong thing in an Isar proof.
   678 
   679   The extra transitivity rules can be used as follows: 
   680 
   681 lemma "(a::'a::order) > z"
   682 proof -
   683   have "a >= b" (is "_ >= ?rhs")
   684     sorry
   685   also have "?rhs >= c" (is "_ >= ?rhs")
   686     sorry
   687   also (xtrans) have "?rhs = d" (is "_ = ?rhs")
   688     sorry
   689   also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
   690     sorry
   691   also (xtrans) have "?rhs > f" (is "_ > ?rhs")
   692     sorry
   693   also (xtrans) have "?rhs > z"
   694     sorry
   695   finally (xtrans) show ?thesis .
   696 qed
   697 
   698   Alternatively, one can use "declare xtrans [trans]" and then
   699   leave out the "(xtrans)" above.
   700 *)
   701 
   702 end