1\DOC list_ss 2 3\TYPE {list_ss : simpset} 4 5\SYNOPSIS 6Simplification set for lists. 7 8\KEYWORDS 9simplification, list. 10 11\DESCRIBE 12The simplification set {list_ss} is a version of {arith_ss} enhanced 13for the theory of lists. The following rewrites are currently used to 14augment those already present from {arith_ss}: 15{ 16 |- (!l. APPEND [] l = l) /\ 17 !l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2 18 |- (!l1 l2 l3. (APPEND l1 l2 = APPEND l1 l3) = (l2 = l3)) /\ 19 !l1 l2 l3. (APPEND l2 l1 = APPEND l3 l1) = (l2 = l3) 20 |- (!l. EL 0 l = HD l) /\ !l n. EL (SUC n) l = EL n (TL l) 21 |- (!P. EVERY P [] = T) /\ !P h t. EVERY P (h::t) = P h /\ EVERY P t 22 |- (FLAT [] = []) /\ !h t. FLAT (h::t) = APPEND h (FLAT t) 23 |- (LENGTH [] = 0) /\ !h t. LENGTH (h::t) = SUC (LENGTH t) 24 |- (!f. MAP f [] = []) /\ !f h t. MAP f (h::t) = f h::MAP f t 25 |- (!f. MAP2 f [] [] = []) /\ 26 !f h1 t1 h2 t2. 27 MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2 28 |- (!x. MEM x [] = F) /\ !x h t. MEM x (h::t) = (x = h) \/ MEM x t 29 |- (NULL [] = T) /\ !h t. NULL (h::t) = F 30 |- (REVERSE [] = []) /\ !h t. REVERSE (h::t) = APPEND (REVERSE t) [h] 31 |- (SUM [] = 0) /\ !h t. SUM (h::t) = h + SUM t 32 |- !h t. HD (h::t) = h 33 |- !h t. TL (h::t) = t 34 |- !l1 l2 l3. APPEND l1 (APPEND l2 l3) = APPEND (APPEND l1 l2) l3 35 |- !l. ~NULL l ==> (HD l::TL l = l) 36 |- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1') 37 |- !l1 l2. LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2 38 |- !l f. LENGTH (MAP f l) = LENGTH l 39 |- !f l1 l2. MAP f (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2) 40 |- !a1 a0. ~(a0::a1 = []) 41 |- !a1 a0. ~([] = a0::a1) 42 |- !l f. ((MAP f l = []) = (l = [])) /\ 43 (([] = MAP f l) = (l = [])) 44 |- !l. APPEND l [] = l 45 |- !l x. ~(l = x::l) /\ ~(x::l = l) 46 |- (!v f. case v f [] = v) /\ 47 !v f a0 a1. case v f (a0::a1) = f a0 a1 48 |- (!l1 l2. ([] = APPEND l1 l2) = (l1 = []) /\ (l2 = [])) /\ 49 !l1 l2. (APPEND l1 l2 = []) = (l1 = []) /\ (l2 = []) 50 |- (ZIP ([][]) = []) /\ 51 !x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2) 52 |- (UNZIP [] = ([],[])) /\ 53 !x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l)) 54 |- !P l1 l2. EVERY P (APPEND l1 l2) = EVERY P l1 /\ EVERY P l2 55 |- !P l1 l2. EXISTS P (APPEND l1 l2) = EXISTS P l1 \/ EXISTS P l2 56 |- !e l1 l2. MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 57 |- (!x. LAST [x] = x) /\ !x y z. LAST (x::y::z) = LAST (y::z) 58 |- (!x. FRONT [x] = []) /\ !x y z. FRONT (x::y::z) = x::FRONT (y::z) 59 |- (!f e. FOLDL f e [] = e) /\ 60 !f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l 61 |- (!f e. FOLDR f e [] = e) /\ 62 !f e x l. FOLDR f e (x::l) = f x (FOLDR f e l) 63} 64 65\SEEALSO 66BasicProvers.RW_TAC, BasicProvers.SRW_TAC, 67simpLib.SIMP_TAC, simpLib.SIMP_CONV, simpLib.SIMP_RULE, 68BasicProvers.bool_ss, bossLib.std_ss, bossLib.arith_ss. 69 70 71\ENDDOC 72