src/HOL/SetInterval.ML
changeset 8956 a7c3538fc2d2
child 9310 ab706fdb0842
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SetInterval.ML	Wed May 24 18:45:29 2000 +0200
     1.3 @@ -0,0 +1,152 @@
     1.4 +(*  Title:      HOL/SetInterval.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   2000  TU Muenchen
     1.8 +
     1.9 +Set Intervals: lessThan, greaterThan, atLeast, atMost
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +(*** lessThan ***)
    1.14 +
    1.15 +Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
    1.16 +by (Blast_tac 1);
    1.17 +qed "lessThan_iff";
    1.18 +AddIffs [lessThan_iff];
    1.19 +
    1.20 +Goalw [lessThan_def] "lessThan (0::nat) = {}";
    1.21 +by (Simp_tac 1);
    1.22 +qed "lessThan_0";
    1.23 +Addsimps [lessThan_0];
    1.24 +
    1.25 +Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
    1.26 +by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.27 +by (Blast_tac 1);
    1.28 +qed "lessThan_Suc";
    1.29 +
    1.30 +Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
    1.31 +by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
    1.32 +qed "lessThan_Suc_atMost";
    1.33 +
    1.34 +Goal "(UN m::nat. lessThan m) = UNIV";
    1.35 +by (Blast_tac 1);
    1.36 +qed "UN_lessThan_UNIV";
    1.37 +
    1.38 +Goalw [lessThan_def, atLeast_def]
    1.39 +    "!!k:: 'a::linorder. -lessThan k = atLeast k";
    1.40 +by Auto_tac;
    1.41 +by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    1.42 +by (blast_tac (claset() addIs [order_le_less_trans RS 
    1.43 +	                       (order_less_irrefl RS notE)]) 1);
    1.44 +qed "Compl_lessThan";
    1.45 +
    1.46 +Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
    1.47 +by Auto_tac;
    1.48 +qed "single_Diff_lessThan";
    1.49 +Addsimps [single_Diff_lessThan];
    1.50 +
    1.51 +(*** greaterThan ***)
    1.52 +
    1.53 +Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
    1.54 +by (Blast_tac 1);
    1.55 +qed "greaterThan_iff";
    1.56 +AddIffs [greaterThan_iff];
    1.57 +
    1.58 +Goalw [greaterThan_def] "greaterThan 0 = range Suc";
    1.59 +by (blast_tac (claset() addDs [gr0_conv_Suc RS iffD1]) 1);
    1.60 +qed "greaterThan_0";
    1.61 +Addsimps [greaterThan_0];
    1.62 +
    1.63 +Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
    1.64 +by (auto_tac (claset() addEs [linorder_neqE], simpset()));
    1.65 +qed "greaterThan_Suc";
    1.66 +
    1.67 +Goal "(INT m::nat. greaterThan m) = {}";
    1.68 +by (Blast_tac 1);
    1.69 +qed "INT_greaterThan_UNIV";
    1.70 +
    1.71 +Goalw [greaterThan_def, atMost_def, le_def]
    1.72 +    "!!k:: 'a::linorder. -greaterThan k = atMost k";
    1.73 +by Auto_tac;
    1.74 +by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    1.75 +by (blast_tac (claset() addIs [order_le_less_trans RS 
    1.76 +	                       (order_less_irrefl RS notE)]) 1);
    1.77 +qed "Compl_greaterThan";
    1.78 +
    1.79 +Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
    1.80 +by (simp_tac (simpset() addsimps [Compl_greaterThan RS sym]) 1);
    1.81 +qed "Compl_atMost";
    1.82 +
    1.83 +Addsimps [Compl_greaterThan, Compl_atMost];
    1.84 +
    1.85 +(*** atLeast ***)
    1.86 +
    1.87 +Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
    1.88 +by (Blast_tac 1);
    1.89 +qed "atLeast_iff";
    1.90 +AddIffs [atLeast_iff];
    1.91 +
    1.92 +Goalw [atLeast_def, UNIV_def] "atLeast (0::nat) = UNIV";
    1.93 +by (Simp_tac 1);
    1.94 +qed "atLeast_0";
    1.95 +Addsimps [atLeast_0];
    1.96 +
    1.97 +Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
    1.98 +by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.99 +by (simp_tac (simpset() addsimps [order_le_less]) 1);
   1.100 +by (Blast_tac 1);
   1.101 +qed "atLeast_Suc";
   1.102 +
   1.103 +Goal "(UN m::nat. atLeast m) = UNIV";
   1.104 +by (Blast_tac 1);
   1.105 +qed "UN_atLeast_UNIV";
   1.106 +
   1.107 +Goalw [lessThan_def, atLeast_def, le_def]
   1.108 +    "!!k:: 'a::linorder. -atLeast k = lessThan k";
   1.109 +by Auto_tac;
   1.110 +by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
   1.111 +by (blast_tac (claset() addIs [order_le_less_trans RS 
   1.112 +	                       (order_less_irrefl RS notE)]) 1);
   1.113 +qed "Compl_atLeast";
   1.114 +
   1.115 +Addsimps [Compl_lessThan, Compl_atLeast];
   1.116 +
   1.117 +(*** atMost ***)
   1.118 +
   1.119 +Goalw [atMost_def] "(i: atMost k) = (i<=k)";
   1.120 +by (Blast_tac 1);
   1.121 +qed "atMost_iff";
   1.122 +AddIffs [atMost_iff];
   1.123 +
   1.124 +Goalw [atMost_def] "atMost (0::nat) = {0}";
   1.125 +by (Simp_tac 1);
   1.126 +qed "atMost_0";
   1.127 +Addsimps [atMost_0];
   1.128 +
   1.129 +Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   1.130 +by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
   1.131 +by (Blast_tac 1);
   1.132 +qed "atMost_Suc";
   1.133 +
   1.134 +Goal "(UN m::nat. atMost m) = UNIV";
   1.135 +by (Blast_tac 1);
   1.136 +qed "UN_atMost_UNIV";
   1.137 +
   1.138 +Goalw [atMost_def, le_def]
   1.139 +    "!!k:: 'a::linorder. -atMost k = greaterThan k";
   1.140 +by Auto_tac;
   1.141 +by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
   1.142 +by (blast_tac (claset() addIs [order_le_less_trans RS 
   1.143 +	                       (order_less_irrefl RS notE)]) 1);
   1.144 +qed "Compl_atMost";
   1.145 +Addsimps [Compl_atMost];
   1.146 +
   1.147 +
   1.148 +(*** Combined properties ***)
   1.149 +
   1.150 +Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
   1.151 +by (blast_tac (claset() addIs [order_antisym]) 1);
   1.152 +qed "atMost_Int_atLeast";
   1.153 +
   1.154 +
   1.155 +