Package char-def: char-def

Information

Files

• Package tarball char-def-1.5.tgz
• Theory file char-def.thy (included in the package tarball)

Defined Type Operators

• Data
  • Char
    • Data.Char.char
    • Data.Char.plane
    • Data.Char.position

Defined Constants

• Data
  • Char
    • Data.Char.destChar
    • Data.Char.destPlane
    • Data.Char.destPosition
    • Data.Char.isChar
    • Data.Char.isPlane
    • Data.Char.isPosition
    • Data.Char.mkChar
    • Data.Char.mkPlane
    • Data.Char.mkPosition

Theorems

⊦ ∀p. Data.Char.isPosition p ⇔ T

⊦ ∀p.
    Data.Char.isPlane p ⇔
    Data.Byte.< p
      (Data.Byte.fromNatural
         (Number.Numeral.bit1
            (Number.Numeral.bit0
               (Number.Numeral.bit0
                  (Number.Numeral.bit0
                     (Number.Numeral.bit1 Number.Numeral.zero))))))

⊦ (∀a. Data.Char.mkChar (Data.Char.destChar a) = a) ∧
  ∀r. Data.Char.isChar r ⇔ Data.Char.destChar (Data.Char.mkChar r) = r

⊦ (∀a. Data.Char.mkPlane (Data.Char.destPlane a) = a) ∧
  ∀r. Data.Char.isPlane r ⇔ Data.Char.destPlane (Data.Char.mkPlane r) = r

⊦ (∀a. Data.Char.mkPosition (Data.Char.destPosition a) = a) ∧
  ∀r.
    Data.Char.isPosition r ⇔
    Data.Char.destPosition (Data.Char.mkPosition r) = r

⊦ ∀pl pos.
    Data.Char.isChar (Data.Pair., pl pos) ⇔
    let pli = Data.Char.destPlane pl in
    let posi = Data.Char.destPosition pos in
    ¬(pli = Data.Byte.fromNatural Number.Numeral.zero) ∨
    Data.Word16.< posi
      (Data.Word16.fromNatural
         (Number.Numeral.bit0
            (Number.Numeral.bit0
               (Number.Numeral.bit0
                  (Number.Numeral.bit0
                     (Number.Numeral.bit0
                        (Number.Numeral.bit0
                           (Number.Numeral.bit0
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit0
                                    (Number.Numeral.bit0
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit0
                                                   (Number.Numeral.bit1
                                                      (Number.Numeral.bit1
                                                         Number.Numeral.zero))))))))))))))))) ∨
    Data.Word16.<
      (Data.Word16.fromNatural
         (Number.Numeral.bit1
            (Number.Numeral.bit1
               (Number.Numeral.bit1
                  (Number.Numeral.bit1
                     (Number.Numeral.bit1
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit0
                                                   (Number.Numeral.bit1
                                                      (Number.Numeral.bit1
                                                         Number.Numeral.zero)))))))))))))))))
      posi ∧
    Data.Word16.< posi
      (Data.Word16.fromNatural
         (Number.Numeral.bit0
            (Number.Numeral.bit1
               (Number.Numeral.bit1
                  (Number.Numeral.bit1
                     (Number.Numeral.bit1
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit1
                                                   (Number.Numeral.bit1
                                                      (Number.Numeral.bit1
                                                         Number.Numeral.zero)))))))))))))))))

Input Type Operators

• →
• bool
• Data
  • Byte
    • Data.Byte.byte
  • Pair
    • Data.Pair.*
  • Word16
    • Data.Word16.word16
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • let
    • select
    • F
    • T
  • Byte
    • Data.Byte.<
    • Data.Byte.≤
    • Data.Byte.fromNatural
    • Data.Byte.modulus
    • Data.Byte.toNatural
    • Data.Byte.width
  • Pair
    • Data.Pair.,
    • Data.Pair.fst
    • Data.Pair.snd
  • Word16
    • Data.Word16.<
    • Data.Word16.fromNatural
• Number
  • Natural
    • Number.Natural.*
    • Number.Natural.+
    • Number.Natural.<
    • Number.Natural.≤
    • Number.Natural.div
    • Number.Natural.even
    • Number.Natural.exp
    • Number.Natural.mod
    • Number.Natural.suc
  • Numeral
    • Number.Numeral.bit0
    • Number.Numeral.bit1
    • Number.Numeral.zero

Assumptions

⊦ T

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

⊦ F ⇔ ∀p. p

⊦ let = λf x. f x

⊦ (¬) = λp. p ⇒ F

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

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

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

⊦ ∀x. x = x ⇔ T

⊦ ∀n. ¬(Number.Natural.suc n = Number.Numeral.zero)

⊦ Data.Byte.modulus =
  Number.Natural.exp
    (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero))
    Data.Byte.width

⊦ Data.Byte.width =
  Number.Numeral.bit0
    (Number.Numeral.bit0
       (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))

⊦ ∀n. Number.Numeral.bit0 n = Number.Natural.+ n n

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

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

⊦ ∀n. Number.Numeral.bit1 n = Number.Natural.suc (Number.Natural.+ n n)

⊦ ∀x.
    Data.Byte.toNatural (Data.Byte.fromNatural x) =
    Number.Natural.mod x Data.Byte.modulus

⊦ ∀x y. Data.Pair.fst (Data.Pair., x y) = x

⊦ ∀x y. Data.Pair.snd (Data.Pair., x y) = y

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

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

⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1

⊦ ∀n.
    Number.Natural.*
      (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)) n =
    Number.Natural.+ n n

⊦ ∀x y. Data.Byte.< x y ⇔ ¬Data.Byte.≤ y x

⊦ ∀m n. ¬Number.Natural.≤ m n ⇔ Number.Natural.< n m

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

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

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

⊦ ∀x y.
    Data.Byte.≤ x y ⇔
    Number.Natural.≤ (Data.Byte.toNatural x) (Data.Byte.toNatural y)

⊦ ∀m n. Number.Natural.suc m = Number.Natural.suc n ⇔ m = n

⊦ ∀m n.
    Number.Natural.even (Number.Natural.* m n) ⇔
    Number.Natural.even m ∨ Number.Natural.even n

⊦ ∀m n.
    Number.Natural.even (Number.Natural.+ m n) ⇔ Number.Natural.even m ⇔
    Number.Natural.even n

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

⊦ (Number.Natural.even Number.Numeral.zero ⇔ T) ∧
  ∀n. Number.Natural.even (Number.Natural.suc n) ⇔ ¬Number.Natural.even n

⊦ ∀m n. Number.Natural.≤ m n ⇔ Number.Natural.< m n ∨ m = n

⊦ ∀m n. Number.Natural.≤ m n ∧ Number.Natural.≤ n m ⇔ m = n

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

⊦ ∀x y.
    Data.Byte.fromNatural x = Data.Byte.fromNatural y ⇔
    Number.Natural.mod x Data.Byte.modulus =
    Number.Natural.mod y Data.Byte.modulus

⊦ ∀m n.
    Number.Natural.* m n = Number.Numeral.zero ⇔
    m = Number.Numeral.zero ∨ n = Number.Numeral.zero

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

⊦ ∀m n p.
    Number.Natural.* m (Number.Natural.+ n p) =
    Number.Natural.+ (Number.Natural.* m n) (Number.Natural.* m p)

⊦ ∀m n p.
    Number.Natural.exp m (Number.Natural.+ n p) =
    Number.Natural.* (Number.Natural.exp m n) (Number.Natural.exp m p)

⊦ ∀m n p.
    Number.Natural.* (Number.Natural.+ m n) p =
    Number.Natural.+ (Number.Natural.* m p) (Number.Natural.* n p)

⊦ ∀m n p.
    Number.Natural.* m n = Number.Natural.* m p ⇔
    m = Number.Numeral.zero ∨ n = p

⊦ ∀m n p.
    Number.Natural.≤ (Number.Natural.* m n) (Number.Natural.* m p) ⇔
    m = Number.Numeral.zero ∨ Number.Natural.≤ n p

⊦ ∀m n p.
    Number.Natural.< (Number.Natural.* m n) (Number.Natural.* m p) ⇔
    ¬(m = Number.Numeral.zero) ∧ Number.Natural.< n p

⊦ (∀m.
     Number.Natural.exp m Number.Numeral.zero =
     Number.Numeral.bit1 Number.Numeral.zero) ∧
  ∀m n.
    Number.Natural.exp m (Number.Natural.suc n) =
    Number.Natural.* m (Number.Natural.exp m n)

⊦ (∀m. Number.Natural.≤ m Number.Numeral.zero ⇔ m = Number.Numeral.zero) ∧
  ∀m n.
    Number.Natural.≤ m (Number.Natural.suc n) ⇔
    m = Number.Natural.suc n ∨ Number.Natural.≤ m n

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

⊦ ∀m n q r.
    m = Number.Natural.+ (Number.Natural.* q n) r ∧ Number.Natural.< r n ⇒
    Number.Natural.div m n = q ∧ Number.Natural.mod m n = r

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

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

⊦ ∀m n p.
    Number.Natural.+ m n = Number.Natural.+ n m ∧
    Number.Natural.+ (Number.Natural.+ m n) p =
    Number.Natural.+ m (Number.Natural.+ n p) ∧
    Number.Natural.+ m (Number.Natural.+ n p) =
    Number.Natural.+ n (Number.Natural.+ m p)

⊦ (∀n. Number.Natural.+ Number.Numeral.zero n = n) ∧
  (∀m. Number.Natural.+ m Number.Numeral.zero = m) ∧
  (∀m n.
     Number.Natural.+ (Number.Natural.suc m) n =
     Number.Natural.suc (Number.Natural.+ m n)) ∧
  ∀m n.
    Number.Natural.+ m (Number.Natural.suc n) =
    Number.Natural.suc (Number.Natural.+ m n)

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

⊦ (∀n. Number.Natural.* Number.Numeral.zero n = Number.Numeral.zero) ∧
  (∀m. Number.Natural.* m Number.Numeral.zero = Number.Numeral.zero) ∧
  (∀n. Number.Natural.* (Number.Numeral.bit1 Number.Numeral.zero) n = n) ∧
  (∀m. Number.Natural.* m (Number.Numeral.bit1 Number.Numeral.zero) = m) ∧
  (∀m n.
     Number.Natural.* (Number.Natural.suc m) n =
     Number.Natural.+ (Number.Natural.* m n) n) ∧
  ∀m n.
    Number.Natural.* m (Number.Natural.suc n) =
    Number.Natural.+ m (Number.Natural.* m n)