src/HOL/Ord.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5673 5dc45f449198
child 6073 fba734ba6894
permissions -rw-r--r--
tidying
     1 (*  Title:      HOL/Ord.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The type class for ordered types
     7 *)
     8 
     9 (*Tell Blast_tac about overloading of < and <= to reduce the risk of
    10   its applying a rule for the wrong type*)
    11 Blast.overloaded ("op <", domain_type); 
    12 Blast.overloaded ("op <=", domain_type);
    13 
    14 (** mono **)
    15 
    16 val [prem] = Goalw [mono_def]
    17     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
    18 by (REPEAT (ares_tac [allI, impI, prem] 1));
    19 qed "monoI";
    20 
    21 Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
    22 by (Fast_tac 1);
    23 qed "monoD";
    24 
    25 
    26 section "Orders";
    27 
    28 (** Reflexivity **)
    29 
    30 Addsimps [order_refl];
    31 
    32 (*This form is useful with the classical reasoner*)
    33 Goal "!!x::'a::order. x = y ==> x <= y";
    34 by (etac ssubst 1);
    35 by (rtac order_refl 1);
    36 qed "order_eq_refl";
    37 
    38 Goal "~ x < (x::'a::order)";
    39 by (simp_tac (simpset() addsimps [order_less_le]) 1);
    40 qed "order_less_irrefl";
    41 Addsimps [order_less_irrefl];
    42 
    43 Goal "(x::'a::order) <= y = (x < y | x = y)";
    44 by (simp_tac (simpset() addsimps [order_less_le]) 1);
    45    (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
    46 by (blast_tac (claset() addSIs [order_refl]) 1);
    47 qed "order_le_less";
    48 
    49 (** Asymmetry **)
    50 
    51 Goal "(x::'a::order) < y ==> ~ (y<x)";
    52 by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
    53 qed "order_less_not_sym";
    54 
    55 (* [| n<m;  ~P ==> m<n |] ==> P *)
    56 bind_thm ("order_less_asym", order_less_not_sym RS swap);
    57 
    58 
    59 (** Useful for simplification, but too risky to include by default. **)
    60 
    61 Goal "(x::'a::order) < y ==>  (~ y < x) = True";
    62 by (blast_tac (claset() addEs [order_less_asym]) 1);
    63 qed "order_less_imp_not_less";
    64 
    65 Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
    66 by (blast_tac (claset() addEs [order_less_asym]) 1);
    67 qed "order_less_imp_triv";
    68 
    69 Goal "(x::'a::order) < y ==>  (x = y) = False";
    70 by Auto_tac;
    71 qed "order_less_imp_not_eq";
    72 
    73 Goal "(x::'a::order) < y ==>  (y = x) = False";
    74 by Auto_tac;
    75 qed "order_less_imp_not_eq2";
    76 
    77 
    78 (** min **)
    79 
    80 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
    81 by (simp_tac (simpset() addsimps prems) 1);
    82 qed "min_leastL";
    83 
    84 val prems = Goalw [min_def]
    85  "(!!x::'a::order. least <= x) ==> min x least = least";
    86 by (cut_facts_tac prems 1);
    87 by (Asm_simp_tac 1);
    88 by (blast_tac (claset() addIs [order_antisym]) 1);
    89 qed "min_leastR";
    90 
    91 
    92 section "Linear/Total Orders";
    93 
    94 Goal "!!x::'a::linorder. x<y | x=y | y<x";
    95 by (simp_tac (simpset() addsimps [order_less_le]) 1);
    96 by (cut_facts_tac [linorder_linear] 1);
    97 by (Blast_tac 1);
    98 qed "linorder_less_linear";
    99 
   100 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
   101 by (Simp_tac 1);
   102 by (cut_facts_tac [linorder_linear] 1);
   103 by (blast_tac (claset() addIs [order_trans]) 1);
   104 qed "le_max_iff_disj";
   105 
   106 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
   107 by (Simp_tac 1);
   108 by (cut_facts_tac [linorder_linear] 1);
   109 by (blast_tac (claset() addIs [order_trans]) 1);
   110 qed "max_le_iff_conj";
   111 Addsimps [max_le_iff_conj];
   112 
   113 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
   114 by (Simp_tac 1);
   115 by (cut_facts_tac [linorder_linear] 1);
   116 by (blast_tac (claset() addIs [order_trans]) 1);
   117 qed "le_min_iff_conj";
   118 Addsimps [le_min_iff_conj];
   119 (* AddIffs screws up a blast_tac in MiniML *)
   120 
   121 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
   122 by (Simp_tac 1);
   123 by (cut_facts_tac [linorder_linear] 1);
   124 by (blast_tac (claset() addIs [order_trans]) 1);
   125 qed "min_le_iff_disj";
   126 
   127 Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
   128 by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
   129 by Auto_tac;
   130 qed "linorder_neq_iff";
   131 
   132 (*** eliminates ~= in premises ***)
   133 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);