1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6val _ = new_theory "more_list"; 7 8 9(* 10app load [ 11 "numTheory", "listTheory", "rich_listTheory", "listLib", "pred_setLib", 12 "more_setTheory", 13 "arithLib", "Psyntax" ]; 14*) 15 16open combinTheory numTheory arithmeticTheory 17 listTheory rich_listTheory listLib more_setTheory 18 numLib Psyntax ; 19 20 21open tactics; 22 23 24 25val MAP2_APPEND = store_thm 26 ("MAP2_APPEND", 27 ���!s1 s2 t1 t2 (f:'a->'b->'c). 28 (LENGTH s1 = LENGTH s2) ==> 29 (MAP2 f (APPEND s1 t1) (APPEND s2 t2) = 30 APPEND (MAP2 f s1 s2) (MAP2 f t1 t2))���, 31 LIST_INDUCT_TAC 32 THENL 33 [ LIST_INDUCT_TAC 34 THEN REWRITE_TAC[LENGTH,APPEND,MAP2,SUC_NOT], 35 36 GEN_TAC 37 THEN LIST_INDUCT_TAC 38 THEN REWRITE_TAC[LENGTH,NOT_SUC] 39 THEN REWRITE_TAC[ADD1,EQ_MONO_ADD_EQ] 40 THEN REWRITE_TAC[APPEND,MAP2] 41 THEN REPEAT GEN_TAC 42 THEN DISCH_TAC 43 THEN RES_TAC 44 THEN ASM_REWRITE_TAC[] 45 ] 46 ); 47 48val AND_EL = store_thm 49 ("AND_EL", 50 ���(AND_EL [] = T) /\ 51 (!x l. AND_EL (CONS x l) = (x /\ AND_EL l))���, 52 REWRITE_TAC[AND_EL_DEF] 53 THEN REWRITE_TAC[ALL_EL] 54 THEN REWRITE_TAC[combinTheory.I_THM] 55 ); 56 57val AND_EL_APPEND = store_thm 58 ("AND_EL_APPEND", 59 ���!s t. AND_EL (APPEND s t) = (AND_EL s /\ AND_EL t)���, 60 REWRITE_TAC[AND_EL_DEF] 61 THEN LIST_INDUCT_TAC 62 THEN REWRITE_TAC[APPEND,ALL_EL] 63 THEN ASM_REWRITE_TAC[CONJ_ASSOC] 64 ); 65 66(* =============================================================== *) 67(* LENGTH_FILTER says that if we filter a list into two using P *) 68(* as a predicate, then the sum of the lengths of the two parts *) 69(* must equal the length of the whole. *) 70(* =============================================================== *) 71 72val LENGTH_FILTER = store_thm 73 ("LENGTH_FILTER", 74 ���!(l:'a list) P. 75 LENGTH (FILTER P l) + LENGTH (FILTER ($~ o P) l) = LENGTH l���, 76 LIST_INDUCT_TAC 77 THEN REWRITE_TAC[FILTER] 78 THENL 79 [ REWRITE_TAC[LENGTH,ADD_0], 80 81 REWRITE_TAC[o_THM] 82 THEN REPEAT GEN_TAC 83 THEN COND_CASES_TAC 84 THEN ASM_REWRITE_TAC[LENGTH,ADD_CLAUSES] 85 ] 86 ); 87 88(* =============================================================== *) 89(* Applying LENGTH_FILTER to a specific filter, we can calculate *) 90(* the length of the partitions of num lists where the partition *) 91(* separates the bottom of a range from the larger members. *) 92(* For all lists of numbers l, the number of elements of value n *) 93(* or more equals the number of elements of value n plus the *) 94(* number of elements of value more than n. *) 95(* =============================================================== *) 96 97Theorem LENGTH_FILTER_LESS_EQ: 98 !l n. LENGTH (FILTER (\y. n = y) l) + LENGTH (FILTER (\y. n < y) l) = 99 LENGTH (FILTER (\y. n <= y) l) 100Proof 101 REWRITE_TAC 102 [(GENL [���l:num list���,���n:num���] 103 o REWRITE_RULE[ARITH_PROVE ��� (n=y) /\ (n <= y) <=> (n = y)���, 104 ARITH_PROVE ���~(n=y) /\ (n <= y) <=> (n < y)���] 105 o CONV_RULE (DEPTH_CONV BETA_CONV) 106 o REWRITE_RULE[FILTER_FILTER,o_THM] 107 o ISPECL[���FILTER (\y. n <= y) l���,���\y:num. n = y���]) 108 LENGTH_FILTER] 109QED 110 111 112(* 113FILTER_MAP; 114 |- !f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l) 115*) 116 117 118val SL = 119 new_recursive_definition 120 {rec_axiom = listTheory.list_Axiom, 121 name = "SL", 122 def = ���(SL NIL = {}) /\ 123 (SL (CONS (y:'a) l) = y INSERT (SL l))���}; 124 125 126val SL_APPEND = store_thm 127 ("SL_APPEND", 128 ���!(l1: 'a list) l2. SL (APPEND l1 l2) = (SL l1 UNION SL l2)���, 129 LIST_INDUCT_TAC 130 THEN ASM_REWRITE_TAC[APPEND,SL,UNION] 131 ); 132 133 134val SL_FLAT = store_thm 135 ("SL_FLAT", 136 ���!(l: 'a list list). SL (FLAT l) = UNION_SET (SL (MAP SL l))���, 137 LIST_INDUCT_TAC 138 THEN REWRITE_TAC[FLAT,MAP,SL,UNION_SET] 139 THEN ASM_REWRITE_TAC[SL_APPEND] 140 ); 141 142val SL_MAP = store_thm 143 ("SL_MAP", 144 ���!l (f: 'a->'b). SL (MAP f l) = IMAGE f (SL l)���, 145 LIST_INDUCT_TAC 146 THEN ASM_REWRITE_TAC[MAP,SL,IMAGE] 147 ); 148 149val DELETE_DIFF_SL = 150 store_thm 151 ("DELETE_DIFF_SL", 152 ���!xs s (e:'a). 153 s DELETE e DIFF SL xs = s DIFF SL (e::xs)���, 154 LIST_INDUCT_TAC 155 THEN REWRITE_TAC[SL,DIFFF] 156 ); 157 158 159val DL = 160 new_recursive_definition 161 {rec_axiom = listTheory.list_Axiom, 162 name = "DL", 163 def = ���(DL NIL = T) /\ 164 (DL (CONS (y:'a) l) = (~(y IN SL l) /\ DL l))���}; 165 166 167 168val _ = export_theory(); 169 170val _ = print_theory_to_file "-" "more_list.lst"; 171 172val _ = html_theory "more_list"; 173