src/HOL/UNITY/LessThan.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/LessThan/LessThan
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
lessThan, greaterThan, atLeast, atMost
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
paulson@4776
    10
open LessThan;
paulson@4776
    11
paulson@4776
    12
paulson@4776
    13
(*** lessThan ***)
paulson@4776
    14
paulson@4776
    15
goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
paulson@4776
    16
by (Blast_tac 1);
paulson@4776
    17
qed "lessThan_iff";
paulson@4776
    18
AddIffs [lessThan_iff];
paulson@4776
    19
paulson@4776
    20
goalw thy [lessThan_def] "lessThan 0 = {}";
paulson@4776
    21
by (Simp_tac 1);
paulson@4776
    22
qed "lessThan_0";
paulson@4776
    23
Addsimps [lessThan_0];
paulson@4776
    24
paulson@4776
    25
goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
paulson@4776
    26
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@4776
    27
by (Blast_tac 1);
paulson@4776
    28
qed "lessThan_Suc";
paulson@4776
    29
paulson@4776
    30
goal thy "(UN m. lessThan m) = UNIV";
paulson@4776
    31
by (Blast_tac 1);
paulson@4776
    32
qed "UN_lessThan_UNIV";
paulson@4776
    33
paulson@4776
    34
goalw thy [lessThan_def, atLeast_def, le_def]
paulson@4776
    35
    "Compl(lessThan k) = atLeast k";
paulson@4776
    36
by (Blast_tac 1);
paulson@4776
    37
qed "Compl_lessThan";
paulson@4776
    38
paulson@4776
    39
paulson@4776
    40
(*** greaterThan ***)
paulson@4776
    41
paulson@4776
    42
goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
paulson@4776
    43
by (Blast_tac 1);
paulson@4776
    44
qed "greaterThan_iff";
paulson@4776
    45
AddIffs [greaterThan_iff];
paulson@4776
    46
paulson@4776
    47
goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
paulson@4776
    48
by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
paulson@4776
    49
qed "greaterThan_0";
paulson@4776
    50
Addsimps [greaterThan_0];
paulson@4776
    51
paulson@4776
    52
goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
paulson@4776
    53
by Safe_tac;
paulson@4776
    54
by (blast_tac (claset() addIs [less_trans]) 1);
paulson@4776
    55
by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
paulson@4776
    56
by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
paulson@4776
    57
qed "greaterThan_Suc";
paulson@4776
    58
paulson@4776
    59
goal thy "(INT m. greaterThan m) = {}";
paulson@4776
    60
by (Blast_tac 1);
paulson@4776
    61
qed "INT_greaterThan_UNIV";
paulson@4776
    62
paulson@4776
    63
goalw thy [greaterThan_def, atMost_def, le_def]
paulson@4776
    64
    "Compl(greaterThan k) = atMost k";
paulson@4776
    65
by (Blast_tac 1);
paulson@4776
    66
qed "Compl_greaterThan";
paulson@4776
    67
paulson@4776
    68
goalw thy [greaterThan_def, atMost_def, le_def]
paulson@4776
    69
    "Compl(atMost k) = greaterThan k";
paulson@4776
    70
by (Blast_tac 1);
paulson@4776
    71
qed "Compl_atMost";
paulson@4776
    72
paulson@4776
    73
goal thy "less_than ^^ {k} = greaterThan k";
paulson@4776
    74
by (Blast_tac 1);
paulson@4776
    75
qed "Image_less_than";
paulson@4776
    76
paulson@4776
    77
Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
paulson@4776
    78
paulson@4776
    79
(*** atLeast ***)
paulson@4776
    80
paulson@4776
    81
goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
paulson@4776
    82
by (Blast_tac 1);
paulson@4776
    83
qed "atLeast_iff";
paulson@4776
    84
AddIffs [atLeast_iff];
paulson@4776
    85
paulson@4776
    86
goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
paulson@4776
    87
by (Simp_tac 1);
paulson@4776
    88
qed "atLeast_0";
paulson@4776
    89
Addsimps [atLeast_0];
paulson@4776
    90
paulson@4776
    91
goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
paulson@4776
    92
by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
paulson@4776
    93
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
paulson@4776
    94
by (Blast_tac 1);
paulson@4776
    95
qed "atLeast_Suc";
paulson@4776
    96
paulson@4776
    97
goal thy "(UN m. atLeast m) = UNIV";
paulson@4776
    98
by (Blast_tac 1);
paulson@4776
    99
qed "UN_atLeast_UNIV";
paulson@4776
   100
paulson@4776
   101
goalw thy [lessThan_def, atLeast_def, le_def]
paulson@4776
   102
    "Compl(atLeast k) = lessThan k";
paulson@4776
   103
by (Blast_tac 1);
paulson@4776
   104
qed "Compl_atLeast";
paulson@4776
   105
paulson@4776
   106
goal thy "less_than^-1 ^^ {k} = lessThan k";
paulson@4776
   107
by (Blast_tac 1);
paulson@4776
   108
qed "Image_inverse_less_than";
paulson@4776
   109
paulson@4776
   110
Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
paulson@4776
   111
paulson@4776
   112
(*** atMost ***)
paulson@4776
   113
paulson@4776
   114
goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
paulson@4776
   115
by (Blast_tac 1);
paulson@4776
   116
qed "atMost_iff";
paulson@4776
   117
AddIffs [atMost_iff];
paulson@4776
   118
paulson@4776
   119
goalw thy [atMost_def] "atMost 0 = {0}";
paulson@4776
   120
by (Simp_tac 1);
paulson@4776
   121
qed "atMost_0";
paulson@4776
   122
Addsimps [atMost_0];
paulson@4776
   123
paulson@4776
   124
goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
paulson@4776
   125
by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
paulson@4776
   126
by (Blast_tac 1);
paulson@4776
   127
qed "atMost_Suc";
paulson@4776
   128
paulson@4776
   129
goal thy "(UN m. atMost m) = UNIV";
paulson@4776
   130
by (Blast_tac 1);
paulson@4776
   131
qed "UN_atMost_UNIV";
paulson@4776
   132
paulson@4776
   133
goalw thy [atMost_def, le_def]
paulson@4776
   134
    "Compl(atMost k) = greaterThan k";
paulson@4776
   135
by (Blast_tac 1);
paulson@4776
   136
qed "Compl_atMost";
paulson@4776
   137
Addsimps [Compl_atMost];
paulson@4776
   138
paulson@4776
   139
paulson@4776
   140
(*** Combined properties ***)
paulson@4776
   141
paulson@4776
   142
goal thy "atMost n Int atLeast n = {n}";
paulson@4776
   143
by (blast_tac (claset() addIs [le_anti_sym]) 1);
paulson@4776
   144
qed "atMost_Int_atLeast";
paulson@4776
   145
paulson@4776
   146