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