src/HOL/Ord.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6301 08245f5a436d
child 6433 228237ec56e5
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 AddIffs [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 (* Transitivity *)
    59 
    60 Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
    61 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
    62 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
    63 qed "order_less_trans";
    64 
    65 
    66 (** Useful for simplification, but too risky to include by default. **)
    67 
    68 Goal "(x::'a::order) < y ==>  (~ y < x) = True";
    69 by (blast_tac (claset() addEs [order_less_asym]) 1);
    70 qed "order_less_imp_not_less";
    71 
    72 Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
    73 by (blast_tac (claset() addEs [order_less_asym]) 1);
    74 qed "order_less_imp_triv";
    75 
    76 Goal "(x::'a::order) < y ==>  (x = y) = False";
    77 by Auto_tac;
    78 qed "order_less_imp_not_eq";
    79 
    80 Goal "(x::'a::order) < y ==>  (y = x) = False";
    81 by Auto_tac;
    82 qed "order_less_imp_not_eq2";
    83 
    84 
    85 (** min **)
    86 
    87 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
    88 by (simp_tac (simpset() addsimps prems) 1);
    89 qed "min_leastL";
    90 
    91 val prems = Goalw [min_def]
    92  "(!!x::'a::order. least <= x) ==> min x least = least";
    93 by (cut_facts_tac prems 1);
    94 by (Asm_simp_tac 1);
    95 by (blast_tac (claset() addIs [order_antisym]) 1);
    96 qed "min_leastR";
    97 
    98 
    99 section "Linear/Total Orders";
   100 
   101 Goal "!!x::'a::linorder. x<y | x=y | y<x";
   102 by (simp_tac (simpset() addsimps [order_less_le]) 1);
   103 by (cut_facts_tac [linorder_linear] 1);
   104 by (Blast_tac 1);
   105 qed "linorder_less_linear";
   106 
   107 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
   108 by (simp_tac (simpset() addsimps [order_less_le]) 1);
   109 by (cut_facts_tac [linorder_linear] 1);
   110 by (blast_tac (claset() addIs [order_antisym]) 1);
   111 qed "linorder_not_less";
   112 
   113 Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
   114 by (simp_tac (simpset() addsimps [order_less_le]) 1);
   115 by (cut_facts_tac [linorder_linear] 1);
   116 by (blast_tac (claset() addIs [order_antisym]) 1);
   117 qed "linorder_not_le";
   118 
   119 Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
   120 by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
   121 by Auto_tac;
   122 qed "linorder_neq_iff";
   123 
   124 (* eliminates ~= in premises *)
   125 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
   126 
   127 (** min & max **)
   128 
   129 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
   130 by (Simp_tac 1);
   131 by (cut_facts_tac [linorder_linear] 1);
   132 by (blast_tac (claset() addIs [order_trans]) 1);
   133 qed "le_max_iff_disj";
   134 
   135 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
   136 by (simp_tac (simpset() addsimps [order_le_less]) 1);
   137 by (cut_facts_tac [linorder_less_linear] 1);
   138 by (blast_tac (claset() addIs [order_less_trans]) 1);
   139 qed "less_max_iff_disj";
   140 
   141 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
   142 by (Simp_tac 1);
   143 by (cut_facts_tac [linorder_linear] 1);
   144 by (blast_tac (claset() addIs [order_trans]) 1);
   145 qed "max_le_iff_conj";
   146 Addsimps [max_le_iff_conj];
   147 
   148 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
   149 by (Simp_tac 1);
   150 by (cut_facts_tac [linorder_linear] 1);
   151 by (blast_tac (claset() addIs [order_trans]) 1);
   152 qed "le_min_iff_conj";
   153 Addsimps [le_min_iff_conj];
   154 (* AddIffs screws up a blast_tac in MiniML *)
   155 
   156 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
   157 by (Simp_tac 1);
   158 by (cut_facts_tac [linorder_linear] 1);
   159 by (blast_tac (claset() addIs [order_trans]) 1);
   160 qed "min_le_iff_disj";
   161 
   162 Goalw [min_def]
   163  "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
   164 by (Simp_tac 1);
   165 qed "split_min";
   166 
   167 Goalw [max_def]
   168  "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
   169 by (Simp_tac 1);
   170 qed "split_max";