1(* ------------------------------------------------------------------------- *) 2(* Sublist Theory *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "sublist"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories *) 23(* val _ = load "helperListTheory"; *) 24open helperListTheory; 25 26(* open dependent theories *) 27open listTheory arithmeticTheory; 28open listRangeTheory; (* for listRangeINC_def *) 29 30 31(* ------------------------------------------------------------------------- *) 32(* Sublist Theory Documentation *) 33(* ------------------------------------------------------------------------- *) 34(* Datatypes and overloads: 35 l1 <= l2 = sublist l1 l2 36*) 37(* Definitions and Theorems (# are exported): 38 39 Sublist: 40 sublist_def |- (!x. [] <= x <=> T) /\ (!t1 h1. h1::t1 <= [] <=> F) /\ 41 !t2 t1 h2 h1. h1::t1 <= h2::t2 <=> 42 (h1 = h2) /\ t1 <= t2 \/ h1 <> h2 /\ h1::t1 <= t2 43 sublist_nil |- !p. [] <= p 44 sublist_cons |- !h p q. p <= q <=> h::p <= h::q 45 sublist_of_nil |- !p. p <= [] <=> (p = []) 46 sublist_cons_eq |- !h. (!p q. h::p <= q ==> p <= q) <=> !p q. p <= q ==> p <= h::q 47 sublist_cons_remove |- !h p q. h::p <= q ==> p <= q 48 sublist_cons_include |- !h p q. p <= q ==> p <= h::q 49 sublist_length |- !p q. p <= q ==> LENGTH p <= LENGTH q 50 sublist_refl |- !p. p <= p 51 sublist_antisym |- !p q. p <= q /\ q <= p ==> (p = q) 52 sublist_trans |- !p q r. p <= q /\ q <= r ==> p <= r 53 sublist_snoc |- !h p q. p <= q ==> SNOC h p <= SNOC h q 54 sublist_member_sing |- !ls x. MEM x ls ==> [x] <= ls 55 sublist_take |- !ls n. TAKE n ls <= ls 56 sublist_drop |- !ls n. DROP n ls <= ls 57 sublist_tail |- !ls. ls <> [] ==> TL ls <= ls 58 sublist_front |- !ls. ls <> [] ==> FRONT ls <= ls 59 sublist_head_sing |- !ls. ls <> [] ==> [HD ls] <= ls 60 sublist_last_sing |- !ls. ls <> [] ==> [LAST ls] <= ls 61 sublist_every |- !l ls. l <= ls ==> !P. EVERY P ls ==> EVERY P l 62 63 More sublists: 64 sublist_induct |- !P. (!y. P [] y) /\ 65 (!h x y. P x y /\ x <= y ==> P (h::x) (h::y)) /\ 66 (!h x y. P x y /\ x <= y ==> P x (h::y)) ==> !x y. x <= y ==> P x y 67 sublist_append_remove |- !p q x. x ++ p <= q ==> p <= q 68 sublist_append_include |- !p q x. p <= q ==> p <= x ++ q 69 sublist_append_suffix |- !p q. p <= p ++ q 70 sublist_append_prefix |- !p q. p <= q ++ p 71 sublist_prefix |- !x p q. p <= q <=> x ++ p <= x ++ q 72 sublist_prefix_nil |- !p q. p ++ q <= q ==> (p = []) 73 sublist_append_if |- !p q. p <= q ==> !h. p ++ [h] <= q ++ [h] 74 sublist_append_only_if |- !p q h. p ++ [h] <= q ++ [h] ==> p <= q 75 sublist_append_iff |- !p q h. p <= q <=> p ++ [h] <= q ++ [h] 76 sublist_suffix |- !x p q. p <= q <=> p ++ x <= q ++ x 77 sublist_append_pair |- !a b c d. a <= b /\ c <= d ==> a ++ c <= b ++ d 78 sublist_append_extend |- !h t q. h::t <= q <=> ?x y. (q = x ++ h::y) /\ t <= y 79 80 Applications of sublist: 81 MAP_SUBLIST |- !f p q. p <= q ==> MAP f p <= MAP f q 82 SUM_SUBLIST |- !p q. p <= q ==> SUM p <= SUM q 83 listRangeINC_sublist |- !m n. m < n ==> [m; n] <= [m .. n] 84 listRangeLHI_sublist |- !m n. m + 1 < n ==> [m; n - 1] <= [m ..< n] 85*) 86 87(* ------------------------------------------------------------------------- *) 88(* Sublist: an order-preserving portion of a list *) 89(* ------------------------------------------------------------------------- *) 90 91(* Definition of sublist *) 92val sublist_def = Define` 93 (sublist [] x = T) /\ 94 (sublist (h1::t1) [] = F) /\ 95 (sublist (h1::t1) (h2::t2) <=> 96 ((h1 = h2) /\ sublist t1 t2 \/ ~(h1 = h2) /\ sublist (h1::t1) t2)) 97`; 98 99(* Overload sublist by infix operator *) 100val _ = overload_on ("<=", ``sublist``); 101(* 102> sublist_def; 103val it = |- (!x. [] <= x <=> T) /\ (!t1 h1. h1::t1 <= [] <=> F) /\ 104 !t2 t1 h2 h1. h1::t1 <= h2::t2 <=> 105 (h1 = h2) /\ t1 <= t2 \/ h1 <> h2 /\ h1::t1 <= t2: thm 106*) 107 108(* Theorem: [] <= p *) 109(* Proof: by sublist_def *) 110val sublist_nil = store_thm( 111 "sublist_nil", 112 ``!p. [] <= p``, 113 rw[sublist_def]); 114 115(* Theorem: p <= q <=> h::p <= h::q *) 116(* Proof: by sublist_def *) 117val sublist_cons = store_thm( 118 "sublist_cons", 119 ``!h p q. p <= q <=> h::p <= h::q``, 120 rw[sublist_def]); 121 122(* Theorem: p <= [] <=> (p = []) *) 123(* Proof: 124 If p = [], then [] <= [] by sublist_nil 125 If p = h::t, then h::t <= [] = F by sublist_def 126*) 127val sublist_of_nil = store_thm( 128 "sublist_of_nil", 129 ``!p. p <= [] <=> (p = [])``, 130 (Cases_on `p` >> rw[sublist_def])); 131 132(* Theorem: (!p q. (h::p) <= q ==> p <= q) = (!p q. p <= q ==> p <= (h::q)) *) 133(* Proof: 134 If part: (!p q. (h::p) <= q ==> p <= q) ==> (!p q. p <= q ==> p <= (h::q)) 135 p <= q 136 ==> h::p <= h::q by sublist_cons 137 ==> p <= h::q by implication 138 Only-if part: (!p q. p <= q ==> p <= (h::q)) ==> (!p q. (h::p) <= q ==> p <= q) 139 (h::p) <= q 140 ==> (h::p) <= (h::q) by implication 141 ==> p <= q by sublist_cons 142*) 143val sublist_cons_eq = store_thm( 144 "sublist_cons_eq", 145 ``!h. (!p q. (h::p) <= q ==> p <= q) = (!p q. p <= q ==> p <= (h::q))``, 146 rw[EQ_IMP_THM] >> 147 metis_tac[sublist_cons]); 148 149(* Theorem: h::p <= q ==> p <= q *) 150(* Proof: 151 By induction on q. 152 Base: !h p. h::p <= [] ==> p <= [] 153 True since h::p <= [] = F by sublist_def 154 155 Step: !h p. h::p <= q ==> p <= q ==> 156 !h h' p. h'::p <= h::q ==> p <= h::q 157 If p = [], true by sublist_nil 158 If p = h''::t, 159 p <= h::q 160 <=> (h'' = h) /\ t <= q \/ h'' <> h /\ h''::t <= q by sublist_def 161 If h'' = h, then t <= q by sublist_def, induction hypothesis 162 If h'' <> h, then h''::t <= q by sublist_def, induction hypothesis 163*) 164val sublist_cons_remove = store_thm( 165 "sublist_cons_remove", 166 ``!h p q. h::p <= q ==> p <= q``, 167 Induct_on `q` >- 168 rw[sublist_def] >> 169 rpt strip_tac >> 170 (Cases_on `p` >> simp[sublist_def]) >> 171 (Cases_on `h'' = h` >> metis_tac[sublist_def])); 172 173(* Theorem: p <= q ==> p <= h::q *) 174(* Proof: by sublist_cons_eq, sublist_cons_remove *) 175val sublist_cons_include = store_thm( 176 "sublist_cons_include", 177 ``!h p q. p <= q ==> p <= h::q``, 178 metis_tac[sublist_cons_eq, sublist_cons_remove]); 179 180(* Theorem: p <= q ==> LENGTH p <= LENGTH q *) 181(* Proof: 182 By induction on q. 183 Base: !p. p <= [] ==> LENGTH p <= LENGTH [] 184 Note p = [] by sublist_of_nil 185 Thus true by arithemtic 186 Step: !p. p <= q ==> LENGTH p <= LENGTH q ==> 187 !h p. p <= h::q ==> LENGTH p <= LENGTH (h::q) 188 If p = [], LENGTH p = 0 by LENGTH 189 and 0 <= LENGTH (h::q). 190 If p = h'::t, 191 If h = h', 192 (h::t) <= (h::q) 193 <=> t <= q by sublist_def, same heads 194 ==> LENGTH t <= LENGTH q by inductive hypothesis 195 ==> SUC(LENGTH t) <= SUC(LENGTH q) 196 = LENGTH (h::t) <= LENGTH (h::q) 197 If ~(h = h'), 198 (h'::t) <= (h::q) 199 <=> (h'::t) <= q by sublist_def, different heads 200 ==> LENGTH (h'::t) <= LENGTH q by inductive hypothesis 201 ==> LENGTH (h'::t) <= SUC(LENGTH q) by arithemtic 202 = LENGTH (h'::t) <= LENGTH (h::q) 203*) 204val sublist_length = store_thm( 205 "sublist_length", 206 ``!p q. p <= q ==> LENGTH p <= LENGTH q``, 207 Induct_on `q` >- 208 rw[sublist_of_nil] >> 209 rpt strip_tac >> 210 (Cases_on `p` >> simp[]) >> 211 (Cases_on `h = h'` >> fs[sublist_def]) >> 212 `LENGTH (h'::t) <= LENGTH q` by rw[] >> 213 `LENGTH t < LENGTH (h'::t)` by rw[LENGTH_TL_LT] >> 214 decide_tac); 215 216(* Theorem: [Reflexive] p <= p *) 217(* Proof: 218 By induction on p. 219 Base: [] <= [], true by sublist_nil 220 Step: p <= p ==> !h. h::p <= h::p, true by sublist_cons 221*) 222val sublist_refl = store_thm( 223 "sublist_refl", 224 ``!p:'a list. p <= p``, 225 Induct >- 226 rw[sublist_nil] >> 227 rw[GSYM sublist_cons]); 228(* Faster just by definition *) 229val sublist_refl = store_thm( 230 "sublist_refl", 231 ``!p:'a list. p <= p``, 232 Induct >> rw[sublist_def]); 233 234(* Theorem: [Anti-symmetric] !p q. (p <= q) /\ (q <= p) ==> (p = q) *) 235(* Proof: 236 By induction on q. 237 Base: !p. p <= [] /\ [] <= p ==> (p = []) 238 Note p <= [] already gives p = [] by sublist_of_nil 239 Step: !p. p <= q /\ q <= p ==> (p = q) ==> 240 !h p. p <= h::q /\ h::q <= p ==> (p = h::q) 241 If p = [], h::q <= [] = F by sublist_def 242 If p = (h'::t), 243 If h = h', 244 ((h::t) <= (h::q)) /\ ((h::q) <= (h::t)) 245 <=> (t <= q) and (q <= t) by sublist_def, same heads 246 ==> t = q by inductive hypothesis 247 <=> (h::t) = (h::q) by list equality 248 If ~(h = h'), 249 ((h'::t) <= (h::q)) /\ ((h::q) <= (h'::t)) 250 <=> ((h'::t) <= q) /\ ((h::q) <= t) by sublist_def, different heads 251 ==> (LENGTH (h'::t) <= LENGTH q) /\ 252 (LENGTH (h::q) <= LENGTH t) by sublist_length 253 ==> (LENGTh t < LENGTH q) /\ 254 (LENGTH q < LENGTH t) by LENGTH_TL_LT 255 = F by arithmetic 256 Hence the implication is T. 257*) 258val sublist_antisym = store_thm( 259 "sublist_antisym", 260 ``!p q:'a list. p <= q /\ q <= p ==> (p = q)``, 261 Induct_on `q` >- 262 rw[sublist_of_nil] >> 263 rpt strip_tac >> 264 Cases_on `p` >- 265 fs[sublist_def] >> 266 (Cases_on `h' = h` >> fs[sublist_def]) >> 267 `LENGTH (h'::t) <= LENGTH q /\ LENGTH (h::q) <= LENGTH t` by rw[sublist_length] >> 268 fs[LENGTH_TL_LT]); 269 270(* Theorem [Transitive]: for all lists p, q, r; (p <= q) /\ (q <= r) ==> (p <= r) *) 271(* Proof: 272 By induction on list r and taking note of cases. 273 By induction on r. 274 Base: !p q. p <= q /\ q <= [] ==> p <= [] 275 Note q = [] by sublist_of_nil 276 so p = [] by sublist_of_nil 277 Step: !p q. p <= q /\ q <= r ==> p <= r ==> 278 !h p q. p <= q /\ q <= h::r ==> p <= h::r 279 If p = [], true by sublist_nil 280 If p = h'::t, to show: 281 h'::t <= q /\ q <= h::r ==> 282 (h' = h) /\ t <= r \/ 283 h' <> h /\ h'::t <= r by sublist_def 284 If q = [], [] <= h::r = F by sublist_def 285 If q = h''::t', this reduces to: 286 (1) h' = h'' /\ t <= t' /\ h'' = h /\ t' <= r ==> t <= r 287 Note t <= t' /\ t' <= r ==> t <= r by induction hypothesis 288 (2) h' = h'' /\ t <= t' /\ h'' <> h /\ h''::t' <= r ==> h''::t <= r 289 Note t <= t' ==> h''::t <= h''::t' by sublist_cons 290 With h''::t' <= r ==> h''::t <= r by induction hypothesis 291 (3) h' <> h'' /\ h'::t <= t' /\ h'' = h /\ t' <= r ==> 292 (h' = h) /\ t <= r \/ h' <> h /\ h'::t <= r 293 Note h'::t <= t' ==> t <= t' by sublist_cons_remove 294 With t' <= r ==> t <= r by induction hypothesis 295 Or simply h'::t <= t' /\ t' <= r 296 ==> h'::t <= r by induction hypothesis 297 Hence this is true. 298 (4) h' <> h'' /\ h'::t <= t' /\ h'' <> h /\ h''::t' <= r ==> 299 (h' = h) /\ t <= r \/ h' <> h /\ h'::t <= r 300 Same reasoning as (3). 301*) 302val sublist_trans = store_thm( 303 "sublist_trans", 304 ``!p q r:'a list. p <= q /\ q <= r ==> p <= r``, 305 Induct_on `r` >- 306 fs[sublist_of_nil] >> 307 rpt strip_tac >> 308 (Cases_on `p` >> fs[sublist_def]) >> 309 (Cases_on `q` >> fs[sublist_def]) >- 310 metis_tac[] >- 311 metis_tac[sublist_cons] >- 312 metis_tac[sublist_cons_remove] >> 313 metis_tac[sublist_cons_remove]); 314 315(* The above theorems show that sublist is a partial ordering. *) 316 317(* Theorem: p <= q ==> SNOC h p <= SNOC h q *) 318(* Proof: 319 By induction on q. 320 Base: !h p. p <= [] ==> SNOC h p <= SNOC h [] 321 Note p = [] by sublist_of_nil 322 Thus SNOC h [] <= SNOC h [] by sublist_refl 323 Step: !h p. p <= q ==> SNOC h p <= SNOC h q ==> 324 !h h' p. p <= h::q ==> SNOC h' p <= SNOC h' (h::q) 325 If p = [], 326 Note [] <= q by sublist_nil 327 Thus SNOC h' [] 328 <= SNOC h' q by induction hypothesis 329 <= h::SNOC h' q by sublist_cons_include 330 = SNOC h' (h::q) by SNOC 331 If p = h''::t, 332 If h = h'', 333 Then t <= q by sublist_def, same heads 334 ==> SNOC h' t <= SNOC h' q by induction hypothesis 335 ==> h::SNOC h' t <= h::SNOC h' q by rw[sublist_cons 336 or SNOC h' (h::t) <= SNOC h' (h::q) by SNOC 337 or SNOC h' p <= SNOC h' (h::q) by p = h::t 338 If h <> h'', 339 Then p <= q by sublist_def, different heads 340 ==> SNOC h' p <= SNOC h' q by induction hypothesis 341 ==> SNOC h' p <= h::SNOC h' q by sublist_cons_include 342*) 343val sublist_snoc = store_thm( 344 "sublist_snoc", 345 ``!h p q. p <= q ==> SNOC h p <= SNOC h q``, 346 Induct_on `q` >- 347 rw[sublist_of_nil, sublist_refl] >> 348 rw[sublist_def] >> 349 Cases_on `p` >- 350 rw[sublist_nil, sublist_cons_include] >> 351 metis_tac[sublist_def, sublist_cons, SNOC]); 352 353(* Theorem: MEM x ls ==> [x] <= ls *) 354(* Proof: 355 By induction on ls. 356 Base: !x. MEM x [] ==> [x] <= [] 357 True since MEM x [] = F. 358 Step: !x. MEM x ls ==> [x] <= ls ==> 359 !h x. MEM x (h::ls) ==> [x] <= h::ls 360 If x = h, 361 Then [h] <= h::ls by sublist_nil, sublist_cons 362 If x <> h, 363 Then MEM h ls by MEM x (h::ls) 364 ==> [x] <= ls by induction hypothesis 365 ==> [x] <= h::ls by sublist_cons_include 366*) 367val sublist_member_sing = store_thm( 368 "sublist_member_sing", 369 ``!ls x. MEM x ls ==> [x] <= ls``, 370 Induct >- 371 rw[] >> 372 rw[] >- 373 rw[sublist_nil, GSYM sublist_cons] >> 374 rw[sublist_cons_include]); 375 376(* Theorem: TAKE n ls <= ls *) 377(* Proof: 378 By induction on ls. 379 Base: !n. TAKE n [] <= [] 380 LHS = TAKE n [] = [] by TAKE_def 381 <= [] = RHS by sublist_nil 382 Step: !n. TAKE n ls <= ls ==> !h n. TAKE n (h::ls) <= h::ls 383 If n = 0, 384 TAKE 0 (h::ls) 385 = [] by TAKE_def 386 <= h::ls by sublist_nil 387 If n <> 0, 388 TAKE n (h::ls) 389 = h::TAKE (n - 1) ls by TAKE_def 390 Now TAKE (n - 1) ls <= ls by induction hypothesis 391 Thus h::TAKE (n - 1) ls <= h::ls by sublist_cons 392*) 393val sublist_take = store_thm( 394 "sublist_take", 395 ``!ls n. TAKE n ls <= ls``, 396 Induct >- 397 rw[sublist_nil] >> 398 rpt strip_tac >> 399 Cases_on `n = 0` >- 400 rw[sublist_nil] >> 401 rw[GSYM sublist_cons]); 402 403(* Theorem: DROP n ls <= ls *) 404(* Proof: 405 By induction on ls. 406 Base: !n. DROP n [] <= [] 407 LHS = DROP n [] = [] by DROP_def 408 <= [] = RHS by sublist_nil 409 Step: !n. DROP n ls <= ls ==> !h n. DROP n (h::ls) <= h::ls 410 If n = 0, 411 DROP 0 (h::ls) 412 = h::ls by DROP_def 413 <= h::ls by sublist_refl 414 If n <> 0, 415 DROP n (h::ls) 416 = DROP n ls by DROP_def 417 <= ls by induction hypothesis 418 <= h::ls by sublist_cons_include 419*) 420val sublist_drop = store_thm( 421 "sublist_drop", 422 ``!ls n. DROP n ls <= ls``, 423 Induct >- 424 rw[sublist_nil] >> 425 rpt strip_tac >> 426 Cases_on `n = 0` >- 427 rw[sublist_refl] >> 428 rw[sublist_cons_include]); 429 430(* Theorem: ls <> [] ==> TL ls <= ls *) 431(* Proof: 432 Note TL ls = DROP 1 ls by TAIL_BY_DROP, ls <> [] 433 Thus TL ls <= ls by sublist_drop 434*) 435val sublist_tail = store_thm( 436 "sublist_tail", 437 ``!ls. ls <> [] ==> TL ls <= ls``, 438 rw[TAIL_BY_DROP, sublist_drop]); 439 440(* Theorem: ls <> [] ==> FRONT ls <= ls *) 441(* Proof: 442 Note FRONT ls = TAKE (LENGTH ls - 1) ls by FRONT_BY_TAKE 443 so FRONT ls <= ls by sublist_take 444*) 445val sublist_front = store_thm( 446 "sublist_front", 447 ``!ls. ls <> [] ==> FRONT ls <= ls``, 448 rw[FRONT_BY_TAKE, sublist_take]); 449 450(* Theorem: ls <> [] ==> [HD ls] <= ls *) 451(* Proof: HEAD_MEM, sublist_member_sing *) 452val sublist_head_sing = store_thm( 453 "sublist_head_sing", 454 ``!ls. ls <> [] ==> [HD ls] <= ls``, 455 rw[HEAD_MEM, sublist_member_sing]); 456 457(* Theorem: ls <> [] ==> [LAST ls] <= ls *) 458(* Proof: LAST_MEM, sublist_member_sing *) 459val sublist_last_sing = store_thm( 460 "sublist_last_sing", 461 ``!ls. ls <> [] ==> [LAST ls] <= ls``, 462 rw[LAST_MEM, sublist_member_sing]); 463 464(* Theorem: l <= ls ==> !P. EVERY P ls ==> EVERY P l` *) 465(* Proof: 466 By induction on ls. 467 Base: !l. l <= [] ==> !P. EVERY P [] ==> EVERY P l 468 Note l <= [] ==> l = [] by sublist_of_nil 469 and EVERY P [] = T by implication, or EVERY_DEF 470 Step: !l. l <= ls ==> !P. EVERY P ls ==> EVERY P l ==> 471 !h l. l <= h::ls ==> !P. EVERY P (h::ls) ==> EVERY P l 472 l <= h::ls 473 If l = [], then EVERY P [] = T by EVERY_DEF 474 Otherwise, let l = k::t by list_CASES 475 Note EVERY P (h::ls) 476 ==> P h /\ EVERY P ls by EVERY_DEF 477 Then k::t <= h::ls 478 ==> k = h /\ t <= ls 479 or k <> h /\ k::t <= ls by sublist_def 480 For the first case, h = k, 481 P k /\ EVERY P t by induction hypothesis 482 ==> EVERY P (k::t) = EVERY P l by EVERY_DEF 483 For the second case, h <> k, 484 EVERY P (k::t) = EVERY P l by induction hypothesis 485*) 486val sublist_every = store_thm( 487 "sublist_every", 488 ``!l ls. l <= ls ==> !P. EVERY P ls ==> EVERY P l``, 489 Induct_on `ls` >- 490 rw[sublist_of_nil] >> 491 (Cases_on `l` >> simp[]) >> 492 metis_tac[sublist_def, EVERY_DEF]); 493 494(* ------------------------------------------------------------------------- *) 495(* More sublists, applying partial order properties *) 496(* ------------------------------------------------------------------------- *) 497 498(* Observation: 499When doing induction proofs on sublists about p <= q, 500Always induct on q, then take cases on p. 501*) 502 503(* The following induction theorem is already present during definition: 504> theorem "sublist_ind"; 505val it = |- !P. (!x. P [] x) /\ (!h1 t1. P (h1::t1) []) /\ 506 (!h1 t1 h2 t2. P t1 t2 /\ P (h1::t1) t2 ==> P (h1::t1) (h2::t2)) ==> 507 !v v1. P v v1: thm 508 509Just prove it as an exercise. 510*) 511 512(* Theorem: [Induction] For any property P satisfying, 513 (a) !y. P [] y = T 514 (b) !h x y. P x y /\ sublist x y ==> P (h::x) (h::y) 515 (c) !h x y. P x y /\ sublist x y ==> P x (h::y) 516 then !x y. sublist x y ==> P x y. 517*) 518(* Proof: 519 By induction on y. 520 Base: !x. x <= [] ==> P x [] 521 Note x = [] by sublist_of_nil 522 and P [] [] = T by given 523 Step: !x. x <= y ==> P x y ==> 524 !h x. x <= h::y ==> P x (h::y) 525 If x = [], then [] <= h::y = F by sublist_def 526 If x = h'::t, 527 If h' = h, t <= y by sublist_def, same heads 528 Thus P t y by induction hypothesis 529 and P t y /\ t <= y ==> P (h::t) (h::y) = P x (h::y) 530 If h' <> h, x <= y by sublist_def, different heads 531 Thus P x y by induction hypothesis 532 and P x y /\ x <= y ==> P x (h::y). 533*) 534val sublist_induct = store_thm( 535 "sublist_induct", 536 ``!P. (!y. P [] y) /\ 537 (!h x y. P x y /\ x <= y ==> P (h::x) (h::y)) /\ 538 (!h x y. P x y /\ x <= y ==> P x (h::y)) ==> 539 !x y. x <= y ==> P x y``, 540 ntac 2 strip_tac >> 541 Induct_on `y` >- 542 rw[sublist_of_nil] >> 543 rpt strip_tac >> 544 (Cases_on `x` >> fs[sublist_def])); 545 546(* Theorem: [Eliminate append from left]: (x ++ p) <= q ==> sublist p <= q *) 547(* Proof: 548 By induction on the extra list x. 549 The induction step follows from sublist_cons_remove. 550 551 By induction on x. 552 Base: !p q. [] ++ p <= q ==> p <= q 553 True since [] ++ p = p by APPEND 554 Step: !p q. x ++ p <= q ==> p <= q ==> 555 !h p q. h::x ++ p <= q ==> p <= q 556 h::x ++ p <= q 557 = h::(x ++ p) <= q by APPEND 558 ==> (x ++ p) <= q by sublist_cons_remove 559 ==> p <= q by induction hypothesis 560*) 561val sublist_append_remove = store_thm( 562 "sublist_append_remove", 563 ``!p q x. x ++ p <= q ==> p <= q``, 564 Induct_on `x` >> metis_tac[sublist_cons_remove, APPEND]); 565 566(* Theorem: [Include append to right] p <= q ==> p <= (x ++ q) *) 567(* Proof: 568 By induction on list x. 569 The induction step follows by sublist_cons_include. 570 571 By induction on x. 572 Base: !p q. p <= q ==> p <= [] ++ q 573 True since [] ++ q = q by APPEND 574 Step: !p q. p <= q ==> p <= x ++ q ==> 575 !h p q. p <= q ==> p <= h::x ++ q 576 p <= q 577 ==> p <= x ++ q by induction hypothesis 578 ==> p <= h::(x ++ q) by sublist_cons_include 579 = p <= h::x ++ q by APPEND 580*) 581val sublist_append_include = store_thm( 582 "sublist_append_include", 583 ``!p q x. p <= q ==> p <= x ++ q``, 584 Induct_on `x` >> metis_tac[sublist_cons_include, APPEND]); 585 586(* Theorem: [append after] p <= (p ++ q) *) 587(* Proof: 588 By induction on list p, and note that p and (p ++ q) have the same head. 589 Base: !q. [] <= [] ++ q, true by sublist_nil 590 Step: !q. p <= p ++ q ==> !h q. h::p <= h::p ++ q 591 p <= p ++ q by induction hypothesis 592 ==> h::p <= h::(p ++ q) by sublist_cons 593 ==> h::p <= h::p ++ q by APPEND 594*) 595val sublist_append_suffix = store_thm( 596 "sublist_append_suffix", 597 ``!p q. p <= p ++ q``, 598 Induct_on `p` >> rw[sublist_def]); 599 600(* Theorem: [append before] p <= (q ++ p) *) 601(* Proof: 602 By induction on q. 603 Base: !p. p <= [] ++ p 604 Note [] ++ p = p by APPEND 605 and p <= p by sublist_refl 606 Step: !p. p <= q ++ p ==> !h p. p <= h::q ++ p 607 p <= q ++ p by induction hypothesis 608 ==> p <= h::(q ++ p) by sublist_cons_include 609 = p <= h::q ++ p by APPEND 610*) 611val sublist_append_prefix = store_thm( 612 "sublist_append_prefix", 613 ``!p q. p <= q ++ p``, 614 Induct_on `q` >- 615 rw[sublist_refl] >> 616 rw[sublist_cons_include]); 617 618(* Theorem: [prefix append] p <= q <=> (x ++ p) <= (x ++ q) *) 619(* Proof: 620 By induction on x. 621 Base: !p q. p <= q <=> [] ++ p <= [] ++ q 622 Since [] ++ p = p /\ [] ++ q = q by APPEND 623 This is trivially true. 624 Step: !p q. p <= q <=> x ++ p <= x ++ q ==> 625 !h p q. p <= q <=> h::x ++ p <= h::x ++ q 626 p <= q <=> x ++ p <= x ++ q by induction hypothesis 627 <=> h::(x ++ p) <= h::(x ++ q) by sublist_cons 628 <=> h::x ++ p <= h::x ++ q by APPEND 629*) 630val sublist_prefix = store_thm( 631 "sublist_prefix", 632 ``!x p q. p <= q <=> (x ++ p) <= (x ++ q)``, 633 Induct_on `x` >> metis_tac[sublist_cons, APPEND]); 634 635(* Theorem: [no append to left] !p q. (p ++ q) <= q ==> p = [] *) 636(* Proof: 637 By induction on q. 638 Base: !p. p ++ [] <= [] ==> (p = []) 639 Note p ++ [] = p by APPEND 640 and p <= [] ==> p = [] by sublist_of_nil 641 Step: !p. p ++ q <= q ==> (p = []) ==> 642 !h p. p ++ h::q <= h::q ==> (p = []) 643 If p = [], true trivially. 644 If p = h'::t, 645 (h'::t) ++ (h::q) <= h::q 646 = h'::(t ++ h::q) <= h::q by APPEND 647 If h' = h, 648 Then t ++ h::q <= q by sublist_def, same heads 649 or (t ++ [h]) ++ q <= q by APPEND 650 ==> t ++ [h] = [] by induction hypothesis 651 which is F, hence h' <> h. 652 If h' <> h, 653 Then p ++ h::q <= q by sublist_def, different heads 654 or (p ++ [h]) ++ q <= q by APPEND 655 ==> (p ++ [h]) = [] by induction hypothesis 656 which is F, hence neither h' <> h. 657 All these shows that p = h'::t is impossible. 658*) 659val sublist_prefix_nil = store_thm( 660 "sublist_prefix_nil", 661 ``!p q. (p ++ q) <= q ==> (p = [])``, 662 Induct_on `q` >- 663 rw[sublist_of_nil] >> 664 rpt strip_tac >> 665 (Cases_on `p` >> fs[sublist_def]) >| [ 666 `t ++ h::q = (t ++ [h])++ q` by rw[] >> 667 `t ++ [h] <> []` by rw[] >> 668 metis_tac[], 669 `(t ++ h::q) <= q` by metis_tac[sublist_cons_remove] >> 670 `t ++ h::q = (t ++ [h])++ q` by rw[] >> 671 `t ++ [h] <> []` by rw[] >> 672 metis_tac[] 673 ]); 674 675(* Theorem: [tail append - if] p <= q ==> (p ++ [h]) <= (q ++ [h]) *) 676(* Proof: 677 By sublist induction, this is to show: 678 (1) [h] <= q ++ [h] 679 Note [h] <= [h] by sublist_refl 680 ==> [h] <= q ++ [h] by sublist_append_prefix 681 (2) h::(p ++ [h']) <= h::(q ++ [h']) 682 Note p ++ [h'] <= q ++ [h'] by induction hypothesis 683 ==> h::(p ++ [h']) <= h::(q ++ [h']) by sublist_cons 684 (3) p ++ [h'] <= h::(q ++ [h']) 685 Note p ++ [h'] <= q ++ [h'] by induction hypothesis 686 ==> p ++ [h'] <= h::(q + [h']) by sublist_cons_include 687*) 688(* First method *) 689val sublist_append_if = store_thm( 690 "sublist_append_if", 691 ``!p q h. p <= q ==> (p ++ [h]) <= (q ++ [h])``, 692 Induct_on `q` >- 693 rw[sublist_of_nil, sublist_refl] >> 694 rpt strip_tac >> 695 (Cases_on `p` >> fs[sublist_def]) >- 696 (Cases_on `h' = h` >> rw[sublist_append_prefix]) >> 697 metis_tac[APPEND]); 698(* Second method -- change goal to match *) 699val sublist_append_if = store_thm( 700 "sublist_append_if", 701 ``!p q. p <= q ==> !h. (p ++ [h]) <= (q ++ [h])``, 702 ho_match_mp_tac sublist_induct >> 703 rw[] >- 704 rw[sublist_refl, sublist_append_prefix] >- 705 metis_tac[sublist_cons] >> 706 rw[sublist_cons_include]); 707(* Third method *) 708val sublist_append_if = store_thm( 709 "sublist_append_if", 710 ``!p q h. p <= q ==> (p ++ [h]) <= (q ++ [h])``, 711 rw[sublist_snoc, GSYM SNOC_APPEND]); 712 713(* Theorem: [tail append - only if] p ++ [h] <= q ++ [h] ==> p <= q *) 714(* Proof: 715 By induction on q. 716 Base: !p h. p ++ [h] <= [] ++ [h] ==> p <= [] 717 Note [] ++ [h] = [h] by APPEND 718 and p ++ [h] <= [h] ==> p = [] by sublist_prefix_nil 719 and [] <= [] by sublist_nil 720 Step: !p h. p ++ [h] <= q ++ [h] ==> p <= q ==> 721 !h p h'. p ++ [h'] <= h::q ++ [h'] ==> p <= h::q 722 If p = [], [h'] <= h::q ++ [h'] = F by sublist_def 723 If p = h''::t, 724 h''::t ++ [h'] = h''::(t ++ [h']) by APPEND 725 If h'' = h', 726 Then t ++ [h'] <= q ++ [h'] by sublist_def, same heads 727 ==> t <= q by induction hypothesis 728 If h'' <> h', 729 Then h''::t ++ [h'] <= q ++ [h'] by sublist_def, different heads 730 ==> h''::t <= q by induction hypothesis 731*) 732val sublist_append_only_if = store_thm( 733 "sublist_append_only_if", 734 ``!p q h. (p ++ [h]) <= (q ++ [h]) ==> p <= q``, 735 Induct_on `q` >- 736 metis_tac[sublist_prefix_nil, sublist_nil, APPEND] >> 737 rpt strip_tac >> 738 (Cases_on `p` >> fs[sublist_def]) >- 739 metis_tac[] >> 740 `h''::(t ++ [h']) = (h''::t) ++ [h']` by rw[] >> 741 metis_tac[]); 742 743(* Theorem: [tail append] p <= q <=> p ++ [h] <= q ++ [h] *) 744(* Proof: by sublist_append_if, sublist_append_only_if *) 745val sublist_append_iff = store_thm( 746 "sublist_append_iff", 747 ``!p q h. p <= q <=> (p ++ [h]) <= (q ++ [h])``, 748 metis_tac[sublist_append_if, sublist_append_only_if]); 749 750(* Theorem: [suffix append] sublist p q ==> sublist (p ++ x) (q ++ x) *) 751(* Proof: 752 By induction on x. 753 Base: !p q. p <= q <=> p ++ [] <= q ++ [] 754 True by p ++ [] = p, q ++ [] = q by APPEND 755 Step: !p q. p <= q <=> p ++ x <= q ++ x ==> 756 !h p q. p <= q <=> p ++ h::x <= q ++ h::x 757 p <= q 758 <=> (p ++ [h]) <= (q ++ [h]) by sublist_append_iff 759 <=> (p ++ [h]) ++ x <= (q ++ [h]) ++ x by induction hypothesis 760 <=> p ++ (h::x) <= q ++ (h::x) by APPEND 761*) 762val sublist_suffix = store_thm( 763 "sublist_suffix", 764 ``!x p q. p <= q <=> (p ++ x) <= (q ++ x)``, 765 Induct >- 766 rw[] >> 767 rpt strip_tac >> 768 `!z. z ++ h::x = (z ++ [h]) ++ x` by rw[] >> 769 metis_tac[sublist_append_iff]); 770 771(* Theorem : (a <= b) /\ (c <= d) ==> (a ++ c) <= (b ++ d) *) 772(* Proof: 773 Note a ++ c <= a ++ d by sublist_prefix 774 and a ++ d <= b ++ d by sublist_suffix 775 ==> a ++ c <= b ++ d by sublist_trans 776*) 777val sublist_append_pair = store_thm( 778 "sublist_append_pair", 779 ``!a b c d. (a <= b) /\ (c <= d) ==> (a ++ c) <= (b ++ d)``, 780 metis_tac[sublist_prefix, sublist_suffix, sublist_trans]); 781 782(* Theorem: [Extended Append, or Decomposition] (h::t) <= q <=> ?x y. (q = x ++ (h::y)) /\ (t <= y) *) 783(* Proof: 784 By induction on list q. 785 Base case is to prove: 786 sublist (h::t) [] <=> ?x y. ([] = x ++ (h::y)) /\ (sublist t y) 787 Hypothesis sublist (h::t) [] is F by SUBLIST_NIL. 788 In the conclusion, [] cannot be decomposed, hence implication is valid. 789 Step case is to prove: 790 (sublist (h::t) q <=> ?x y. (q = x ++ (h::y)) /\ (sublist t y)) ==> 791 (sublist (h::t) (h'::q) <=> ?x y. (h'::q = x ++ (h::y)) /\ (sublist t y)) 792 Applying SUBLIST definition and split the if-and-only-if parts, there are 4 cases: 793 When h = h', if part: 794 sublist (h::t) (h::q) ==> ?x y. (h::q = x ++ (h::y)) /\ (sublist t y) 795 For this case, choose x=[], y=q, and sublist (h::t) (h::q) = sublist t q, by SUBLIST same head. 796 When h = h', only-if part: 797 ?x y. (h::q = x ++ (h::y)) /\ (sublist t y) ==> sublist (h::t) (h::q) 798 Take cases on x. 799 When x = [], 800 h::q = h::y ==> q = y, 801 hence sublist t y = sublist t q ==> sublist (h::t) (h::q) by SUBLIST same head. 802 When x = h''::t', 803 h::q = (h''::t') ++ (h::y) = h''::(t' ++ (h::y)) ==> 804 q = t' ++ (h::y), 805 hence sublist t y ==> sublist t q (by SUBLIST_APPENDR_I) ==> sublist (h::t) (h::q). 806 When ~(h=h'), if part: 807 sublist (h::t) (h'::q) ==> ?x y. (h'::q = x ++ (h::y)) /\ (sublist t y) 808 From hypothesis, 809 sublist (h::t) (h'::q) 810 = sublist (h::t) q when ~(h=h'), by SUBLIST definition 811 ==> ?x1 y1. (q = x1 ++ (h::y1)) /\ (sublist t y1)) by inductive hypothesis 812 Now (h'::q) = (h'::(x1 ++ (h::y1)) = (h'::x1) ++ (h::y1) by APPEND associativity 813 So taking x = h'::x1, y = y1, this gives the conclusion. 814 When ~(h=h'), only-if part: 815 ?x y. (h'::q = x ++ (h::y)) /\ (sublist t y) ==> sublist (h::t) (h'::q) 816 The case x = [] is impossible by list equality, since ~(h=h'). 817 Hence x = h'::t', giving: 818 q = t'++(h::y) /\ (sublist t y) 819 = sublist (h::t) q by inductive hypothesis (only-if) 820 ==> sublist (h::t) (h'::q) by SUBLIST, different head. 821*) 822val sublist_append_extend = store_thm( 823 "sublist_append_extend", 824 ``!h t q. h::t <= q <=> ?x y. (q = x ++ (h::y)) /\ (t <= y)``, 825 ntac 2 strip_tac >> 826 Induct >- 827 rw[sublist_of_nil] >> 828 rpt strip_tac >> 829 (Cases_on `h = h'` >> rw[EQ_IMP_THM]) >| [ 830 `h::q = [] ++ [h] ++ q` by rw[] >> 831 metis_tac[sublist_cons], 832 `h::t <= h::y` by rw[GSYM sublist_cons] >> 833 `x ++ [h] ++ y = x ++ (h::y)` by rw[] >> 834 metis_tac[sublist_append_include], 835 `h::t <= q` by metis_tac[sublist_def] >> 836 metis_tac[APPEND, APPEND_ASSOC], 837 `h::t <= h::y` by rw[GSYM sublist_cons] >> 838 `x ++ [h] ++ y = x ++ (h::y)` by rw[] >> 839 metis_tac[sublist_append_include] 840 ]); 841 842 843(* ------------------------------------------------------------------------- *) 844(* Application of sublist. *) 845(* ------------------------------------------------------------------------- *) 846 847(* Theorem: p <= q ==> (MAP f p) <= (MAP f q) *) 848(* Proof: 849 By induction on q. 850 Base: !p. p <= [] ==> MAP f p <= MAP f [] 851 Note p = [] by sublist_of_nil 852 and MAP f [] by MAP 853 so [] <= [] by sublist_nil 854 Step: !p. p <= q ==> MAP f p <= MAP f q ==> 855 !h p. p <= h::q ==> MAP f p <= MAP f (h::q) 856 If p = [], [] <= h::q = F by sublist_def 857 If p = h'::t, 858 If h' = h, 859 Then t <= q by sublist_def, same heads 860 ==> MAP f t <= MAP f q by induction hypothesis 861 ==> h::MAP f t <= h::MAP f q by sublist_cons 862 ==> MAP f (h::t) <= MAP f (h::q) by MAP 863 or MAP f p <= MAP f (h::q) by p = h::t 864 If h' <> h, 865 Then p <= q by sublist_def, different heads 866 ==> MAP f p <= MAP f q by induction hypothesis 867 ==> MAP f p <= h::MAP f q by sublist_cons_include 868 or MAP f p <= MAP f (h::q) by MAP 869*) 870val MAP_SUBLIST = store_thm( 871 "MAP_SUBLIST", 872 ``!f p q. p <= q ==> (MAP f p) <= (MAP f q)``, 873 strip_tac >> 874 Induct_on `q` >- 875 rw[sublist_of_nil, sublist_nil] >> 876 rpt strip_tac >> 877 (Cases_on `p` >> simp[sublist_def]) >> 878 metis_tac[sublist_def, sublist_cons_include, MAP]); 879 880(* Theorem: l1 <= l2 ==> SUM l1 <= SUM l2 *) 881(* Proof: 882 By induction on q. 883 Base: !p. p <= [] ==> SUM p <= SUM [] 884 Note p = [] by sublist_of_nil 885 and SUM [] = 0 by SUM 886 Hence true. 887 Step: !p. p <= q ==> SUM p <= SUM q ==> 888 !h p. p <= h::q ==> SUM p <= SUM (h::q) 889 If p = [], [] <= h::q = F by sublist_def 890 If p = h'::t, 891 If h' = h, 892 Then t <= q by sublist_def, same heads 893 ==> SUM t <= SUM q by induction hypothesis 894 ==> h + SUM t <= h + SUM q by arithmetic 895 ==> SUM (h::t) <= SUM (h::q) by SUM 896 or SUM p <= SUM (h::q) by p = h::t 897 If h' <> h, 898 Then p <= q by sublist_def, different heads 899 ==> SUM p <= SUM q by induction hypothesis 900 ==> SUM p <= h + SUM q by arithmetic 901 ==> SUM p <= SUM (h::q) by SUM 902*) 903val SUM_SUBLIST = store_thm( 904 "SUM_SUBLIST", 905 ``!p q. p <= q ==> SUM p <= SUM q``, 906 Induct_on `q` >- 907 rw[sublist_of_nil] >> 908 rpt strip_tac >> 909 (Cases_on `p` >> fs[sublist_def]) >> 910 `h' + SUM t <= SUM q` by metis_tac[SUM] >> 911 decide_tac); 912 913(* Theorem: m < n ==> [m; n] <= [m .. n] *) 914(* Proof: 915 By induction on n. 916 Base: !m. m < 0 ==> [m; 0] <= [m .. 0], true by m < 0 = F. 917 Step: !m. m < n ==> [m; n] <= [m .. n] ==> 918 !m. m < SUC n ==> [m; SUC n] <= [m .. SUC n] 919 Note m < SUC n means m <= n. 920 If m = n, LHS = [n; SUC n] 921 RHS = [n .. (n + 1)] = [n; SUC n] by ADD1 922 = LHS, thus true by sublist_refl 923 If m < n, [m; n] <= [m .. n] by induction hypothesis 924 SNOC (SUC n) [m; n] <= SNOC (SUC n) [m .. n] by sublist_snoc 925 [m; n; SUC n] <= [m .. SUC n] by SNOC, listRangeINC_SNOC 926 But [m; SUC n] <= [m; n; SUC n] by sublist_def 927 Thus [m; SUC n] <= [m .. SUC n] by sublist_trans 928*) 929val listRangeINC_sublist = store_thm( 930 "listRangeINC_sublist", 931 ``!m n. m < n ==> [m; n] <= [m .. n]``, 932 Induct_on `n` >- 933 rw[] >> 934 rpt strip_tac >> 935 `(m = n) \/ m < n` by decide_tac >| [ 936 rw[listRangeINC_def, ADD1] >> 937 rw[sublist_refl], 938 `[m; n] <= [m .. n]` by rw[] >> 939 `SNOC (SUC n) [m; n] <= SNOC (SUC n) [m .. n]` by rw[sublist_snoc] >> 940 `SNOC (SUC n) [m; n] = [m; n; SUC n]` by rw[] >> 941 `SNOC (SUC n) [m .. n] = [m .. SUC n]` by rw[listRangeINC_SNOC, ADD1] >> 942 `[m; SUC n] <= [m; n; SUC n]` by rw[sublist_def] >> 943 metis_tac[sublist_trans] 944 ]); 945 946(* Theorem: m + 1 < n ==> [m; (n - 1)] <= [m ..< n] *) 947(* Proof: 948 By induction on n. 949 Base: !m. m + 1 < 0 ==> [m; 0 - 1] <= [m ..< 0], true by m + 1 < 0 = F. 950 Step: !m. m + 1 < n ==> [m; n - 1] <= [m ..< n] ==> 951 !m. m + 1 < SUC n ==> [m; SUC n - 1] <= [m ..< SUC n] 952 Note m + 1 < SUC n means m + 1 <= n. 953 If m + 1 = n, LHS = [m; SUC n - 1] = [m; n] 954 RHS = [m ..< (n + 1)] = [m; n] by ADD1 955 = LHS, thus true by sublist_refl 956 If m + 1 < n, [m; n - 1] <= [m ..< n] by induction hypothesis 957 SNOC n [m; n - 1] <= SNOC n [m ..< n] by sublist_snoc 958 [m; n - 1; n] <= [m ..< SUC n] by SNOC, listRangeLHI_SNOC, ADD1 959 But [m; SUC n - 1] <= [m; n] <= [m; n - 1; n] by sublist_def 960 Thus [m; SUC n - 1] <= [m ..< SUC n] by sublist_trans 961*) 962val listRangeLHI_sublist = store_thm( 963 "listRangeLHI_sublist", 964 ``!m n. m + 1 < n ==> [m; (n - 1)] <= [m ..< n]``, 965 Induct_on `n` >- 966 rw[] >> 967 rpt strip_tac >> 968 `SUC n - 1 = n` by decide_tac >> 969 `(m + 1 = n) \/ m + 1 < n` by decide_tac >| [ 970 rw[listRangeLHI_def, ADD1] >> 971 rw[sublist_refl], 972 `[m; n - 1] <= [m ..< n]` by rw[] >> 973 `SNOC n [m; n - 1] <= SNOC n [m ..< n]` by rw[sublist_snoc] >> 974 `SNOC n [m; n - 1] = [m; n - 1; n]` by rw[] >> 975 `SNOC n [m ..< n] = [m ..< SUC n]` by rw[listRangeLHI_SNOC, ADD1] >> 976 `[m; SUC n - 1] <= [m; n - 1; n]` by rw[sublist_def] >> 977 metis_tac[sublist_trans] 978 ]); 979 980(* ------------------------------------------------------------------------- *) 981 982(* export theory at end *) 983val _ = export_theory(); 984 985(*===========================================================================*) 986