Filtering...

read-object

books/kestrel/file-io-light/read-object

Included Books

state channels iprint-oracle-updates
other
(in-package "ACL2")
local
(local (include-book "kestrel/utilities/state" :dir :system))
local
(local (include-book "channels"))
local
(local (include-book "iprint-oracle-updates"))
in-theory
(in-theory (disable mv-nth read-object))
local
(local (defthmd assoc-equal-when-not-symbolp-and-open-channels-p
    (implies (and (not (symbolp channel)) (open-channels-p channels))
      (equal (assoc-equal channel channels) nil))
    :hints (("Goal" :in-theory (enable open-channels-p ordered-symbol-alistp)))))
mv-nth-0-of-read-object-ifftheorem
(defthm mv-nth-0-of-read-object-iff
  (iff (mv-nth 0 (read-object channel state))
    (not (consp (cddr (assoc-equal channel (open-input-channels state))))))
  :hints (("Goal" :in-theory (enable read-object))))
state-p1-of-mv-nth-2-of-read-objecttheorem
(defthm state-p1-of-mv-nth-2-of-read-object
  (implies (state-p1 state)
    (state-p1 (mv-nth 2 (read-object channel state))))
  :hints (("Goal" :in-theory (enable read-object
       symbolp-when-assoc-equal-of-open-input-channels-and-state-p1
       assoc-equal-when-not-symbolp-and-open-channels-p))))
state-p-of-mv-nth-2-of-read-objecttheorem
(defthm state-p-of-mv-nth-2-of-read-object
  (implies (state-p state)
    (state-p (mv-nth 2 (read-object channel state))))
  :hints (("Goal" :in-theory (enable state-p))))
open-input-channels-of-mv-nth-2-of-read-objecttheorem
(defthm open-input-channels-of-mv-nth-2-of-read-object
  (equal (open-input-channels (mv-nth 2 (read-object channel state)))
    (if (consp (cddr (assoc-equal channel (open-input-channels state))))
      (add-pair channel
        (cons (cadr (assoc-equal channel (open-input-channels state)))
          (cdddr (assoc-equal channel (open-input-channels state))))
        (open-input-channels state))
      (open-input-channels state)))
  :hints (("Goal" :in-theory (enable read-object))))
open-input-channel-p1-of-mv-nth-2-of-read-objecttheorem
(defthm open-input-channel-p1-of-mv-nth-2-of-read-object
  (implies (open-input-channel-p1 channel typ state)
    (open-input-channel-p1 channel
      typ
      (mv-nth 2 (read-object channel2 state))))
  :hints (("Goal" :in-theory (enable read-object open-input-channel-p1))))
open-input-channel-p-of-mv-nth-2-of-read-objecttheorem
(defthm open-input-channel-p-of-mv-nth-2-of-read-object
  (implies (open-input-channel-p channel typ state)
    (open-input-channel-p channel
      typ
      (mv-nth 2 (read-object channel2 state))))
  :hints (("Goal" :in-theory (enable open-input-channel-p))))
open-input-channel-any-p1-of-mv-nth-2-of-read-objecttheorem
(defthm open-input-channel-any-p1-of-mv-nth-2-of-read-object
  (implies (open-input-channel-any-p1 channel state)
    (open-input-channel-any-p1 channel
      (mv-nth 2 (read-object channel2 state))))
  :hints (("Goal" :in-theory (enable open-input-channel-any-p1))))
open-input-channel-any-p-of-mv-nth-2-of-read-objecttheorem
(defthm open-input-channel-any-p-of-mv-nth-2-of-read-object
  (implies (open-input-channel-any-p channel state)
    (open-input-channel-any-p channel
      (mv-nth 2 (read-object channel2 state))))
  :hints (("Goal" :in-theory (enable open-input-channel-any-p))))
<-of-len-of-channel-contents-of-mv-nth-2-of-read-object-alttheorem
(defthm <-of-len-of-channel-contents-of-mv-nth-2-of-read-object-alt
  (implies (consp (cddr (assoc-equal channel (open-input-channels state))))
    (< (len (cddr (assoc-equal channel
            (open-input-channels (mv-nth 2 (read-object channel state))))))
      (len (cddr (assoc-equal channel (open-input-channels state))))))
  :hints (("Goal" :in-theory (enable read-object))))