open-channels

(in-package "ACL2")

(defsection open-channel-lemmas
  :parents (std/io)
  :short "Lemmas about when various @(see state)-modifying functions
  do and don't affect the list of open channels."
  :long "<p>When programming with I/O, you may need to write functions that
      modify state in some way (perhaps by doing I/O) and exit
      returning a state which has some channels open, perhaps for
      further reading and writing later in your program.  Then, to
      prove guard theorems elsewhere, you'll need returns theorems
      about your function showing that those channels are open, either
      because they were open before the function ran and the function
      didn't close them, or because the function itself opened
      them.</p>

   <p>This book contains lemmas that can help you prove such returns
      theorems.  For each built-in I/O function, there is a lemma
      saying that, under appropriate hypotheses, it doesn't close your
      open input or output channels.</p>"
  (local (in-theory (enable open-input-channel
        open-output-channel
        close-input-channel
        close-output-channel
        read-char$
        read-byte$
        read-object
        princ$
        write-byte$
        print-object$
        set-serialize-character)))
  "<p>First are lemmas about @('open-input-channel-p1').</p>"
  (defthm open-input-channel-p1-under-open-input-channel
    (implies (open-input-channel-p1 channel type state)
      (b* (((mv other-channel state) (open-input-channel fname other-type state)))
        (implies (implies (equal other-channel channel)
            (equal other-type type))
          (open-input-channel-p1 channel type state)))))
  (defthm open-input-channel-p1-under-open-output-channel
    (implies (open-input-channel-p1 channel type state)
      (b* (((mv & state) (open-output-channel fname other-type state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-close-input-channel
    (implies (and (open-input-channel-p1 channel type state)
        (not (equal channel other-channel)))
      (b* ((state (close-input-channel other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-close-output-channel
    (implies (open-input-channel-p1 channel type state)
      (b* ((state (close-output-channel other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-read-char$
    (implies (open-input-channel-p1 channel type state)
      (b* (((mv & state) (read-char$ other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-read-byte$
    (implies (open-input-channel-p1 channel type state)
      (b* (((mv & state) (read-byte$ other-channel state)))
        (open-input-channel-p1 channel type state))))
  (local (in-theory (enable read-acl2-oracle update-acl2-oracle)))
  (defthm open-input-channel-p1-under-read-object
    (implies (open-input-channel-p1 channel type state)
      (b* (((mv & & state) (read-object other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-princ$
    (implies (open-input-channel-p1 channel type state)
      (b* ((state (princ$ x other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-write-byte$
    (implies (open-input-channel-p1 channel type state)
      (b* ((state (write-byte$ byte other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-print-object$
    (implies (open-input-channel-p1 channel type state)
      (b* ((state (print-object$ byte other-channel state)))
        (open-input-channel-p1 channel type state))))
  (defthm open-input-channel-p1-under-set-serialize-character
    (implies (open-input-channel-p1 channel type state)
      (b* ((state (set-serialize-character c state)))
        (open-input-channel-p1 channel type state))))
  "<p>Next are lemmas about @('open-output-channel-p1').</p>"
  (defthm open-output-channel-p1-under-open-input-channel
    (implies (open-output-channel-p1 channel type state)
      (b* (((mv & state) (open-input-channel fname other-type state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-open-output-channel
    (implies (open-output-channel-p1 channel type state)
      (b* (((mv other-channel state) (open-output-channel fname other-type state)))
        (implies (implies (equal other-channel channel)
            (equal other-type type))
          (open-output-channel-p1 channel type state)))))
  (defthm open-output-channel-p1-under-close-input-channel
    (implies (open-output-channel-p1 channel type state)
      (b* ((state (close-input-channel other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-close-output-channel
    (implies (and (open-output-channel-p1 channel type state)
        (not (equal channel other-channel)))
      (b* ((state (close-output-channel other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-read-char$
    (implies (open-output-channel-p1 channel type state)
      (b* (((mv & state) (read-char$ other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-read-byte$
    (implies (open-output-channel-p1 channel type state)
      (b* (((mv & state) (read-byte$ other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-read-object
    (implies (open-output-channel-p1 channel type state)
      (b* (((mv & & state) (read-object other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-princ$
    (implies (open-output-channel-p1 channel type state)
      (b* ((state (princ$ x other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-write-byte$
    (implies (open-output-channel-p1 channel type state)
      (b* ((state (write-byte$ byte other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-print-object$
    (implies (open-output-channel-p1 channel type state)
      (b* ((state (print-object$ byte other-channel state)))
        (open-output-channel-p1 channel type state))))
  (defthm open-output-channel-p1-under-set-serialize-character
    (implies (open-output-channel-p1 channel type state)
      (b* ((state (set-serialize-character c state)))
        (open-output-channel-p1 channel type state)))))