1structure listSimps :> listSimps = 2struct 3 4open boolLib HolKernel simpLib 5open listTheory listSyntax; 6 7(*-==============================================================-*) 8(*- CONVERSIONS added by TT 03 Dec 2009 -*) 9(*-==============================================================-*) 10 11structure Parse = 12struct 13 open Parse 14 val (Type,Term) = parse_from_grammars listTheory.list_grammars 15 fun == q x = Type q 16end 17open Parse 18 19val APPEND_EVAL_CONV = 20 PURE_REWRITE_CONV [listTheory.APPEND_NIL, listTheory.APPEND] 21 22(* 23 takes a list of the form ``x1::x2::..::xn::l`` and converts it to 24 ``[x1;x2;...;xn]++l`` 25*) 26 27local 28 val NORM_CONS_conv1 = REWR_CONV (CONJUNCT2 listTheory.APPEND) 29 val NORM_CONS_conv2 = REWR_CONV (CONJUNCT1 listTheory.APPEND) 30 fun NORM_CONS_conv t = ((NORM_CONS_conv1 THENC RAND_CONV NORM_CONS_conv) 31 ORELSEC NORM_CONS_conv2) t 32in 33 fun NORM_CONS_CONV tt = 34 let 35 val (eL, r) = strip_cons tt 36 val _ = if null eL orelse is_nil r then raise UNCHANGED else () 37 val t' = mk_append (listSyntax.mk_list (eL, type_of (hd eL)), r) 38 in 39 GSYM (NORM_CONS_conv t') 40 end 41end 42 43(* 44 takes a list of the form ``[x1;...;xn] ++ [y1;...;ym]`` and converts it to 45 ``[x1;...;xn;y1;...;ym]`` 46*) 47 48fun APPEND_SIMPLE_LISTS_CONV t = 49 let 50 val (l1, l2) = dest_append t 51 val _ = if is_list l1 andalso is_list l2 then () else raise UNCHANGED 52 in 53 APPEND_EVAL_CONV t 54 end 55 handle HOL_ERR _ => raise UNCHANGED 56 57(* 58 takes a list of the form ``(l ++ [x1;...;xn]) ++ [y1;...;ym]`` and converts 59 it to ``l ++ [x1;...;xn;y1;...;ym]`` 60*) 61 62fun APPEND_SIMPLE_LISTS_ASSOC_CONV t = 63 let 64 val (l1, l2) = dest_append t 65 val (l11, l12) = dest_append l1 66 val _ = if is_list l2 andalso is_list l12 then () else raise UNCHANGED 67 in 68 (REWR_CONV (GSYM listTheory.APPEND_ASSOC) 69 THENC RAND_CONV APPEND_EVAL_CONV) t 70 end 71 handle HOL_ERR _ => raise UNCHANGED 72 73(* --------------------------------------------------------------------- *) 74(* NORM_CONS_APPEND_NO_EVAL_CONV : conv *) 75(* bring appends and conses into normal form. The resulting list is *) 76(* consists of appending serveral lists. Cons operations are put into *) 77(* lists just containing these elements. Empty lists are removed and *) 78(* associative of append used. Moreover, some rewrites for SNOC and *) 79(* REVERSE are applied *) 80(* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *) 81(* REVERSE (x5::x6::x7::(l3 ++ l4 ++ l5)) ++ [x8;x9]))) = *) 82(* [x1; x2] ++ l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *) 83(* REVERSE l3 ++ [x7; x6; x5; x8; x9; x3] *) 84(* --------------------------------------------------------------------- *) 85 86val NORM_CONS_APPEND_NO_EVAL_CONV = 87 (TOP_DEPTH_CONV NORM_CONS_CONV) THENC 88 (PURE_REWRITE_CONV [listTheory.APPEND_NIL, listTheory.APPEND_ASSOC, 89 listTheory.SNOC_APPEND, listTheory.REVERSE_APPEND, 90 listTheory.REVERSE_DEF]) THENC 91 (DEPTH_CONV ((QCHANGED_CONV APPEND_SIMPLE_LISTS_ASSOC_CONV) ORELSEC 92 (QCHANGED_CONV APPEND_SIMPLE_LISTS_CONV))) 93 94 95(* --------------------------------------------------------------------- *) 96(* NORM_CONS_APPEND_CONV : conv *) 97(* The normal form produced by NORM_CONS_APPEND_NO_EVAL_CONV is useful *) 98(* for the tools developed below. It's the one this lib is mainly *) 99(* interested in. However, the REWRITES for APPEND as for example *) 100(* included in list_ss destroy this normal form. Therefore, *) 101(* simplification easily loops when for example using list_ss with this *) 102(* conversion. *) 103(* *) 104(* In order to avoid such problems, NORM_CONS_APPEND_CONV used *) 105(* NORM_CONS_APPEND_NO_EVAL_CONV followed by rewrites of APPEND *) 106(* The result is moving conses for the first list outwards: *) 107(* *) 108(* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *) 109(* REVERSE (x5::x6::x7::(l3 ++ l4 ++ l5)) ++ [x8;x9]))) = *) 110(* x1::x2::(l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *) 111(* REVERSE l3 ++ [x7; x6; x5; x8; x9; x3] *) 112(* --------------------------------------------------------------------- *) 113 114val NORM_CONS_APPEND_CONV = NORM_CONS_APPEND_NO_EVAL_CONV THENC APPEND_EVAL_CONV 115 116val GSYM_CONS_APPEND_CONV = 117 PURE_REWRITE_CONV [GSYM (CONJUNCT2 listTheory.APPEND)] 118 119(* --------------------------------------------------------------------- *) 120(* LIST_EQ_SIMP_CONV : conv *) 121(* --------------------------------------------------------------------- *) 122 123(*examples 124val t = ``[x1;x2] ++ l1 ++ l2 ++ [x3] ++ l3 = x1::x2'::l1' ++ l3`` 125 |- ([x1; x2] ++ l1 ++ l2 ++ [x3] ++ l3 = x1::x2'::l1' ++ l3) <=> 126 (x2 = x2') /\ (l1 ++ l2 ++ [x3] = l1') 127 128val t = ``[x1;x2] ++ l1 ++ l2 ++ [x3] ++ [x4;x5;x6] = x1'::l1' ++ [x5;x6]`` 129 130 |- ([x1; x2] ++ l1 ++ l2 ++ [x3] ++ [x4; x5; x6] = x1'::l1' ++ [x5; x6]) <=> 131 (x1 = x1') /\ (x2::(l1 ++ l2 ++ [x3; x4]) = l1') : thm 132 133val t = ``l1 ++ l2 ++ [x3] ++ l3 = l1 ++ l2' ++ x3'::l3`` 134 135 |- (l1 ++ l2 ++ [x3] ++ l3 = l1 ++ l2' ++ x3'::l3) <=> 136 (l2 = l2') /\ (x3 = x3') 137 138val t = ``[x1;x2;x3] ++ l2 ++ [x3] ++ l3 = [x1;x2] ++ l1 ++ l2' ++ l3`` 139 140 |- ([x1; x2; x3] ++ l2 ++ [x3] ++ l3 = [x1; x2] ++ l1 ++ l2' ++ l3) <=> 141 (x3::(l2 ++ [x3]) = l1 ++ l2') 142 143val t = ``(x::l) = (l ++ l)`` 144 145 146ListConv1.LIST_EQ_SIMP_CONV t 147 148*) 149 150local 151 fun strip_cons_append tt = 152 let 153 val (eL, b) = strip_cons tt 154 val lL = strip_append b 155 in 156 (eL, lL) 157 end 158 159 fun EQ_CONV c = LHS_CONV c THENC RHS_CONV c 160 161 fun is_non_empty_list t = is_list t andalso not (is_nil t) 162 fun is_right_cons lL1 lL2 = 163 (is_non_empty_list (last lL1)) andalso (is_non_empty_list (last lL2)) 164 fun is_right_same lL1 lL2 = 165 ((length lL1 + length lL2) > 2) andalso (aconv (last lL1) (last lL2)) 166 fun left_nil_intro_CONV l = if is_append l then raise UNCHANGED else 167 (ISPEC l (GSYM (CONJUNCT1 listTheory.APPEND))) 168 169 fun LIST_EQ_SIMP_CONV___internal_right_elim conv l = 170 let 171 val (l1, l2) = dest_eq l 172 val lL1 = strip_append l1 173 val lL2 = strip_append l2 174 in 175 if (is_right_same lL1 lL2) then 176 ((EQ_CONV left_nil_intro_CONV) THENC 177 (REWR_CONV (CONJUNCT2 listTheory.APPEND_11)) THENC 178 (LIST_EQ_SIMP_CONV___internal_right_elim conv)) l 179 else if (is_right_cons lL1 lL2) then 180 let 181 val (L1,_) = dest_list (last lL1) 182 val (L2,_) = dest_list (last lL2) 183 val n1 = length L1 184 val n2 = length L2 185 val (turn, L1, L2, n1, n2) = 186 if n1 <= n2 then (false, L1, L2, n1, n2) else 187 (true, L2, L1, n2, n1) 188 189 val thm0 = ((if turn then SYM_CONV else ALL_CONV) 190 THENC (EQ_CONV left_nil_intro_CONV)) l 191 handle UNCHANGED => REFL l 192 val thm1 = if n1 = n2 then thm0 else 193 let 194 val (L21, L22) = Lib.split_after (n2 - n1) L2 195 val ty = type_of (hd L21) 196 val L21_t = listSyntax.mk_list (L21, ty) 197 val L22_t = listSyntax.mk_list (L22, ty) 198 val split_thm = 199 GSYM (APPEND_EVAL_CONV (mk_append (L21_t, L22_t))) 200 in 201 CONV_RULE ((RHS_CONV o RHS_CONV) 202 (RAND_CONV (K split_thm) THENC 203 REWR_CONV listTheory.APPEND_ASSOC)) thm0 204 end 205 206 val thm2a = 207 PART_MATCH 208 (lhs o rand) 209 (CONJUNCT2 listTheory.APPEND_11_LENGTH) (rhs (concl thm1)) 210 val thm2b = 211 CONV_RULE 212 ((RATOR_CONV o RAND_CONV) 213 (REWRITE_CONV [listTheory.LENGTH, prim_recTheory.INV_SUC_EQ])) 214 thm2a 215 val thm2 = TRANS thm1 (MP thm2b TRUTH) 216 217 val thm3 = 218 if turn 219 then CONV_RULE 220 ((RHS_CONV o RATOR_CONV o RAND_CONV) SYM_CONV) thm2 221 else thm2 222 223 val thm4 = CONV_RULE ((RHS_CONV o RATOR_CONV o RAND_CONV) 224 (LIST_EQ_SIMP_CONV___internal_right_elim conv)) thm3 225 in 226 thm4 227 end 228 else conv l 229 end handle HOL_ERR _ => raise UNCHANGED 230 231 fun is_left_cons lL1 lL2 = 232 (is_non_empty_list (hd lL1)) andalso (is_non_empty_list (hd lL2)) 233 fun is_left_same lL1 lL2 = 234 (length lL1 + length lL2 > 2) andalso (aconv (hd lL1) (hd lL2)) 235 fun right_nil_intro_CONV l = if is_append l then raise UNCHANGED 236 else 237 ISPEC l (GSYM listTheory.APPEND_NIL) 238 239 fun LIST_EQ_SIMP_CONV___internal_left_elim conv l = 240 let 241 val (l1, l2) = dest_eq l 242 val lL1 = strip_append l1 243 val lL2 = strip_append l2 244 in 245 if (is_left_same lL1 lL2) then 246 ((EQ_CONV right_nil_intro_CONV) THENC 247 (REWR_CONV (CONJUNCT1 listTheory.APPEND_11)) THENC 248 LIST_EQ_SIMP_CONV___internal_left_elim conv) l 249 else if (is_left_cons lL1 lL2) then 250 let 251 val (L1,_) = dest_list (hd lL1) 252 val (L2,_) = dest_list (hd lL2) 253 val n1 = length L1 254 val n2 = length L2 255 val (turn, L1, L2, n1, n2) = 256 if n1 <= n2 then (false, L1, L2, n1, n2) else 257 (true, L2, L1, n2, n1) 258 259 val thm0 = ((if turn then SYM_CONV else ALL_CONV) THENC 260 (EQ_CONV right_nil_intro_CONV)) l 261 handle UNCHANGED => REFL l 262 val thm1 = if n1 = n2 then thm0 else 263 let 264 val (L21, L22) = Lib.split_after n1 L2 265 val ty = type_of (hd L21) 266 val L21_t = listSyntax.mk_list (L21, ty) 267 val L22_t = listSyntax.mk_list (L22, ty) 268 val split_thm = 269 GSYM (APPEND_EVAL_CONV (mk_append (L21_t, L22_t))) 270 in 271 CONV_RULE ((RHS_CONV o RHS_CONV) 272 (RATOR_CONV (RAND_CONV (K split_thm)) THENC 273 REWR_CONV (GSYM listTheory.APPEND_ASSOC))) thm0 274 end 275 276 val thm2a = 277 PART_MATCH (lhs o rand) (CONJUNCT1 listTheory.APPEND_11_LENGTH) 278 (rhs (concl thm1)) 279 val thm2b = 280 CONV_RULE 281 ((RATOR_CONV o RAND_CONV) 282 (REWRITE_CONV [listTheory.LENGTH, prim_recTheory.INV_SUC_EQ])) 283 thm2a 284 val thm2 = TRANS thm1 (MP thm2b TRUTH) 285 286 val thm3 = if turn then 287 CONV_RULE ((RHS_CONV o RAND_CONV) SYM_CONV) thm2 else thm2 288 289 val thm4 = CONV_RULE ((RHS_CONV o RAND_CONV) 290 (LIST_EQ_SIMP_CONV___internal_left_elim conv)) thm3 291 in 292 thm4 293 end 294 else conv l 295 end handle HOL_ERR _ => raise UNCHANGED 296 297 val APPEND_LEFT_ASSOC_CONV = 298 PURE_REWRITE_CONV [GSYM listTheory.APPEND_ASSOC] 299 300 fun LIST_EQ_SIMP_CONV___internal t = 301 let 302 val (l1, l2) = dest_eq t 303 in 304 if (aconv l1 l2) then EQT_INTRO (REFL l1) else 305 (LIST_EQ_SIMP_CONV___internal_right_elim 306 (APPEND_LEFT_ASSOC_CONV THENC 307 LIST_EQ_SIMP_CONV___internal_left_elim 308 NORM_CONS_APPEND_CONV)) t 309 end handle HOL_ERR _ => raise UNCHANGED 310in 311 local 312 val conv = 313 EQ_CONV NORM_CONS_APPEND_NO_EVAL_CONV 314 THENC LIST_EQ_SIMP_CONV___internal 315 THENC REWRITE_CONV [listTheory.APPEND_eq_NIL, listTheory.NOT_CONS_NIL, 316 GSYM listTheory.NOT_CONS_NIL, listTheory.CONS_11] 317 in 318 fun LIST_EQ_SIMP_CONV t = 319 let 320 val (l1', _) = dest_eq t 321 val _ = if is_list_type (type_of l1') then () else raise UNCHANGED 322 in 323 conv t 324 end 325 end 326 327 val LIST_EQ_ss = 328 simpLib.name_ss "list EQ" 329 (simpLib.conv_ss 330 {name = "LIST_EQ_SIMP_CONV", 331 trace = 2, 332 key = SOME ([],Term `l1:'a list = l2:'a list`), 333 conv = K (K (CHANGED_CONV LIST_EQ_SIMP_CONV))}) 334end 335 336 337(*--------------------------------------------------------------------------- 338 For the simplifier. 339 ---------------------------------------------------------------------------*) 340 341val LIST_ss = BasicProvers.thy_ssfrag "list" 342val _ = BasicProvers.augment_srw_ss [LIST_EQ_ss] 343 344(*--------------------------------------------------------------------------- 345 For computeLib 346 ---------------------------------------------------------------------------*) 347 348val list_rws = computeLib.add_thms 349 [ 350 ALL_DISTINCT, APPEND, APPEND_NIL, CONS_11, DROP_compute, EL_restricted, 351 EL_simp_restricted, EVERY_DEF, EXISTS_DEF, FILTER, FIND_def, FLAT, FOLDL, 352 FOLDR, FRONT_DEF, GENLIST_AUX_compute, GENLIST_NUMERALS, HD, INDEX_FIND_def, 353 INDEX_OF_def, LAST_compute, LENGTH, LEN_DEF, LIST_APPLY_def, LIST_BIND_def, 354 LIST_IGNORE_BIND_def, LIST_LIFT2_def, LIST_TO_SET_THM, LLEX_def, LRC_def, 355 LUPDATE_compute, MAP, MAP2, NOT_CONS_NIL, NOT_NIL_CONS, NULL_DEF, oEL_def, 356 oHD_def, 357 PAD_LEFT, PAD_RIGHT, REVERSE_REV, REV_DEF, SHORTLEX_def, SNOC, SUM_ACC_DEF, 358 SUM_SUM_ACC, 359 TAKE_compute, TL, UNZIP, ZIP, computeLib.lazyfy_thm list_case_compute, 360 dropWhile_def, isPREFIX, list_size_def, nub_def, splitAtPki_def 361 ] 362 363fun list_compset () = 364 let 365 val base = reduceLib.num_compset() 366 in 367 list_rws base; base 368 end 369 370end (* struct *) 371