1(*===========================================================================*) 2(* HOL90 Version 7 *) 3(* *) 4(* FILE NAME: list_conv1.sml *) 5(* *) 6(* DESCRIPTION: Defined procedures for list induction and definition *) 7(* by primitive recursion on lists. Derived inference *) 8(* rules for reasoning about lists. *) 9(* *) 10(* The induction/primitive recursion are really only for *) 11(* compatibility with old HOL. *) 12(* *) 13(* AUTHOR: T. F. Melham (87.05.30) *) 14(* *) 15(* USES FILES: ind.ml, prim_rec.ml, numconv.ml *) 16(* *) 17(* University of Cambridge *) 18(* Hardware Verification Group *) 19(* Computer Laboratory *) 20(* New Museums Site *) 21(* Pembroke Street *) 22(* Cambridge CB2 3QG *) 23(* England *) 24(* *) 25(* COPYRIGHT: T. F. Melham 1987 1990 *) 26(* *) 27(* REVISION HISTORY: 90.09.08 *) 28(* TRANSLATED to hol90 (KLS, Dec 20, 1992) *) 29(* New conversions/tactics (PC 11/7/94-most translated by BTG from WW HOL88) *) 30(* Minor tweak to EL_CONV to take account of swap in quantifiers in defn *) 31(* of EL. (KLS october'94) *) 32(* MINOR REVISIONS: (KLS, May 4, 2002) *) 33(* *) 34(* NOTE: Most of this functionality is out-of-date and can be replaced with *) 35(* EVAL or CBV_CONV *) 36(*===========================================================================*) 37 38structure ListConv1 :> ListConv1 = 39struct 40 41open HolKernel Parse boolLib Num_conv Rsyntax Prim_rec listSyntax; 42 43fun mk_list {els,ty} = listSyntax.mk_list(els,ty) 44 45val ERR = mk_HOL_ERR "List_conv"; 46 47structure Parse = 48struct 49 open Parse 50 val (Type,Term) = parse_from_grammars rich_listTheory.rich_list_grammars 51 fun == q x = Type q 52end 53open Parse 54 55val % = Term; 56val alpha_ty = Type.alpha 57val bool_ty = Type.bool; 58 59val int_of_term = Arbnum.toInt o numSyntax.dest_numeral; 60fun term_of_int i = numSyntax.mk_numeral(Arbnum.fromInt i) 61 62val list_INDUCT = listTheory.list_INDUCT 63val list_Axiom = listTheory.list_Axiom; 64 65(* --------------------------------------------------------------------*) 66(* LIST_INDUCT: (thm # thm) -> thm *) 67(* *) 68(* A1 |- t[[]] A2 |- !tl. t[tl] ==> !h. t[CONS h t] *) 69(* ---------------------------------------------------------- *) 70(* A1 u A2 |- !l. t[l] *) 71(* *) 72(* --------------------------------------------------------------------*) 73 74fun LIST_INDUCT (base,step) = 75 let val {Bvar,Body} = dest_forall(concl step) 76 val {ant,conseq} = dest_imp Body 77 val {Bvar=h,Body=con} = dest_forall conseq 78 val P = Psyntax.mk_abs(Bvar, ant) 79 val b1 = genvar bool_ty 80 val b2 = genvar bool_ty 81 val base' = EQ_MP (SYM(BETA_CONV (%`^P []`))) base 82 val step' = DISCH ant (SPEC h (UNDISCH(SPEC Bvar step))) 83 val hypth = SYM(RIGHT_BETA(REFL (%`^P ^Bvar`))) 84 val concth = SYM(RIGHT_BETA(REFL (%`^P(CONS ^h ^Bvar)`))) 85 val IND = SPEC P (INST_TYPE [alpha_ty |-> type_of h] list_INDUCT) 86 val th1 = SUBST[b1 |-> hypth, b2 |-> concth] 87 (%`^(concl step') = (^b1 ==> ^b2)`) 88 (REFL (concl step')) 89 val th2 = GEN Bvar (DISCH (%`^P ^Bvar`) 90 (GEN h(UNDISCH (EQ_MP th1 step')))) 91 val th3 = SPEC Bvar (MP IND (CONJ base' th2)) 92 in 93 GEN Bvar (EQ_MP (BETA_CONV(concl th3)) th3) 94 end 95 handle HOL_ERR _ => raise ERR "LIST_INDUCT" ""; 96 97 98(* --------------------------------------------------------------------*) 99(* *) 100(* LIST_INDUCT_TAC *) 101(* *) 102(* [A] !l.t[l] *) 103(* ================================ *) 104(* [A] t[[]], [A,t[l]] !h. t[CONS h t] *) 105(* *) 106(* --------------------------------------------------------------------*) 107 108val LIST_INDUCT_TAC = INDUCT_THEN list_INDUCT ASSUME_TAC; 109 110(* --------------------------------------------------------------------*) 111(* *) 112(* SNOC_INDUCT_TAC *) 113(* *) 114(* [A] !l.t[l] *) 115(* ================================ *) 116(* [A] t[[]], [A,t[l]] !h. t[SNOC x t] *) 117(* *) 118(* --------------------------------------------------------------------*) 119(* PC 11/7/94 *) 120 121val SNOC_INDUCT_TAC = 122 let val SNOC_INDUCT = rich_listTheory.SNOC_INDUCT 123 in INDUCT_THEN SNOC_INDUCT ASSUME_TAC 124 end; 125 126 127(* --------------------------------------------------------------------*) 128(* Definition by primitive recursion for lists *) 129(* (For compatibility of new/old HOL.) *) 130(* --------------------------------------------------------------------*) 131 132fun new_list_rec_definition (name,tm) = 133 new_recursive_definition{name=name,rec_axiom=list_Axiom,def=tm} 134 135(* --------------------------------------------------------------------*) 136(* LENGTH_CONV: compute the length of a list *) 137(* *) 138(* A call to LENGTH_CONV `LENGTH[x1;...;xn]` returns: *) 139(* *) 140(* |- LENGTH [x1;...;xn] = n where n is a numeral constant *) 141(* --------------------------------------------------------------------*) 142 143local val LEN = listTheory.LENGTH 144 val suctm = numSyntax.suc_tm 145 fun SUC (i,th) = let val n = term_of_int i 146 in TRANS (AP_TERM suctm th) (SYM(num_CONV n)) 147 end 148 fun itfn cth h (i,th) = (i+1, 149 TRANS (SPEC (rand(lhs(concl th))) (SPEC h cth)) (SUC (i,th))) 150 val check = assert(equal "LENGTH" o #Name o dest_const) 151in 152fun LENGTH_CONV tm = 153 let val {Rator,Rand} = dest_comb tm 154 val _ = check Rator 155 val ty = case dest_type(type_of Rand) 156 of {Args=[ty],...} => ty 157 | _ => raise ERR "LENGTH_CONV" "" 158 val (Nil,cons) = CONJ_PAIR (INST_TYPE [alpha_ty |-> ty] LEN) 159 in 160 snd(itlist (itfn cons) (fst(dest_list (rand tm))) (1,Nil)) 161 end 162 handle HOL_ERR _ => raise ERR "LENGTH_CONV" "" 163end; 164 165(* --------------------------------------------------------------------*) 166(* list_EQ_CONV: equality of lists. *) 167(* *) 168(* This conversion proves or disproves the equality of two lists, given*) 169(* a conversion for deciding the equality of elements. *) 170(* *) 171(* A call to: *) 172(* *) 173(* list_EQ_CONV conv `[x1;...;xn] = [y1;...;ym]` *) 174(* *) 175(* returns: *) 176(* *) 177(* |- ([x1;...;xn] = [y1;...;ym]) = F *) 178(* *) 179(* if: *) 180(* *) 181(* 1: ~(n=m) or 2: conv proves |- (xi = yi) = F for any 1<=i<=n,m *) 182(* *) 183(* and: *) 184(* *) 185(* |- ([x1;...;xn] = [y1;...;ym]) = T *) 186(* *) 187(* if: *) 188(* *) 189(* 1: (n=m) and xi is syntactically identical to yi for 1<=i<=n,m, o *) 190(* 2: (n=m) and conv proves |- (xi=yi)=T for 1<=i<=n,m *) 191(* --------------------------------------------------------------------*) 192 193local 194val cnil = rich_listTheory.NOT_CONS_NIL 195val lne = rich_listTheory.LIST_NOT_EQ 196val nel = rich_listTheory.NOT_EQ_LIST 197val leq = rich_listTheory.EQ_LIST 198fun Cons ty = 199 let val lty = mk_type{Tyop="list",Args=[ty]} 200 val cty = mk_type{Tyop="fun", 201 Args=[ty,mk_type{Tyop="fun",Args=[lty,lty]}]} 202 in 203 fn h => fn t => mk_comb{Rator=mk_comb{Rator=mk_const{Name="CONS",Ty=cty}, 204 Rand=h}, Rand=t} 205 end 206fun Nil ty = mk_const{Name="NIL",Ty=mk_type{Tyop="list",Args=[ty]}} 207fun split n l = 208 if (n=0) 209 then ([],l) 210 else ((curry (op ::) (hd l))##I)(split (n-1) (tl l)) 211fun itfn cnv [leq,lne,nel] (h1,h2) th = 212 if (is_neg (concl th)) 213 then let val {lhs=l1,rhs=l2} = dest_eq(dest_neg (concl th)) 214 in SPEC h2 (SPEC h1 (MP (SPEC l2 (SPEC l1 lne)) th)) 215 end 216 else let val {lhs=l1,rhs=l2} = dest_eq(concl th) 217 val heq = cnv (mk_eq{lhs=h1,rhs=h2}) 218 in 219 if (rand(concl heq) = T) 220 then let val th1 = MP (SPEC h2 (SPEC h1 leq)) (EQT_ELIM heq) 221 in MP (SPEC l2 (SPEC l1 th1)) th 222 end 223 else let val th1 = MP (SPEC h2 (SPEC h1 nel)) (EQF_ELIM heq) 224 in SPEC l2 (SPEC l1 th1) 225 end 226 end 227 | itfn _ _ _ _ = raise ERR "list_EQ_CONV" "" 228in 229fun list_EQ_CONV cnv tm = 230 let val {lhs,rhs} = dest_eq tm 231 val l1 = fst(dest_list lhs) 232 val l2 = fst(dest_list rhs) 233 in 234 if (l1=l2) 235 then EQT_INTRO(REFL (rand tm)) 236 else let val ty = case dest_type(type_of(rand tm)) 237 of {Args=[ty],...} => ty 238 | _ => raise ERR "list_EQ_CONV" "" 239 val n = length l1 240 and m = length l2 241 val thms = map (INST_TYPE [alpha_ty |-> ty]) [leq,lne,nel] 242 val ifn = itfn cnv thms 243 in 244 if n<m 245 then let val (exd,x,xs) = case split n l2 246 of (exd,(x::xs)) => (exd,x,xs) 247 | _ => raise ERR "list_EQ_CONV" "" 248 val rest = itlist (Cons ty) xs (Nil ty) 249 val thm1 = SPEC rest 250 (SPEC x (INST_TYPE [alpha_ty |-> ty] 251 cnil)) 252 in EQF_INTRO(itlist ifn (combine(l1,exd))(NOT_EQ_SYM thm1)) 253 end 254 else if m<n 255 then let val (exd,x,xs) = case split n l1 256 of (exd,(x::xs)) => (exd,x,xs) 257 | _ => raise ERR "list_EQ_CONV" "" 258 val rest = itlist (Cons ty) xs (Nil ty) 259 val thm1 = SPEC rest 260 (SPEC x(INST_TYPE[alpha_ty |-> ty] cnil)) 261 in EQF_INTRO(itlist ifn (combine(exd,l2)) thm1) 262 end 263 else let val thm = itlist ifn (combine(l1,l2)) (REFL (Nil ty)) 264 in 265 EQF_INTRO thm handle HOL_ERR _ => EQT_INTRO thm 266 end 267 end 268 end 269 handle HOL_ERR _ => raise ERR "list_EQ_CONV" "" 270end; 271 272(*---------------------------------------------------------------------*) 273(* APPEND_CONV: this conversion maps terms of the form *) 274(* *) 275(* `APPEND [x1;...;xm] [y1;...;yn]` *) 276(* *) 277(* to the equation: *) 278(* *) 279(* |- APPEND [x1;...;xm] [y1;...;yn] = [x1;...;xm;y1;...;yn] *) 280(* *) 281(* ADDED: TFM 91.10.26 *) 282(*---------------------------------------------------------------------*) 283 284local val (th1,th2) = CONJ_PAIR (listTheory.APPEND) 285 val th3 = SPECL [%`l1: 'a list`, %`l2: 'a list`] th2 286 val th4 = GENL [%`l2: 'a list`, %`l1: 'a list`] th3 287 fun itfn (cns,ath) v th = 288 let val th1 = AP_TERM (mk_comb{Rator=cns,Rand=v}) th 289 val l = rand(rator(rand(rator(concl th)))) 290 in TRANS (SPEC v (SPEC l ath)) th1 291 end 292in 293fun APPEND_CONV tm = 294 let val (l1,l2) = listSyntax.dest_append tm 295 val (els,ty) = dest_list l1 296 in 297 if (null els) 298 then ISPEC l2 th1 299 else let val cns = rator(rator l1) 300 val step = ISPEC l2 th4 301 and base = ISPEC l2 th1 302 in 303 itlist (itfn (cns,step)) els base 304 end 305 end 306 handle HOL_ERR _ => raise ERR "APPEND_CONV" "" 307end; 308 309(* --------------------------------------------------------------------*) 310(* MAP_CONV conv `MAP f [e1;...;en]`. [TFM 92.04.16 *) 311(* *) 312(* Returns |- MAP f [e1;...;en] = [r1;...;rn] *) 313(* where conv `f ei` returns |- f ei = ri for 1 <= i <= n *) 314(* --------------------------------------------------------------------*) 315 316local val (mn,mc) = CONJ_PAIR(listTheory.MAP) 317in 318fun MAP_CONV conv tm = 319 let val (fnn,l) = listSyntax.dest_map tm 320 val (els,ty) = dest_list l 321 val nth = ISPEC fnn mn 322 and cth = ISPEC fnn mc 323 val cns = rator(rator(rand(snd(strip_forall(concl cth))))) 324 fun APcons t1 t2 = MK_COMB(AP_TERM cns t2,t1) 325 fun itfn e th = 326 let val t = rand(rand(rator(concl th))) 327 val th1 = SPEC t(SPEC e cth) 328 in TRANS th1 (APcons th (conv (mk_comb{Rator=fnn,Rand=e}))) 329 end 330 in 331 itlist itfn els nth 332 end 333 handle HOL_ERR _ => raise ERR "MAP_CONV" "" 334end; 335 336(*-==============================================================-*) 337(* Based on the hol88 file "list.ml". *) 338(* Converted to hol90 - 04.03.94 - BtG *) 339(* *) 340(* NOTE: exception handling *) 341(* ****************** *) 342(* Most conversions themselves should not raise exceptions *) 343(* unless applied to inappropriate terms. *) 344(* Rather than lose the information about what failure originated *) 345(* the exception, we choose to propagate the originating message, *) 346(* and in addition record the exception handlers involved, so a *) 347(* trace of the exception handling is possible. We also include *) 348(* some of the character string which originated the exception. *) 349(* *) 350(*-==============================================================-*) 351 352(* ------------------------------------------------------------------------- *) 353(* EQ_LENGTH_INDUCT_TAC : tactic *) 354(* A ?- !l1 l2. (LENGTH l1 = LENGTH l2) ==> t[l1, l2] *) 355(* ==================================================== EQ_LENGTH_INDUCT_TAC *) 356(* A ?- t[ []/l1, []/l2 ] *) 357(* A,LENGTH l1 = LENGTH l2 ?- t[(CONS h l1)/l1,(CONS h' l2)/l2] *) 358(* ------------------------------------------------------------------------- *) 359 360val EQ_LENGTH_INDUCT_TAC = 361 let val SUC_NOT = arithmeticTheory.SUC_NOT 362 and NOT_SUC = numTheory.NOT_SUC 363 and INV_SUC_EQ = prim_recTheory.INV_SUC_EQ 364 and LENGTH = rich_listTheory.LENGTH 365 in 366 LIST_INDUCT_TAC THENL[ 367 LIST_INDUCT_TAC THENL[ 368 REPEAT (CONV_TAC FORALL_IMP_CONV) THEN DISCH_THEN (K ALL_TAC), 369 REWRITE_TAC[LENGTH,SUC_NOT]], 370 GEN_TAC THEN LIST_INDUCT_TAC 371 THEN REWRITE_TAC[LENGTH,NOT_SUC,INV_SUC_EQ] 372 THEN GEN_TAC THEN REPEAT (CONV_TAC FORALL_IMP_CONV) THEN DISCH_TAC] 373 end; 374 375(* ------------------------------------------------------------------------- *) 376(* EQ_LENGTH_SNOC_INDUCT_TAC : tactic *) 377(* A ?- !l1 l2.(LENGTH l1 = LENGTH l2) ==> t[l1,l2] *) 378(* =============================================== EQ_LENGTH_SNOC_INDUCT_TAC *) 379(* A ?- t[ []/l1, []/l2 ] *) 380(* A,LENGTH l1 = LENGTH l2 ?- t[(SNOC h l1)/l1,(SNOC h' l2)/l2] *) 381(* ------------------------------------------------------------------------- *) 382 383val EQ_LENGTH_SNOC_INDUCT_TAC = 384 let val SUC_NOT = arithmeticTheory.SUC_NOT 385 and NOT_SUC = numTheory.NOT_SUC 386 and INV_SUC_EQ = prim_recTheory.INV_SUC_EQ 387 and LENGTH = rich_listTheory.LENGTH 388 and LENGTH_SNOC = rich_listTheory.LENGTH_SNOC 389 in 390 SNOC_INDUCT_TAC THENL[ 391 SNOC_INDUCT_TAC THENL[ 392 REPEAT (CONV_TAC FORALL_IMP_CONV) THEN DISCH_THEN (K ALL_TAC), 393 REWRITE_TAC[LENGTH,LENGTH_SNOC,SUC_NOT]], 394 GEN_TAC THEN SNOC_INDUCT_TAC 395 THEN REWRITE_TAC[LENGTH,LENGTH_SNOC,NOT_SUC,INV_SUC_EQ] 396 THEN GEN_TAC THEN REPEAT (CONV_TAC FORALL_IMP_CONV) THEN DISCH_TAC] 397 end; 398 399(*-==============================================================-*) 400(*- CONVERSIONS added by WW 31 Jan 94 -*) 401(*-==============================================================-*) 402 403(*---------------------------------------------------------------------------*) 404(*- Reductions *) 405(*- FOLDR_CONV conv (���FOLDR f e [a0,...an]���) ---> *) 406(* |- FOLDR f e [a0,...an] = tm *) 407(* FOLDR_CONV evaluates the input expression by iteratively apply *) 408(* the function f the successive element of the list starting from *) 409(* the end of the list. tm is the result of the calculation. *) 410(* FOLDR_CONV returns a theorem stating this fact. During each *) 411(* iteration, an expression (���f e' ai���) is evaluated. The user *) 412(* supplied conversion conv is used to derive a theorem *) 413(* |- f e' ai = e'' which is then used to reduce the expression *) 414(* to e''. For example, *) 415(* *) 416(* - FOLDR_CONV ((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC SUC_CONV) *) 417(* (���FOLDR (\l x. SUC x) 0 ([(x0:'a);x1;x2;x3;x4;x5])���); *) 418(* = val it = |- FOLDR (\l x. SUC x) 0 [x0; x1; x2; x3; x4; x5] = 6 : thm *) 419(* *) 420(* In general, if the function f is an explicit lambda abstraction *) 421(* (\x x'. t[x,x']), the conversion should be in the form *) 422(* ((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC conv')) *) 423(* where conv' applied to t[x,x'] returns the theorem |-t[x,x'] = e''. *) 424(*---------------------------------------------------------------------------*) 425 426 427val FOLDR_CONV = 428 let val (bthm,ithm) = CONJ_PAIR (rich_listTheory.FOLDR) in 429 fn conv => fn tm => 430 let val (f,e,l) = listSyntax.dest_foldr tm 431 val ithm' = ISPECL[f,e] ithm 432 val (els,lty) = (dest_list l) 433 fun itfn a th = 434 let val l' = case snd(strip_comb(lhs(concl th))) 435 of [f',e',l'] => l' 436 | _ => raise ERR "FOLDR_CONV" "" 437 val lem = SUBS [th](SPECL[a,l'] ithm') 438 in 439 TRANS lem (QCONV conv (rhs (concl lem))) 440 end 441 in 442 (itlist itfn els (ISPECL [f,e] bthm)) 443 end 444 handle e => raise wrap_exn "List_conv" "FOLDR_CONV" e 445 end; 446 447(*---------------------------------------------------------------------------*) 448(* FOLDL_CONV conv (���FOLDL f e [a0,...an]���) ---> *) 449(* |- FOLDL f e [a0,...an] = tm *) 450(* FOLDL_CONV evaluates the input expression by iteratively apply *) 451(* the function f the successive element of the list starting from *) 452(* the head of the list. tm is the result of the calculation. *) 453(* FOLDL_CONV returns a theorem stating this fact. During each *) 454(* iteration, an expression (���f e' ai���) is evaluated. The user *) 455(* supplied conversion conv is used to derive a theorem *) 456(* |- f e' ai = e'' which is then used to reduce the expression *) 457(* to e''. For example, *) 458(* *) 459(* - FOLDL_CONV ((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC SUC_CONV) *) 460(* (���FOLDL (\l x. SUC l) 0 ([(x0:'a);x1;x2;x3;x4;x5])���); *) 461(* val it = |- FOLDL (\x l. SUC x) 0 [x0; x1; x2; x3; x4; x5] = 6 : thm *) 462(* *) 463(* In general, if the function f is an explicit lambda abstraction *) 464(* (\x x'. t[x,x']), the conversion should be in the form *) 465(* ((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC conv')) *) 466(* where conv' applied to t[x,x'] returns the theorem |-t[x,x'] = e''. *) 467(*---------------------------------------------------------------------------*) 468 469local 470 val (bcnv, ithm) = 471 (Conv.REWR_CONV ## Drule.SPEC_ALL) (CONJ_PAIR listTheory.FOLDL) 472 fun dest_exl tm = 473 let 474 val (_, e, l) = listSyntax.dest_foldl tm 475 in 476 (e, Lib.total listSyntax.dest_cons l) 477 end 478 fun with_foldl f x = Lib.with_exn f x (ERR "FOLDL_CONV" "") 479in 480 fun FOLDL_CONV cnv tm = 481 let 482 val (f, e, l) = with_foldl listSyntax.dest_foldl tm 483 val (ll, lty) = with_foldl listSyntax.dest_list l 484 in 485 if List.null ll 486 then bcnv tm 487 else let 488 val rule = CONV_RULE (RHS_CONV (RATOR_CONV (RAND_CONV cnv))) 489 val ety = Term.type_of e 490 val ev = Term.mk_var ("e", ety) 491 val xv = Term.mk_var ("x", lty) 492 val lv = Term.mk_var ("l", Term.type_of l) 493 val ithm = Drule.INST_TY_TERM 494 ([Term.mk_var ("f", Term.type_of f) |-> f], 495 [Type.alpha |-> lty, Type.beta |-> ety]) ithm 496 fun iter tm = 497 case dest_exl tm of 498 (e, NONE) => bcnv tm 499 | (e, SOME (x, l)) => 500 RIGHT_CONV_RULE iter 501 (rule (Thm.INST [ev |-> e, xv |-> x, lv |-> l] ithm)) 502 in 503 iter tm 504 end 505 end 506end 507 508(* --------------------------------------------------------------------- *) 509(* list_FOLD_CONV : thm -> conv -> conv *) 510(* list_FOLD_CONV foldthm conv tm *) 511(* where cname is the name of constant and foldthm is a theorem of the *) 512(* the following form: *) 513(* |- !x0 ... xn. CONST x0 ... xn = FOLD[LR] f e l *) 514(* and conv is a conversion which will be passed to FOLDR_CONV or *) 515(* FOLDL_CONV to reduce the right-hand side of the above theorem *) 516(* --------------------------------------------------------------------- *) 517 518val list_FOLD_CONV = 519 fn foldthm => fn conv => fn tm => 520 (let val (cname,args) = (strip_comb tm) 521 val fthm = ISPECL args foldthm 522 val {lhs=left,rhs=right} = dest_eq(concl fthm) 523 val const = fst(strip_comb left) 524 val f = #Name(dest_const(fst(strip_comb right))) 525 in 526 if (not(cname = const)) 527 then raise ERR"list_FOLD_CONV" 528 ("theorem and term are different:"^ 529 (term_to_string cname)^" vs "^(term_to_string const)) 530 else if (f = "FOLDL") then 531 TRANS fthm (FOLDL_CONV conv right) 532 else if (f = "FOLDR") then 533 TRANS fthm (FOLDR_CONV conv right) 534 else raise ERR "list_FOLD_CONV" ("not FOLD theorem, uses instead: "^f) 535 end) 536 handle e => raise wrap_exn "List_conv" "list_FOLD_CONV" e 537 538val SUM_CONV = 539 list_FOLD_CONV (rich_listTheory.SUM_FOLDR) reduceLib.ADD_CONV; 540 541(*---------------------------------------------------------------------*) 542(* Filter *) 543(* FILTER_CONV conv (���FILTER P [a0,...an]���) ---> *) 544(* |- FILTER P [a0,...,an] = [...,ai,...] *) 545(* where conv (���P ai���) returns a theorem |- P ai = T for all ai *) 546(* in the resulting list. *) 547(*---------------------------------------------------------------------*) 548 549val FILTER_CONV = 550 let val (bth,ith) = CONJ_PAIR (rich_listTheory.FILTER) in 551 fn conv => fn tm => 552 (let val (P,l) = listSyntax.dest_filter tm 553 val bth' = ISPEC P bth and ith' = ISPEC P ith 554 val lis = #1(dest_list l) 555 fun ffn x th = 556 let val {lhs=left,rhs=right} = dest_eq(concl th) 557 val (p,ls) = case strip_comb left 558 of (_,[p,ls]) => (p,ls) 559 | _ => raise ERR "FILTER_CONV" "" 560 val fthm = SPECL [x,ls] ith' and cthm = conv (���^P ^x���) 561 in 562 (CONV_RULE (RAND_CONV COND_CONV) (SUBS[cthm,th]fthm)) 563 end 564 in 565 (itlist ffn lis bth') 566 end) 567 handle e => raise wrap_exn "List_conv" "FILTER_CONV" e 568 end; 569 570(*----------------------------------------------------------------*) 571(* SNOC_CONV : conv *) 572(* SNOC_CONV (���SNOC x [x0,...xn]���) ---> *) 573(* |- SNOC x [x0,...xn] = [x0,...,xn,x] *) 574(*----------------------------------------------------------------*) 575 576val SNOC_CONV = 577 let val (bthm,sthm) = CONJ_PAIR (rich_listTheory.SNOC) in 578 fn tm => 579 let val (d,lst) = listSyntax.dest_snoc tm 580 val ty = type_of lst 581 val (lst',ety) = (dest_list lst) 582 val EMP = (���[]:^(ty_antiq ty)���) 583 and CONS = Term`CONS:^(ty_antiq ety)-> ^(ty_antiq ty)->^(ty_antiq ty)` 584 fun itfn x (lst,ithm) = 585 (mk_comb{Rator=mk_comb{Rator=CONS,Rand=x},Rand=lst}, 586 (SUBS[ithm](ISPECL[d,x,lst]sthm))) 587 in 588 snd(itlist itfn lst' (EMP,(ISPEC d bthm))) 589 end 590 handle e => raise wrap_exn "List_conv" "SNOC_CONV" e 591 end; 592 593 594(*----------------------------------------------------------------*) 595(* REVERSE_CONV : conv *) 596(* REVERSE_CONV (���REVERSE [x0,...,xn]���) ---> *) 597(* |- REVERSE [x0,...,xn] = [xn,...,x0] *) 598(*----------------------------------------------------------------*) 599 600local 601 val reverse_empty = CONJUNCT1 listTheory.REVERSE_DEF 602 val cnv1 = Conv.REWR_CONV listTheory.REVERSE_REV 603 val cnv2 = Conv.REWR_CONV reverse_empty 604 val dst = listSyntax.dest_list o listSyntax.dest_reverse 605in 606 fun REVERSE_CONV tm = 607 let 608 val (l, ty) = Lib.with_exn dst tm (ERR "REVERSE_CONV" "") 609 in 610 if List.null l 611 then cnv2 tm 612 else let 613 val (rev_empty, rev_cons) = 614 Drule.CONJ_PAIR 615 (Thm.INST_TYPE [Type.alpha |-> ty] listTheory.REV_DEF) 616 val cnv3 = Conv.REWR_CONV rev_cons 617 in 618 (cnv1 619 THENC Lib.funpow (List.length l - 1) 620 (fn c => c THENC cnv3) cnv3 621 THENC Conv.REWR_CONV rev_empty) tm 622 end 623 end 624end 625 626(*----------------------------------------------------------------*) 627(* FLAT_CONV : conv *) 628(* FLAT_CONV (���FLAT [[x00,...,x0n],...,[xm0,...xmn]]���) ---> *) 629(* |- (���FLAT [[x00,...,x0n],...,[xm0,...xmn]]���) = *) 630(* [x00,...,x0n,...,xm0,...xmn] *) 631(*----------------------------------------------------------------*) 632 633val FLAT_CONV = 634 let 635 val (fnil,fnilcons,fconscons) = 636 case CONJUNCTS listTheory.FLAT_compute of 637 [c1,c2,c3] => (c1,c2,c3) 638 | _ => raise Fail "FLAT_compute of wrong shape" 639 fun doit t = 640 let 641 val arg = dest_flat t 642 handle HOL_ERR _ => raise ERR "FLAT_CONV" "Not a FLAT term" 643 val (els,listend) = strip_cons arg 644 val _ = (listSyntax.is_nil listend andalso 645 List.all listSyntax.is_list els) orelse 646 raise ERR "FLAT_CONV" "Argument to FLAT not a list" 647 fun recurse t = 648 if listSyntax.is_nil (rand t) then REWR_CONV fnil t 649 else 650 let 651 val (h,_) = listSyntax.dest_cons (rand t) 652 in 653 if listSyntax.is_nil h then 654 (REWR_CONV fnilcons THENC recurse) t 655 else 656 (REWR_CONV fconscons THENC RAND_CONV recurse) t 657 end 658 in 659 recurse t 660 end 661 in 662 doit 663 end 664 665(*-----------------------------------------------------------------------*) 666(* EL_CONV : conv *) 667(* The argument to this conversion should be in the form of *) 668(* (���EL k [x0, x1, ..., xk, ..., xn]���) *) 669(* It returns a theorem *) 670(* |- EL k [x0, x1, ..., xk, ..., xn] = xk *) 671(* iff 0 <= k <= n, otherwise failure occurs. *) 672(*-----------------------------------------------------------------------*) 673 674val bcT = CONJUNCT1 bool_case_thm 675val bcF = CONJUNCT2 bool_case_thm 676fun EL_CONV t = 677 let 678 val (N_t,list) = listSyntax.dest_el t 679 handle HOL_ERR _ => raise ERR "EL_CONV" "Arg not of form EL k l" 680 fun len a t = 681 case Lib.total listSyntax.dest_cons t of 682 NONE => if same_const listSyntax.nil_tm t then a 683 else raise ERR "EL_CONV" "Arg 2 not a concrete list" 684 | SOME (_, t') => len (Arbnum.+(Arbnum.one, a)) t' 685 val length = len Arbnum.zero list 686 val N = numSyntax.dest_numeral N_t 687 handle HOL_ERR _ => raise ERR "EL_CONV" "Arg 1 not a numeral" 688 in 689 if Arbnum.<(N, length) then 690 let 691 val RED = reduceLib.REDUCE_CONV 692 fun recurse t = 693 (REWR_CONV listTheory.EL_compute THENC 694 RATOR_CONV (RATOR_CONV (RAND_CONV RED)) THENC 695 IFC (REWR_CONV bcF) 696 (FORK_CONV (RED, REWR_CONV listTheory.TL) THENC recurse) 697 (REWR_CONV bcT THENC REWR_CONV listTheory.HD)) t 698 in 699 recurse t 700 end 701 else raise ERR "EL_CONV" "Numeric argument too large" 702 end 703 704(*-----------------------------------------------------------------------*) 705(* ELL_CONV : conv *) 706(* It takes a term of the form (���ELL k [x(n-1), ... x0]���) and returns*) 707(* |- ELL k [x(n-1), ..., x0] = x(k) *) 708(*-----------------------------------------------------------------------*) 709 710val ELL_CONV = 711 let val bthm = rich_listTheory.ELL_0_SNOC 712 and ithm = rich_listTheory.ELL_SUC_SNOC 713 fun iter count (d,lst) elty = 714 let val n = (ref count) and x = (ref d) and l = (ref lst) 715 val th = ref (ISPECL[(term_of_int (!n)), !x, 716 mk_list{els=(!l),ty=elty}]ithm) 717 in 718 (while (not(!n = 0)) do 719 (n := !n - 1; 720 x := (last (!l)); 721 l := butlast (!l); 722 th := TRANS (RIGHT_CONV_RULE ((RATOR_CONV o RAND_CONV) 723 num_CONV) (!th)) 724 (CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)SNOC_CONV) 725 (ISPECL[(term_of_int (!n)), (!x), 726 mk_list{els=(!l),ty=elty}]ithm))) 727 ; 728 (x := last(!l); l := butlast(!l); 729 (TRANS (!th) 730 (CONV_RULE 731 ((RATOR_CONV o RAND_CONV o RAND_CONV) SNOC_CONV) 732 (ISPECL [mk_list{els=(!l),ty=elty},!x] bthm))))) 733 end 734 in 735 fn tm => 736 (let val (N,lst) = rich_listSyntax.dest_ell tm 737 val ty = type_of lst 738 val (lst',ety) = (dest_list lst) 739 val n = int_of_term N 740 in 741 if not(n < (length lst')) 742 then raise ERR "ELL_CONV" ("index too large: "^(int_to_string n)) 743 else if (n = 0) 744 then 745 (CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)SNOC_CONV) 746 (ISPECL[mk_list{els=butlast lst',ty=ety},(last lst')]bthm)) 747 else 748 SUBS_OCCS[([1],SYM (num_CONV N))] 749 (CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)SNOC_CONV) 750 (iter (n - 1) ((last lst'), (butlast lst')) ety)) 751 end) 752 handle e => raise wrap_exn "List_conv" "ELL_CONV" e 753 end; 754 755(* --------------------------------------------------------------------- *) 756(* MAP2_CONV conv (���MAP2 f [x1,...,xn] [y1,...,yn]���) *) 757(* *) 758(* Returns |- MAP2 f [x1,...,xn] [y1,...,yn] = [r1,...,rn] *) 759(* where conv (���f xi yi���) returns |- f xi yi = ri for 1 <= i <= n *) 760(* --------------------------------------------------------------------- *) 761 762val MAP2_CONV = 763 let val (mn,mc) = CONJ_PAIR(rich_listTheory.MAP2) in 764 fn conv => fn tm => 765 (let val (fnc,l1,l2) = listSyntax.dest_map2 tm 766 val (el1s,ty1) = dest_list l1 767 and (el2s,ty2) = dest_list l2 768 val els = combine (el1s,el2s) 769 val nth = ISPEC fnc mn and cth = ISPEC fnc mc 770 val cns = rator(rator(rand(snd(strip_forall(concl cth))))) 771 fun itfn (e1,e2) th = 772 let val (f,t1,t2) = case strip_comb(lhs(concl th)) 773 of (_,[f,t1,t2]) => (f,t1,t2) 774 | _ => raise ERR "MAP2_CONV" "" 775 val th1 = SPECL [e1, t1, e2, t2] cth 776 val r = conv(mk_comb{Rator=mk_comb{Rator=fnc,Rand=e1},Rand=e2}) 777 in 778 (SUBS[r,th]th1) 779 end 780 in 781 itlist itfn els nth 782 end) 783 handle e => raise wrap_exn "List_conv" "MAP2_CONV" e 784 end; 785 786(* --------------------------------------------------------------------- *) 787(* ALL_EL_CONV : conv -> conv *) 788(* ALL_EL_CONV conv (���ALL_EL P [x0,...,xn]���) ---> *) 789(* |- ALL_EL P [x0,...,xn] = T *) 790(* iff conv (���P xi���)---> |- P xi = T for all i *) 791(* |- ALL_EL P [x0,...,xn] = F otherwise *) 792(* --------------------------------------------------------------------- *) 793 794fun thm_eq th1 th2 = (Thm.dest_thm th1 = Thm.dest_thm th2); 795 796val ALL_EL_CONV = 797 let val (bth,ith) = CONJ_PAIR (rich_listTheory.ALL_EL) 798 val AND_THM = op_mk_set thm_eq (flatten(map (CONJ_LIST 5) 799 [(SPEC (���T���) AND_CLAUSES),(SPEC (���F���) AND_CLAUSES)])) 800 in 801 fn conv => fn tm => 802 (let val (P,l) = listSyntax.dest_every tm 803 val bth' = ISPEC P bth and ith' = ISPEC P ith 804 val lis = #1(dest_list l) 805 fun ffn x th = 806 let val {lhs=left,rhs=right} = dest_eq(concl th) 807 val (p,ls) = case strip_comb left 808 of (_,[p,ls]) => (p,ls) 809 | _ => raise ERR "ALL_EL_CONV" "" 810 val fthm = SPECL [x,ls] ith' 811 and cthm = conv (mk_comb{Rator=P,Rand=x}) 812 in 813 SUBS AND_THM (SUBS[cthm,th]fthm) 814 end 815 in 816 (itlist ffn lis bth') 817 end) 818 handle e => raise wrap_exn "List_conv" "ALL_EL_CONV" e 819 end; 820 821(* --------------------------------------------------------------------- *) 822(* SOME_EL_CONV : conv -> conv *) 823(* SOME_EL_CONV conv (���SOME_EL P [x0,...,xn]���) ---> *) 824(* |- SOME_EL P [x0,...,xn] = F *) 825(* iff conv (���P xi���)---> |- P xi = F for all i*) 826(* |- SOME_EL P [x0,...,xn] = F otherwise *) 827(* --------------------------------------------------------------------- *) 828 829val SOME_EL_CONV = 830 let val (bth,ith) = CONJ_PAIR (rich_listTheory.SOME_EL) 831 val OR_THM = op_mk_set thm_eq (flatten(map (CONJ_LIST 5) 832 [(SPEC (���T���) OR_CLAUSES),(SPEC (���F���) OR_CLAUSES)])) 833 in 834 fn conv => fn tm => 835 (let val (P,l) = listSyntax.dest_exists tm 836 val bth' = ISPEC P bth and ith' = ISPEC P ith 837 val lis = #1(dest_list l) 838 fun ffn x th = 839 let val {lhs=left,rhs=right} = dest_eq(concl th) 840 val (p,ls) = case strip_comb left 841 of (_,[p,ls]) => (p,ls) 842 | _ => raise ERR "SOME_EL_CONV" "" 843 val fthm = SPECL [x,ls] ith' and cthm = conv (���^P ^x���) 844 in 845 SUBS OR_THM (SUBS[cthm,th]fthm) 846 end 847 in 848 (itlist ffn lis bth') 849 end) 850 handle e => raise wrap_exn "List_conv" "SOME_EL_CONV" e 851 end; 852 853(* --------------------------------------------------------------------- *) 854(* IS_EL_CONV : conv -> conv *) 855(* IS_EL_CONV conv (���IS_EL P [x0,...,xn]���) ---> *) 856(* |- IS_EL x [x0,...,xn] = T iff conv (���x = xi���) ---> *) 857(* |- (x = xi) = F for an i *) 858(* |- IS_EL x [x0,...,xn] = F otherwise *) 859(* --------------------------------------------------------------------- *) 860 861val IS_EL_CONV = 862 let val bth = rich_listTheory.IS_EL_DEF in 863 fn conv => fn tm => 864 let val (x,l) = listSyntax.dest_mem tm 865 val bth' = ISPECL[x,l] bth 866 val right = rhs (concl bth') 867 in 868 TRANS bth' (SOME_EL_CONV conv right) 869 end 870 handle e => raise wrap_exn "List_conv" "IS_EL_CONV" e 871 end; 872 873(* --------------------------------------------------------------------- *) 874(* LAST_CONV : conv *) 875(* LAST_CONV (���LAST [x0,...,xn]���) ---> |- LAST [x0,...,xn] = xn *) 876(* --------------------------------------------------------------------- *) 877 878val LAST_CONV = 879 let val bth = rich_listTheory.LAST in 880 fn tm => 881 (let val l = listSyntax.dest_last tm 882 val (l',lty) = dest_list l 883 in 884 if ((length l') = 0) then raise ERR"LAST_CONV" "empty list" 885 else 886 (let val x = last l' and lis = mk_list{els=(butlast l'),ty=lty} 887 val bth' = ISPECL[x,lis] bth 888 in 889 CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)SNOC_CONV) bth' 890 end) 891 end) 892 handle e => raise wrap_exn "List_conv" "LAST_CONV" e 893 end; 894 895(* --------------------------------------------------------------------- *) 896(* BUTLAST_CONV : conv *) 897(* BUTLAST_CONV (���BUTLAST [x0,...,xn-1,xn]���) ---> *) 898(* |- BUTLAST [x0,...,xn-1,xn] = [x0,...,xn-1] *) 899(* --------------------------------------------------------------------- *) 900 901val BUTLAST_CONV = 902 let val bth = rich_listTheory.BUTLAST in 903 fn tm => 904 (let val l = listSyntax.dest_front tm 905 val (l',lty) = dest_list l 906 in 907 if ((length l') = 0) 908 then raise ERR "BUTLAST_CONV" "empty list" 909 else 910 (let val x = last l' and lis = mk_list{els=(butlast l'),ty=lty} 911 val bth' = ISPECL[x,lis] bth 912 in 913 CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)SNOC_CONV) bth' 914 end) 915 end) 916 handle e => raise wrap_exn "List_conv" "BUTLAST_CONV" e 917 end; 918 919fun SUC_CONV tm = 920 let val {Rator=SUC,Rand} = dest_comb tm 921 val n = term_of_int (int_of_term Rand + 1) 922 in 923 SYM (num_CONV n) 924 end; 925 926(*---------------------------------------------------------------*) 927(* SEG_CONV : conv *) 928(* SEG_CONV (���SEG m k [x0,...,xk,...,xm+k,...xn]���) ---> *) 929(* |- SEG m k [x0,...,xk,...,xm+k,...xn] = [xk,...xm+k-1] *) 930(*---------------------------------------------------------------*) 931 932val SEG_CONV = 933 let val [bthm,mthm,kthm] = CONJ_LIST 3 rich_listTheory.SEG 934 val SUC = numSyntax.suc_tm 935 fun mifn mthm' x th = 936 let val (M',L) = case snd(strip_comb(lhs(concl th))) 937 of [M',_,L] => (M',L) 938 | _ => raise ERR "SEG_CONV" "" 939 in 940 SUBS [(SUC_CONV(mk_comb{Rator=SUC,Rand=M'})),th] 941 (SPECL[M',x,L]mthm') 942 end 943 fun kifn kthm' x th = 944 let val (K',L) = case snd(strip_comb(lhs(concl th))) 945 of [_,K',L] => (K',L) 946 | _ => raise ERR "SEG_CONV" "" 947 in 948 SUBS [(SUC_CONV(mk_comb{Rator=SUC,Rand=K'})),th] 949 (SPECL[K',x,L]kthm') 950 end 951 in 952 fn tm => 953 (let val (M,K,L) = rich_listSyntax.dest_seg tm 954 val (lis,lty) = dest_list L 955 val m = int_of_term M and k = int_of_term K 956 in 957 if ((m + k) > (length lis)) 958 then raise ERR "SEG_CONV" ("indexes too large: "^(int_to_string m)^ 959 " and "^(int_to_string k)) 960 else if (m = 0) 961 then (ISPECL [K,L] bthm) 962 else let val mthm' = INST_TYPE [alpha |-> lty] mthm 963 in 964 if (k = 0) then 965 let val (ls,lt) = Lib.split_after m lis 966 val bthm' = ISPECL[(���0���),mk_list{els=lt,ty=lty}] bthm 967 in 968 (itlist (mifn mthm') ls bthm') 969 end 970 else 971 let val (lk,(ls,lt)) = (I##Lib.split_after m) 972 (Lib.split_after k lis) 973 val bthm' = ISPECL[(���0���),(mk_list{els=lt,ty=lty})] bthm 974 val kthm' = SUBS[SYM(num_CONV M)] 975 (INST_TYPE[alpha |-> lty] 976 (SPEC (term_of_int(m-1)) kthm)) 977 val bbthm = itlist (mifn mthm') ls bthm' 978 in 979 (itlist (kifn kthm') lk bbthm) 980 end 981 end 982 end) 983 handle e => raise wrap_exn "List_conv" "SEG_CONV" e 984 end; 985 986(*-----------------------------------------------------------------------*) 987(* LASTN_CONV : conv *) 988(* It takes a term (���LASTN k [x0, ..., x(n-k), ..., x(n-1)]���) *) 989(* and returns the following theorem: *) 990(* |- LASTN k [x0, ..., x(n-k), ..., x(n-1)] = [x(n-k), ..., x(n-1)] *) 991(*-----------------------------------------------------------------------*) 992 993val LASTN_CONV = 994 let val LASTN_LENGTH_APPEND = rich_listTheory.LASTN_LENGTH_APPEND 995 and bthm = CONJUNCT1 (rich_listTheory.LASTN) 996 and ithm = (rich_listTheory.LASTN_LENGTH_ID) 997 fun len_conv ty lst = LENGTH_CONV 998 (mk_comb{Rator=(���LENGTH:(^(ty_antiq ty))list -> num���),Rand=lst}) 999 in 1000 fn tm => 1001 (let val (N,lst) = rich_listSyntax.dest_lastn tm 1002 val n = int_of_term N 1003 in 1004 if (n = 0) then (ISPEC lst bthm) 1005 else 1006 (let val (bits,lty) = (dest_list lst) 1007 val len = (length bits) 1008 in 1009 if (n > len) 1010 then raise ERR"SEG_CONV" 1011 ("index too large"^(int_to_string n)) 1012 else if (n = len) then 1013 (SUBS[len_conv lty lst] (ISPEC lst ithm)) 1014 else 1015 (let val (l1,l2) = (Lib.split_after (len - n) bits) 1016 val l1' = mk_list{els=l1,ty=lty} 1017 and l2' = mk_list{els=l2,ty=lty} 1018 val APP = (���APPEND:(^(ty_antiq lty))list -> (^(ty_antiq lty))list -> (^(ty_antiq lty))list���) 1019 val thm2 = len_conv lty l2' 1020 val thm3 = APPEND_CONV 1021 (mk_comb{Rator=mk_comb{Rator=APP,Rand=l1'}, 1022 Rand=l2'}) 1023 in 1024 SUBS[thm2,thm3](ISPECL [l2',l1'] LASTN_LENGTH_APPEND) 1025 end) 1026 end) 1027 end) 1028 handle e => raise wrap_exn "List_conv" "SEG_CONV" e 1029 end; 1030 1031(*-----------------------------------------------------------------------*) 1032(* BUTLASTN_CONV : conv *) 1033(* It takes a term (���BUTLASTN k [x0,x1,...,x(n-k),...,x(n-1)]���) *) 1034(* and returns the following theorem: *) 1035(* |- BUTLASTN k [x0, x1, ..., x(n-k),...,x(n-1)] = [x0, ..., x(n-k-1)] *) 1036(*-----------------------------------------------------------------------*) 1037 1038val BUTLASTN_CONV = 1039 let val bthm = CONJUNCT1 (rich_listTheory.BUTLASTN) 1040 val lthm = (rich_listTheory.BUTLASTN_LENGTH_NIL) 1041 val athm = (rich_listTheory.BUTLASTN_LENGTH_APPEND) 1042 fun len_conv ty lst = LENGTH_CONV 1043 (mk_comb{Rator=(���LENGTH:(^(ty_antiq ty))list -> num���),Rand=lst}) 1044 in 1045 fn tm => 1046 (let val (N,lst) = rich_listSyntax.dest_butlastn tm 1047 val n = int_of_term N 1048 in 1049 if (n = 0) then (ISPEC lst bthm) 1050 else 1051 (let val (bits,lty) = dest_list lst 1052 val len = (length bits) 1053 in 1054 if (n > len) then 1055 raise ERR"BUTLASTN_CONV" 1056 ("index too large: "^(int_to_string n)) 1057 else if (n = len) then 1058 let val thm1 = len_conv lty lst in 1059 (SUBS[thm1](ISPEC lst lthm)) 1060 end 1061 else 1062 (let val (l1,l2) = (Lib.split_after (len - n) bits) 1063 val l1' = mk_list{els=l1,ty=lty} 1064 and l2' = mk_list{els=l2,ty=lty } 1065 val APP = 1066 (���APPEND:(^(ty_antiq lty))list 1067 -> (^(ty_antiq lty))list 1068 -> (^(ty_antiq lty))list���) 1069 val thm2 = len_conv lty l2' 1070 val thm3 = APPEND_CONV 1071 (mk_comb{Rator=mk_comb{Rator=APP, Rand=l1'}, 1072 Rand=l2'}) 1073 in 1074 (SUBS[thm2,thm3](ISPECL [l2',l1'] athm)) 1075 end) 1076 end) 1077 end) 1078 handle e => raise wrap_exn "List_conv" "BUTLASTN_CONV" e 1079 end; 1080 1081(*-----------------------------------------------------------------------*) 1082(* BUTFIRSTN_CONV : conv *) 1083(* BUTFIRSTN_CONV (���BUTFIRSTN k [x0,...,xk,...,xn]���) ---> *) 1084(* |- BUTFIRSTN k [x0,...,xk,...,xn] = [xk,...,xn] *) 1085(*-----------------------------------------------------------------------*) 1086 1087val BUTFIRSTN_CONV = 1088 let val (bthm,ithm) = CONJ_PAIR rich_listTheory.BUTFIRSTN 1089 val SUC = numSyntax.suc_tm 1090 fun itfn ithm' x th = 1091 let val (N',L') = case strip_comb(lhs(concl th)) 1092 of (_,[N',L']) => (N',L') 1093 | _ => raise ERR "BUTFIRSTN_CONV" "" 1094 in 1095 SUBS[(SUC_CONV(mk_comb{Rator=SUC,Rand=N'})),th] 1096 (SPECL[N',x,L']ithm') 1097 end 1098 in 1099 fn tm => 1100 let val (K,L) = listSyntax.dest_drop tm 1101 val k = int_of_term K and (lis,lty) = dest_list L in 1102 if (k > (length lis)) 1103 then raise ERR "BUTFIRSTN_CONV" 1104 ("index too large: "^(int_to_string k)) 1105 else if (k = 0) then (ISPEC L bthm) 1106 else 1107 let val (ll,lr) = Lib.split_after k lis 1108 val bthm' = ISPEC (mk_list{els=lr,ty=lty}) bthm 1109 val ithm' = INST_TYPE[alpha |-> lty]ithm 1110 in 1111 itlist (itfn ithm') ll bthm' 1112 end 1113 end 1114 handle e => raise wrap_exn "List_conv" "BUTFIRSTN_CONV" e 1115 end; 1116 1117(*-----------------------------------------------------------------------*) 1118(* FIRSTN_CONV : conv *) 1119(* FIRSTN_CONV (���FIRSTN k [x0,...,xk,...,xn]���) ---> *) 1120(* |- FIRSTN k [x0,...,xk,...,xn] = [x0,...,xk] *) 1121(*-----------------------------------------------------------------------*) 1122 1123val FIRSTN_CONV = 1124 let val (bthm,ithm) = CONJ_PAIR rich_listTheory.FIRSTN 1125 val SUC = numSyntax.suc_tm 1126 fun itfn ithm' x th = 1127 let val (N',L') = case strip_comb(lhs(concl th)) 1128 of (_,[N',L']) => (N',L') 1129 | _ => raise ERR "FIRSTN_CONV" "" 1130 in 1131 SUBS[(SUC_CONV(mk_comb{Rator=SUC,Rand=N'})),th] 1132 (SPECL[N',x,L']ithm') 1133 end 1134 in 1135 fn tm => 1136 (let val (K,L) = listSyntax.dest_take tm 1137 val k = int_of_term K and (lis,lty) = dest_list L 1138 in 1139 if k > length lis 1140 then raise ERR "FIRSTN_CONV" ("index too large: "^(int_to_string k)) 1141 else if (k = 0) then ISPEC L bthm 1142 else 1143 let val (ll,lr) = Lib.split_after k lis 1144 val bthm' = ISPEC (mk_list{els=lr,ty=lty}) bthm 1145 val ithm' = INST_TYPE[alpha |-> lty] ithm 1146 in 1147 itlist (itfn ithm') ll bthm' 1148 end 1149 end) 1150 handle e => raise wrap_exn "List_conv" "FIRSTN_CONV" e 1151 end; 1152 1153(*-----------------------------------------------------------------------*) 1154(* SCANL_CONV : conv -> conv *) 1155(* SCANL_CONV conv (���SCANL f e [x0,...,xn]���) ---> *) 1156(* |- SCANL f e [x0,...,xn] = [e, t0, ..., tn] *) 1157(* where conv (���f ei xi���) ---> |- f ei xi = ti *) 1158(*-----------------------------------------------------------------------*) 1159 1160val SCANL_CONV = 1161 let val (bthm,ithm) = CONJ_PAIR rich_listTheory.SCANL in 1162 fn conv => fn tm => 1163 (let val (f,e,l) = rich_listSyntax.dest_scanl tm 1164 val bthm' = ISPEC f bthm and ithm' = ISPEC f ithm 1165 fun scan_conv tm' = 1166 let val (E,L) = case snd(strip_comb tm') 1167 of [_,E,L] => (E,L) 1168 | _ => raise ERR "SCANL_CONV" "" 1169 in 1170 if (is_const L) then (SPEC E bthm') 1171 else 1172 let val (x,l) = case snd(strip_comb L) 1173 of [x,l] => (x,l) 1174 | _ => raise ERR "SCANL_CONV" "" 1175 val th1 = conv (mk_comb{Rator=mk_comb{Rator=f,Rand=E}, 1176 Rand=x}) 1177 val th2 = SUBS[th1](SPECL[E,x,l] ithm') 1178 val th3 = scan_conv 1179 (last(snd(strip_comb(rhs(concl th2))))) 1180 in 1181 SUBS[th3]th2 1182 end 1183 end 1184 in 1185 (scan_conv tm) 1186 end) 1187 handle e => raise wrap_exn "List_conv" "SCANL_CONV" e 1188 end; 1189 1190(*-----------------------------------------------------------------------*) 1191(* SCANR_CONV : conv -> conv *) 1192(* SCANR_CONV conv (���SCANR f e [x0,...,xn]���) ---> *) 1193(* |- SCANR f e [x0,...,xn] = [t0, ..., tn, e] *) 1194(* where conv (���f xi ei���) ---> |- f xi ei = ti *) 1195(*-----------------------------------------------------------------------*) 1196 1197val SCANR_CONV = 1198 let val (bthm,ithm) = CONJ_PAIR (rich_listTheory.SCANR) 1199 val HD = rich_listTheory.HD in 1200 fn conv => fn tm => 1201 (let val (f,e,l) = rich_listSyntax.dest_scanr tm 1202 val bthm' = ISPEC f bthm and ithm' = ISPEC f ithm 1203 fun scan_conv tm' = 1204 let val (E,L) = case snd(strip_comb tm') 1205 of [_,E,L] => (E,L) 1206 | _ => raise ERR "SCANR_CONV" "" 1207 in 1208 if (is_const L) then (SPEC E bthm') 1209 else 1210 let val (x,l) = case snd(strip_comb L) 1211 of [x,l] => (x,l) 1212 | _ => raise ERR "SCANR_CONV" "" 1213 val th2 = (SPECL[E,x,l] ithm') 1214 val th3 = scan_conv 1215 (last(snd(strip_comb(rhs(concl th2))))) 1216 val th4 = PURE_ONCE_REWRITE_RULE[HD](SUBS[th3]th2) 1217 val th5 = conv (hd(snd(strip_comb(rhs(concl th4))))) 1218 in 1219 SUBS[th5]th4 1220 end 1221 end 1222 in 1223 (scan_conv tm) 1224 end) 1225 handle e => raise wrap_exn "List_conv" "SCANR_CONV" e 1226 end; 1227 1228(*-----------------------------------------------------------------------*) 1229(* REPLICATE_CONV : conv *) 1230(* REPLICATE conv (���REPLICATE n x���) ---> *) 1231(* |- REPLICATE n x = [x, ..., x] *) 1232(*-----------------------------------------------------------------------*) 1233 1234val REPLICATE_CONV = 1235 let val (bthm,ithm) = CONJ_PAIR (rich_listTheory.REPLICATE) 1236 fun dec n = term_of_int((int_of_term n) - 1) 1237 fun repconv (bthm', ithm') tm = 1238 let val n = case snd(strip_comb tm) 1239 of [n,_] => n 1240 | _ => raise ERR "REPLICATE_CONV" "" 1241 in 1242 if ((int_of_term n) = 0) then bthm' 1243 else let val th1 = SUBS_OCCS [([1],SYM (num_CONV n))] 1244 (SPEC (dec n) ithm') 1245 in 1246 CONV_RULE ((RAND_CONV o RAND_CONV) 1247 (repconv(bthm',ithm'))) 1248 th1 1249 end 1250 end 1251 in 1252 fn tm => 1253 (let val (n,x) = rich_listSyntax.dest_replicate tm 1254 val bthm' = ISPEC x bthm 1255 val nv = mk_var{Name="n",Ty=(==`:num`==)} 1256 val ithm' = GEN nv (ISPECL[nv,x] ithm) 1257 in 1258 (repconv (bthm',ithm') tm) 1259 end) 1260 handle e => raise wrap_exn "List_conv" "REPLICATE_CONV" e 1261 end; 1262 1263(*-----------------------------------------------------------------------*) 1264(* GENLIST_CONV : conv -> conv *) 1265(* GENLIST conv (���GENLIST f n���) ---> *) 1266(* |- GENLIST f n = [f 0,f 1, ...,f(n-1)] *) 1267(*-----------------------------------------------------------------------*) 1268 1269val GENLIST_CONV = 1270 let val (bthm,ithm) = CONJ_PAIR listTheory.GENLIST 1271 fun dec n = term_of_int((int_of_term n) - 1) 1272 fun genconv (bthm,ithm) conv tm = 1273 let val n = last(snd(strip_comb tm)) 1274 in 1275 if ((int_of_term n) = 0) then CONV_RULE(ONCE_DEPTH_CONV conv) bthm 1276 else (let val th1 = SUBS[SYM (num_CONV n)](SPEC (dec n) ithm) 1277 val th2 = RIGHT_CONV_RULE ((RATOR_CONV o RAND_CONV) conv) th1 1278 in 1279 RIGHT_CONV_RULE (RAND_CONV (genconv (bthm,ithm) conv)) th2 1280 end) 1281 end 1282 in 1283 fn conv => fn tm => 1284 (let val (f,n) = listSyntax.dest_genlist tm 1285 val bthm' = ISPEC f bthm and ithm' = ISPEC f ithm 1286 in 1287 RIGHT_CONV_RULE (TOP_DEPTH_CONV SNOC_CONV) 1288 (genconv (bthm',ithm') conv tm) 1289 end) 1290 handle e => raise wrap_exn "List_conv" "GENLIST_CONV" e 1291 end; 1292 1293(* PC 11/7/94 *) 1294 1295(* --------------------------------------------------------------------- *) 1296(* AND_EL_CONV : conv *) 1297(* AND_EL_CONV (���AND_EL [x0,...,xn]���) ---> *) 1298(* |- AND_EL [x0,...,xn] = T iff |- xi = T for all i *) 1299(* |- AND_EL [x0,...,xn] = F otherwise *) 1300(* --------------------------------------------------------------------- *) 1301 1302val AND_EL_CONV = 1303 list_FOLD_CONV (rich_listTheory.AND_EL_FOLDR) (REWRITE_CONV[AND_CLAUSES]); 1304 1305(* --------------------------------------------------------------------- *) 1306(* OR_EL_CONV : conv *) 1307(* OR_EL_CONV (���OR_EL [x0,...,xn]���) ---> *) 1308(* |- OR_EL [x0,...,xn] = T iff |- xi = T for any i *) 1309(* |- OR_EL [x0,...,xn] = F otherwise *) 1310(* --------------------------------------------------------------------- *) 1311 1312val OR_EL_CONV = 1313 list_FOLD_CONV rich_listTheory.OR_EL_FOLDR (REWRITE_CONV[OR_CLAUSES]); 1314 1315 1316 1317end; (* List_conv1 *) 1318