Filtering...

base-lists

books/acl2s/base-lists
other
(in-package "ACL2S")
other
(include-book "defdata/top" :ttags :all)
other
(include-book "std/lists/top" :dir :system)
other
(include-book "definec" :ttags :all)
other
(include-book "check-equal")
other
(include-book "acl2s/ccg/ccg" :dir :system :uncertified-okp nil :ttags ((:ccg)) :load-compiled-file nil)
other
(set-termination-method :ccg)
other
(local (set-defunc-timeout 1000))
other
(in-theory (enable true-listp
    len
    append
    rev
    revappend
    no-duplicatesp-equal
    make-character-list
    nthcdr
    subseq-list
    resize-list
    last
    butlast
    remove
    member
    subsetp
    intersectp
    union-equal
    set-difference-equal
    intersection-equal))
other
(add-macro-fn tlp true-listp)
tl-fixmacro
(defmacro tl-fix
  (x)
  `(true-list-fix ,ACL2S::X))
other
(add-macro-fn tl-fix true-list-fix)
other
(definec bin-app
  (x :tl y :tl)
  :tl (if (endp x)
    y
    (cons (car x)
      (bin-app (cdr x) y))))
other
(make-n-ary-macro app bin-app nil t)
other
(add-macro-fn app bin-app)
other
(defthm app-assoc
  (implies (and (tlp x)
      (tlp y)
      (tlp z))
    (equal (app (app x y) z)
      (app x (app y z)))))
other
(defthm app-nil
  (implies (tlp x)
    (equal (app x nil) x)))
other
(defthm app-of-cons
  (implies (and (tlp x) (tlp y))
    (equal (app (cons a x) y)
      (cons a (app x y)))))
other
(defthm app-of-rcons
  (implies (and (tlp x) (tlp y))
    (equal (app (rcons a x) y)
      (app x (cons a y))))
  :hints (("goal" :in-theory (enable rcons))))
other
(defthm app-under-iff
  (implies (and (tlp x) (tlp y))
    (iff (app x y)
      (or x y))))
other
(defthm app-of-repeat-to-cons-of-same
  (implies (tlp x)
    (equal (app (repeat n a)
        (cons a x))
      (cons a
        (app (repeat n a) x))))
  :hints (("goal" :in-theory (enable repeat))))
other
(defthm app-when-prefixp
  (implies (and (tlp x)
      (tlp y)
      (prefixp x y))
    (equal (app x
        (nthcdr (len x) y))
      y))
  :hints (("goal" :in-theory (enable prefixp))))
other
(defthm app-of-take-and-nthcdr
  (implies (and (tlp x)
      (<= (nfix n) (len x)))
    (equal (app (take n x)
        (nthcdr n x))
      x)))
==macro
(defmacro ==
  (x y)
  `(equal ,ACL2S::X ,ACL2S::Y))
=/=macro
(defmacro =/=
  (x y)
  `(not (equal ,ACL2S::X ,ACL2S::Y)))
!=macro
(defmacro !=
  (x y)
  `(not (equal ,ACL2S::X ,ACL2S::Y)))
=>macro
(defmacro =>
  (x y)
  `(implies ,ACL2S::X ,ACL2S::Y))
->macro
(defmacro ->
  (x y)
  `(implies ,ACL2S::X ,ACL2S::Y))
<-macro
(defmacro <-
  (x y)
  `(implies ,ACL2S::Y ,ACL2S::X))
!macro
(defmacro ! (x) `(not ,ACL2S::X))
^macro
(defmacro ^ (&rest args) `(and ,@ACL2S::ARGS))
vmacro
(defmacro v (&rest args) `(or ,@ACL2S::ARGS))
other
(definec in
  (a :all x :tl)
  :bool (and (consp x)
    (or (== a (car x))
      (in a (cdr x)))))
other
(definec nin
  (a :all x :tl)
  :bool (not (in a x)))
other
(defdata non-empty-true-list
  (cons all true-list))
other
(defdata-alias ne-tl
  non-empty-true-list)
other
(add-macro-fn ne-tlp
  non-empty-true-listp)
other
(definec left
  (x :cons)
  :all (car x))
other
(definec right
  (x :cons)
  :all (cdr x))
other
(definec head
  (x :ne-tl)
  :all (car x))
other
(definec tail
  (x :ne-tl)
  :tl (cdr x))
other
(definec lcons
  (x :all y :tl)
  :ne-tl (cons x y))
other
(definec lnth
  (n :nat l :tl)
  :all :pre (< n (len l))
  (nth n l))
other
(check= (lnth 2 '(0 1 2 3)) 2)
other
(definec lnthcdr
  (n :nat l :tl)
  :tl :pre (<= n (len l))
  (nthcdr n l))
other
(check= (lnthcdr 2 '(0 1 2 3)) '(2 3))
other
(defdata str-all (list string all))
other
(defdata l-str-all
  (listof str-all))
other
(definec-no-test gen-car-cdr-aux-1
  (car :var cdr
    :var carstr
    :string cdrstr
    :string res
    :l-str-all)
  :l-str-all (if (endp res)
    res
    (b* ((e (first res)) (str (first e))
        (exp (second e)))
      (list* `(,(STR::CAT ACL2S::CARSTR ACL2S::STR) `(,',CAR ,,EXP))
        `(,(STR::CAT ACL2S::CDRSTR ACL2S::STR) `(,',CDR ,,EXP))
        (gen-car-cdr-aux-1 car
          cdr
          carstr
          cdrstr
          (cdr res))))))
other
(check= (gen-car-cdr-aux-1 'head
    'tail
    "h"
    "t"
    '(("" x)))
  `(("h" `(head ,ACL2S::X)) ("t" `(tail ,ACL2S::X))))
other
(definec-no-test gen-car-cdr-aux
  (car :var cdr
    :var carstr
    :string cdrstr
    :string depth
    :nat res
    :l-str-all)
  :l-str-all (declare (xargs :consider-only-ccms (depth)))
  (cond ((endp res) (gen-car-cdr-aux car
        cdr
        carstr
        cdrstr
        depth
        `(("" x))))
    ((== depth 0) res)
    (t (app (if (consp (cdr res))
          res
          nil)
        (gen-car-cdr-aux car
          cdr
          carstr
          cdrstr
          (1- depth)
          (gen-car-cdr-aux-1 car
            cdr
            carstr
            cdrstr
            res))))))
other
(check= (gen-car-cdr-aux 'head
    'tail
    "h"
    "t"
    1
    nil)
  `(("h" `(head ,ACL2S::X)) ("t" `(tail ,ACL2S::X))))
other
(check= (gen-car-cdr-aux 'head
    'tail
    "h"
    "t"
    2
    nil)
  `(("h" `(head ,ACL2S::X)) ("t" `(tail ,ACL2S::X))
    ("hh" `(head (head ,ACL2S::X)))
    ("th" `(tail (head ,ACL2S::X)))
    ("ht" `(head (tail ,ACL2S::X)))
    ("tt" `(tail (tail ,ACL2S::X)))))
other
(definec gen-car-cdr-defs-fn
  (l :l-str-all prefix
    :string suffix
    :string pkg
    :string)
  :all :pre (!= pkg "")
  (if (endp l)
    l
    (b* ((mname (s+ (cat prefix (caar l) suffix)
           :pkg pkg)) (x (fix-intern$ "X" pkg)))
      (cons `(defmacro ,ACL2S::MNAME (,ACL2S::X) ,(CADAR ACL2S::L))
        (gen-car-cdr-defs-fn (cdr l)
          prefix
          suffix
          pkg)))))
other
(definec gen-car-cdr-macros-fn
  (car :var cdr
    :var carstr
    :string cdrstr
    :string prefix
    :string suffix
    :string depth
    :nat pkg
    :string)
  :all :pre (!= pkg "")
  :skip-tests t
  (let ((l (gen-car-cdr-aux car
         cdr
         carstr
         cdrstr
         depth
         nil)))
    `(encapsulate nil
      ,@(ACL2S::GEN-CAR-CDR-DEFS-FN ACL2S::L ACL2S::PREFIX ACL2S::SUFFIX ACL2S::PKG))))
other
(check= (gen-car-cdr-macros-fn 'head
    'tail
    "A"
    "D"
    "LC"
    "R"
    2
    "ACL2S")
  `(encapsulate nil
    (defmacro lcar (x) `(head ,ACL2S::X))
    (defmacro lcdr (x) `(tail ,ACL2S::X))
    (defmacro lcaar
      (x)
      `(head (head ,ACL2S::X)))
    (defmacro lcdar
      (x)
      `(tail (head ,ACL2S::X)))
    (defmacro lcadr
      (x)
      `(head (tail ,ACL2S::X)))
    (defmacro lcddr
      (x)
      `(tail (tail ,ACL2S::X)))))
gen-car-cdr-macrosmacro
(defmacro gen-car-cdr-macros
  (car cdr
    carstr
    cdrstr
    prefix
    suffix
    depth)
  `(make-event (gen-car-cdr-macros-fn ',CAR
      ',CDR
      ,ACL2S::CARSTR
      ,ACL2S::CDRSTR
      ,ACL2S::PREFIX
      ,ACL2S::SUFFIX
      ,ACL2S::DEPTH
      (current-package state))))
other
(gen-car-cdr-macros head
  tail
  "A"
  "D"
  "LC"
  "R"
  4)
lcarmacro
(defmacro lcar (x) `(head ,ACL2S::X))
lcdrmacro
(defmacro lcdr (x) `(tail ,ACL2S::X))
lcaarmacro
(defmacro lcaar
  (x)
  `(head (head ,ACL2S::X)))
lcadrmacro
(defmacro lcadr
  (x)
  `(head (tail ,ACL2S::X)))
lcdarmacro
(defmacro lcdar
  (x)
  `(tail (head ,ACL2S::X)))
lcddrmacro
(defmacro lcddr
  (x)
  `(tail (tail ,ACL2S::X)))
lcaaarmacro
(defmacro lcaaar
  (x)
  `(head (head (head ,ACL2S::X))))
lcaadrmacro
(defmacro lcaadr
  (x)
  `(head (head (tail ,ACL2S::X))))
lcadarmacro
(defmacro lcadar
  (x)
  `(head (tail (head ,ACL2S::X))))
lcaddrmacro
(defmacro lcaddr
  (x)
  `(head (tail (tail ,ACL2S::X))))
lcdaarmacro
(defmacro lcdaar
  (x)
  `(tail (head (head ,ACL2S::X))))
lcdadrmacro
(defmacro lcdadr
  (x)
  `(tail (head (tail ,ACL2S::X))))
lcddarmacro
(defmacro lcddar
  (x)
  `(tail (tail (head ,ACL2S::X))))
lcdddrmacro
(defmacro lcdddr
  (x)
  `(tail (tail (tail ,ACL2S::X))))
lcaaaarmacro
(defmacro lcaaaar
  (x)
  `(head (head (head (head ,ACL2S::X)))))
lcaaadrmacro
(defmacro lcaaadr
  (x)
  `(head (head (head (tail ,ACL2S::X)))))
lcaadarmacro
(defmacro lcaadar
  (x)
  `(head (head (tail (head ,ACL2S::X)))))
lcaaddrmacro
(defmacro lcaaddr
  (x)
  `(head (head (tail (tail ,ACL2S::X)))))
lcadaarmacro
(defmacro lcadaar
  (x)
  `(head (tail (head (head ,ACL2S::X)))))
lcadadrmacro
(defmacro lcadadr
  (x)
  `(head (tail (head (tail ,ACL2S::X)))))
lcaddarmacro
(defmacro lcaddar
  (x)
  `(head (tail (tail (head ,ACL2S::X)))))
lcadddrmacro
(defmacro lcadddr
  (x)
  `(head (tail (tail (tail ,ACL2S::X)))))
lcdaaarmacro
(defmacro lcdaaar
  (x)
  `(tail (head (head (head ,ACL2S::X)))))
lcdaadrmacro
(defmacro lcdaadr
  (x)
  `(tail (head (head (tail ,ACL2S::X)))))
lcdadarmacro
(defmacro lcdadar
  (x)
  `(tail (head (tail (head ,ACL2S::X)))))
lcdaddrmacro
(defmacro lcdaddr
  (x)
  `(tail (head (tail (tail ,ACL2S::X)))))
lcddaarmacro
(defmacro lcddaar
  (x)
  `(tail (tail (head (head ,ACL2S::X)))))
lcddadrmacro
(defmacro lcddadr
  (x)
  `(tail (tail (head (tail ,ACL2S::X)))))
lcdddarmacro
(defmacro lcdddar
  (x)
  `(tail (tail (tail (head ,ACL2S::X)))))
lcddddrmacro
(defmacro lcddddr
  (x)
  `(tail (tail (tail (tail ,ACL2S::X)))))
other
(gen-car-cdr-macros head
  tail
  "A"
  "D"
  "LC"
  "R"
  4)
lfirstmacro
(defmacro lfirst (x) `(lcar ,ACL2S::X))
lsecondmacro
(defmacro lsecond
  (x)
  `(lcadr ,ACL2S::X))
lthirdmacro
(defmacro lthird
  (x)
  `(lcaddr ,ACL2S::X))
lfourthmacro
(defmacro lfourth
  (x)
  `(lcadddr ,ACL2S::X))
lfifthmacro
(defmacro lfifth
  (x)
  `(lcar (lcddddr ,ACL2S::X)))
lsixthmacro
(defmacro lsixth
  (x)
  `(lcadr (lcddddr ,ACL2S::X)))
lseventhmacro
(defmacro lseventh
  (x)
  `(lcaddr (lcddddr ,ACL2S::X)))
leighthmacro
(defmacro leighth
  (x)
  `(lcadddr (lcddddr ,ACL2S::X)))
lninthmacro
(defmacro lninth
  (x)
  `(lcar (lcddddr (lcddddr ,ACL2S::X))))
ltenthmacro
(defmacro ltenth
  (x)
  `(lcadr (lcddddr (lcddddr ,ACL2S::X))))
other
(defthm expand-len-with-trigger-cdr
  (implies (and (<= c (len x))
      (posp c))
    (<= (1- c) (len (cdr x))))
  :rule-classes ((:forward-chaining :trigger-terms ((< (len x) c) (cdr x)))))
other
(defthm len-non-nil-with-trigger-cdr
  (implies (and (<= c (len x))
      (posp c))
    x)
  :rule-classes ((:forward-chaining :trigger-terms ((< (len x) c)))))
other
(defthm cddr-implies-cdr-trigger-cddr
  (implies (cddr x) (cdr x))
  :rule-classes ((:forward-chaining :trigger-terms ((cddr x)))))
other
(defthm tlp-implies-tlpcdr-trigger-cdr
  (implies (true-listp x)
    (true-listp (cdr x)))
  :rule-classes ((:forward-chaining :trigger-terms ((cdr x)))))
other
(defthm tlp-consp-cdr-implies-tail-trigger-tail
  (implies (and (true-listp x) (consp (cdr x)))
    (tail x))
  :rule-classes ((:forward-chaining :trigger-terms ((tail x)))))
other
(defthm tlp-consp-implies-tlp-tail-trigger-tail
  (implies (and (true-listp x) x)
    (true-listp (tail x)))
  :rule-classes ((:forward-chaining :trigger-terms ((tail x)))))
other
(defthm consp-cdr-implies-right-trigger-right
  (implies (consp (cdr x))
    (right x))
  :rule-classes ((:forward-chaining :trigger-terms ((right x)))))
other
(defthm tlp-consp-implies-tlp-right-trigger-right
  (implies (and (true-listp x) x)
    (true-listp (right x)))
  :rule-classes ((:forward-chaining :trigger-terms ((right x)))))
other
(defthm left-cons
  (equal (left (cons x y)) x))
other
(defthm right-cons
  (equal (right (cons x y)) y))
other
(defthm left-consp
  (implies (force (consp x))
    (equal (left x) (car x))))
other
(defthm right-consp
  (implies (force (consp x))
    (equal (right x) (cdr x))))
other
(defthm head-cons
  (implies (force (tlp y))
    (equal (head (cons x y)) x)))
other
(defthm tail-cons
  (implies (force (tlp y))
    (equal (tail (cons x y)) y)))
other
(defthm head-consp
  (implies (and (force (tlp x))
      (force x))
    (equal (head x) (car x))))
other
(defthm tail-consp
  (implies (and (force (tlp x))
      (force x))
    (equal (tail x) (cdr x))))
other
(in-theory (disable tail
    tail-definition-rule
    head
    head-definition-rule
    left
    left-definition-rule
    right
    right-definition-rule))
other
(definec snoc
  (l :tl e :all)
  :ne-tl (append l (list e)))
lsnocmacro
(defmacro lsnoc
  (l e)
  `(snoc ,ACL2S::L ,ACL2S::E))
other
(definec snocl
  (l :ne-tl)
  :tl (butlast l 1))
other
(definec snocr
  (l :ne-tl)
  :all (car (last l)))
other
(register-data-constructor (ne-tlp snoc)
  ((tlp snocl) (allp snocr))
  :rule-classes nil
  :proper nil)
other
(definec lendp
  (x :tl)
  :bool (atom x))
other
(definec llen
  (x :tl)
  :nat (len x))
other
(definec lrev
  (x :tl)
  :tl (rev x))
other
(defthm app-of-snoc
  (implies (and (tlp x) (tlp y))
    (equal (app (snoc x a) y)
      (app x (cons a y)))))
other
(defthm len-of-app
  (implies (and (tlp x) (tlp y))
    (equal (len (app x y))
      (+ (len x) (len y)))))