src/HOL/SetInterval.ML
author wenzelm
Thu Jul 13 23:09:03 2000 +0200 (2000-07-13)
changeset 9310 ab706fdb0842
parent 8956 a7c3538fc2d2
child 13596 ee5f79b210c1
permissions -rw-r--r--
removed duplicate Compl_atMost;
paulson@8956
     1
(*  Title:      HOL/SetInterval.ML
paulson@8956
     2
    ID:         $Id$
paulson@8956
     3
    Author:     Tobias Nipkow
paulson@8956
     4
    Copyright   2000  TU Muenchen
paulson@8956
     5
paulson@8956
     6
Set Intervals: lessThan, greaterThan, atLeast, atMost
paulson@8956
     7
*)
paulson@8956
     8
paulson@8956
     9
paulson@8956
    10
(*** lessThan ***)
paulson@8956
    11
paulson@8956
    12
Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
paulson@8956
    13
by (Blast_tac 1);
paulson@8956
    14
qed "lessThan_iff";
paulson@8956
    15
AddIffs [lessThan_iff];
paulson@8956
    16
paulson@8956
    17
Goalw [lessThan_def] "lessThan (0::nat) = {}";
paulson@8956
    18
by (Simp_tac 1);
paulson@8956
    19
qed "lessThan_0";
paulson@8956
    20
Addsimps [lessThan_0];
paulson@8956
    21
paulson@8956
    22
Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
paulson@8956
    23
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
paulson@8956
    24
by (Blast_tac 1);
paulson@8956
    25
qed "lessThan_Suc";
paulson@8956
    26
paulson@8956
    27
Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
paulson@8956
    28
by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
paulson@8956
    29
qed "lessThan_Suc_atMost";
paulson@8956
    30
paulson@8956
    31
Goal "(UN m::nat. lessThan m) = UNIV";
paulson@8956
    32
by (Blast_tac 1);
paulson@8956
    33
qed "UN_lessThan_UNIV";
paulson@8956
    34
paulson@8956
    35
Goalw [lessThan_def, atLeast_def]
paulson@8956
    36
    "!!k:: 'a::linorder. -lessThan k = atLeast k";
paulson@8956
    37
by Auto_tac;
paulson@8956
    38
by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
paulson@8956
    39
by (blast_tac (claset() addIs [order_le_less_trans RS 
paulson@8956
    40
	                       (order_less_irrefl RS notE)]) 1);
paulson@8956
    41
qed "Compl_lessThan";
paulson@8956
    42
paulson@8956
    43
Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
paulson@8956
    44
by Auto_tac;
paulson@8956
    45
qed "single_Diff_lessThan";
paulson@8956
    46
Addsimps [single_Diff_lessThan];
paulson@8956
    47
paulson@8956
    48
(*** greaterThan ***)
paulson@8956
    49
paulson@8956
    50
Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
paulson@8956
    51
by (Blast_tac 1);
paulson@8956
    52
qed "greaterThan_iff";
paulson@8956
    53
AddIffs [greaterThan_iff];
paulson@8956
    54
paulson@8956
    55
Goalw [greaterThan_def] "greaterThan 0 = range Suc";
paulson@8956
    56
by (blast_tac (claset() addDs [gr0_conv_Suc RS iffD1]) 1);
paulson@8956
    57
qed "greaterThan_0";
paulson@8956
    58
Addsimps [greaterThan_0];
paulson@8956
    59
paulson@8956
    60
Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
paulson@8956
    61
by (auto_tac (claset() addEs [linorder_neqE], simpset()));
paulson@8956
    62
qed "greaterThan_Suc";
paulson@8956
    63
paulson@8956
    64
Goal "(INT m::nat. greaterThan m) = {}";
paulson@8956
    65
by (Blast_tac 1);
paulson@8956
    66
qed "INT_greaterThan_UNIV";
paulson@8956
    67
paulson@8956
    68
Goalw [greaterThan_def, atMost_def, le_def]
paulson@8956
    69
    "!!k:: 'a::linorder. -greaterThan k = atMost k";
paulson@8956
    70
by Auto_tac;
paulson@8956
    71
by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
paulson@8956
    72
by (blast_tac (claset() addIs [order_le_less_trans RS 
paulson@8956
    73
	                       (order_less_irrefl RS notE)]) 1);
paulson@8956
    74
qed "Compl_greaterThan";
paulson@8956
    75
paulson@8956
    76
Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
paulson@8956
    77
by (simp_tac (simpset() addsimps [Compl_greaterThan RS sym]) 1);
paulson@8956
    78
qed "Compl_atMost";
paulson@8956
    79
paulson@8956
    80
Addsimps [Compl_greaterThan, Compl_atMost];
paulson@8956
    81
paulson@8956
    82
(*** atLeast ***)
paulson@8956
    83
paulson@8956
    84
Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
paulson@8956
    85
by (Blast_tac 1);
paulson@8956
    86
qed "atLeast_iff";
paulson@8956
    87
AddIffs [atLeast_iff];
paulson@8956
    88
paulson@8956
    89
Goalw [atLeast_def, UNIV_def] "atLeast (0::nat) = UNIV";
paulson@8956
    90
by (Simp_tac 1);
paulson@8956
    91
qed "atLeast_0";
paulson@8956
    92
Addsimps [atLeast_0];
paulson@8956
    93
paulson@8956
    94
Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
paulson@8956
    95
by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
paulson@8956
    96
by (simp_tac (simpset() addsimps [order_le_less]) 1);
paulson@8956
    97
by (Blast_tac 1);
paulson@8956
    98
qed "atLeast_Suc";
paulson@8956
    99
paulson@8956
   100
Goal "(UN m::nat. atLeast m) = UNIV";
paulson@8956
   101
by (Blast_tac 1);
paulson@8956
   102
qed "UN_atLeast_UNIV";
paulson@8956
   103
paulson@8956
   104
Goalw [lessThan_def, atLeast_def, le_def]
paulson@8956
   105
    "!!k:: 'a::linorder. -atLeast k = lessThan k";
paulson@8956
   106
by Auto_tac;
paulson@8956
   107
by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
paulson@8956
   108
by (blast_tac (claset() addIs [order_le_less_trans RS 
paulson@8956
   109
	                       (order_less_irrefl RS notE)]) 1);
paulson@8956
   110
qed "Compl_atLeast";
paulson@8956
   111
paulson@8956
   112
Addsimps [Compl_lessThan, Compl_atLeast];
paulson@8956
   113
paulson@8956
   114
(*** atMost ***)
paulson@8956
   115
paulson@8956
   116
Goalw [atMost_def] "(i: atMost k) = (i<=k)";
paulson@8956
   117
by (Blast_tac 1);
paulson@8956
   118
qed "atMost_iff";
paulson@8956
   119
AddIffs [atMost_iff];
paulson@8956
   120
paulson@8956
   121
Goalw [atMost_def] "atMost (0::nat) = {0}";
paulson@8956
   122
by (Simp_tac 1);
paulson@8956
   123
qed "atMost_0";
paulson@8956
   124
Addsimps [atMost_0];
paulson@8956
   125
paulson@8956
   126
Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
paulson@8956
   127
by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
paulson@8956
   128
by (Blast_tac 1);
paulson@8956
   129
qed "atMost_Suc";
paulson@8956
   130
paulson@8956
   131
Goal "(UN m::nat. atMost m) = UNIV";
paulson@8956
   132
by (Blast_tac 1);
paulson@8956
   133
qed "UN_atMost_UNIV";
paulson@8956
   134
paulson@8956
   135
paulson@8956
   136
(*** Combined properties ***)
paulson@8956
   137
paulson@8956
   138
Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
paulson@8956
   139
by (blast_tac (claset() addIs [order_antisym]) 1);
paulson@8956
   140
qed "atMost_Int_atLeast";