1(* non-interactive mode 2*) 3open HolKernel Parse boolLib; 4val _ = new_theory "extra_list"; 5 6(* interactive mode 7val () = loadPath := union ["..", "../finished"] (!loadPath); 8val () = app load 9 ["bossLib", 10 "pred_setTheory", 11 "realLib", 12 "pairTheory", 13 "combinTheory", 14 "res_quanLib", 15 "dividesTheory", 16 "primeTheory", 17 "gcdTheory", 18 "prob_extraTools", 19 "millerTools"]; 20val () = show_assums := true; 21*) 22 23open bossLib listTheory numTheory arithmeticTheory HurdUseful 24 pred_setTheory subtypeTheory extra_numTheory rich_listTheory; 25 26infixr 0 ++ << || THENC ORELSEC ORELSER ##; 27infix 1 >>; 28 29val op++ = op THEN; 30val op<< = op THENL; 31val op|| = op ORELSE; 32val op>> = op THEN1; 33 34(* ------------------------------------------------------------------------- *) 35(* Definitions. *) 36(* ------------------------------------------------------------------------- *) 37 38val sum_def = Define `(sum [] = (0:num)) /\ (sum (n :: ns) = n + sum ns)`; 39 40val prod_def = Define `(prod [] = (1:num)) /\ (prod (n :: ns) = n * prod ns)`; 41 42val kill_dups_def = Define 43 `kill_dups = FOLDR (\(h:'a) t. if MEM h t then t else h::t) []`; 44 45val list_def = Define `list = (EVERY : ('a -> bool) -> 'a list -> bool)`; 46 47val gtlist_def = Define `gtlist n l = n < LENGTH l`; 48 49(* ------------------------------------------------------------------------- *) 50(* Theorems. *) 51(* ------------------------------------------------------------------------- *) 52 53val MEM_NIL = store_thm 54 ("MEM_NIL", 55 ``!l. (!(x:'a). ~MEM x l) = (l = [])``, 56 Cases >> RW_TAC std_ss [MEM] 57 ++ RW_TAC std_ss [MEM] 58 ++ PROVE_TAC []); 59 60val MAP_ID = store_thm 61 ("MAP_ID", 62 ``!(l:'a list). MAP (\x. x) l = l``, 63 Induct >> RW_TAC list_ss [] 64 ++ RW_TAC list_ss []); 65 66val MAP_MEM = store_thm 67 ("MAP_MEM", 68 ``!(f:'a->'b) l x. MEM x (MAP f l) = ?y. MEM y l /\ (x = f y)``, 69 Induct_on `l` >> RW_TAC list_ss [MEM] 70 ++ RW_TAC list_ss [MEM] 71 ++ EQ_TAC << 72 [RW_TAC list_ss [] << 73 [PROVE_TAC [], 74 PROVE_TAC []], 75 PROVE_TAC []]); 76 77val APPEND_MEM = store_thm 78 ("APPEND_MEM", 79 ``!(x:'a) l1 l2. MEM x (APPEND l1 l2) = (MEM x l1 \/ MEM x l2)``, 80 Induct_on `l1` >> RW_TAC list_ss [MEM] 81 ++ RW_TAC list_ss [MEM] 82 ++ PROVE_TAC []); 83 84val MEM_NIL_MAP_CONS = store_thm 85 ("MEM_NIL_MAP_CONS", 86 ``!(x:'a) l. ~MEM [] (MAP (CONS x) l)``, 87 STRIP_TAC 88 ++ Induct >> RW_TAC list_ss [MEM] 89 ++ RW_TAC list_ss [MEM]); 90 91val FILTER_TRUE = store_thm 92 ("FILTER_TRUE", 93 ``!(l:'a list). FILTER (\x. T) l = l``, 94 Induct >> RW_TAC list_ss [FILTER] 95 ++ RW_TAC list_ss [FILTER]); 96 97val FILTER_FALSE = store_thm 98 ("FILTER_FALSE", 99 ``!(l:'a list). FILTER (\x. F) l = []``, 100 Induct >> RW_TAC list_ss [FILTER] 101 ++ RW_TAC list_ss [FILTER]); 102 103val LENGTH_FILTER = store_thm 104 ("LENGTH_FILTER", 105 ``!P (l:'a list). LENGTH (FILTER P l) <= LENGTH l``, 106 GEN_TAC 107 ++ Induct_on `l` 108 ++ RW_TAC list_ss [FILTER]); 109 110val FILTER_MEM = store_thm 111 ("FILTER_MEM", 112 ``!P (x:'a) l. MEM x (FILTER P l) ==> P x``, 113 NTAC 2 STRIP_TAC 114 ++ Induct >> RW_TAC std_ss [MEM, FILTER] 115 ++ (RW_TAC std_ss [MEM, FILTER] ++ PROVE_TAC [])); 116 117val MEM_FILTER = store_thm 118 ("MEM_FILTER", 119 ``!P l (x:'a). MEM x (FILTER P l) ==> MEM x l``, 120 STRIP_TAC 121 ++ Induct >> RW_TAC list_ss [FILTER] 122 ++ RW_TAC list_ss [FILTER, MEM] 123 ++ PROVE_TAC []); 124 125val FILTER_OUT_ELT = store_thm 126 ("FILTER_OUT_ELT", 127 ``!(x:'a) l. MEM x l \/ (FILTER (\y. ~(y = x)) l = l)``, 128 STRIP_TAC 129 ++ Induct >> RW_TAC list_ss [FILTER] 130 ++ (RW_TAC list_ss [MEM, FILTER] 131 ++ PROVE_TAC [])); 132 133val IS_PREFIX_NIL = store_thm 134 ("IS_PREFIX_NIL", 135 ``!(x:'a list). IS_PREFIX x [] /\ (IS_PREFIX [] x = (x = []))``, 136 STRIP_TAC 137 ++ Cases_on `x` 138 ++ RW_TAC list_ss [IS_PREFIX]); 139 140val IS_PREFIX_REFL = store_thm 141 ("IS_PREFIX_REFL", 142 ``!(x:'a list). IS_PREFIX x x``, 143 Induct ++ RW_TAC list_ss [IS_PREFIX]); 144 145val IS_PREFIX_ANTISYM = store_thm 146 ("IS_PREFIX_ANTISYM", 147 ``!(x:'a list) y. IS_PREFIX y x /\ IS_PREFIX x y ==> (x = y)``, 148 Induct >> RW_TAC list_ss [IS_PREFIX_NIL] 149 ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL] 150 ++ ONCE_REWRITE_TAC [IS_PREFIX] 151 ++ PROVE_TAC []); 152 153val IS_PREFIX_TRANS = store_thm 154 ("IS_PREFIX_TRANS", 155 ``!(x:'a list) y z. IS_PREFIX x y /\ IS_PREFIX y z ==> IS_PREFIX x z``, 156 Induct >> PROVE_TAC [IS_PREFIX_NIL] 157 ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL, IS_PREFIX] 158 ++ Cases_on `z` >> RW_TAC list_ss [IS_PREFIX_NIL, IS_PREFIX] 159 ++ RW_TAC list_ss [IS_PREFIX] 160 ++ PROVE_TAC []); 161 162val IS_PREFIX_BUTLAST = store_thm 163 ("IS_PREFIX_BUTLAST", 164 ``!x:'a y. IS_PREFIX (x::y) (BUTLAST (x::y))``, 165 Induct_on `y` 166 >> RW_TAC list_ss [BUTLAST_CONS, IS_PREFIX] 167 ++ RW_TAC list_ss [BUTLAST_CONS, IS_PREFIX]); 168 169val IS_PREFIX_LENGTH = store_thm 170 ("IS_PREFIX_LENGTH", 171 ``!(x:'a list) y. IS_PREFIX y x ==> LENGTH x <= LENGTH y``, 172 Induct >> RW_TAC list_ss [LENGTH] 173 ++ Cases_on `y` >> RW_TAC list_ss [IS_PREFIX_NIL] 174 ++ RW_TAC list_ss [IS_PREFIX, LENGTH]); 175 176val IS_PREFIX_LENGTH_ANTI = store_thm 177 ("IS_PREFIX_LENGTH_ANTI", 178 ``!(x:'a list) y. IS_PREFIX y x /\ (LENGTH x = LENGTH y) ==> (x = y)``, 179 Induct >> PROVE_TAC [LENGTH_NIL] 180 ++ Cases_on `y` >> RW_TAC list_ss [LENGTH_NIL] 181 ++ RW_TAC list_ss [IS_PREFIX, LENGTH]); 182 183val IS_PREFIX_SNOC = store_thm 184 ("IS_PREFIX_SNOC", 185 ``!(x:'a) y z. IS_PREFIX (SNOC x y) z = IS_PREFIX y z \/ (z = SNOC x y)``, 186 Induct_on `y` 187 >> (Cases_on `z` 188 ++ RW_TAC list_ss [SNOC, IS_PREFIX_NIL, IS_PREFIX] 189 ++ PROVE_TAC []) 190 ++ Cases_on `z` >> RW_TAC list_ss [IS_PREFIX] 191 ++ RW_TAC list_ss [SNOC, IS_PREFIX] 192 ++ PROVE_TAC []); 193 194val FOLDR_MAP = store_thm 195 ("FOLDR_MAP", 196 ``!(f :'b -> 'c -> 'c) (e :'c) (g :'a -> 'b) (l :'a list). 197 FOLDR f e (MAP g l) = FOLDR (\x y. f (g x) y) e l``, 198 RW_TAC list_ss [] 199 ++ Induct_on `l` >> RW_TAC list_ss [MAP, FOLDR] 200 ++ RW_TAC list_ss [MAP, FOLDR]); 201 202val LAST_MEM = store_thm 203 ("LAST_MEM", 204 ``!(h:'a) t. MEM (LAST (h::t)) (h::t)``, 205 Induct_on `t` >> RW_TAC list_ss [MEM, LAST_CONS] 206 ++ RW_TAC std_ss [LAST_CONS] 207 ++ ONCE_REWRITE_TAC [MEM] 208 ++ RW_TAC std_ss []); 209 210val LAST_MAP_CONS = store_thm 211 ("LAST_MAP_CONS", 212 ``!(b:bool) h t. ?x. LAST (MAP (CONS b) (h::t)) = b::x``, 213 Induct_on `t` >> RW_TAC list_ss [LAST_CONS] 214 ++ POP_ASSUM MP_TAC 215 ++ RW_TAC list_ss [LAST_CONS]); 216 217val EXISTS_LONGEST = store_thm 218 ("EXISTS_LONGEST", 219 ``!(x:'a list) y. ?z. MEM z (x::y) 220 /\ (!w. MEM w (x::y) ==> LENGTH w <= LENGTH z)``, 221 Induct_on `y` >> RW_TAC list_ss [MEM] 222 ++ ONCE_REWRITE_TAC [MEM] 223 ++ REPEAT STRIP_TAC 224 ++ POP_ASSUM (MP_TAC o SPEC ``h:'a list``) 225 ++ STRIP_TAC 226 ++ EXISTS_TAC ``if LENGTH z <= LENGTH x then x else (z:'a list)`` 227 ++ ZAP_TAC std_ss [LESS_EQ_TRANS]); 228 229val SUM_CONST = store_thm 230 ("SUM_CONST", 231 ``!l c. (!x. MEM x l ==> (x = c)) ==> (sum l = LENGTH l * c)``, 232 Induct >> RW_TAC arith_ss [LENGTH, sum_def] 233 ++ RW_TAC std_ss [LENGTH, sum_def, MEM, MULT] 234 ++ PROVE_TAC [ADD_COMM]); 235 236val MEM_KILL_DUPS = store_thm 237 ("MEM_KILL_DUPS", 238 ``!l (x:'a). MEM x (kill_dups l) = MEM x l``, 239 Induct >> RW_TAC list_ss [MEM, kill_dups_def, FOLDR] 240 ++ REWRITE_TAC [kill_dups_def, FOLDR] 241 ++ RW_TAC std_ss [GSYM kill_dups_def, MEM] 242 ++ Cases_on `x = h` >> RW_TAC std_ss [] 243 ++ RW_TAC std_ss []); 244 245val IN_LIST = store_thm 246 ("IN_LIST", 247 ``!(h:'a) t p. 248 ([] IN list p) /\ ((h::t) IN list p = h IN p /\ t IN list p)``, 249 RW_TAC std_ss [list_def, SPECIFICATION, EVERY_DEF]); 250 251val IN_GTLIST = store_thm 252 ("IN_GTLIST", 253 ``!n (l:'a list). l IN gtlist n = n < LENGTH l``, 254 RW_TAC std_ss [gtlist_def, SPECIFICATION]); 255 256val LIST_UNIV = store_thm 257 ("LIST_UNIV", 258 ``list (UNIV : 'a -> bool) = UNIV``, 259 SET_EQ_TAC 260 ++ Induct >> RW_TAC std_ss [IN_LIST, IN_UNIV] 261 ++ RW_TAC std_ss [IN_LIST, IN_UNIV]); 262 263val LIST_SUBSET = store_thm 264 ("LIST_SUBSET", 265 ``!p q. p SUBSET q ==> list p SUBSET list q``, 266 RW_TAC std_ss [SUBSET_DEF] 267 ++ Induct_on `x` >> RW_TAC std_ss [IN_LIST] 268 ++ RW_TAC std_ss [IN_LIST]); 269 270val NIL_SUBTYPE = store_thm 271 ("NIL_SUBTYPE", 272 ``!(x : 'a -> bool). [] IN list x``, 273 RW_TAC std_ss [IN_LIST, LENGTH, IN_INTER]); 274 275val CONS_SUBTYPE = store_thm 276 ("CONS_SUBTYPE", 277 ``!(x : 'a -> bool). 278 CONS IN ((x -> list x -> list x) INTER (UNIV -> UNIV -> gtlist 0) INTER 279 (UNIV -> gtlist 0 -> gtlist 1))``, 280 RW_TAC arith_ss [IN_FUNSET, IN_LIST, IN_GTLIST, LENGTH, IN_INTER]); 281 282val MAP_SUBTYPE = store_thm 283 ("MAP_SUBTYPE", 284 ``!(x:'a->bool) (y:'b->bool) n. 285 MAP IN (((x -> y) -> list x -> list y) INTER 286 (UNIV -> gtlist n -> gtlist n))``, 287 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST, LENGTH_MAP] 288 ++ Induct_on `x''` >> RW_TAC std_ss [MAP, IN_LIST] 289 ++ RW_TAC std_ss [MAP, IN_LIST]); 290 291val HD_SUBTYPE = store_thm 292 ("HD_SUBTYPE", 293 ``!x. HD IN ((gtlist 0 INTER list x) -> x)``, 294 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST] 295 ++ Cases_on `x'` 296 >> (Q.PAT_X_ASSUM `0 < LENGTH []` MP_TAC 297 ++ RW_TAC arith_ss [LENGTH]) 298 ++ POP_ASSUM MP_TAC 299 ++ RW_TAC std_ss [IN_LIST, HD]); 300 301val TL_SUBTYPE = store_thm 302 ("TL_SUBTYPE", 303 ``!x. TL IN (((gtlist 0 INTER list x) -> list x) INTER 304 (gtlist 1 -> gtlist 0))``, 305 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST] << 306 [Cases_on `x'` 307 >> (Q.PAT_X_ASSUM `0 < LENGTH []` MP_TAC 308 ++ RW_TAC arith_ss [LENGTH]) 309 ++ POP_ASSUM MP_TAC 310 ++ RW_TAC std_ss [IN_LIST, TL], 311 POP_ASSUM MP_TAC 312 ++ Cases_on `x` >> RW_TAC arith_ss [LENGTH] 313 ++ Cases_on `t` >> RW_TAC arith_ss [LENGTH] 314 ++ RW_TAC arith_ss [LENGTH, TL]]); 315 316val LENGTH_SUBTYPE = store_thm 317 ("LENGTH_SUBTYPE", 318 ``LENGTH IN ((gtlist 0 -> gtnum 0) INTER (gtlist 1 -> gtnum 1))``, 319 RW_TAC std_ss [IN_FUNSET, IN_INTER, IN_GTLIST, IN_GTNUM]); 320 321val GTLIST0_SUBTYPE_REWRITE = store_thm 322 ("GTLIST0_SUBTYPE_REWRITE", 323 ``!l. l IN gtlist 0 ==> ~(l = []) /\ ~([] = l)``, 324 Cases 325 ++ RW_TAC arith_ss [IN_GTLIST, LENGTH]); 326 327val GTLIST1_SUBTYPE_REWRITE = store_thm 328 ("GTLIST1_SUBTYPE_REWRITE", 329 ``!l h. l IN gtlist 1 ==> ~(l = [h]) /\ ~([h] = l)``, 330 Cases >> RW_TAC arith_ss [IN_GTLIST, LENGTH] 331 ++ Cases_on `t` 332 ++ RW_TAC arith_ss [IN_GTLIST, LENGTH]); 333 334val GTLIST0_SUBTYPE_JUDGEMENT = store_thm 335 ("GTLIST0_SUBTYPE_JUDGEMENT", 336 ``!l m. 337 LENGTH l IN gtnum 0 \/ ~([] = l) \/ ~(l = []) ==> l IN gtlist 0``, 338 Cases 339 ++ RW_TAC std_ss [IN_GTLIST, IN_GTNUM, LENGTH] 340 ++ DECIDE_TAC); 341 342val GTLIST1_SUBTYPE_JUDGEMENT = store_thm 343 ("GTLIST1_SUBTYPE_JUDGEMENT", 344 ``!l m. LENGTH l IN gtnum 1 ==> l IN gtlist 1``, 345 RW_TAC std_ss [IN_GTLIST, IN_GTNUM] 346 ++ DECIDE_TAC); 347 348val GTLIST1_SUBSET_GTLIST0 = store_thm 349 ("GTLIST1_SUBSET_GTLIST0", 350 ``gtlist 1 SUBSET gtlist 0``, 351 RW_TAC std_ss [SUBSET_DEF, IN_GTLIST] 352 ++ DECIDE_TAC); 353 354(* non-interactive mode 355*) 356val _ = export_theory (); 357