1 (* Title: HOL/Orderings.thy
2 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
5 header {* Abstract orderings *}
9 uses "~~/src/Provers/order.ML"
12 subsection {* Quasi orders *}
14 class preorder = ord +
15 assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"
16 and order_refl [iff]: "x \<le> x"
17 and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
20 text {* Reflexivity. *}
22 lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
23 -- {* This form is useful with the classical reasoner. *}
24 by (erule ssubst) (rule order_refl)
26 lemma less_irrefl [iff]: "\<not> x < x"
27 by (simp add: less_le_not_le)
29 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
30 unfolding less_le_not_le by blast
35 lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
36 by (simp add: less_le_not_le)
38 lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
39 by (drule less_not_sym, erule contrapos_np) simp
42 text {* Transitivity. *}
44 lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
45 by (auto simp add: less_le_not_le intro: order_trans)
47 lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
48 by (auto simp add: less_le_not_le intro: order_trans)
50 lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
51 by (auto simp add: less_le_not_le intro: order_trans)
54 text {* Useful for simplification, but too risky to include by default. *}
56 lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
57 by (blast elim: less_asym)
59 lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
60 by (blast elim: less_asym)
63 text {* Transitivity rules for calculational reasoning *}
65 lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
72 "preorder (op \<ge>) (op >)"
73 proof qed (auto simp add: less_le_not_le intro: order_trans)
78 subsection {* Partial orders *}
80 class order = preorder +
81 assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
84 text {* Reflexivity. *}
86 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
87 by (auto simp add: less_le_not_le intro: antisym)
89 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
90 -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
91 by (simp add: less_le) blast
93 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
94 unfolding less_le by blast
97 text {* Useful for simplification, but too risky to include by default. *}
99 lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
102 lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
106 text {* Transitivity rules for calculational reasoning *}
108 lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
109 by (simp add: less_le)
111 lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
112 by (simp add: less_le)
115 text {* Asymmetry. *}
117 lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
118 by (blast intro: antisym)
120 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
121 by (blast intro: antisym)
123 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
124 by (erule contrapos_pn, erule subst, rule less_irrefl)
127 text {* Least value operator *}
130 Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
131 "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
133 lemma Least_equality:
135 and "\<And>y. P y \<Longrightarrow> x \<le> y"
137 unfolding Least_def by (rule the_equality)
138 (blast intro: assms antisym)+
142 and "\<And>y. P y \<Longrightarrow> x \<le> y"
143 and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
145 unfolding Least_def by (rule theI2)
146 (blast intro: assms antisym)+
149 text {* Dual order *}
152 "order (op \<ge>) (op >)"
153 by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
158 subsection {* Linear (total) orders *}
160 class linorder = order +
161 assumes linear: "x \<le> y \<or> y \<le> x"
164 lemma less_linear: "x < y \<or> x = y \<or> y < x"
165 unfolding less_le using less_le linear by blast
167 lemma le_less_linear: "x \<le> y \<or> y < x"
168 by (simp add: le_less less_linear)
170 lemma le_cases [case_names le ge]:
171 "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
172 using linear by blast
174 lemma linorder_cases [case_names less equal greater]:
175 "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
176 using less_linear by blast
178 lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
179 apply (simp add: less_le)
180 using linear apply (blast intro: antisym)
183 lemma not_less_iff_gr_or_eq:
184 "\<not>(x < y) \<longleftrightarrow> (x > y | x = y)"
185 apply(simp add:not_less le_less)
189 lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
190 apply (simp add: less_le)
191 using linear apply (blast intro: antisym)
194 lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
195 by (cut_tac x = x and y = y in less_linear, auto)
197 lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
198 by (simp add: neq_iff) blast
200 lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
201 by (blast intro: antisym dest: not_less [THEN iffD1])
203 lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
204 by (blast intro: antisym dest: not_less [THEN iffD1])
206 lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
207 by (blast intro: antisym dest: not_less [THEN iffD1])
209 lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
212 lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
215 (*FIXME inappropriate name (or delete altogether)*)
216 lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
220 text {* Dual order *}
223 "linorder (op \<ge>) (op >)"
224 by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
229 definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
230 [code del]: "min a b = (if a \<le> b then a else b)"
232 definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
233 [code del]: "max a b = (if a \<le> b then b else a)"
235 lemma min_le_iff_disj:
236 "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
237 unfolding min_def using linear by (auto intro: order_trans)
239 lemma le_max_iff_disj:
240 "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
241 unfolding max_def using linear by (auto intro: order_trans)
243 lemma min_less_iff_disj:
244 "min x y < z \<longleftrightarrow> x < z \<or> y < z"
245 unfolding min_def le_less using less_linear by (auto intro: less_trans)
247 lemma less_max_iff_disj:
248 "z < max x y \<longleftrightarrow> z < x \<or> z < y"
249 unfolding max_def le_less using less_linear by (auto intro: less_trans)
251 lemma min_less_iff_conj [simp]:
252 "z < min x y \<longleftrightarrow> z < x \<and> z < y"
253 unfolding min_def le_less using less_linear by (auto intro: less_trans)
255 lemma max_less_iff_conj [simp]:
256 "max x y < z \<longleftrightarrow> x < z \<and> y < z"
257 unfolding max_def le_less using less_linear by (auto intro: less_trans)
259 lemma split_min [noatp]:
260 "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
261 by (simp add: min_def)
263 lemma split_max [noatp]:
264 "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
265 by (simp add: max_def)
269 text {* Explicit dictionaries for code generation *}
271 lemma min_ord_min [code, code unfold, code inline del]:
272 "min = ord.min (op \<le>)"
273 by (rule ext)+ (simp add: min_def ord.min_def)
275 declare ord.min_def [code]
277 lemma max_ord_max [code, code unfold, code inline del]:
278 "max = ord.max (op \<le>)"
279 by (rule ext)+ (simp add: max_def ord.max_def)
281 declare ord.max_def [code]
284 subsection {* Reasoning tools setup *}
290 val print_structures: Proof.context -> unit
291 val setup: theory -> theory
292 val order_tac: thm list -> Proof.context -> int -> tactic
295 structure Orders: ORDERS =
298 (** Theory and context data **)
300 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
301 (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
303 structure Data = GenericDataFun
305 type T = ((string * term list) * Order_Tac.less_arith) list;
307 identifier of the structure, list of operations and record of theorems
308 needed to set up the transitivity reasoner,
309 identifier and operations identify the structure uniquely. *)
312 fun merge _ = AList.join struct_eq (K fst);
315 fun print_structures ctxt =
317 val structs = Data.get (Context.Proof ctxt);
318 fun pretty_term t = Pretty.block
319 [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
320 Pretty.str "::", Pretty.brk 1,
321 Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
322 fun pretty_struct ((s, ts), _) = Pretty.block
323 [Pretty.str s, Pretty.str ":", Pretty.brk 1,
324 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
326 Pretty.writeln (Pretty.big_list "Order structures:" (map pretty_struct structs))
332 fun struct_tac ((s, [eq, le, less]), thms) prems =
334 fun decomp thy (@{const Trueprop} $ t) =
337 (* exclude numeric types: linear arithmetic subsumes transitivity *)
338 let val T = type_of t
340 T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
342 fun rel (bin_op $ t1 $ t2) =
343 if excluded t1 then NONE
344 else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
345 else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
346 else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
349 fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
351 | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
354 | decomp thy _ = NONE;
357 "order" => Order_Tac.partial_tac decomp thms prems
358 | "linorder" => Order_Tac.linear_tac decomp thms prems
359 | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
362 fun order_tac prems ctxt =
363 FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
368 fun add_struct_thm s tag =
369 Thm.declaration_attribute
370 (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
372 Thm.declaration_attribute
373 (fn _ => Data.map (AList.delete struct_eq s));
375 val attribute = Attrib.syntax
376 (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
377 Args.del >> K NONE) --| Args.colon (* FIXME ||
378 Scan.succeed true *) ) -- Scan.lift Args.name --
379 Scan.repeat Args.term
380 >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
381 | ((NONE, n), ts) => del_struct (n, ts)));
384 (** Diagnostic command **)
386 val print = Toplevel.unknown_context o
387 Toplevel.keep (Toplevel.node_case
388 (Context.cases (print_structures o ProofContext.init) print_structures)
389 (print_structures o Proof.context_of));
392 OuterSyntax.improper_command "print_orders"
393 "print order structures available to transitivity reasoner" OuterKeyword.diag
394 (Scan.succeed (Toplevel.no_timing o print));
400 Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
401 Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
410 text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
415 (* The type constraint on @{term op =} below is necessary since the operation
416 is not a parameter of the locale. *)
418 declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
420 declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
422 declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
424 declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
426 declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
428 declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
430 declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
432 declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
434 declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
436 declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
438 declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
440 declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
442 declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
444 declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
446 declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
453 declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
455 declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
457 declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
459 declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
461 declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
463 declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
465 declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
467 declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
469 declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
471 declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
473 declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
475 declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
477 declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
479 declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
481 declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
483 declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
485 declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
487 declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
489 declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
491 declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
499 fun prp t thm = (#prop (rep_thm thm) = t);
501 fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
502 let val prems = prems_of_ss ss;
503 val less = Const (@{const_name less}, T);
504 val t = HOLogic.mk_Trueprop(le $ s $ r);
505 in case find_first (prp t) prems of
507 let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
508 in case find_first (prp t) prems of
510 | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
512 | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
514 handle THM _ => NONE;
516 fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
517 let val prems = prems_of_ss ss;
518 val le = Const (@{const_name less_eq}, T);
519 val t = HOLogic.mk_Trueprop(le $ r $ s);
520 in case find_first (prp t) prems of
522 let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
523 in case find_first (prp t) prems of
525 | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
527 | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
529 handle THM _ => NONE;
531 fun add_simprocs procs thy =
532 Simplifier.map_simpset (fn ss => ss
533 addsimprocs (map (fn (name, raw_ts, proc) =>
534 Simplifier.simproc thy name raw_ts proc) procs)) thy;
535 fun add_solver name tac =
536 Simplifier.map_simpset (fn ss => ss addSolver
537 mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
541 ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
542 ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
544 #> add_solver "Transitivity" Orders.order_tac
545 (* Adding the transitivity reasoners also as safe solvers showed a slight
546 speed up, but the reasoning strength appears to be not higher (at least
547 no breaking of additional proofs in the entire HOL distribution, as
548 of 5 March 2004, was observed). *)
553 subsection {* Name duplicates *}
555 lemmas order_less_le = less_le
556 lemmas order_eq_refl = preorder_class.eq_refl
557 lemmas order_less_irrefl = preorder_class.less_irrefl
558 lemmas order_le_less = order_class.le_less
559 lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
560 lemmas order_less_imp_le = preorder_class.less_imp_le
561 lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
562 lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
563 lemmas order_neq_le_trans = order_class.neq_le_trans
564 lemmas order_le_neq_trans = order_class.le_neq_trans
566 lemmas order_antisym = antisym
567 lemmas order_less_not_sym = preorder_class.less_not_sym
568 lemmas order_less_asym = preorder_class.less_asym
569 lemmas order_eq_iff = order_class.eq_iff
570 lemmas order_antisym_conv = order_class.antisym_conv
571 lemmas order_less_trans = preorder_class.less_trans
572 lemmas order_le_less_trans = preorder_class.le_less_trans
573 lemmas order_less_le_trans = preorder_class.less_le_trans
574 lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
575 lemmas order_less_imp_triv = preorder_class.less_imp_triv
576 lemmas order_less_asym' = preorder_class.less_asym'
578 lemmas linorder_linear = linear
579 lemmas linorder_less_linear = linorder_class.less_linear
580 lemmas linorder_le_less_linear = linorder_class.le_less_linear
581 lemmas linorder_le_cases = linorder_class.le_cases
582 lemmas linorder_not_less = linorder_class.not_less
583 lemmas linorder_not_le = linorder_class.not_le
584 lemmas linorder_neq_iff = linorder_class.neq_iff
585 lemmas linorder_neqE = linorder_class.neqE
586 lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
587 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
588 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
591 subsection {* Bounded quantifiers *}
594 "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
595 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
596 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
597 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
599 "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
600 "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
601 "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
602 "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)
605 "_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
606 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
607 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
608 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
610 "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
611 "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
612 "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
613 "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
616 "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
617 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
618 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
619 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
622 "_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
623 "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
624 "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
625 "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
627 "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
628 "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
629 "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
630 "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
633 "ALL x<y. P" => "ALL x. x < y \<longrightarrow> P"
634 "EX x<y. P" => "EX x. x < y \<and> P"
635 "ALL x<=y. P" => "ALL x. x <= y \<longrightarrow> P"
636 "EX x<=y. P" => "EX x. x <= y \<and> P"
637 "ALL x>y. P" => "ALL x. x > y \<longrightarrow> P"
638 "EX x>y. P" => "EX x. x > y \<and> P"
639 "ALL x>=y. P" => "ALL x. x >= y \<longrightarrow> P"
640 "EX x>=y. P" => "EX x. x >= y \<and> P"
644 val All_binder = Syntax.binder_name @{const_syntax All};
645 val Ex_binder = Syntax.binder_name @{const_syntax Ex};
646 val impl = @{const_syntax "op -->"};
647 val conj = @{const_syntax "op &"};
648 val less = @{const_syntax less};
649 val less_eq = @{const_syntax less_eq};
652 [((All_binder, impl, less), ("_All_less", "_All_greater")),
653 ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
654 ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
655 ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
657 fun matches_bound v t =
658 case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
660 fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
661 fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
664 fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
665 (case AList.lookup (op =) trans (q, c, d) of
668 if matches_bound v t andalso not (contains_var v u) then mk v l u P
669 else if matches_bound v u andalso not (contains_var v t) then mk v g t P
672 in [tr' All_binder, tr' Ex_binder] end
676 subsection {* Transitivity reasoning *}
681 lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c"
684 lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
687 lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c"
690 lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c"
695 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
696 (!!x y. x < y ==> f x < f y) ==> f a < c"
698 assume r: "!!x y. x < y ==> f x < f y"
699 assume "a < b" hence "f a < f b" by (rule r)
700 also assume "f b < c"
701 finally (order_less_trans) show ?thesis .
704 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
705 (!!x y. x < y ==> f x < f y) ==> a < f c"
707 assume r: "!!x y. x < y ==> f x < f y"
709 also assume "b < c" hence "f b < f c" by (rule r)
710 finally (order_less_trans) show ?thesis .
713 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
714 (!!x y. x <= y ==> f x <= f y) ==> f a < c"
716 assume r: "!!x y. x <= y ==> f x <= f y"
717 assume "a <= b" hence "f a <= f b" by (rule r)
718 also assume "f b < c"
719 finally (order_le_less_trans) show ?thesis .
722 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
723 (!!x y. x < y ==> f x < f y) ==> a < f c"
725 assume r: "!!x y. x < y ==> f x < f y"
727 also assume "b < c" hence "f b < f c" by (rule r)
728 finally (order_le_less_trans) show ?thesis .
731 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
732 (!!x y. x < y ==> f x < f y) ==> f a < c"
734 assume r: "!!x y. x < y ==> f x < f y"
735 assume "a < b" hence "f a < f b" by (rule r)
736 also assume "f b <= c"
737 finally (order_less_le_trans) show ?thesis .
740 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
741 (!!x y. x <= y ==> f x <= f y) ==> a < f c"
743 assume r: "!!x y. x <= y ==> f x <= f y"
745 also assume "b <= c" hence "f b <= f c" by (rule r)
746 finally (order_less_le_trans) show ?thesis .
749 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
750 (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
752 assume r: "!!x y. x <= y ==> f x <= f y"
754 also assume "b <= c" hence "f b <= f c" by (rule r)
755 finally (order_trans) show ?thesis .
758 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
759 (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
761 assume r: "!!x y. x <= y ==> f x <= f y"
762 assume "a <= b" hence "f a <= f b" by (rule r)
763 also assume "f b <= c"
764 finally (order_trans) show ?thesis .
767 lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
768 (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
770 assume r: "!!x y. x <= y ==> f x <= f y"
771 assume "a <= b" hence "f a <= f b" by (rule r)
772 also assume "f b = c"
773 finally (ord_le_eq_trans) show ?thesis .
776 lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
777 (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
779 assume r: "!!x y. x <= y ==> f x <= f y"
781 also assume "b <= c" hence "f b <= f c" by (rule r)
782 finally (ord_eq_le_trans) show ?thesis .
785 lemma ord_less_eq_subst: "a < b ==> f b = c ==>
786 (!!x y. x < y ==> f x < f y) ==> f a < c"
788 assume r: "!!x y. x < y ==> f x < f y"
789 assume "a < b" hence "f a < f b" by (rule r)
790 also assume "f b = c"
791 finally (ord_less_eq_trans) show ?thesis .
794 lemma ord_eq_less_subst: "a = f b ==> b < c ==>
795 (!!x y. x < y ==> f x < f y) ==> a < f c"
797 assume r: "!!x y. x < y ==> f x < f y"
799 also assume "b < c" hence "f b < f c" by (rule r)
800 finally (ord_eq_less_trans) show ?thesis .
804 Note that this list of rules is in reverse order of priorities.
825 lemmas (in order) [trans] =
829 lemmas (in preorder) [trans] =
836 lemmas (in order) [trans] =
839 lemmas (in ord) [trans] =
848 lemmas order_trans_rules =
881 text {* These support proving chains of decreasing inequalities
882 a >= b >= c ... in Isar proofs. *}
885 "a = b ==> b > c ==> a > c"
886 "a > b ==> b = c ==> a > c"
887 "a = b ==> b >= c ==> a >= c"
888 "a >= b ==> b = c ==> a >= c"
889 "(x::'a::order) >= y ==> y >= x ==> x = y"
890 "(x::'a::order) >= y ==> y >= z ==> x >= z"
891 "(x::'a::order) > y ==> y >= z ==> x > z"
892 "(x::'a::order) >= y ==> y > z ==> x > z"
893 "(a::'a::order) > b ==> b > a ==> P"
894 "(x::'a::order) > y ==> y > z ==> x > z"
895 "(a::'a::order) >= b ==> a ~= b ==> a > b"
896 "(a::'a::order) ~= b ==> a >= b ==> a > b"
897 "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c"
898 "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
899 "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
900 "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
904 "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
905 by (subgoal_tac "f b >= f c", force, force)
907 lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
908 (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
909 by (subgoal_tac "f a >= f b", force, force)
911 lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
912 (!!x y. x >= y ==> f x >= f y) ==> a > f c"
913 by (subgoal_tac "f b >= f c", force, force)
915 lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
916 (!!x y. x > y ==> f x > f y) ==> f a > c"
917 by (subgoal_tac "f a > f b", force, force)
919 lemma xt6: "(a::'a::order) >= f b ==> b > c ==>
920 (!!x y. x > y ==> f x > f y) ==> a > f c"
921 by (subgoal_tac "f b > f c", force, force)
923 lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
924 (!!x y. x >= y ==> f x >= f y) ==> f a > c"
925 by (subgoal_tac "f a >= f b", force, force)
927 lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
928 (!!x y. x > y ==> f x > f y) ==> a > f c"
929 by (subgoal_tac "f b > f c", force, force)
931 lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
932 (!!x y. x > y ==> f x > f y) ==> f a > c"
933 by (subgoal_tac "f a > f b", force, force)
935 lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
938 Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
939 for the wrong thing in an Isar proof.
941 The extra transitivity rules can be used as follows:
943 lemma "(a::'a::order) > z"
945 have "a >= b" (is "_ >= ?rhs")
947 also have "?rhs >= c" (is "_ >= ?rhs")
949 also (xtrans) have "?rhs = d" (is "_ = ?rhs")
951 also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
953 also (xtrans) have "?rhs > f" (is "_ > ?rhs")
955 also (xtrans) have "?rhs > z"
957 finally (xtrans) show ?thesis .
960 Alternatively, one can use "declare xtrans [trans]" and then
961 leave out the "(xtrans)" above.
965 subsection {* Monotonicity, least value operator and min/max *}
970 definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
971 "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
973 lemma monoI [intro?]:
974 fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
975 shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
976 unfolding mono_def by iprover
979 fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
980 shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
981 unfolding mono_def by iprover
983 definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
984 "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
986 lemma strict_monoI [intro?]:
987 assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
988 shows "strict_mono f"
989 using assms unfolding strict_mono_def by auto
991 lemma strict_monoD [dest?]:
992 "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
993 unfolding strict_mono_def by auto
995 lemma strict_mono_mono [dest?]:
996 assumes "strict_mono f"
1001 show "f x \<le> f y"
1002 proof (cases "x = y")
1003 case True then show ?thesis by simp
1005 case False with `x \<le> y` have "x < y" by simp
1006 with assms strict_monoD have "f x < f y" by auto
1007 then show ?thesis by simp
1016 lemma strict_mono_eq:
1017 assumes "strict_mono f"
1018 shows "f x = f y \<longleftrightarrow> x = y"
1021 show "x = y" proof (cases x y rule: linorder_cases)
1022 case less with assms strict_monoD have "f x < f y" by auto
1023 with `f x = f y` show ?thesis by simp
1025 case equal then show ?thesis .
1027 case greater with assms strict_monoD have "f y < f x" by auto
1028 with `f x = f y` show ?thesis by simp
1032 lemma strict_mono_less_eq:
1033 assumes "strict_mono f"
1034 shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
1037 with assms strict_mono_mono monoD show "f x \<le> f y" by auto
1039 assume "f x \<le> f y"
1040 show "x \<le> y" proof (rule ccontr)
1041 assume "\<not> x \<le> y" then have "y < x" by simp
1042 with assms strict_monoD have "f y < f x" by auto
1043 with `f x \<le> f y` show False by simp
1047 lemma strict_mono_less:
1048 assumes "strict_mono f"
1049 shows "f x < f y \<longleftrightarrow> x < y"
1051 by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
1054 fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1055 shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
1056 by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
1059 fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
1060 shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
1061 by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
1065 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
1066 by (simp add: min_def)
1068 lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
1069 by (simp add: max_def)
1071 lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
1072 apply (simp add: min_def)
1073 apply (blast intro: order_antisym)
1076 lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
1077 apply (simp add: max_def)
1078 apply (blast intro: order_antisym)
1082 subsection {* Top and bottom elements *}
1084 class top = preorder +
1086 assumes top_greatest [simp]: "x \<le> top"
1088 class bot = preorder +
1090 assumes bot_least [simp]: "bot \<le> x"
1093 subsection {* Dense orders *}
1095 class dense_linear_order = linorder +
1096 assumes gt_ex: "\<exists>y. x < y"
1097 and lt_ex: "\<exists>y. y < x"
1098 and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
1101 subsection {* Wellorders *}
1103 class wellorder = linorder +
1104 assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
1107 lemma wellorder_Least_lemma:
1110 shows "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k"
1112 have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
1113 using assms proof (induct k rule: less_induct)
1114 case (less x) then have "P x" by simp
1115 show ?case proof (rule classical)
1116 assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
1117 have "\<And>y. P y \<Longrightarrow> x \<le> y"
1118 proof (rule classical)
1120 assume "P y" and "\<not> x \<le> y"
1121 with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
1122 by (auto simp add: not_le)
1123 with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
1125 then show "x \<le> y" by auto
1127 with `P x` have Least: "(LEAST a. P a) = x"
1128 by (rule Least_equality)
1129 with `P x` show ?thesis by simp
1132 then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
1135 lemmas LeastI = wellorder_Least_lemma(1)
1136 lemmas Least_le = wellorder_Least_lemma(2)
1138 -- "The following 3 lemmas are due to Brian Huffman"
1139 lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
1140 by (erule exE) (erule LeastI)
1143 "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
1144 by (blast intro: LeastI)
1147 "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
1148 by (blast intro: LeastI_ex)
1150 lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
1151 apply (simp (no_asm_use) add: not_le [symmetric])
1152 apply (erule contrapos_nn)
1153 apply (erule Least_le)
1159 subsection {* Order on bool *}
1161 instantiation bool :: "{order, top, bot}"
1165 le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
1168 less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
1171 top_bool_eq: "top = True"
1174 bot_bool_eq: "bot = False"
1177 qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
1181 lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
1182 by (simp add: le_bool_def)
1184 lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
1185 by (simp add: le_bool_def)
1187 lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
1188 by (simp add: le_bool_def)
1190 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
1191 by (simp add: le_bool_def)
1194 "False \<le> b \<longleftrightarrow> True"
1195 "True \<le> b \<longleftrightarrow> b"
1196 "False < b \<longleftrightarrow> b"
1197 "True < b \<longleftrightarrow> False"
1198 unfolding le_bool_def less_bool_def by simp_all
1201 subsection {* Order on functions *}
1203 instantiation "fun" :: (type, ord) ord
1207 le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
1210 less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
1216 instance "fun" :: (type, preorder) preorder proof
1217 qed (auto simp add: le_fun_def less_fun_def
1218 intro: order_trans order_antisym intro!: ext)
1220 instance "fun" :: (type, order) order proof
1221 qed (auto simp add: le_fun_def intro: order_antisym ext)
1223 instantiation "fun" :: (type, top) top
1227 top_fun_eq: "top = (\<lambda>x. top)"
1230 qed (simp add: top_fun_eq le_fun_def)
1234 instantiation "fun" :: (type, bot) bot
1238 bot_fun_eq: "bot = (\<lambda>x. bot)"
1241 qed (simp add: bot_fun_eq le_fun_def)
1245 lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
1246 unfolding le_fun_def by simp
1248 lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
1249 unfolding le_fun_def by simp
1251 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
1252 unfolding le_fun_def by simp
1255 Handy introduction and elimination rules for @{text "\<le>"}
1256 on unary and binary predicates
1260 assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
1262 apply (rule le_funI)
1263 apply (rule le_boolI)
1268 lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
1269 apply (erule le_funE)
1270 apply (erule le_boolE)
1274 lemma predicate2I [Pure.intro!, intro!]:
1275 assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
1277 apply (rule le_funI)+
1278 apply (rule le_boolI)
1283 lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
1284 apply (erule le_funE)+
1285 apply (erule le_boolE)
1289 lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
1290 by (rule predicate1D)
1292 lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
1293 by (rule predicate2D)