8956

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 
Goalw [atMost_def, le_def]


136 
"!!k:: 'a::linorder. atMost k = greaterThan k";


137 
by Auto_tac;


138 
by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);


139 
by (blast_tac (claset() addIs [order_le_less_trans RS


140 
(order_less_irrefl RS notE)]) 1);


141 
qed "Compl_atMost";


142 
Addsimps [Compl_atMost];


143 


144 


145 
(*** Combined properties ***)


146 


147 
Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";


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


149 
qed "atMost_Int_atLeast";


150 


151 


152 
