Package parser-all-thm: Properties of the whole stream parser

Information

Files

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

Theorems

⊦ ∀p xs. length (parse p xs) ≤ length xs

⊦ ∀p f xs. parse (map p f) xs = map f (parse p xs)

⊦ ∀p e l. inverse p e ⇒ parse p (fromList (concat (map e l))) = fromList l

⊦ ∀p e x xs. inverse p e ⇒ parse p (append (e x) xs) = cons x (parse p xs)

⊦ ∀p e xs ys ye.
    strongInverse p e ∧ toList (parse p xs) = (ys, ye) ⇒
    ye ∨ xs = fromList (concat (map e ys))

⊦ ∀p xs.
    parse p xs =
    case apply p xs of
      none → case xs of error → error | eof → eof | cons y ys → error
    | some (y, ys) → cons y (parse p ys)

⊦ (∀p. parse p error = error) ∧ (∀p. parse p eof = eof) ∧
  ∀p x xs.
    parse p (cons x xs) =
    case dest p x xs of none → error | some (y, ys) → cons y (parse p ys)

External Type Operators

• →
• bool
• Data
  • List
    • list
  • Option
    • option
  • Pair
    • ×
• Number
  • Natural
    • natural
• Parser
  • parser
  • Stream
    • stream

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • ⊥
    • ⊤
  • List
    • ::
    • @
    • []
    • concat
    • map
  • Option
    • case
    • none
    • some
  • Pair
    • ,
• Number
  • Natural
    • ≤
    • suc
    • zero
• Parser
  • apply
  • dest
  • inverse
  • map
  • parse
  • strongInverse
  • Stream
    • append
    • case
    • cons
    • eof
    • error
    • fromList
    • isProperSuffix
    • isSuffix
    • length
    • map
    • toList

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ length eof = 0

⊦ length error = 0

⊦ concat [] = []

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ ∀xs. ¬isProperSuffix xs xs

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀a. ¬(some a = none)

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀f. map f [] = []

⊦ ∀p. parse p eof = eof

⊦ ∀p. parse p error = error

⊦ ∀p. apply p eof = none

⊦ ∀p. apply p error = none

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀l. fromList l = append l eof

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

⊦ ∀b f. case b f none = b

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

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀x xs. length (cons x xs) = suc (length xs)

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

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

⊦ ∀a b. some a = some b ⇔ a = b

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀h t. concat (h :: t) = h @ concat t

⊦ ∀xs ys. isSuffix xs ys ⇒ length xs ≤ length ys

⊦ ∀b f a. case b f (some a) = f a

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

⊦ ∀xs y ys. isProperSuffix xs (cons y ys) ⇔ isSuffix xs ys

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

⊦ ∀f. ∃fn. ∀a b. fn (a, b) = f a b

⊦ ∀p x xs. apply p (cons x xs) = dest p x xs

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

⊦ ∀xs ys zs. append (xs @ ys) zs = append xs (append ys zs)

⊦ ∀f h t. map f (h :: t) = f h :: map f t

⊦ ∀xs. xs = error ∨ xs = eof ∨ ∃x xt. xs = cons x xt

⊦ ∀p. (∀xs. (∀ys. isProperSuffix ys xs ⇒ p ys) ⇒ p xs) ⇒ ∀xs. p xs

⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x

⊦ ∀p. p [] ∧ (∀h t. p t ⇒ p (h :: t)) ⇒ ∀l. p l

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

⊦ ∀p e. inverse p e ⇔ ∀x xs. apply p (append (e x) xs) = some (x, xs)

⊦ (∀xs. append [] xs = xs) ∧
  ∀h t xs. append (h :: t) xs = cons h (append t xs)

⊦ ∀p xs.
    apply p xs = none ∨
    ∃y ys. apply p xs = some (y, ys) ∧ isProperSuffix ys xs

⊦ ∀p x xs.
    dest p x xs = none ∨ ∃y ys. dest p x xs = some (y, ys) ∧ isSuffix ys xs

⊦ ∀p e.
    strongInverse p e ⇔
    inverse p e ∧
    ∀xs y ys. apply p xs = some (y, ys) ⇒ xs = append (e y) ys

⊦ ∀p x xs.
    parse p (cons x xs) =
    case dest p x xs of none → error | some (y, ys) → cons y (parse p ys)

⊦ (∀f. map f error = error) ∧ (∀f. map f eof = eof) ∧
  ∀f x xs. map f (cons x xs) = cons (f x) (map f xs)

⊦ ∀p f x xs.
    dest (map p f) x xs =
    case dest p x xs of none → none | some (y, ys) → some (f y, ys)

⊦ toList error = ([], ⊤) ∧ toList eof = ([], ⊥) ∧
  ∀x xs. toList (cons x xs) = let (l, e) ← toList xs in (x :: l, e)

⊦ (∀e b f. case e b f error = e) ∧ (∀e b f. case e b f eof = b) ∧
  ∀e b f x xs. case e b f (cons x xs) = f x xs

OpenTheory package document generated by opentheory 1.3 (release 20150429)