src/HOL/Ord.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7494 45905028bb1d
child 7617 e783adccf39e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 AddXIs [monoI];
    21 
    22 Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
    23 by (Fast_tac 1);
    24 qed "monoD";
    25 AddXDs [monoD];
    26 
    27 
    28 section "Orders";
    29 
    30 (** Reflexivity **)
    31 
    32 AddIffs [order_refl];
    33 
    34 (*This form is useful with the classical reasoner*)
    35 Goal "!!x::'a::order. x = y ==> x <= y";
    36 by (etac ssubst 1);
    37 by (rtac order_refl 1);
    38 qed "order_eq_refl";
    39 
    40 Goal "~ x < (x::'a::order)";
    41 by (simp_tac (simpset() addsimps [order_less_le]) 1);
    42 qed "order_less_irrefl";
    43 Addsimps [order_less_irrefl];
    44 
    45 Goal "(x::'a::order) <= y = (x < y | x = y)";
    46 by (simp_tac (simpset() addsimps [order_less_le]) 1);
    47    (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
    48 by (blast_tac (claset() addSIs [order_refl]) 1);
    49 qed "order_le_less";
    50 
    51 (** Asymmetry **)
    52 
    53 Goal "(x::'a::order) < y ==> ~ (y<x)";
    54 by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
    55 qed "order_less_not_sym";
    56 
    57 (* [| n<m;  ~P ==> m<n |] ==> P *)
    58 bind_thm ("order_less_asym", order_less_not_sym RS swap);
    59 
    60 (* Transitivity *)
    61 
    62 Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
    63 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
    64 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
    65 qed "order_less_trans";
    66 
    67 Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z";
    68 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
    69 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
    70 qed "order_le_less_trans";
    71 
    72 Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z";
    73 by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
    74 by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
    75 qed "order_less_le_trans";
    76 
    77 
    78 (** Useful for simplification, but too risky to include by default. **)
    79 
    80 Goal "(x::'a::order) < y ==>  (~ y < x) = True";
    81 by (blast_tac (claset() addEs [order_less_asym]) 1);
    82 qed "order_less_imp_not_less";
    83 
    84 Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
    85 by (blast_tac (claset() addEs [order_less_asym]) 1);
    86 qed "order_less_imp_triv";
    87 
    88 Goal "(x::'a::order) < y ==>  (x = y) = False";
    89 by Auto_tac;
    90 qed "order_less_imp_not_eq";
    91 
    92 Goal "(x::'a::order) < y ==>  (y = x) = False";
    93 by Auto_tac;
    94 qed "order_less_imp_not_eq2";
    95 
    96 
    97 (** min **)
    98 
    99 val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
   100 by (simp_tac (simpset() addsimps prems) 1);
   101 qed "min_leastL";
   102 
   103 val prems = Goalw [min_def]
   104  "(!!x::'a::order. least <= x) ==> min x least = least";
   105 by (cut_facts_tac prems 1);
   106 by (Asm_simp_tac 1);
   107 by (blast_tac (claset() addIs [order_antisym]) 1);
   108 qed "min_leastR";
   109 
   110 
   111 section "Linear/Total Orders";
   112 
   113 Goal "!!x::'a::linorder. x<y | 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 1);
   117 qed "linorder_less_linear";
   118 
   119 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
   120 by (simp_tac (simpset() addsimps [order_less_le]) 1);
   121 by (cut_facts_tac [linorder_linear] 1);
   122 by (blast_tac (claset() addIs [order_antisym]) 1);
   123 qed "linorder_not_less";
   124 
   125 Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
   126 by (simp_tac (simpset() addsimps [order_less_le]) 1);
   127 by (cut_facts_tac [linorder_linear] 1);
   128 by (blast_tac (claset() addIs [order_antisym]) 1);
   129 qed "linorder_not_le";
   130 
   131 Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
   132 by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
   133 by Auto_tac;
   134 qed "linorder_neq_iff";
   135 
   136 (* eliminates ~= in premises *)
   137 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
   138 
   139 (** min & max **)
   140 
   141 Goalw [min_def] "min (x::'a::order) x = x";
   142 by (Simp_tac 1);
   143 qed "min_same";
   144 Addsimps [min_same];
   145 
   146 Goalw [max_def] "max (x::'a::order) x = x";
   147 by (Simp_tac 1);
   148 qed "max_same";
   149 Addsimps [max_same];
   150 
   151 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
   152 by (Simp_tac 1);
   153 by (cut_facts_tac [linorder_linear] 1);
   154 by (blast_tac (claset() addIs [order_trans]) 1);
   155 qed "le_max_iff_disj";
   156 
   157 qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y" 
   158 	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);
   159 qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y" 
   160 	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);
   161 AddSIs[le_maxI1, le_maxI2];
   162 
   163 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
   164 by (simp_tac (simpset() addsimps [order_le_less]) 1);
   165 by (cut_facts_tac [linorder_less_linear] 1);
   166 by (blast_tac (claset() addIs [order_less_trans]) 1);
   167 qed "less_max_iff_disj";
   168 
   169 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
   170 by (Simp_tac 1);
   171 by (cut_facts_tac [linorder_linear] 1);
   172 by (blast_tac (claset() addIs [order_trans]) 1);
   173 qed "max_le_iff_conj";
   174 Addsimps [max_le_iff_conj];
   175 
   176 Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";
   177 by (simp_tac (simpset() addsimps [order_le_less]) 1);
   178 by (cut_facts_tac [linorder_less_linear] 1);
   179 by (blast_tac (claset() addIs [order_less_trans]) 1);
   180 qed "max_less_iff_conj";
   181 Addsimps [max_less_iff_conj];
   182 
   183 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
   184 by (Simp_tac 1);
   185 by (cut_facts_tac [linorder_linear] 1);
   186 by (blast_tac (claset() addIs [order_trans]) 1);
   187 qed "le_min_iff_conj";
   188 Addsimps [le_min_iff_conj];
   189 (* AddIffs screws up a blast_tac in MiniML *)
   190 
   191 Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";
   192 by (simp_tac (simpset() addsimps [order_le_less]) 1);
   193 by (cut_facts_tac [linorder_less_linear] 1);
   194 by (blast_tac (claset() addIs [order_less_trans]) 1);
   195 qed "min_less_iff_conj";
   196 Addsimps [min_less_iff_conj];
   197 
   198 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
   199 by (Simp_tac 1);
   200 by (cut_facts_tac [linorder_linear] 1);
   201 by (blast_tac (claset() addIs [order_trans]) 1);
   202 qed "min_le_iff_disj";
   203 
   204 Goalw [min_def]
   205  "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
   206 by (Simp_tac 1);
   207 qed "split_min";
   208 
   209 Goalw [max_def]
   210  "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
   211 by (Simp_tac 1);
   212 qed "split_max";