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