Package char-thm: Properties of Unicode characters
Information
| name | char-thm |
| version | 1.9 |
| description | Properties of Unicode characters |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-02-05 |
| requires | bool char-def pair |
| show | Data.Bool Data.Byte Data.Char Data.Pair Data.Word16 |
Files
- Package tarball char-thm-1.9.tgz
- Theory file char-thm.thy (included in the package tarball)
Theorems
⊦ ∀pos. ∃w. pos = mkPosition w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b
⊦ ∀pos. ∃w. pos = mkPosition w ∧ destPosition pos = w
⊦ ∀pl. ∃b. isPlane b ∧ pl = mkPlane b ∧ destPlane pl = b
⊦ ∀c. ∃pl pos. isChar (pl, pos) ∧ c = mkChar (pl, pos)
⊦ ∀c.
∃pl pos.
isChar (pl, pos) ∧ c = mkChar (pl, pos) ∧ destChar c = (pl, pos)
Input Type Operators
- →
- bool
- Data
- Byte
- byte
- Char
- char
- plane
- position
- Pair
- ×
- Word16
- word16
- Byte
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊤
- Char
- destChar
- destPlane
- destPosition
- isChar
- isPlane
- mkChar
- mkPlane
- mkPosition
- Pair
- ,
- fst
- snd
- Bool
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀a. mkChar (destChar a) = a
⊦ ∀a. mkPlane (destPlane a) = a
⊦ ∀a. mkPosition (destPosition a) = a
⊦ ∀r. destPosition (mkPosition r) = r
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀xy. (fst xy, snd xy) = xy
⊦ ∀r. isPlane r ⇔ destPlane (mkPlane r) = r
⊦ ∀r. isChar r ⇔ destChar (mkChar r) = r
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q