Boyer_Moore/testset/list.ml

   1 let mytheory2 = ref [
   2 `(ZIP [] [] = []) /\ (ZIP (CONS h1 t1) (CONS h2 t2) = CONS (h1,h2) (ZIP t1 t2))`;
   3 `~(CONS h t = [])`;
   4 `(LAST [h:A] = h) /\ (LAST (CONS h (CONS k t)) = LAST (CONS k t))`;
   5 `APPEND (l:A list) [] = l`;
   6 `APPEND (l:A list) (APPEND m n) = APPEND (APPEND l m) n`;
   7 `REVERSE (APPEND (l:A list) m) = APPEND (REVERSE m) (REVERSE l)`;
   8 `REVERSE(REVERSE (l:A list)) = l`;
   9 `(CONS h1 t1 = CONS h2 t2) <=> (h1 = h2) /\ (t1 = t2)`;
  10 `LENGTH(APPEND (l:A list) (m:A list)) = LENGTH l + LENGTH m`;
  11 `MAP (f:A->B) (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)`;
  12 `LENGTH (MAP (f:A->B) l) = LENGTH l`;
  13 `(LENGTH (l:A list) = 0) <=> (l = [])`;
  14 `(LENGTH l = SUC n) /\ (l = CONS h t) ==> (LENGTH t = n)`;
  15 `ALL (\x. f x = g x) l ==> (MAP f l = MAP g l)`;
  16 `(MEM x l /\ P x ==> Q x) /\ ALL P l ==> ALL Q l`;
  17 `~(EX P l) <=> ALL (\x. ~(P x)) l`;
  18 `~(ALL P l) <=> EX (\x. ~(P x)) l`;
  19 `ALL P (MAP f l) <=> ALL (P o f) l`;
  20 `ALL (\x. T) l`;
  21 `ALL2 (\x y. f x = f y) l m ==> (MAP f l = MAP f m)`;
  22 `ALL2 P (MAP f l) l <=> ALL (\a. P (f a) a) l`;
  23 `ALL (\x. f(x) = x) l ==> (MAP f l = l)`;
  24 `ALL2 (\x y. P x /\ Q x y) l m <=> ALL P l /\ ALL2 Q l m`;
  25 `ITLIST f (APPEND l1 l2) a = ITLIST f l1 (ITLIST f l2 a)`;
  26 `ITLIST f (APPEND l [a]) b = ITLIST f l (f a b)`;
  27 `ALL (\x. P x ==> Q x) l /\ ALL P l ==> ALL Q l`;
  28 `ALL P l /\ ALL Q l <=> ALL (\x. P x /\ Q x) l`;
  29 `(MEM x l /\ P x ==> Q x) /\ EX P l ==> EX Q l`;
  30 `(MEM x l ==> P x) <=> ALL P l`;
  31 `LENGTH(REPLICATE n x) = n`;
  32 `EX P (MAP f l) <=> EX (P o f) l`;
  33 `(ALL (P x) l) <=> ALL (\s. P x s) l`;
  34 `MEM x (APPEND l1 l2) <=> MEM x l1 \/ MEM x l2`;
  35 `FILTER P (APPEND l1 l2) = APPEND (FILTER P l1) (FILTER P l2)`;
  36 `FILTER P (MAP f l) = MAP f (FILTER (P o f) l)`;
  37 `MEM x (FILTER P l) <=> P x /\ MEM x l`;
  38 `(LENGTH l1 = LENGTH l2) ==> (MAP FST (ZIP l1 l2) = l1)`;
  39 `(LENGTH l1 = LENGTH l2) ==> (MAP SND (ZIP l1 l2) = l2)`;
  40 `MEM (x,ASSOC x l) l <=> MEM x (MAP FST l)`;
  41 `ALL P (APPEND l1 l2) <=> ALL P l1 /\ ALL P l2`;
  42 `n < LENGTH l ==> MEM (EL n l) l`;
  43 `ALL2 P (MAP f l) (MAP g m) = ALL2 (\x y. P (f x) (g y)) l m`;
  44 `ALL2 P l m /\ ALL2 Q l m <=> ALL2 (\x y. P x y /\ Q x y) l m`;
  45 `ALL2 P l l <=> ALL (\x. P x x) l`;
  46 `(APPEND l m = []) <=> (l = []) /\ (m = [])`;
  47 `(LENGTH l = LENGTH m) ==> (LENGTH(MAP2 f l m) = LENGTH m)`;
  48 `(P x ==> Q x) ==> ALL P l ==> ALL Q l`;
  49 `((P:A->B->bool) x y ==> Q x y) ==> ALL2 P l l' ==> ALL2 Q l l'`
  50 ]