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