Package char-utf8-thm: char-utf8-thm

Information

Files

• Package tarball char-utf8-thm-1.0.tgz
• Theory file char-utf8-thm.thy (included in the package tarball)

Theorems

⊦ Parser.isParser Data.Char.UTF8.decoder.parse

⊦ Parser.destParser Data.Char.UTF8.decoder = Data.Char.UTF8.decoder.parse

⊦ Parser.parse Data.Char.UTF8.decoder =
  Parser.Stream.case Data.Option.none Data.Option.none
    Data.Char.UTF8.decoder.parse

Input Type Operators

• →
• bool
• Data
  • Byte
    • Data.Byte.byte
  • Char
    • Data.Char.char
    • Data.Char.plane
    • Data.Char.position
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.*
  • Word16
    • Data.Word16.word16
• Number
  • Natural
    • Number.Natural.natural
• Parser
  • Parser.parser
  • Stream
    • Parser.Stream.stream

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • let
    • select
    • F
    • T
  • Byte
    • Data.Byte.bit
    • Data.Byte.fromNatural
  • Char
    • Data.Char.mkChar
    • Data.Char.mkPlane
    • Data.Char.mkPosition
    • UTF8
      • Data.Char.UTF8.decoder
        • Data.Char.UTF8.decoder.decode1
        • Data.Char.UTF8.decoder.decode2
        • Data.Char.UTF8.decoder.decode3
        • Data.Char.UTF8.decoder.parse
      • Data.Char.UTF8.parseContinuationByte
      • Data.Char.UTF8.parseThreeContinuationBytes
      • Data.Char.UTF8.parseTwoContinuationBytes
  • Option
    • Data.Option.case
    • Data.Option.none
    • Data.Option.some
  • Pair
    • Data.Pair.,
  • Word16
    • Data.Word16.fromBytes
• Number
  • Numeral
    • Number.Numeral.bit0
    • Number.Numeral.bit1
    • Number.Numeral.zero
• Parser
  • Parser.destParser
  • Parser.isParser
  • Parser.mkParser
  • Parser.parse
  • Parser.partialMap
  • Stream
    • Parser.Stream.case
    • Parser.Stream.eof
    • Parser.Stream.error
    • Parser.Stream.isProperSuffix
    • Parser.Stream.isSuffix
    • Parser.Stream.stream

Assumptions

⊦ T

⊦ Data.Char.UTF8.decoder = Parser.mkParser Data.Char.UTF8.decoder.parse

⊦ ∀x. Parser.Stream.isSuffix x x

⊦ let = λf x. f x

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

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

⊦ ∀x. x = x ⇔ T

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

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

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

⊦ ∀f y. (λx. f x) y = f y

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

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

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

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

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

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

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

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

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

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

⊦ ∀p.
    Parser.isParser p ⇔
    ∀x xs.
      Data.Option.case T
        (λ(Data.Pair., y xs'). Parser.Stream.isSuffix xs' xs) (p x xs)

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

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

⊦ ∀b0 s.
    Data.Char.UTF8.decoder.parse b0 s =
    (if Data.Byte.bit b0
       (Number.Numeral.bit1
          (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))
     then (if Data.Byte.bit b0
        (Number.Numeral.bit0
           (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))
      then (if Data.Byte.bit b0
         (Number.Numeral.bit1
            (Number.Numeral.bit0
               (Number.Numeral.bit1 Number.Numeral.zero)))
       then (if Data.Byte.bit b0
          (Number.Numeral.bit0
             (Number.Numeral.bit0
                (Number.Numeral.bit1 Number.Numeral.zero)))
        then (if Data.Byte.bit b0
           (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero))
         then Data.Option.none
         else Parser.parse
           (Parser.partialMap (Data.Char.UTF8.decoder.decode3 b0)
              Data.Char.UTF8.parseThreeContinuationBytes) s)
        else Parser.parse
          (Parser.partialMap (Data.Char.UTF8.decoder.decode2 b0)
             Data.Char.UTF8.parseTwoContinuationBytes) s)
       else Parser.parse
         (Parser.partialMap (Data.Char.UTF8.decoder.decode1 b0)
            Data.Char.UTF8.parseContinuationByte) s) else Data.Option.none)
     else let
       (λpl.
          let
            (λpos.
               let (λch. Data.Option.some (Data.Pair., ch s))
                 (Data.Char.mkChar (Data.Pair., pl pos)))
            (Data.Char.mkPosition
               (Data.Word16.fromBytes
                  (Data.Byte.fromNatural Number.Numeral.zero) b0)))
       (Data.Char.mkPlane (Data.Byte.fromNatural Number.Numeral.zero)))