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