wneuper/isa: src/HOL/Ord.ML@199721f2eb2d

     1 (*  Title:      HOL/Ord.ML

     2     ID:         $Id$

     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory

     4     Copyright   1993  University of Cambridge

     6 The type class for ordered types

     7 *)

     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);

    14 (** mono **)

    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];

    22 Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";

    23 by (Fast_tac 1);

    24 qed "monoD";

    25 AddXDs [monoD];

    28 section "Orders";

    30 (** Reflexivity **)

    32 AddIffs [order_refl];

    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";

    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];

    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";

    51 (** Asymmetry **)

    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";

    57 (* [| n<m;  ~P ==> m<n |] ==> P *)

    58 bind_thm ("order_less_asym", order_less_not_sym RS swap);

    60 (* Transitivity *)

    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";

    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";

    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";

    78 (** Useful for simplification, but too risky to include by default. **)

    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";

    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";

    88 Goal "(x::'a::order) < y ==>  (x = y) = False";

    89 by Auto_tac;

    90 qed "order_less_imp_not_eq";

    92 Goal "(x::'a::order) < y ==>  (y = x) = False";

    93 by Auto_tac;

    94 qed "order_less_imp_not_eq2";

    97 (** min **)

    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";

   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";

   111 section "Linear/Total Orders";

   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";

   119 val prems = goal thy

   120  "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";

   121 by(cut_facts_tac [linorder_less_linear] 1);

   122 by(REPEAT(eresolve_tac (prems@[disjE]) 1));

   123 qed "linorder_less_split";

   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_less";

   131 Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";

   132 by (simp_tac (simpset() addsimps [order_less_le]) 1);

   133 by (cut_facts_tac [linorder_linear] 1);

   134 by (blast_tac (claset() addIs [order_antisym]) 1);

   135 qed "linorder_not_le";

   137 Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";

   138 by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);

   139 by Auto_tac;

   140 qed "linorder_neq_iff";

   142 (* eliminates ~= in premises *)

   143 bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);

   145 (** min & max **)

   147 Goalw [min_def] "min (x::'a::order) x = x";

   148 by (Simp_tac 1);

   149 qed "min_same";

   150 Addsimps [min_same];

   152 Goalw [max_def] "max (x::'a::order) x = x";

   153 by (Simp_tac 1);

   154 qed "max_same";

   155 Addsimps [max_same];

   157 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";

   158 by (Simp_tac 1);

   159 by (cut_facts_tac [linorder_linear] 1);

   160 by (blast_tac (claset() addIs [order_trans]) 1);

   161 qed "le_max_iff_disj";

   163 qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y"

   164 	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);

   165 qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y"

   166 	(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);

   167 (*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)

   169 Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";

   170 by (simp_tac (simpset() addsimps [order_le_less]) 1);

   171 by (cut_facts_tac [linorder_less_linear] 1);

   172 by (blast_tac (claset() addIs [order_less_trans]) 1);

   173 qed "less_max_iff_disj";

   175 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";

   176 by (Simp_tac 1);

   177 by (cut_facts_tac [linorder_linear] 1);

   178 by (blast_tac (claset() addIs [order_trans]) 1);

   179 qed "max_le_iff_conj";

   180 Addsimps [max_le_iff_conj];

   182 Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";

   183 by (simp_tac (simpset() addsimps [order_le_less]) 1);

   184 by (cut_facts_tac [linorder_less_linear] 1);

   185 by (blast_tac (claset() addIs [order_less_trans]) 1);

   186 qed "max_less_iff_conj";

   187 Addsimps [max_less_iff_conj];

   189 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";

   190 by (Simp_tac 1);

   191 by (cut_facts_tac [linorder_linear] 1);

   192 by (blast_tac (claset() addIs [order_trans]) 1);

   193 qed "le_min_iff_conj";

   194 Addsimps [le_min_iff_conj];

   195 (* AddIffs screws up a blast_tac in MiniML *)

   197 Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";

   198 by (simp_tac (simpset() addsimps [order_le_less]) 1);

   199 by (cut_facts_tac [linorder_less_linear] 1);

   200 by (blast_tac (claset() addIs [order_less_trans]) 1);

   201 qed "min_less_iff_conj";

   202 Addsimps [min_less_iff_conj];

   204 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";

   205 by (Simp_tac 1);

   206 by (cut_facts_tac [linorder_linear] 1);

   207 by (blast_tac (claset() addIs [order_trans]) 1);

   208 qed "min_le_iff_disj";

   210 Goalw [min_def]

   211  "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";

   212 by (Simp_tac 1);

   213 qed "split_min";

   215 Goalw [max_def]

   216  "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";

   217 by (Simp_tac 1);

   218 qed "split_max";

author	nipkow
	Mon, 22 Nov 1999 12:10:27 +0100
changeset 8024	199721f2eb2d
parent 7617	e783adccf39e
child 8214	d612354445b6
permissions	-rw-r--r--