Package char-thm: char-thm

Information

name	char-thm
version	1.0
description	char-thm
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-02-19
show	Data.Bool

Files

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

Theorems

⊦ ∀pl. ∃b. Data.Char.isPlane b ∧ pl = Data.Char.mkPlane b

⊦ ∀pos. ∃w. Data.Char.isPosition w ∧ pos = Data.Char.mkPosition w

⊦ ∀pl.
    ∃b.
      Data.Char.isPlane b ∧ pl = Data.Char.mkPlane b ∧
      Data.Char.destPlane pl = b

⊦ ∀pos.
    ∃w.
      Data.Char.isPosition w ∧ pos = Data.Char.mkPosition w ∧
      Data.Char.destPosition pos = w

⊦ ∀c.
    ∃pl pos.
      Data.Char.isChar (Data.Pair., pl pos) ∧
      c = Data.Char.mkChar (Data.Pair., pl pos)

⊦ ∀c.
    ∃pl pos.
      Data.Char.isChar (Data.Pair., pl pos) ∧
      c = Data.Char.mkChar (Data.Pair., pl pos) ∧
      Data.Char.destChar c = Data.Pair., pl pos

Input Type Operators

→
bool
Data
- Byte
  - Data.Byte.byte
- Char
  - Data.Char.char
  - Data.Char.plane
  - Data.Char.position
- Pair
  - Data.Pair.*
- Word16
  - Data.Word16.word16

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - F
  - T
- 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
- Pair
  - Data.Pair.,
  - Data.Pair.fst
  - Data.Pair.snd

Assumptions

⊦ T

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

⊦ ∀x. x = x ⇔ T

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

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

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

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

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

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