Package parser-all-thm: Theorems about the whole stream parser

Information

name	parser-all-thm
version	1.2
description	Theorems about the whole stream parser
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-03-20
show	Data.Bool

Files

Package tarball parser-all-thm-1.2.tgz
Theory file parser-all-thm.thy (included in the package tarball)

Theorems

⊦ ∀p s.
Number.Natural.≤ (Parser.Stream.length (Parser.parseStream p s))
(Parser.Stream.length s)

⊦ ∀p e l.
    Parser.inverse p e ⇒
    Parser.parseStream p
      (Parser.Stream.fromList (Data.List.concat (Data.List.map e l))) =
    Parser.Stream.fromList l

⊦ ∀p e x s.
    Parser.inverse p e ⇒
    Parser.parseStream p (Parser.Stream.append (e x) s) =
    Parser.Stream.stream x (Parser.parseStream p s)

⊦ ∀p e s.
    Parser.strongInverse p e ⇒
    Data.Option.case T
      (λl.
         Parser.Stream.toList s =
         Data.Option.some (Data.List.concat (Data.List.map e l)))
      (Parser.Stream.toList (Parser.parseStream p s))

Input Type Operators

→
bool
Data
- List
  - Data.List.list
- Option
  - Data.Option.option
- Pair
  - Data.Pair.*
Number
- Natural
  - Number.Natural.natural
Parser
- Parser.parser
- Stream
  - Parser.Stream.stream

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - select
  - F
  - T
- List
  - Data.List.::
  - Data.List.@
  - Data.List.[]
  - Data.List.concat
  - Data.List.map
- Option
  - Data.Option.case
  - Data.Option.none
  - Data.Option.some
- Pair
  - Data.Pair.,
Number
- Natural
  - Number.Natural.≤
  - Number.Natural.suc
- Numeral
  - Number.Numeral.zero
Parser
- Parser.destParser
- Parser.inverse
- Parser.parse
- Parser.parseStream
- Parser.strongInverse
- Stream
  - Parser.Stream.append
  - Parser.Stream.eof
  - Parser.Stream.error
  - Parser.Stream.fromList
  - Parser.Stream.isProperSuffix
  - Parser.Stream.isSuffix
  - Parser.Stream.length
  - Parser.Stream.stream
  - Parser.Stream.toList

Assumptions

⊦ T

⊦ ∀n. Number.Natural.≤ Number.Numeral.zero n

⊦ ∀n. Number.Natural.≤ n n

⊦ F ⇔ ∀p. p

⊦ ∀x. ¬Parser.Stream.isProperSuffix x x

⊦ (¬) = λp. p ⇒ F

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

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

⊦ ∀a'. ¬(Data.Option.none = Data.Option.some a')

⊦ ∀x. x = x ⇔ T

⊦ ∀l. Parser.Stream.fromList l = Parser.Stream.append l Parser.Stream.eof

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

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

⊦ ∀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

⊦ ∀a a'. Data.Option.some a = Data.Option.some a' ⇔ a = a'

⊦ ∀m n.
Number.Natural.≤ (Number.Natural.suc m) (Number.Natural.suc n) ⇔
Number.Natural.≤ m n

⊦ ∀x y.
Parser.Stream.isSuffix x y ⇒
Number.Natural.≤ (Parser.Stream.length x) (Parser.Stream.length y)

⊦ ∀l. l = Data.List.[] ∨ ∃h t. l = Data.List.:: h t

⊦ (∨) = λ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

⊦ ∀m n p.
Number.Natural.≤ m n ∧ Number.Natural.≤ n p ⇒ Number.Natural.≤ m p

⊦ ∀x y z.
Parser.Stream.append (Data.List.@ x y) z =
Parser.Stream.append x (Parser.Stream.append y z)

⊦ ∀l s.
    Parser.Stream.toList (Parser.Stream.append l s) =
    Data.Option.case Data.Option.none
      (λls. Data.Option.some (Data.List.@ l ls)) (Parser.Stream.toList s)

⊦ Data.List.concat Data.List.[] = Data.List.[] ∧
  ∀h t.
    Data.List.concat (Data.List.:: h t) =
    Data.List.@ h (Data.List.concat t)

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

⊦ ∀p. (∀x. (∀y. Parser.Stream.isProperSuffix y x ⇒ p y) ⇒ p x) ⇒ ∀x. p x

⊦ ∀P. P Data.List.[] ∧ (∀a0 a1. P a1 ⇒ P (Data.List.:: a0 a1)) ⇒ ∀x. P x

⊦ ∀x y a b. Data.Pair., x y = Data.Pair., a b ⇔ x = a ∧ y = b

⊦ ∀p e.
    Parser.inverse p e ⇔
    ∀x s.
      Parser.parse p (Parser.Stream.append (e x) s) =
      Data.Option.some (Data.Pair., x s)

⊦ Parser.Stream.length Parser.Stream.error = Number.Numeral.zero ∧
  Parser.Stream.length Parser.Stream.eof = Number.Numeral.zero ∧
  ∀a s.
    Parser.Stream.length (Parser.Stream.stream a s) =
    Number.Natural.suc (Parser.Stream.length s)

⊦ (∀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

⊦ (∀s. Parser.Stream.append Data.List.[] s = s) ∧
  ∀h t s.
    Parser.Stream.append (Data.List.:: h t) s =
    Parser.Stream.stream h (Parser.Stream.append t s)

⊦ ∀p s.
    Parser.parse p s = Data.Option.none ∨
    ∃b s'.
      Parser.parse p s = Data.Option.some (Data.Pair., b s') ∧
      Parser.Stream.isProperSuffix s' s

⊦ (∀f. Data.List.map f Data.List.[] = Data.List.[]) ∧
  ∀f h t.
    Data.List.map f (Data.List.:: h t) =
    Data.List.:: (f h) (Data.List.map f t)

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

⊦ Parser.Stream.toList Parser.Stream.error = Data.Option.none ∧
  Parser.Stream.toList Parser.Stream.eof = Data.Option.some Data.List.[] ∧
  ∀a s.
    Parser.Stream.toList (Parser.Stream.stream a s) =
    Data.Option.case Data.Option.none
      (λl. Data.Option.some (Data.List.:: a l)) (Parser.Stream.toList s)

⊦ (∀p. Parser.parse p Parser.Stream.error = Data.Option.none) ∧
  (∀p. Parser.parse p Parser.Stream.eof = Data.Option.none) ∧
  ∀p a s.
    Parser.parse p (Parser.Stream.stream a s) = Parser.destParser p a s

⊦ ∀p e.
    Parser.strongInverse p e ⇔
    Parser.inverse p e ∧
    ∀s x s'.
      Parser.parse p s = Data.Option.some (Data.Pair., x s') ⇒
      s = Parser.Stream.append (e x) s'

⊦ ∀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'

⊦ ∀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)