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