Filtering...

channels

books/kestrel/file-io-light/channels

Included Books

unsigned-byte-listp-def typed-io-listp
other
(in-package "ACL2")
include-book
(include-book "kestrel/bv-lists/unsigned-byte-listp-def" :dir :system)
local
(local (include-book "typed-io-listp"))
in-theory
(in-theory (disable open-channels-p
    add-pair
    open-channel-listp
    open-channel1))
local
(local (defthm assoc-equal-when-ordered-symbol-alistp-and-symbol<-of-caar
    (implies (and (ordered-symbol-alistp alist)
        (symbol< key (car (car alist))))
      (equal (assoc-equal key alist) nil))
    :hints (("Goal" :in-theory (enable ordered-symbol-alistp assoc-equal)))))
in-theory
(in-theory (disable channel-headerp))
channel-headerp-of-listtheorem
(defthm channel-headerp-of-list
  (equal (channel-headerp (list a b c d))
    (and (equal a :header)
      (member-eq b *file-types*)
      (stringp c)
      (integerp d)))
  :hints (("Goal" :in-theory (enable channel-headerp))))
stringp-of-caddr-when-channel-headerptheorem
(defthmd stringp-of-caddr-when-channel-headerp
  (implies (channel-headerp header) (stringp (caddr header)))
  :hints (("Goal" :in-theory (enable channel-headerp))))
integerp-of-cadddr-when-channel-headerptheorem
(defthmd integerp-of-cadddr-when-channel-headerp
  (implies (channel-headerp header)
    (integerp (cadddr header)))
  :hints (("Goal" :in-theory (enable channel-headerp))))
typed-io-listp-of-cdr-and-cadr-of-cartheorem
(defthm typed-io-listp-of-cdr-and-cadr-of-car
  (implies (open-channel1 l)
    (typed-io-listp (cdr l) (cadr (car l))))
  :hints (("Goal" :in-theory (enable open-channel1))))
typed-io-listp-of-cdr-gentheorem
(defthm typed-io-listp-of-cdr-gen
  (implies (and (open-channel1 l) (equal typ (cadr (car l))))
    (typed-io-listp (cdr l) typ)))
open-channel-listp-of-add-pair-strongtheorem
(defthm open-channel-listp-of-add-pair-strong
  (implies (open-channel-listp l)
    (equal (open-channel-listp (add-pair key value l))
      (open-channel1 value)))
  :hints (("Goal" :in-theory (enable open-channel-listp add-pair))))
open-channel1-of-cdr-of-assoc-equaltheorem
(defthm open-channel1-of-cdr-of-assoc-equal
  (implies (and (assoc-equal channel channels)
      (open-channel-listp channels))
    (open-channel1 (cdr (assoc-equal channel channels))))
  :hints (("Goal" :in-theory (enable open-channels-p open-channel-listp))))
ordered-symbol-alistp-of-add-pairtheorem
(defthm ordered-symbol-alistp-of-add-pair
  (implies (ordered-symbol-alistp x)
    (equal (ordered-symbol-alistp (add-pair key val x))
      (symbolp key)))
  :hints (("Goal" :in-theory (enable add-pair ordered-symbol-alistp))))
open-channels-p-of-add-pair-strongtheorem
(defthm open-channels-p-of-add-pair-strong
  (implies (open-channels-p channels)
    (equal (open-channels-p (add-pair channel value channels))
      (and (symbolp channel) (open-channel1 value))))
  :hints (("Goal" :in-theory (e/d (open-channels-p) (add-pair len)))))
open-channel1-of-constheorem
(defthm open-channel1-of-cons
  (equal (open-channel1 (cons header rest))
    (and (channel-headerp header)
      (typed-io-listp rest (cadr header))))
  :hints (("Goal" :in-theory (enable open-channel1 channel-headerp))))
channel-headerp-of-cadr-of-assoc-equal-ifftheorem
(defthm channel-headerp-of-cadr-of-assoc-equal-iff
  (implies (open-channel-listp channels)
    (iff (channel-headerp (cadr (assoc-equal channel channels)))
      (assoc-equal channel channels)))
  :hints (("Goal" :in-theory (enable open-channel-listp channel-headerp))))
channel-headerp-of-cadr-of-assoc-equal-iff-2theorem
(defthm channel-headerp-of-cadr-of-assoc-equal-iff-2
  (implies (open-channels-p channels)
    (iff (channel-headerp (cadr (assoc-equal channel channels)))
      (assoc-equal channel channels)))
  :hints (("Goal" :in-theory (enable open-channels-p))))
typed-io-listp-of-cdddr-of-assoc-equal-and-cadr-of-cadr-of-assoc-equaltheorem
(defthm typed-io-listp-of-cdddr-of-assoc-equal-and-cadr-of-cadr-of-assoc-equal
  (implies (open-channel-listp channels)
    (typed-io-listp (cdddr (assoc-equal channel channels))
      (cadr (cadr (assoc-equal channel channels)))))
  :hints (("Goal" :in-theory (enable open-channel-listp channel-headerp typed-io-listp))))
typed-io-listp-of-cdddr-of-assoc-equal-and-cadr-of-cadr-of-assoc-equal-2theorem
(defthm typed-io-listp-of-cdddr-of-assoc-equal-and-cadr-of-cadr-of-assoc-equal-2
  (implies (and (symbolp channel) (open-channels-p channels))
    (typed-io-listp (cdddr (assoc-equal channel channels))
      (cadr (cadr (assoc-equal channel channels)))))
  :hints (("Goal" :in-theory (enable open-channels-p))))
equal-of-add-pair-sametheorem
(defthm equal-of-add-pair-same
  (implies (open-channels-p channels)
    (equal (equal (add-pair channel value channels) channels)
      (and (assoc-eq channel channels)
        (equal value (cdr (assoc-eq channel channels))))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (enable add-pair open-channel-listp open-channels-p))))
true-list-of-cddr-of-assoc-equal-when-open-channel-listptheorem
(defthm true-list-of-cddr-of-assoc-equal-when-open-channel-listp
  (implies (open-channel-listp channels)
    (true-listp (cddr (assoc-equal channel channels))))
  :hints (("Goal" :in-theory (enable open-channel-listp open-channel1))))
nat-listp-of-cddr-of-assoc-equal-when-open-channel-listptheorem
(defthm nat-listp-of-cddr-of-assoc-equal-when-open-channel-listp
  (implies (and (open-channel-listp channels)
      (equal (cadr (cadr (assoc-equal channel channels))) :byte))
    (nat-listp (cddr (assoc-equal channel channels))))
  :hints (("Goal" :in-theory (enable open-channel-listp
       open-channel1
       nat-listp-when-typed-io-listp-of-byte))))
unsigned-byte-listp-of-cddr-of-assoc-equal-when-open-channel-listptheorem
(defthm unsigned-byte-listp-of-cddr-of-assoc-equal-when-open-channel-listp
  (implies (and (open-channel-listp channels)
      (equal (cadr (cadr (assoc-equal channel channels))) :byte))
    (unsigned-byte-listp 8
      (cddr (assoc-equal channel channels))))
  :hints (("Goal" :in-theory (enable open-channel-listp
       open-channel1
       unsigned-byte-listp-when-typed-io-listp-of-byte))))
character-listp-of-cddr-of-assoc-equal-when-open-channel-listptheorem
(defthm character-listp-of-cddr-of-assoc-equal-when-open-channel-listp
  (implies (and (open-channel-listp channels)
      (equal (cadr (cadr (assoc-equal channel channels)))
        :character))
    (character-listp (cddr (assoc-equal channel channels))))
  :hints (("Goal" :in-theory (enable open-channel-listp open-channel1))))
open-channel-listp-of-constheorem
(defthm open-channel-listp-of-cons
  (equal (open-channel-listp (cons ch chs))
    (and (open-channel1 (cdr ch)) (open-channel-listp chs)))
  :hints (("Goal" :in-theory (enable open-channel-listp))))
ordered-symbol-alistp-of-remove1-assoc-equaltheorem
(defthm ordered-symbol-alistp-of-remove1-assoc-equal
  (implies (ordered-symbol-alistp channels)
    (ordered-symbol-alistp (remove1-assoc-equal channel channels)))
  :hints (("Goal" :in-theory (enable ordered-symbol-alistp))))
open-channel-listp-of-remove1-assoc-equal-alttheorem
(defthm open-channel-listp-of-remove1-assoc-equal-alt
  (implies (open-channel-listp channels)
    (open-channel-listp (remove1-assoc-equal channel channels)))
  :hints (("Goal" :in-theory (enable open-channel-listp))))
local
(local (in-theory (disable ordered-symbol-alistp)))
open-channels-p-of-remove1-assoc-equal-alttheorem
(defthm open-channels-p-of-remove1-assoc-equal-alt
  (implies (open-channels-p channels)
    (open-channels-p (remove1-assoc-equal channel channels)))
  :hints (("Goal" :in-theory (enable open-channels-p))))
open-input-channel-p1-forward-to-assoc-equaltheorem
(defthm open-input-channel-p1-forward-to-assoc-equal
  (implies (open-input-channel-p1 channel typ state)
    (assoc-equal channel (open-input-channels state)))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable open-input-channel-p1))))
symbolp-when-assoc-equal-and-open-channels-ptheorem
(defthmd symbolp-when-assoc-equal-and-open-channels-p
  (implies (and (assoc-equal channel channels)
      (open-channels-p channels))
    (symbolp channel))
  :hints (("Goal" :in-theory (enable open-channels-p ordered-symbol-alistp))))
symbolp-when-assoc-equal-of-open-input-channels-and-state-p1theorem
(defthmd symbolp-when-assoc-equal-of-open-input-channels-and-state-p1
  (implies (and (assoc-equal channel (open-input-channels state))
      (state-p1 state))
    (symbolp channel))
  :hints (("Goal" :in-theory (e/d (symbolp-when-assoc-equal-and-open-channels-p state-p1)
       (open-input-channels all-boundp)))))
symbolp-when-assoc-equal-of-open-input-channels-and-state-ptheorem
(defthmd symbolp-when-assoc-equal-of-open-input-channels-and-state-p
  (implies (and (assoc-equal channel (open-input-channels state))
      (state-p state))
    (symbolp channel))
  :hints (("Goal" :in-theory (e/d (state-p symbolp-when-assoc-equal-of-open-input-channels-and-state-p1)
       (open-input-channels)))))
assoc-equal-of-open-input-channels-when-open-input-channel-ptheorem
(defthm assoc-equal-of-open-input-channels-when-open-input-channel-p
  (implies (open-input-channel-p channel :byte state)
    (assoc-equal channel (open-input-channels state)))
  :hints (("Goal" :in-theory (enable open-input-channel-p open-input-channel-p1))))