Package parser-comb-thm: Theorems about the basic parser combinators

Information

name	parser-comb-thm
version	1.0
description	Theorems about the basic parser combinators
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-03-18
show	Data.Bool

Files

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

Theorems

⊦ Parser.isParser Parser.parseAll.pa

⊦ Parser.isParser Parser.parseNone.pn

⊦ Parser.destParser Parser.parseNone = Parser.parseNone.pn

⊦ ∀p. Parser.isParser (Parser.destParser p)

⊦ Parser.inverse Parser.parseAll (λa. Data.List.:: a Data.List.[])

⊦ Parser.strongInverse Parser.parseAll (λa. Data.List.:: a Data.List.[])

⊦ ∀s. Parser.parse Parser.parseNone s = Data.Option.none

⊦ ∀pb pc. Parser.isParser (Parser.parsePair.pbc pb pc)

⊦ ∀f p. Parser.isParser (Parser.partialMap.pf f p)

⊦ ∀pb pc.
Parser.destParser (Parser.parsePair pb pc) = Parser.parsePair.pbc pb pc

⊦ ∀f p.
Parser.destParser (Parser.partialMap f p) = Parser.partialMap.pf f p

⊦ Parser.parse Parser.parseAll =
Parser.Stream.case Data.Option.none Data.Option.none
(λa s. Data.Option.some (Data.Pair., a s))

⊦ ∀p.
    Parser.parse (Parser.parseSome p) =
    Parser.Stream.case Data.Option.none Data.Option.none
      (λa s.
         if p a then Data.Option.some (Data.Pair., a s)
         else Data.Option.none)

⊦ ∀f.
    Parser.parse (Parser.parseOption f) =
    Parser.Stream.case Data.Option.none Data.Option.none
      (λa s.
         Data.Option.case Data.Option.none
           (λb. Data.Option.some (Data.Pair., b s)) (f a))

⊦ ∀p a s.
Parser.destParser (Parser.parseSome p) a s =
if p a then Data.Option.some (Data.Pair., a s) else Data.Option.none

⊦ ∀f a s.
    Parser.destParser (Parser.parseOption f) a s =
    Data.Option.case Data.Option.none
      (λb. Data.Option.some (Data.Pair., b s)) (f a)

⊦ ∀f e.
    (∀b. f (e b) = Data.Option.some b) ⇒
    Parser.inverse (Parser.parseOption f)
      (λb. Data.List.:: (e b) Data.List.[])

⊦ ∀p a s b s'.
Parser.destParser p a s = Data.Option.some (Data.Pair., b s') ⇒
Parser.Stream.isSuffix s' 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 p g e.
Parser.inverse p e ∧ (∀b. f (g b) = b) ⇒
Parser.inverse (Parser.map f p) (λc. e (g c))

⊦ ∀f p g e.
Parser.inverse p e ∧ (∀b. f (g b) = Data.Option.some b) ⇒
Parser.inverse (Parser.partialMap f p) (λc. e (g c))

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

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

⊦ ∀f p s.
    Parser.parse (Parser.map f p) s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s'). Data.Option.some (Data.Pair., (f b) s'))
      (Parser.parse p s)

⊦ ∀pb pc eb ec.
    Parser.inverse pb eb ∧ Parser.inverse pc ec ⇒
    Parser.inverse (Parser.parsePair pb pc)
      (λ(Data.Pair., b c). Data.List.@ (eb b) (ec c))

⊦ ∀pb pc eb ec.
    Parser.strongInverse pb eb ∧ Parser.strongInverse pc ec ⇒
    Parser.strongInverse (Parser.parsePair pb pc)
      (λ(Data.Pair., b c). Data.List.@ (eb b) (ec c))

⊦ ∀f p a s.
    Parser.destParser (Parser.map f p) a s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s'). Data.Option.some (Data.Pair., (f b) s'))
      (Parser.destParser p a s)

⊦ ∀f p s.
    Parser.parse (Parser.partialMap f p) s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λc. Data.Option.some (Data.Pair., c s')) (f b))
      (Parser.parse p s)

⊦ ∀f e.
    (∀b. f (e b) = Data.Option.some b) ∧
    (∀a1 a2 b.
       f a1 = Data.Option.some b ∧ f a2 = Data.Option.some b ⇒ a1 = a2) ⇒
    Parser.strongInverse (Parser.parseOption f)
      (λb. Data.List.:: (e b) Data.List.[])

⊦ ∀f p g e.
    Parser.strongInverse p e ∧ (∀b. f (g b) = b) ∧
    (∀b1 b2 c. f b1 = c ∧ f b2 = c ⇒ b1 = b2) ⇒
    Parser.strongInverse (Parser.map f p) (λc. e (g c))

⊦ ∀pb pc s.
    Parser.parse (Parser.parsePair pb pc) s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λ(Data.Pair., c s'').
              Data.Option.some (Data.Pair., (Data.Pair., b c) s''))
           (Parser.parse pc s')) (Parser.parse pb s)

⊦ ∀f p g e.
    Parser.strongInverse p e ∧ (∀b. f (g b) = Data.Option.some b) ∧
    (∀b1 b2 c.
       f b1 = Data.Option.some c ∧ f b2 = Data.Option.some c ⇒ b1 = b2) ⇒
    Parser.strongInverse (Parser.partialMap f p) (λc. e (g c))

Input Type Operators

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

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - select
  - F
  - T
- List
  - Data.List.::
  - Data.List.@
  - Data.List.[]
- Option
  - Data.Option.case
  - Data.Option.none
  - Data.Option.some
- Pair
  - Data.Pair.,
Parser
- Parser.destParser
- Parser.inverse
- Parser.isParser
- Parser.map
- Parser.mkParser
- Parser.parse
- Parser.parseAll
  - Parser.parseAll.pa
- Parser.parseNone
  - Parser.parseNone.pn
- Parser.parseOption
- Parser.parsePair
  - Parser.parsePair.pbc
- Parser.parseSome
- Parser.partialMap
  - Parser.partialMap.pf
- Parser.strongInverse
- Stream
  - Parser.Stream.append
  - Parser.Stream.case
  - Parser.Stream.eof
  - Parser.Stream.error
  - Parser.Stream.isProperSuffix
  - Parser.Stream.isSuffix
  - Parser.Stream.stream

Assumptions

⊦ T

⊦ Parser.parseAll = Parser.mkParser Parser.parseAll.pa

⊦ Parser.parseNone = Parser.mkParser Parser.parseNone.pn

⊦ ∀x. Parser.Stream.isSuffix x x

⊦ F ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ F

⊦ ∀t. (∀x. t) ⇔ t

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

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

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

⊦ ∀x. x = x ⇔ T

⊦ ∀f. Parser.parseOption f = Parser.partialMap f Parser.parseAll

⊦ ∀a s. Parser.parseNone.pn a s = Data.Option.none

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

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

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

⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)

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

⊦ ∀x y. Parser.Stream.isProperSuffix x y ⇒ Parser.Stream.isSuffix x y

⊦ ∀a s. Parser.parseAll.pa a s = Data.Option.some (Data.Pair., a s)

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

⊦ ∀pb pc.
Parser.parsePair pb pc = Parser.mkParser (Parser.parsePair.pbc pb pc)

⊦ ∀f p. Parser.partialMap f p = Parser.mkParser (Parser.partialMap.pf f p)

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

⊦ ∀p.
    Parser.parseSome p =
    Parser.parseOption
      (λa. if p a then Data.Option.some a else Data.Option.none)

⊦ ∀f p. Parser.map f p = Parser.partialMap (λb. Data.Option.some (f b)) p

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

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

⊦ ∀t1 t2 t3. t1 ∨ t2 ∨ t3 ⇔ (t1 ∨ t2) ∨ t3

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

⊦ ∀x y z.
Parser.Stream.isSuffix x y ∧ Parser.Stream.isSuffix y z ⇒
Parser.Stream.isSuffix x z

⊦ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2

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

⊦ (∀a. Parser.mkParser (Parser.destParser a) = a) ∧
∀r. Parser.isParser r ⇔ Parser.destParser (Parser.mkParser r) = r

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

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

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

⊦ ∀p e.
    Parser.inverse p e ⇔
    ∀x s.
      Parser.parse p (Parser.Stream.append (e x) s) =
      Data.Option.some (Data.Pair., x 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.
    Parser.isParser p ⇔
    ∀x xs.
      Data.Option.case T
        (λ(Data.Pair., y xs'). Parser.Stream.isSuffix xs' xs) (p x xs)

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

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

⊦ ∀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 ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)

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

⊦ ∀f p a s.
    Parser.partialMap.pf f p a s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λc. Data.Option.some (Data.Pair., c s')) (f b))
      (Parser.destParser p a 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

⊦ ∀pb pc a s.
    Parser.parsePair.pbc pb pc a s =
    Data.Option.case Data.Option.none
      (λ(Data.Pair., b s').
         Data.Option.case Data.Option.none
           (λ(Data.Pair., c s'').
              Data.Option.some (Data.Pair., (Data.Pair., b c) s''))
           (Parser.parse pc s')) (Parser.destParser pb a s)

⊦ ∀p q r.
(p ∨ q ⇔ q ∨ p) ∧ ((p ∨ q) ∨ r ⇔ p ∨ q ∨ r) ∧ (p ∨ q ∨ r ⇔ q ∨ p ∨ r) ∧
(p ∨ p ⇔ p) ∧ (p ∨ p ∨ q ⇔ p ∨ q)