4776

1 
(* Title: HOL/LessThan/LessThan


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
lessThan, greaterThan, atLeast, atMost


7 
*)


8 


9 


10 
(*** lessThan ***)


11 

5069

12 
Goalw [lessThan_def] "(i: lessThan k) = (i<k)";

4776

13 
by (Blast_tac 1);


14 
qed "lessThan_iff";


15 
AddIffs [lessThan_iff];


16 

5069

17 
Goalw [lessThan_def] "lessThan 0 = {}";

4776

18 
by (Simp_tac 1);


19 
qed "lessThan_0";


20 
Addsimps [lessThan_0];


21 

5069

22 
Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";

4776

23 
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);


24 
by (Blast_tac 1);


25 
qed "lessThan_Suc";


26 

5648

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 

6825

31 
Goal "finite (lessThan k)";


32 
by (induct_tac "k" 1);


33 
by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);


34 
by Auto_tac;


35 
qed "finite_lessThan";


36 

5069

37 
Goal "(UN m. lessThan m) = UNIV";

4776

38 
by (Blast_tac 1);


39 
qed "UN_lessThan_UNIV";


40 

5069

41 
Goalw [lessThan_def, atLeast_def, le_def]

5490

42 
"lessThan k = atLeast k";

4776

43 
by (Blast_tac 1);


44 
qed "Compl_lessThan";


45 

7521

46 
Goal "{k}  lessThan k = {k}";


47 
by (Blast_tac 1);


48 
qed "single_Diff_lessThan";


49 
Addsimps [single_Diff_lessThan];

4776

50 


51 
(*** greaterThan ***)


52 

5069

53 
Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";

4776

54 
by (Blast_tac 1);


55 
qed "greaterThan_iff";


56 
AddIffs [greaterThan_iff];


57 

5069

58 
Goalw [greaterThan_def] "greaterThan 0 = range Suc";

4776

59 
by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);


60 
qed "greaterThan_0";


61 
Addsimps [greaterThan_0];


62 

5069

63 
Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k  {Suc k}";

5625

64 
by (auto_tac (claset() addEs [linorder_neqE], simpset()));

4776

65 
qed "greaterThan_Suc";


66 

5069

67 
Goal "(INT m. greaterThan m) = {}";

4776

68 
by (Blast_tac 1);


69 
qed "INT_greaterThan_UNIV";


70 

5069

71 
Goalw [greaterThan_def, atMost_def, le_def]

5490

72 
"greaterThan k = atMost k";

4776

73 
by (Blast_tac 1);


74 
qed "Compl_greaterThan";


75 

5069

76 
Goalw [greaterThan_def, atMost_def, le_def]

5490

77 
"atMost k = greaterThan k";

4776

78 
by (Blast_tac 1);


79 
qed "Compl_atMost";


80 

5069

81 
Goal "less_than ^^ {k} = greaterThan k";

4776

82 
by (Blast_tac 1);


83 
qed "Image_less_than";


84 


85 
Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];


86 


87 
(*** atLeast ***)


88 

5069

89 
Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";

4776

90 
by (Blast_tac 1);


91 
qed "atLeast_iff";


92 
AddIffs [atLeast_iff];


93 

5069

94 
Goalw [atLeast_def, UNIV_def] "atLeast 0 = UNIV";

4776

95 
by (Simp_tac 1);


96 
qed "atLeast_0";


97 
Addsimps [atLeast_0];


98 

5069

99 
Goalw [atLeast_def] "atLeast (Suc k) = atLeast k  {k}";

4776

100 
by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);

5596

101 
by (simp_tac (simpset() addsimps [order_le_less]) 1);

4776

102 
by (Blast_tac 1);


103 
qed "atLeast_Suc";


104 

5069

105 
Goal "(UN m. atLeast m) = UNIV";

4776

106 
by (Blast_tac 1);


107 
qed "UN_atLeast_UNIV";


108 

5069

109 
Goalw [lessThan_def, atLeast_def, le_def]

5490

110 
"atLeast k = lessThan k";

4776

111 
by (Blast_tac 1);


112 
qed "Compl_atLeast";


113 

5069

114 
Goal "less_than^1 ^^ {k} = lessThan k";

4776

115 
by (Blast_tac 1);


116 
qed "Image_inverse_less_than";


117 


118 
Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];


119 


120 
(*** atMost ***)


121 

5069

122 
Goalw [atMost_def] "(i: atMost k) = (i<=k)";

4776

123 
by (Blast_tac 1);


124 
qed "atMost_iff";


125 
AddIffs [atMost_iff];


126 

5069

127 
Goalw [atMost_def] "atMost 0 = {0}";

4776

128 
by (Simp_tac 1);


129 
qed "atMost_0";


130 
Addsimps [atMost_0];


131 

5069

132 
Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";

5596

133 
by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);

4776

134 
by (Blast_tac 1);


135 
qed "atMost_Suc";


136 

6825

137 
Goal "finite (atMost k)";


138 
by (induct_tac "k" 1);


139 
by (simp_tac (simpset() addsimps [atMost_Suc]) 2);


140 
by Auto_tac;


141 
qed "finite_atMost";


142 

5069

143 
Goal "(UN m. atMost m) = UNIV";

4776

144 
by (Blast_tac 1);


145 
qed "UN_atMost_UNIV";


146 

5069

147 
Goalw [atMost_def, le_def]

5490

148 
"atMost k = greaterThan k";

4776

149 
by (Blast_tac 1);


150 
qed "Compl_atMost";


151 
Addsimps [Compl_atMost];


152 


153 


154 
(*** Combined properties ***)


155 

5069

156 
Goal "atMost n Int atLeast n = {n}";

6707

157 
by (blast_tac (claset() addIs [order_antisym]) 1);

4776

158 
qed "atMost_Int_atLeast";


159 


160 

5232

161 


162 


163 
(*** Finally, a few settheoretic laws...


164 
CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)


165 


166 
context Set.thy;


167 

5490

168 
(** Rewrite rules to eliminate A. Conditions can be satisfied by letting B

5232

169 
be any set including A Int C and contained in A Un C, such as B=A or B=C.


170 
**)


171 


172 
Goal "[ A Int C <= B; B <= A Un C ] \

5490

173 
\ ==> (A Int B) Un (A Int C) = B Un C";

5232

174 
by (Blast_tac 1);

5490

175 
qed "set_cancel1";

5232

176 


177 
Goal "[ A Int C <= B; B <= A Un C ] \

5490

178 
\ ==> (A Un B) Int (A Un C) = B Int C";

5232

179 
by (Blast_tac 1);

5490

180 
qed "set_cancel2";

5232

181 


182 
(*The base B=A*)

5490

183 
Goal "A Un (A Int C) = A Un C";

5232

184 
by (Blast_tac 1);

5490

185 
qed "set_cancel3";

5232

186 

5490

187 
Goal "A Int (A Un C) = A Int C";

5232

188 
by (Blast_tac 1);

5490

189 
qed "set_cancel4";

5232

190 


191 
(*The base B=C*)

5490

192 
Goal "(A Int C) Un (A Int C) = C";

5232

193 
by (Blast_tac 1);

5490

194 
qed "set_cancel5";

5232

195 

5490

196 
Goal "(A Un C) Int (A Un C) = C";

5232

197 
by (Blast_tac 1);

5490

198 
qed "set_cancel6";


199 


200 
Addsimps [set_cancel1, set_cancel2, set_cancel3,


201 
set_cancel4, set_cancel5, set_cancel6];

5232

202 


203 


204 
(** More adhoc rules **)


205 


206 
Goal "A Un B  (A  B) = B";


207 
by (Blast_tac 1);


208 
qed "Un_Diff_Diff";

5490

209 
Addsimps [Un_Diff_Diff];

5232

210 


211 
Goal "A Int (B  C) Un C = A Int B Un C";


212 
by (Blast_tac 1);


213 
qed "Int_Diff_Un";


214 


215 
Goal "Union(B) Int A = (UN C:B. C Int A)";


216 
by (Blast_tac 1);


217 
qed "Int_Union2";


218 


219 
Goal "Union(B) Int A = Union((%C. C Int A)``B)";


220 
by (Blast_tac 1);


221 
qed "Int_Union_Union";


222 
