src/HOL/Ord.ML

Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED

(*  Title:      HOL/Ord.ML
    ID:         $Id$
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

The type class for ordered types
*)

(*Tell Blast_tac about overloading of < and <= to reduce the risk of
  its applying a rule for the wrong type*)
Blast.overloaded ("op <", domain_type); 
Blast.overloaded ("op <=", domain_type);

(** mono **)

val [prem] = Goalw [mono_def]
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
by (REPEAT (ares_tac [allI, impI, prem] 1));
qed "monoI";

Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
by (Fast_tac 1);
qed "monoD";


section "Orders";

Addsimps [order_refl];

(*This form is useful with the classical reasoner*)
Goal "!!x::'a::order. x = y ==> x <= y";
by (etac ssubst 1);
by (rtac order_refl 1);
qed "order_eq_refl";

Goal "~ x < (x::'a::order)";
by (simp_tac (simpset() addsimps [order_less_le]) 1);
qed "order_less_irrefl";
Addsimps [order_less_irrefl];

Goal "(x::'a::order) <= y = (x < y | x = y)";
by (simp_tac (simpset() addsimps [order_less_le]) 1);
   (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
by (blast_tac (claset() addSIs [order_refl]) 1);
qed "order_le_less";

(** min **)

val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
by (simp_tac (simpset() addsimps prems) 1);
qed "min_leastL";

val prems = Goalw [min_def]
 "(!!x::'a::order. least <= x) ==> min x least = least";
by (cut_facts_tac prems 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [order_antisym]) 1);
qed "min_leastR";


section "Linear/Total Orders";

Goal "!!x::'a::linorder. x<y | x=y | y<x";
by (simp_tac (simpset() addsimps [order_less_le]) 1);
by (cut_facts_tac [linorder_linear] 1);
by (Blast_tac 1);
qed "linorder_less_linear";

Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
by (Simp_tac 1);
by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_max_iff_disj";

Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
by (Simp_tac 1);
by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "max_le_iff_conj";

Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
by (Simp_tac 1);
by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_min_iff_conj";

Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
by (Simp_tac 1);
by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "min_le_iff_disj";