Package parser-all-def: Definition of the whole stream parser

Information

Files

• Package tarball parser-all-def-1.0.tgz
• Theory file parser-all-def.thy (included in the package tarball)

Defined Constant

• Parser
  • Parser.parseStream

Theorem

⊦ ∀p.
    Parser.parseStream p Parser.Stream.error = Parser.Stream.error ∧
    Parser.parseStream p Parser.Stream.eof = Parser.Stream.eof ∧
    ∀a s.
      Parser.parseStream p (Parser.Stream.stream a s) =
      Data.Option.case Parser.Stream.error
        (λ(Data.Pair., b s').
           Parser.Stream.stream b (Parser.parseStream p s'))
        (Parser.destParser p a s)

Input Type Operators

• →
• bool
• Data
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.*
• Parser
  • Parser.parser
  • Stream
    • Parser.Stream.stream

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • select
    • F
    • T
  • Option
    • Data.Option.case
    • Data.Option.none
    • Data.Option.some
  • Pair
    • Data.Pair.,
• Parser
  • Parser.destParser
  • Stream
    • Parser.Stream.case
    • Parser.Stream.eof
    • Parser.Stream.error
    • Parser.Stream.isProperSuffix
    • Parser.Stream.isSuffix
    • Parser.Stream.stream

Assumptions

⊦ T

⊦ (∃) = λP. P ((select) P)

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λP. P = λx. T

⊦ ∀x. x = x ⇔ T

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀P x. P x ⇒ P ((select) P)

⊦ ∀p. ∃x y. p = Data.Pair., x y

⊦ ∀x. x = Data.Option.none ∨ ∃a. x = Data.Option.some a

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀s s'.
    Parser.Stream.isSuffix s s' ⇔
    s = s' ∨ Parser.Stream.isProperSuffix s s'

⊦ ∀PAIR'. ∃fn. ∀a0 a1. fn (Data.Pair., a0 a1) = PAIR' a0 a1

⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃y. ∀x. P x (y x)

⊦ ∀x.
    x = Parser.Stream.error ∨ x = Parser.Stream.eof ∨
    ∃a0 a1. x = Parser.Stream.stream a0 a1

⊦ ∀p a s b s'.
    Parser.destParser p a s = Data.Option.some (Data.Pair., b s') ⇒
    Parser.Stream.isSuffix s' s

⊦ ∀a0 a1 a0' a1'.
    Parser.Stream.stream a0 a1 = Parser.Stream.stream a0' a1' ⇔
    a0 = a0' ∧ a1 = a1'

⊦ (∀b f. Data.Option.case b f Data.Option.none = b) ∧
  ∀b f a. Data.Option.case b f (Data.Option.some a) = f a

⊦ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

⊦ (∀s. Parser.Stream.isProperSuffix s Parser.Stream.error ⇔ F) ∧
  (∀s. Parser.Stream.isProperSuffix s Parser.Stream.eof ⇔ F) ∧
  ∀s a s'.
    Parser.Stream.isProperSuffix s (Parser.Stream.stream a s') ⇔
    s = s' ∨ Parser.Stream.isProperSuffix s s'

⊦ ∀h.
    (∀f g s.
       (∀s'. Parser.Stream.isProperSuffix s' s ⇒ f s' = g s') ⇒
       h f s = h g s) ⇒ ∃f. ∀s. f s = h f s

⊦ (∀e b f. Parser.Stream.case e b f Parser.Stream.error = e) ∧
  (∀e b f. Parser.Stream.case e b f Parser.Stream.eof = b) ∧
  ∀e b f a s. Parser.Stream.case e b f (Parser.Stream.stream a s) = f a s