1(* load "rich_listTheory"; *) 2open HolKernel boolLib bossLib Q listTheory rich_listTheory arithmeticTheory; 3 4val _ = new_theory "my_list"; 5 6(* ------------------------------------------------------------------------- *) 7 8infix \\ << >> 9 10val op \\ = op THEN; 11val op << = op THENL; 12val op >> = op THEN1; 13 14(* ------------------------------------------------------------------------- *) 15 16val LIST_EQ = store_thm("LIST_EQ", 17 `!a b. (LENGTH a = LENGTH b) /\ 18 (!x. x < LENGTH a ==> (EL x a = EL x b)) ==> 19 (a = b)`, 20 Induct_on `b` >> SIMP_TAC list_ss [LENGTH_NIL] 21 \\ Induct_on `a` \\ RW_TAC list_ss [] 22 >> POP_ASSUM (fn th => PROVE_TAC [(SIMP_RULE list_ss [] o SPEC `0`) th]) 23 \\ POP_ASSUM (fn th => PROVE_TAC 24 [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC x`) th])); 25 26val NULL_SNOC = store_thm("NULL_SNOC", 27 `!l x. ~NULL (SNOC x l)`, 28 Cases \\ SIMP_TAC list_ss [SNOC]); 29 30val FILTER_ALL = store_thm("FILTER_ALL", 31 `!l. (!n. n < LENGTH l ==> ~P (EL n l)) ==> (FILTER P l = [])`, 32 Induct \\ RW_TAC list_ss [] 33 >> (EXISTS_TAC `0` \\ ASM_SIMP_TAC list_ss []) 34 \\ POP_ASSUM (fn th => PROVE_TAC 35 [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC n`) th])); 36 37val FILTER_NONE = store_thm("FILTER_NONE", 38 `!l. (!n. n < LENGTH l ==> P (EL n l)) ==> (FILTER P l = l)`, 39 Induct \\ RW_TAC list_ss [] 40 >> POP_ASSUM (fn th => ASM_SIMP_TAC std_ss 41 [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC n`) th]) 42 \\ POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE list_ss [] o SPEC `0`)); 43 44val MAP_GENLIST = store_thm("MAP_GENLIST", 45 `!f g n. MAP f (GENLIST g n) = GENLIST (f o g) n`, 46 Induct_on `n` \\ ASM_SIMP_TAC list_ss [GENLIST,MAP_SNOC]); 47 48val EL_GENLIST = store_thm("EL_GENLIST", 49 `!f n x. x < n ==> (EL x (GENLIST f n) = f x)`, 50 Induct_on `n` >> SIMP_TAC arith_ss [] 51 \\ REPEAT STRIP_TAC \\ REWRITE_TAC [GENLIST] 52 \\ Cases_on `x < n` 53 \\ POP_ASSUM (fn th => ASSUME_TAC 54 (SUBS [(GSYM o SPECL [`f`,`n`]) LENGTH_GENLIST] th) 55 \\ ASSUME_TAC th) 56 >> ASM_SIMP_TAC bool_ss [EL_SNOC] 57 \\ `x = LENGTH (GENLIST f n)` by FULL_SIMP_TAC arith_ss [LENGTH_GENLIST] 58 \\ ASM_SIMP_TAC bool_ss [EL_LENGTH_SNOC] 59 \\ REWRITE_TAC [LENGTH_GENLIST]); 60 61val HD_GENLIST = save_thm("HD_GENLIST", 62 (SIMP_RULE arith_ss [EL] o SPECL [`f`,`SUC n`,`0`]) EL_GENLIST); 63 64val GENLIST_FUN_EQ = store_thm("GENLIST_FUN_EQ", 65 `!n f g. (!x. x < n ==> (f x = g x)) ==> (GENLIST f n = GENLIST g n)`, 66 metisLib.METIS_TAC [LIST_EQ,GSYM EL_GENLIST,LENGTH_GENLIST]); 67 68val EL_BUTFIRSTN = store_thm("EL_BUTFIRSTN", 69 `!m n l. m + n < LENGTH l ==> 70 (EL m (BUTFIRSTN n l) = EL (m + n) l)`, 71 Induct_on `l` \\ RW_TAC list_ss [] \\ Cases_on `n` 72 \\ FULL_SIMP_TAC list_ss [BUTFIRSTN,ADD_CLAUSES]); 73 74val SNOC_EL_FIRSTN = store_thm("SNOC_EL_FIRSTN", 75 `!n l. n < LENGTH l ==> (SNOC (EL n l) (FIRSTN n l) = FIRSTN (SUC n) l)`, 76 Induct \\ Cases_on `l` \\ ASM_SIMP_TAC list_ss [SNOC,FIRSTN]); 77 78val ZIP_FIRSTN_LEQ = store_thm("ZIP_FIRSTN_LEQ", 79 `!n a b. n <= LENGTH a /\ LENGTH a <= LENGTH b ==> 80 (ZIP (FIRSTN n a,FIRSTN n b) = FIRSTN n (ZIP (a,FIRSTN (LENGTH a) b)))`, 81 Induct \\ ASM_SIMP_TAC list_ss [FIRSTN] 82 \\ Cases \\ Cases \\ ASM_SIMP_TAC list_ss [FIRSTN,ZIP]); 83 84val ZIP_FIRSTN = store_thm("ZIP_FIRSTN", 85 `!n a b. n <= LENGTH a /\ (LENGTH a = LENGTH b) ==> 86 (ZIP (FIRSTN n a,FIRSTN n b) = FIRSTN n (ZIP (a,b)))`, 87 SIMP_TAC arith_ss [ZIP_FIRSTN_LEQ,FIRSTN_LENGTH_ID]); 88 89val EL_FIRSTN = store_thm("EL_FIRSTN", 90 `!n x l. x < n /\ n <= LENGTH l ==> (EL x (FIRSTN n l) = EL x l)`, 91 Induct \\ ASM_SIMP_TAC list_ss [FIRSTN] 92 \\ Cases \\ Cases \\ ASM_SIMP_TAC list_ss [FIRSTN]); 93 94val LENGTH_TL = store_thm("LENGTH_TL", 95 `!l. 0 < LENGTH l ==> (LENGTH (TL l) = LENGTH l - 1)`, 96 Cases \\ SIMP_TAC list_ss []); 97 98val ZIP_APPEND = store_thm("ZIP_APPEND", 99 `!a b c d. (LENGTH a = LENGTH b) /\ 100 (LENGTH c = LENGTH d) ==> 101 (ZIP (a,b) ++ ZIP (c,d) = ZIP (a ++ c,b ++ d))`, 102 Induct_on `b` >> SIMP_TAC list_ss [LENGTH_NIL] 103 \\ Induct_on `d` >> SIMP_TAC list_ss [LENGTH_NIL] 104 \\ Induct_on `a` >> SIMP_TAC list_ss [LENGTH_NIL] 105 \\ Induct_on `c` >> SIMP_TAC list_ss [LENGTH_NIL] 106 \\ MAP_EVERY X_GEN_TAC [`h1`,`h2`,`h3`,`h4`] 107 \\ RW_TAC list_ss [] 108 \\ `LENGTH (h1::c) = LENGTH (h3::d)` 109 by ASM_SIMP_TAC list_ss [] 110 \\ `ZIP (a,b) ++ ZIP (h1::c,h3::d) = ZIP (a ++ h1::c,b ++ h3::d)` 111 by ASM_SIMP_TAC list_ss [] 112 \\ FULL_SIMP_TAC list_ss []); 113 114val ZIP_GENLIST = store_thm("ZIP_GENLIST", 115 `!l f n. (LENGTH l = n) ==> 116 (ZIP (l,GENLIST f n) = GENLIST (\x. (EL x l,f x)) n)`, 117 REPEAT STRIP_TAC 118 \\ `LENGTH (ZIP (l,GENLIST f n)) = LENGTH (GENLIST (\x. (EL x l,f x)) n)` 119 by metisLib.METIS_TAC [LENGTH_GENLIST,LENGTH_ZIP] 120 \\ IMP_RES_TAC LIST_EQ 121 \\ POP_ASSUM MATCH_MP_TAC 122 \\ RW_TAC arith_ss [LENGTH_GENLIST,LENGTH_ZIP,listTheory.EL_ZIP,EL_GENLIST] 123); 124 125val GENLIST_APPEND = store_thm("GENLIST_APPEND", 126 `!f a b. GENLIST f (a + b) = (GENLIST f b) ++ (GENLIST (\t. f (t + b)) a)`, 127 Induct_on `a` 128 \\ ASM_SIMP_TAC list_ss [GENLIST,APPEND_SNOC,arithmeticTheory.ADD_CLAUSES] 129); 130 131val NULL_LENGTH = store_thm("NULL_LENGTH", 132 `!l. NULL l = (LENGTH l = 0)`, 133 Cases \\ METIS_TAC [LENGTH,NULL,SUC_NOT]); 134 135val APPEND_SNOC1 = store_thm("APPEND_SNOC1", 136 `!l1 x l2. SNOC x l1 ++ l2 = l1 ++ x::l2`, 137 METIS_TAC [SNOC_APPEND,CONS_APPEND, APPEND_ASSOC]); 138 139val SNOC_INDUCT_TAC = INDUCT_THEN SNOC_INDUCT ASSUME_TAC; 140 141val FOLDL_MAP2 = store_thm("FOLDL_MAP2", 142 `!f e g l. FOLDL f e (MAP g l) = FOLDL (\x y. f x (g y)) e l`, 143 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN SNOC_INDUCT_TAC 144 THEN ASM_REWRITE_TAC[MAP,FOLDL,FOLDL_SNOC,MAP_SNOC,FOLDR] 145 THEN BETA_TAC THEN REWRITE_TAC[]); 146 147val SPLITP_EVERY = store_thm("SPLITP_EVERY", 148 `!P l. EVERY (\x. ~P x) l ==> (SPLITP P l = (l, []))`, 149 Induct_on `l` THEN SRW_TAC [] [SPLITP]); 150 151val EVERY_GENLIST = store_thm("EVERY_GENLIST", 152 `!n. (!i. i < n ==> P (f i)) ==> EVERY P (GENLIST f n)`, 153 Induct THEN SRW_TAC [] [ALL_EL_SNOC,GENLIST] 154 THEN `!i. i < n ==> P (f i)` by ASM_SIMP_TAC arith_ss [] 155 THEN METIS_TAC []); 156 157(* ------------------------------------------------------------------------- *) 158 159val _ = export_theory(); 160